{-# OPTIONS --without-K --safe #-}
module Data.Sum where
open import Function.Base
open import Data.Unit.Polymorphic.Base using (⊤; tt)
open import Data.Maybe.Base using (Maybe; just; nothing)
open import Level
open import Agda.Builtin.Equality
open import Data.Sum.Base public
module _ {a b} {A : Set a} {B : Set b} where
isInj₁ : A ⊎ B → Maybe A
isInj₁ (inj₁ x) = just x
isInj₁ (inj₂ y) = nothing
isInj₂ : A ⊎ B → Maybe B
isInj₂ (inj₁ x) = nothing
isInj₂ (inj₂ y) = just y
From-inj₁ : A ⊎ B → Set a
From-inj₁ (inj₁ _) = A
From-inj₁ (inj₂ _) = ⊤
from-inj₁ : (x : A ⊎ B) → From-inj₁ x
from-inj₁ (inj₁ x) = x
from-inj₁ (inj₂ _) = _
From-inj₂ : A ⊎ B → Set b
From-inj₂ (inj₁ _) = ⊤
From-inj₂ (inj₂ _) = B
from-inj₂ : (x : A ⊎ B) → From-inj₂ x
from-inj₂ (inj₁ _) = _
from-inj₂ (inj₂ x) = x