module My.SetTheory.Sum.Misc where

-- §──────────────────────────────────────────────────────────────────
-- Required modules
-- §──────────────────────────────────────────────────────────────────

import Data.Empty as DE
import Data.Product as DP
import Data.Sum as DS
import Function as F
import Level as L
import Relation.Nullary as RN

open DP using (_×_ ; _,_)
open DS using (_⊎_)
open F using (_∘_)

-- §──────────────────────────────────────────────────────────────────
-- If A or B holds, and one of them doesn't, the other does.
-- §──────────────────────────────────────────────────────────────────

¬A⇒A⊎B⇒B : {𝓁 𝓂 : L.Level} → {A : Set 𝓁} → {B : Set 𝓂} → RN.¬ A → A ⊎ B → B
¬A⇒A⊎B⇒B ¬a (DS.inj₁ a) = DE.⊥-elim (¬a a)
¬A⇒A⊎B⇒B ¬a (DS.inj₂ b) = b

¬B⇒A⊎B⇒A : {𝓁 𝓂 : L.Level} → {A : Set 𝓁} → {B : Set 𝓂} → RN.¬ B → A ⊎ B → A
¬B⇒A⊎B⇒A ¬b (DS.inj₁ a) = a
¬B⇒A⊎B⇒A ¬b (DS.inj₂ b) = DE.⊥-elim (¬b b)

-- §──────────────────────────────────────────────────────────────────
-- Duality between sum and product.
-- §──────────────────────────────────────────────────────────────────

¬⌈A⊎B⌉⇒¬A׬B : {𝓁 𝓂 : L.Level} → {A : Set 𝓁} → {B : Set 𝓂} →
  RN.¬ (A ⊎ B) → RN.¬ A × RN.¬ B
¬⌈A⊎B⌉⇒¬A׬B ¬⌈a⊎b⌉ = (¬⌈a⊎b⌉ ∘ DS.inj₁ , ¬⌈a⊎b⌉ ∘ DS.inj₂)

-- §──────────────────────────────────────────────────────────────────
-- If three propositions are true, and two of them don't hold, the
-- third does.
-- §──────────────────────────────────────────────────────────────────

¬⌈A⊎B⌉⇒A⊎B⊎C⇒C : {𝓁 𝓂 𝓃 : L.Level} → {A : Set 𝓁} → {B : Set 𝓂} → {C : Set 𝓃}
  → RN.¬ (A ⊎ B) → A ⊎ B ⊎ C → C
¬⌈A⊎B⌉⇒A⊎B⊎C⇒C f (DS.inj₁ a) = DE.⊥-elim (f (DS.inj₁ a))
¬⌈A⊎B⌉⇒A⊎B⊎C⇒C f (DS.inj₂ (DS.inj₁ b)) = DE.⊥-elim (f (DS.inj₂ b))
¬⌈A⊎B⌉⇒A⊎B⊎C⇒C f (DS.inj₂ (DS.inj₂ c)) = c

-- §──────────────────────────────────────────────────────────────────
-- Miscellany
-- §──────────────────────────────────────────────────────────────────

sameSum : {𝓁 : L.Level} → {A : Set 𝓁} → A ⊎ A → A
sameSum = DS.[ F.id , F.id ]