module Data.Set.Eliminators where

open import Prelude
open import Data.Set.Definition
open import HLevels

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

private
  variable
    p : Level
    P : 𝒦 A β†’ Type 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⟩ β†’
            Ο• (x ∷ (y ∷ xs) ⟨ Ο• (y ∷ xs ⟨ P⟨xs⟩ ⟩) ⟩)
               ≑[ i ≔ P (com x y xs i) ]≑
            Ο• (y ∷ (x ∷ xs) ⟨ Ο• (x ∷ xs ⟨ P⟨xs⟩ ⟩) ⟩ )

    c-dup : βˆ€ x xs P⟨xs⟩ β†’
            Ο• (x ∷ (x ∷ xs) ⟨ Ο• (x ∷ xs ⟨ P⟨xs⟩ ⟩) ⟩)
               ≑[ i ≔ P (dup x xs i) ]≑
            Ο• (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 ⟧ (com 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 (com 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)