{-# OPTIONS --safe #-}
module Data.Set where

open import Prelude

infixr 5 _∷_
data 𝒦 (A : Type a) : Type a where
  _∷_ : A β†’ 𝒦 A β†’ 𝒦 A
  βˆ… : 𝒦 A
  dup : βˆ€ x xs β†’ x ∷ x ∷ xs ≑ x ∷ xs
  comm : βˆ€ x y xs β†’ x ∷ y ∷ xs ≑ y ∷ x ∷ xs
  trunc : isSet (𝒦 A)

data π”Ž (A : Type a) (P : 𝒦 A β†’ Type p) : Type (a β„“βŠ” p) where
  βˆ… : π”Ž A P
  _∷_⟨_⟩ : A β†’ (xs : 𝒦 A) β†’ (P⟨xs⟩ : P xs) β†’ π”Ž A P

embed : π”Ž A P β†’ 𝒦 A
embed βˆ… = βˆ…
embed (x ∷ xs ⟨ P⟨xs⟩ ⟩) = x ∷ xs

Alg : (P : 𝒦 A β†’ Type p) β†’ Type _
Alg P = (xs : π”Ž _ P) β†’ P (embed xs)

record Coherent {A : Type a} {P : 𝒦 A β†’ Type p} (Ο• : Alg P) : Type (a β„“βŠ” p) where
  field
    c-trunc : βˆ€ xs β†’ isSet (P xs)

    c-com : βˆ€ x y xs P⟨xs⟩ β†’
            PathP
              (Ξ» i β†’ P (comm x y xs i))
              (Ο• (x ∷ (y ∷ xs) ⟨ Ο• (y ∷ xs ⟨ P⟨xs⟩ ⟩) ⟩))
              (Ο• (y ∷ (x ∷ xs) ⟨ Ο• (x ∷ xs ⟨ P⟨xs⟩ ⟩) ⟩ ))

    c-dup : βˆ€ x xs P⟨xs⟩ β†’
            PathP
              (Ξ» i β†’ P (dup x xs i))
              (Ο• (x ∷ (x ∷ xs) ⟨ Ο• (x ∷ xs ⟨ P⟨xs⟩ ⟩) ⟩))
              (Ο• (x ∷ xs ⟨ P⟨xs⟩ ⟩))
open Coherent public

𝒦-foldr : (A β†’ B β†’ B) β†’ B β†’ Alg (const B)
𝒦-foldr f b βˆ… = b
𝒦-foldr f b (x ∷ xs ⟨ P⟨xs⟩ ⟩) = f x P⟨xs⟩

Ξ¨ : (𝒦 A β†’ Type p) β†’ Type _
Ξ¨ P = Ξ£[ Ο• ⦂ Alg P ] Γ— Coherent Ο•

Ξ¨-syntax : (A : Type a) β†’ (𝒦 A β†’ Type p) β†’ Type _
Ξ¨-syntax _ = Ξ¨

syntax Ξ¨-syntax A (Ξ» x β†’ e) = Ξ¨[ x ⦂ 𝒦 A ] ↦ e

ψ : Type a β†’ Type b β†’ Type _
ψ A B = Ψ {A = A} (const B)

⟦_⟧ : {P : 𝒦 A β†’ Type p} β†’ Ξ¨ P β†’ (xs : 𝒦 A) β†’ P xs
⟦ alg ⟧ βˆ… = alg .fst βˆ…
⟦ alg ⟧ (x ∷ xs) = alg .fst (x ∷ xs ⟨ ⟦ alg ⟧ xs ⟩)
⟦ alg ⟧ (comm x y xs i) = alg .snd .c-com x y xs (⟦ alg ⟧ xs) i
⟦ alg ⟧ (dup x xs i) = alg .snd .c-dup x xs (⟦ alg ⟧ xs) i
⟦ alg ⟧ (trunc xs ys p q i j) =
  isOfHLevel→isOfHLevelDep 2
    (alg .snd .c-trunc)
    (⟦ alg ⟧ xs) (⟦ alg ⟧ ys)
    (cong ⟦ alg ⟧ p) (cong ⟦ alg ⟧ q)
    (trunc xs ys p q)
    i j

prop-coh : {A : Type a} {P : 𝒦 A β†’ Type p} {alg : Alg P} β†’ (βˆ€ xs β†’ isProp (P xs)) β†’ Coherent alg
prop-coh P-isProp .c-trunc xs = isProp→isSet (P-isProp xs)
prop-coh {P = P} {alg = alg} P-isProp .c-dup x xs ψ⟨xs⟩ =
 toPathP (P-isProp (x ∷ xs) (transp (Ξ» i β†’ P (dup x xs i)) i0 (alg (x ∷ (x ∷ xs) ⟨ alg (x ∷ xs ⟨ ψ⟨xs⟩ ⟩) ⟩))) (alg (x ∷ xs ⟨ ψ⟨xs⟩ ⟩)))
prop-coh {P = P} {alg = alg} P-isProp .c-com x y xs ψ⟨xs⟩ =
  toPathP (P-isProp (y ∷ x ∷ xs) (transp (Ξ» i β†’ P (comm x y xs i)) i0 (alg (x ∷ (y ∷ xs) ⟨ alg (y ∷ xs ⟨ ψ⟨xs⟩ ⟩) ⟩))) (alg (y ∷ (x ∷ xs) ⟨ alg (x ∷ xs ⟨ ψ⟨xs⟩ ⟩) ⟩)))

infix 4 _⊜_
record AnEquality (A : Type a) : Type a where
  constructor _⊜_
  field lhs rhs : 𝒦 A
open AnEquality public

EqualityProof-Alg : {B : Type b} (A : Type a) (P : 𝒦 A β†’ AnEquality B) β†’ Type (a β„“βŠ” b)
EqualityProof-Alg A P = Alg (Ξ» xs β†’ let Pxs = P xs in lhs Pxs ≑ rhs Pxs)

eq-coh : {A : Type a} {B : Type b} {P : 𝒦 A β†’ AnEquality B} {alg : EqualityProof-Alg A P} β†’ Coherent alg
eq-coh {P = P} = prop-coh Ξ» xs β†’ let Pxs = P xs in trunc (lhs Pxs) (rhs Pxs)

union-alg : ψ A (𝒦 A β†’ 𝒦 A)
union-alg .fst βˆ…                  ys = ys
union-alg .fst (x ∷ xs ⟨ P⟨xs⟩ ⟩)  ys = x ∷ P⟨xs⟩ ys
union-alg .snd .c-trunc _ = isSetΞ  Ξ» _ β†’ trunc
union-alg .snd .c-com x y xs P⟨xs⟩ i ys = comm x y (P⟨xs⟩ ys) i
union-alg .snd .c-dup x xs P⟨xs⟩ i ys = dup x (P⟨xs⟩ ys) i

infixr 5 _βˆͺ_
_βˆͺ_ : 𝒦 A β†’ 𝒦 A β†’ 𝒦 A
_βˆͺ_ = ⟦ union-alg ⟧

∷-distrib : βˆ€ (x : A) xs ys β†’ x ∷ (xs βˆͺ ys) ≑ xs βˆͺ (x ∷ ys)
∷-distrib x = ⟦ alg x ⟧
  where
  alg : βˆ€ x β†’ Ξ¨[ xs ⦂ 𝒦 A ] ↦ (βˆ€ ys β†’ x ∷ (xs βˆͺ ys) ≑ xs βˆͺ (x ∷ ys))
  alg x .fst βˆ… ys = refl
  alg x .fst (y ∷ xs ⟨ P⟨xs⟩ ⟩) ys = comm x y (xs βˆͺ ys) ΝΎ cong (y ∷_) (P⟨xs⟩ ys)
  alg x .snd = prop-coh Ξ» _ β†’ isPropΞ  Ξ» _ β†’ trunc _ _ 

βˆͺ-idem : (xs : 𝒦 A) β†’ xs βˆͺ xs ≑ xs
βˆͺ-idem = ⟦ alg ⟧
  where
  alg : Ξ¨[ xs ⦂ 𝒦 A ] ↦ ((xs βˆͺ xs) ≑ xs)
  alg .fst βˆ… = refl
  alg .snd = eq-coh
  alg .fst (x ∷ xs ⟨ P⟨xs⟩ ⟩) =
    (x ∷ xs) βˆͺ (x ∷ xs) β‰‘Λ˜βŸ¨ ∷-distrib x (x ∷ xs) xs ⟩
    x ∷ x ∷ xs βˆͺ xs β‰‘βŸ¨ dup x (xs βˆͺ xs) ⟩
    x ∷ xs βˆͺ xs β‰‘βŸ¨ cong (x ∷_) P⟨xs⟩ ⟩
    x ∷ xs ∎

βˆͺ-idΚ³ : (xs : 𝒦 A) β†’ (xs βˆͺ βˆ… ≑ xs)
βˆͺ-idΚ³ = ⟦ alg ⟧
  where
  alg : Ξ¨[ xs ⦂ 𝒦 A ] ↦ (xs βˆͺ βˆ… ≑ xs)
  alg .fst βˆ… = refl
  alg .fst (x ∷ xs ⟨ P⟨xs⟩ ⟩) = cong (x ∷_) P⟨xs⟩
  alg .snd = eq-coh

βˆͺ-com : (xs ys : 𝒦 A) β†’ (xs βˆͺ ys ≑ ys βˆͺ xs)
βˆͺ-com = ⟦ alg ⟧
  where
  alg : Ξ¨[ xs ⦂ 𝒦 A ] ↦ (βˆ€ ys β†’ xs βˆͺ ys ≑ ys βˆͺ xs)
  alg .fst βˆ… ys = sym (βˆͺ-idΚ³ ys)
  alg .fst (x ∷ xs ⟨ P⟨xs⟩ ⟩) ys = cong (x ∷_) (P⟨xs⟩ ys) ; ∷-distrib x ys xs
  alg .snd = prop-coh Ξ» _ β†’ isPropΞ  Ξ» _ β†’ trunc _ _

βˆͺ-assoc : (xs ys zs : 𝒦 A) β†’ ((xs βˆͺ ys) βˆͺ zs ≑ xs βˆͺ (ys βˆͺ zs))
βˆͺ-assoc = ⟦ alg ⟧
  where
  alg : Ξ¨[ xs ⦂ 𝒦 A ] ↦ (βˆ€ ys zs β†’ (xs βˆͺ ys) βˆͺ zs ≑ xs βˆͺ (ys βˆͺ zs))
  alg .fst βˆ… ys zs = refl
  alg .fst (x ∷ xs ⟨ P⟨xs⟩ ⟩) ys zs = cong (x ∷_) (P⟨xs⟩ ys zs)
  alg .snd = prop-coh Ξ» _ β†’ isPropΞ  Ξ» _ β†’ isPropΞ  Ξ» _ β†’ trunc _ _

𝒦-map : (A β†’ B) β†’ 𝒦 A β†’ 𝒦 B
𝒦-map f = ⟦ map-alg f ⟧
  where
  map-alg : (A β†’ B) β†’ Ξ¨[ xs ⦂ 𝒦 A ] ↦ 𝒦 B
  map-alg f .fst βˆ… = βˆ…
  map-alg f .fst (x ∷ _ ⟨ xs ⟩) = f x ∷ xs
  map-alg f .snd .c-trunc _ = trunc
  map-alg f .snd .c-com x y _ = comm (f x) (f y)
  map-alg f .snd .c-dup x _ = dup (f x)

map-βˆͺ : (f : A β†’ B) (xs ys : 𝒦 A) β†’ 𝒦-map f xs βˆͺ 𝒦-map f ys ≑ 𝒦-map f (xs βˆͺ ys)
map-βˆͺ f xs ys = ⟦ alg f ys ⟧ xs
  where
  alg : (f : A β†’ B) (ys : 𝒦 A) β†’ Ξ¨[ xs ⦂ 𝒦 A ] ↦ ((𝒦-map f xs βˆͺ 𝒦-map f ys) ≑ 𝒦-map f (xs βˆͺ ys))
  alg f ys .fst βˆ… = refl
  alg f ys .fst (x ∷ _ ⟨ xs ⟩) = cong (f x ∷_) xs
  alg f ys .snd = prop-coh Ξ» _ β†’ trunc _ _

module _ {A : Type a} where
  open import Truth

  sup-sing : A β†’ 𝒦 A β†’ Ξ© a
  sup-sing x = ⟦ sup-alg x ⟧
    where
    sup-alg : A β†’ Ξ¨[ xs ⦂ 𝒦 A ] ↦ Ξ© _
    sup-alg x .fst βˆ… = True
    sup-alg x .fst (y ∷ _ ⟨ βŸ…xβŸ†βŠ‡xs ⟩) = (x |≑| y) |∧| βŸ…xβŸ†βŠ‡xs
    sup-alg x .snd .c-trunc _ = isSetΞ©
    sup-alg x .snd .c-com y z _ xs = sym (∧-assoc _ _ _) ; cong (_|∧| xs) (∧-com _ _ ) ; ∧-assoc _ _ _
    sup-alg x .snd .c-dup y _ xs = sym (∧-assoc _ _ _) ; cong (_|∧| xs) (∧-idem _)

  βŸ…_βŸ†βŠ‡_ : A β†’ 𝒦 A β†’ Type a
  βŸ… x βŸ†βŠ‡ xs = ProofOf (sup-sing x xs)

  sup-sing-βˆͺ : (x : A) (xs ys : 𝒦 A) β†’ βŸ… x βŸ†βŠ‡ xs β†’ βŸ… x βŸ†βŠ‡ ys β†’ βŸ… x βŸ†βŠ‡ (xs βˆͺ ys)
  sup-sing-βˆͺ x xs ys p q = ⟦ alg x ys q ⟧ xs p
    where
    alg : (x : A) (ys : 𝒦 A) β†’ βŸ… x βŸ†βŠ‡ ys β†’ Ξ¨[ xs ⦂ 𝒦 A ] ↦ (βŸ… x βŸ†βŠ‡ xs β†’ βŸ… x βŸ†βŠ‡ (xs βˆͺ ys))
    alg x ys q .fst βˆ… p = q
    alg x ys q .fst (y ∷ _ ⟨ P⟨xs⟩ ⟩) (p , ps) = p , P⟨xs⟩ ps
    alg x ys q .snd = prop-coh Ξ» xs β†’ isPropβ†’ (IsProp (sup-sing x (xs βˆͺ ys)))