Core.sum

-- The non-dependent sum ⊎ (disjoint union) — Agda's notation: inj₁,
-- inj₂, and the dependent motive-first eliminator ⊎-elim (like
-- ℕ-elim). β on each injection is judgemental (el-sum-beta₁/₂); the
-- uniqueness law (el-sum-eta) is stated judgementally in the theory
-- and derivable here, propositionally, by case analysis at an
-- equality motive. Injection injectivity and disjointness need no
-- rules — both are derivable below, exactly as Foundation's
-- injectivity notes say.
-- case analysis at a constant motive: the canonical swap

import Core.equality (cong, transport)

swap : {a b : 𝕌} → a ⊎ b → b ⊎ a
swap = λa b t. ⊎-elim (x. inj₂ x) (y. inj₁ y) t

-- β on each injection, by computation
swapBeta1 : (a b : 𝕌) (x : a) → swap (inj₁ x) ≡ inj₂ x ∈ b ⊎ a using (Core.sum.swap.eq)
swapBeta1 = λa b x. ⋆

swapBeta2 : (a b : 𝕌) (y : b) → swap (inj₂ y) ≡ inj₁ y ∈ b ⊎ a using (Core.sum.swap.eq)
swapBeta2 = λa b y. ⋆

-- swap is an involution: case analysis with an equality motive, both
-- cases closing by β
swapInvol : (a b : 𝕌) (t : a ⊎ b) → swap (swap t) ≡ t using (Core.sum.swap.eq)
swapInvol = λa b t. ⊎-elim (x. ⋆) (y. ⋆) t

-- the uniqueness (η) law, propositionally: any map out of a ⊎ b IS
-- the eliminator over its own injection images (el-sum-eta's content,
-- derived by ⊎-elim at an equality motive)
sumEta : (a b c : 𝕌)
  (f : a ⊎ b → c)
  (t : a ⊎ b)
  → ⊎-elim (w. c) (x. f (inj₁ x)) (y. f (inj₂ y)) t ≡ f t
sumEta =
  λa b c f t. ⊎-elim (w. ⊎-elim (v. c) (x. f (inj₁ x)) (y. f (inj₂ y)) w ≡ f w) (x. ⋆) (y. ⋆) t

-- the ⊎ TYPE former and its code agree: (a ⊎ b) ≐ a ⊎ b
-- (ty-el-sum), so the conversions between them are the identity
-- case analysis
toCode : {a b : 𝕌} → a ⊎ b → a ⊎ b
toCode = λa b t. ⊎-elim (x. inj₁ x) (y. inj₂ y) t

fromCode : {a b : 𝕌} → a ⊎ b → a ⊎ b
fromCode = λa b t. ⊎-elim (x. inj₁ x) (y. inj₂ y) t

toFromId : (a b : 𝕌) (t : a ⊎ b) → toCode (fromCode t) ≡ t
  using (Core.sum.fromCode.eq, Core.sum.toCode.eq)
toFromId = λa b t. ⊎-elim (x. ⋆) (y. ⋆) t

-- inj₁ is injective — DERIVABLE, no rule needed: a ⊎-elim retraction
-- at constant motive a whose right case returns a fixed default
-- (the compared element itself serves), then congruence
outl : (a b : 𝕌) → a → a ⊎ b → a
outl = λa b d t. ⊎-elim (x. x) (y. d) t

inj1Injective : (a b : 𝕌) (x x' : a) → (inj₁ x ≡ inj₁ x' ∈ a ⊎ b) → x ≡ x' using (Core.sum.outl.eq)
inj1Injective = λa b x x' h. cong (λw. a) (outl _ b x) h

-- inj₁ and inj₂ are disjoint — also derivable: transport the
-- "is-left" code along the bad equation and land a 𝟙-witness in 𝟘
isLeftCode : (a b : 𝕌) → a ⊎ b → 𝕌
isLeftCode = λa b t. ⊎-elim (x. 𝟙) (y. 𝟘) t

inj1NotInj2 : (a b : 𝕌) (x : a) (y : b) → (inj₁ x ≡ inj₂ y ∈ a ⊎ b) → 𝟘
  using (Core.sum.isLeftCode.unfold)
inj1NotInj2 = λa b x y h. transport (isLeftCode a b) h ()

-- the mirror image of outl/inj1Injective, for the right injection
outr : (a b : 𝕌) → b → a ⊎ b → b
outr = λa b d t. ⊎-elim (x. d) (y. y) t

inj2Injective : (a b : 𝕌) (y y' : b) → (inj₂ y ≡ inj₂ y' ∈ a ⊎ b) → y ≡ y' using (Core.sum.outr.eq)
inj2Injective = λa b y y' h. cong (λw. b) (outr a _ y) h