module My.SetTheory.Relation.Trichotomy where

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

import Data.Empty as DE
import Data.Product as DP
import Data.Sum as DS
import Level as L
import Relation.Binary as RB
import Relation.Nullary as RN

open DS using (_⊎_)

import My.SetTheory.Sum.Misc as MySTSM

trichABC⇒A⊎B⊎C : {𝓁 𝓂 𝓃 : L.Level} → {A : Set 𝓁} → {B : Set 𝓂} →
  {C : Set 𝓃} → RB.Tri A B C → A ⊎ B ⊎ C
trichABC⇒A⊎B⊎C (RB.tri< a ¬b ¬c) = DS.inj₁ a
trichABC⇒A⊎B⊎C (RB.tri≈ ¬a b ¬c) = DS.inj₂ (DS.inj₁ b)
trichABC⇒A⊎B⊎C (RB.tri> ¬a ¬b c) = DS.inj₂ (DS.inj₂ c)

trichABC⇒A⇒¬B : {𝓁 𝓂 𝓃 : L.Level} → {A : Set 𝓁} → {B : Set 𝓂} →
  {C : Set 𝓃} → RB.Tri A B C → A → RN.¬ B
trichABC⇒A⇒¬B (RB.tri< a ¬b ¬c) a′ b = ¬b b
trichABC⇒A⇒¬B (RB.tri≈ ¬a b ¬c) a b′ = ¬a a
trichABC⇒A⇒¬B (RB.tri> ¬a ¬b c) a b = ¬b b

trichABC⇒¬⌈A⊎B⌉⇒C : {𝓁 𝓂 𝓃 : L.Level} → {A : Set 𝓁} → {B : Set 𝓂} →
  {C : Set 𝓃} → RB.Tri A B C → RN.¬ (A ⊎ B) → C
trichABC⇒¬⌈A⊎B⌉⇒C (RB.tri< a ¬b ¬c) ¬⌈a⊎b⌉ =
  DE.⊥-elim ((DP.proj₁ (MySTSM.¬⌈A⊎B⌉⇒¬A׬B ¬⌈a⊎b⌉)) a)
trichABC⇒¬⌈A⊎B⌉⇒C (RB.tri≈ ¬a b ¬c) ¬⌈a⊎b⌉ =
  DE.⊥-elim ((DP.proj₂ (MySTSM.¬⌈A⊎B⌉⇒¬A׬B ¬⌈a⊎b⌉)) b)
trichABC⇒¬⌈A⊎B⌉⇒C (RB.tri> ¬a ¬b c) ¬⌈a⊎b⌉ = c

trichABC⇒C⇒¬⌈A⊎B⌉ : {𝓁 𝓂 𝓃 : L.Level} → {A : Set 𝓁} → {B : Set 𝓂} →
  {C : Set 𝓃} → RB.Tri A B C → C → RN.¬ (A ⊎ B)
trichABC⇒C⇒¬⌈A⊎B⌉ (RB.tri< a ¬b ¬c) c (DS.inj₁ a′) = ¬c c
trichABC⇒C⇒¬⌈A⊎B⌉ (RB.tri< a ¬b ¬c) c (DS.inj₂ b) = ¬c c
trichABC⇒C⇒¬⌈A⊎B⌉ (RB.tri≈ ¬a b ¬c) c (DS.inj₁ a) = ¬c c
trichABC⇒C⇒¬⌈A⊎B⌉ (RB.tri≈ ¬a b ¬c) c (DS.inj₂ b′) = ¬c c
trichABC⇒C⇒¬⌈A⊎B⌉ (RB.tri> ¬a ¬b c) c′ (DS.inj₁ a) = ¬a a
trichABC⇒C⇒¬⌈A⊎B⌉ (RB.tri> ¬a ¬b c) c′ (DS.inj₂ b) = ¬b b