{-# OPTIONS --safe #-}
module Data.Set where
open import Prelude
infixr 5 _∪_
data 𝒦 (A : Type a) : Type a where
⟅_⟆ : A → 𝒦 A
_∪_ : 𝒦 A → 𝒦 A → 𝒦 A
∅ : 𝒦 A
ident : ∀ x → ∅ ∪ x ≡ x
idem : ∀ x → x ∪ x ≡ x
comm : ∀ x y → x ∪ y ≡ y ∪ x
assoc : ∀ x y z → (x ∪ y) ∪ z ≡ x ∪ (y ∪ z)
trunc : isSet (𝒦 A)
data 𝔎 {p} (A : Type a) (P : 𝒦 A → Type p) : Type (a ℓ⊔ p) where
∅ : 𝔎 A P
⟅_⟆ : A → 𝔎 A P
_⟨_⟩∪_⟨_⟩ : (xs : 𝒦 A) → (P⟨xs⟩ : P xs) → (ys : 𝒦 A) → (P⟨ys⟩ : P ys) → 𝔎 A P
embed : 𝔎 A P → 𝒦 A
embed ∅ = ∅
embed ⟅ x ⟆ = ⟅ x ⟆
embed (xs ⟨ _ ⟩∪ ys ⟨ _ ⟩) = xs ∪ ys
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
no-eta-equality
field
c-trunc : ∀ xs → isSet (P xs)
c-comm : ∀ xs P⟨xs⟩ ys P⟨ys⟩ →
PathP
(λ i → P (comm xs ys i))
(ϕ (xs ⟨ P⟨xs⟩ ⟩∪ ys ⟨ P⟨ys⟩ ⟩))
(ϕ (ys ⟨ P⟨ys⟩ ⟩∪ xs ⟨ P⟨xs⟩ ⟩))
c-idem : ∀ xs P⟨xs⟩ →
PathP
(λ i → P (idem xs i))
(ϕ (xs ⟨ P⟨xs⟩ ⟩∪ xs ⟨ P⟨xs⟩ ⟩))
P⟨xs⟩
c-ident : ∀ xs P⟨xs⟩ →
PathP
(λ i → P (ident xs i))
(ϕ (∅ ⟨ ϕ ∅ ⟩∪ xs ⟨ P⟨xs⟩ ⟩))
P⟨xs⟩
c-assoc : ∀ xs P⟨xs⟩ ys P⟨ys⟩ zs P⟨zs⟩ →
PathP
(λ i → P (assoc xs ys zs i))
(ϕ ((xs ∪ ys) ⟨ ϕ (xs ⟨ P⟨xs⟩ ⟩∪ ys ⟨ P⟨ys⟩ ⟩) ⟩∪ zs ⟨ P⟨zs⟩ ⟩))
(ϕ (xs ⟨ P⟨xs⟩ ⟩∪ (ys ∪ zs) ⟨ ϕ (ys ⟨ P⟨ys⟩ ⟩∪ zs ⟨ P⟨zs⟩ ⟩) ⟩))
open Coherent public
Ψ : (𝒦 A → Type p) → Type _
Ψ P = Σ[ ϕ ⦂ Alg P ] × Coherent ϕ
infixr -1 Ψ-syntax
Ψ-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 : Level} {P : 𝒦 A → Type p} → Ψ P → (xs : 𝒦 A) → P xs
⟦ alg ⟧ ∅ = alg .fst ∅
⟦ 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
⟦ alg ⟧ ⟅ x ⟆ = alg .fst ⟅ x ⟆
⟦ alg ⟧ (xs ∪ ys) = alg .fst (xs ⟨ ⟦ alg ⟧ xs ⟩∪ ys ⟨ ⟦ alg ⟧ ys ⟩)
⟦ alg ⟧ (ident xs i) = alg .snd .c-ident xs (⟦ alg ⟧ xs) i
⟦ alg ⟧ (idem xs i) = alg .snd .c-idem xs (⟦ alg ⟧ xs) i
⟦ alg ⟧ (comm xs ys i) = alg .snd .c-comm xs (⟦ alg ⟧ xs) ys (⟦ alg ⟧ ys) i
⟦ alg ⟧ (assoc xs ys zs i) = alg .snd .c-assoc xs (⟦ alg ⟧ xs) ys (⟦ alg ⟧ ys) zs (⟦ alg ⟧ zs) i
opaque
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-idem xs ψ⟨xs⟩ =
toPathP (P-isProp xs (transp (λ i → P (idem xs i)) i0 (alg (xs ⟨ ψ⟨xs⟩ ⟩∪ xs ⟨ ψ⟨xs⟩ ⟩ ))) ψ⟨xs⟩)
prop-coh {P = P} {alg = alg} P-isProp .c-ident xs ψ⟨xs⟩ =
toPathP (P-isProp xs (transp (λ i → P (ident xs i)) i0 (alg (∅ ⟨ alg ∅ ⟩∪ xs ⟨ ψ⟨xs⟩ ⟩ ))) ψ⟨xs⟩)
prop-coh {P = P} {alg = alg} P-isProp .c-comm xs ψ⟨xs⟩ ys ψ⟨ys⟩ =
toPathP (P-isProp (ys ∪ xs) (transp (λ i → P (comm xs ys i)) i0 (alg (xs ⟨ ψ⟨xs⟩ ⟩∪ ys ⟨ ψ⟨ys⟩ ⟩ ))) (alg (ys ⟨ ψ⟨ys⟩ ⟩∪ xs ⟨ ψ⟨xs⟩ ⟩ )))
prop-coh {P = P} {alg = alg} P-isProp .c-assoc xs ψ⟨xs⟩ ys ψ⟨ys⟩ zs ψ⟨zs⟩ =
toPathP (P-isProp (xs ∪ (ys ∪ zs)) (transp (λ i → P (assoc xs ys zs i)) i0 (alg ((xs ∪ ys) ⟨ (alg (xs ⟨ ψ⟨xs⟩ ⟩∪ ys ⟨ ψ⟨ys⟩ ⟩ )) ⟩∪ zs ⟨ ψ⟨zs⟩ ⟩ ))) (alg (xs ⟨ ψ⟨xs⟩ ⟩∪ (ys ∪ zs) ⟨ (alg (ys ⟨ ψ⟨ys⟩ ⟩∪ zs ⟨ ψ⟨zs⟩ ⟩ )) ⟩ )))
infix 4 _⊜_
record AnEquality (A : Type a) : Type a where
constructor _⊜_
field lhs rhs : 𝒦 A
open AnEquality
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)
opaque
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)
∪-idʳ : (xs : 𝒦 A) → (xs ∪ ∅ ≡ xs)
∪-idʳ xs = comm xs ∅ ⨾ ident xs
bind-alg : (A → 𝒦 B) → Ψ[ xs ⦂ 𝒦 A ] ↦ 𝒦 B
bind-alg k .fst ∅ = ∅
bind-alg k .fst ⟅ x ⟆ = k x
bind-alg k .fst (xs ⟨ P⟨xs⟩ ⟩∪ ys ⟨ P⟨ys⟩ ⟩) = P⟨xs⟩ ∪ P⟨ys⟩
bind-alg k .snd .c-trunc _ = trunc
bind-alg k .snd .c-comm _ xs _ ys = comm xs ys
bind-alg k .snd .c-idem _ = idem
bind-alg k .snd .c-ident _ = ident
bind-alg k .snd .c-assoc _ xs _ ys _ zs = assoc xs ys zs
infixl 4.5 _>>=_ _>>-_
_>>=_ : 𝒦 A → (A → 𝒦 B) → 𝒦 B
xs >>= k = ⟦ bind-alg k ⟧ xs
infixr 4.5 _>=>_
_>=>_ : (A → 𝒦 B) → (B → 𝒦 C) → A → 𝒦 C
(f >=> g) x = f x >>= g
𝒦-map : (A → B) → 𝒦 A → 𝒦 B
𝒦-map f xs = xs >>= (⟅_⟆ ∘ f)
_>>-_ : 𝒦 A → (A → B) → 𝒦 B
_>>-_ = flip 𝒦-map
∪->>= : (f : A → 𝒦 B) (xs ys : 𝒦 A) → (xs ∪ ys) >>= f ≡ (xs >>= f) ∪ (ys >>= f)
∪->>= f xs ys = refl
>>=-∪ : (xs : 𝒦 A) (f g : A → 𝒦 B) → xs >>= (λ x → f x ∪ g x) ≡ (xs >>= f) ∪ (xs >>= g)
>>=-∪ xs f g = ⟦ alg f g ⟧ xs
where
alg : (f g : A → 𝒦 B) → Ψ[ xs ⦂ 𝒦 A ] ↦ (xs >>= (λ x → f x ∪ g x) ≡ (xs >>= f) ∪ (xs >>= g))
alg f g .snd = eq-coh
alg f g .fst ∅ = sym (ident _)
alg f g .fst ⟅ x ⟆ = refl
alg f g .fst (xs ⟨ P⟨xs⟩ ⟩∪ ys ⟨ P⟨ys⟩ ⟩) =
(xs >>= (λ x → f x ∪ g x) ) ∪ (ys >>= (λ x → f x ∪ g x)) ≡⟨ cong₂ _∪_ P⟨xs⟩ P⟨ys⟩ ⟩
((xs >>= f) ∪ (xs >>= g)) ∪ ((ys >>= f) ∪ (ys >>= g)) ≡⟨ assoc (xs >>= f) _ _ ⟩
(xs >>= f) ∪ ((xs >>= g) ∪ ((ys >>= f) ∪ (ys >>= g))) ≡⟨ cong ((xs >>= f) ∪_) (comm (xs >>= g) _) ⟩
(xs >>= f) ∪ (((ys >>= f) ∪ (ys >>= g)) ∪ (xs >>= g)) ≡⟨ cong ((xs >>= f) ∪_) (assoc (ys >>= f) _ _) ⟩
(xs >>= f) ∪ ((ys >>= f) ∪ ((ys >>= g) ∪ (xs >>= g))) ≡˘⟨ assoc (xs >>= f) _ _ ⟩
((xs >>= f) ∪ (ys >>= f)) ∪ ((ys >>= g) ∪ (xs >>= g)) ≡⟨ cong (((xs >>= f) ∪ (ys >>= f)) ∪_) (comm _ _) ⟩
((xs >>= f) ∪ (ys >>= f)) ∪ ((xs >>= g) ∪ (ys >>= g)) ∎
>>=-id : (xs : 𝒦 A) → xs >>= ⟅_⟆ ≡ xs
>>=-id = ⟦ alg ⟧
where
alg : Ψ[ xs ⦂ 𝒦 A ] ↦ ((xs >>= ⟅_⟆) ≡ xs)
alg .fst ∅ = refl
alg .fst ⟅ x ⟆ = refl
alg .fst (xs ⟨ P⟨xs⟩ ⟩∪ ys ⟨ P⟨ys⟩ ⟩) = cong₂ _∪_ P⟨xs⟩ P⟨ys⟩
alg .snd = prop-coh λ _ → trunc _ _
𝒦-map-comp : (g : B → C) (f : A → B) (xs : 𝒦 A) → 𝒦-map g (𝒦-map f xs) ≡ 𝒦-map (g ∘ f) xs
𝒦-map-comp g f = ⟦ alg g f ⟧
where
alg : (g : B → C) (f : A → B) → Ψ[ xs ⦂ 𝒦 A ] ↦ 𝒦-map g (𝒦-map f xs) ≡ 𝒦-map (g ∘ f) xs
alg g f .snd = eq-coh
alg g f .fst ∅ = refl
alg g f .fst ⟅ x ⟆ = refl
alg g f .fst (xs ⟨ P⟨xs⟩ ⟩∪ ys ⟨ P⟨ys⟩ ⟩) =
𝒦-map g (𝒦-map f (xs ∪ ys)) ≡⟨ cong (𝒦-map g) (∪->>= (⟅_⟆ ∘ f) xs ys) ⟩
𝒦-map g (𝒦-map f xs ∪ 𝒦-map f ys) ≡⟨ ∪->>= (⟅_⟆ ∘ g) (𝒦-map f xs) (𝒦-map f ys) ⟩
𝒦-map g (𝒦-map f xs) ∪ 𝒦-map g (𝒦-map f ys) ≡⟨ cong₂ _∪_ P⟨xs⟩ P⟨ys⟩ ⟩
𝒦-map (g ∘ f) xs ∪ 𝒦-map (g ∘ f) ys ≡˘⟨ ∪->>= (⟅_⟆ ∘ g ∘ f) xs ys ⟩
𝒦-map (g ∘ f) (xs ∪ ys) ∎
⟅?⟆ : Maybe A → 𝒦 A
⟅?⟆ = maybe ∅ ⟅_⟆
𝒦-cat-maybes : (A → Maybe B) → 𝒦 A → 𝒦 B
𝒦-cat-maybes {A = A} {B = B} p xs = xs >>= (⟅?⟆ ∘ p)
_>>_ : 𝒦 A → 𝒦 B → 𝒦 B
xs >> ys = xs >>= const ys
return : A → 𝒦 A
return = ⟅_⟆
>>=∅ : ∀ (x : 𝒦 A) → (x >>= const ∅) ≡ (∅ ⦂ 𝒦 B)
>>=∅ = ⟦ alg ⟧
where
alg : Ψ[ x ⦂ 𝒦 A ] ↦ (x >>= const ∅) ≡ (∅ ⦂ 𝒦 B)
alg .snd = eq-coh
alg .fst ∅ = refl
alg .fst ⟅ x ⟆ = refl
alg .fst (xs ⟨ P⟨xs⟩ ⟩∪ ys ⟨ P⟨ys⟩ ⟩) = cong₂ _∪_ P⟨xs⟩ P⟨ys⟩ ⨾ ident _
>>=-assoc : (xs : 𝒦 A) (f : A → 𝒦 B) (g : B → 𝒦 C) → (xs >>= f) >>= g ≡ xs >>= (λ x → f x >>= g)
>>=-assoc xs f g = ⟦ alg f g ⟧ xs
where
alg : (f : A → 𝒦 B) (g : B → 𝒦 C) → Ψ[ xs ⦂ 𝒦 A ] ↦ (xs >>= f) >>= g ≡ xs >>= (λ x → f x >>= g)
alg f g .snd = eq-coh
alg f g .fst ∅ = refl
alg f g .fst ⟅ x ⟆ = refl
alg f g .fst (xs ⟨ P⟨xs⟩ ⟩∪ ys ⟨ P⟨ys⟩ ⟩) = cong₂ _∪_ P⟨xs⟩ P⟨ys⟩
module _ {a p} {A : Type a} (P : A → Type p) where
open import Truth.Definition p
open import Truth.Combinators
open import Truth.Logic
Any𝒦-alg : Ψ[ xs ⦂ 𝒦 A ] ↦ Ω
Any𝒦-alg .fst ∅ = False
Any𝒦-alg .fst ⟅ y ⟆ = Ω∥ P y ∥
Any𝒦-alg .fst (xs ⟨ P⟨xs⟩ ⟩∪ ys ⟨ P⟨ys⟩ ⟩) = P⟨xs⟩ |∨| P⟨ys⟩
Any𝒦-alg .snd .c-trunc _ = isSetΩ
Any𝒦-alg .snd .c-comm xs P⟨xs⟩ ys P⟨ys⟩ = ∨-com P⟨xs⟩ P⟨ys⟩
Any𝒦-alg .snd .c-idem xs P⟨xs⟩ = ∨-idem P⟨xs⟩
Any𝒦-alg .snd .c-ident xs P⟨xs⟩ = ∨-idˡ _
Any𝒦-alg .snd .c-assoc xs P⟨xs⟩ ys P⟨ys⟩ zs P⟨zs⟩ = ∨-assoc P⟨xs⟩ P⟨ys⟩ P⟨zs⟩
Any𝒦 : 𝒦 A → Type p
Any𝒦 = ProofOf ∘ ⟦ Any𝒦-alg ⟧
isProp-Any : ∀ xs → isProp (Any𝒦 xs)
isProp-Any xs = IsProp (⟦ Any𝒦-alg ⟧ xs)
infixr 5 _𝒦∈_
_𝒦∈_ : A → 𝒦 A → Type _
x 𝒦∈ xs = Any𝒦 (x ≡_) xs
module _ {p q} {P : A → Type p} {Q : A → Type q} where
𝒦-weaken-any : (∀ {x} → P x → Q x) →
∀ xs →
Any𝒦 P xs →
Any𝒦 Q xs
𝒦-weaken-any f = ⟦ alg f ⟧
where
open import HITs.PropositionalTruncation
alg : (∀ {x} → P x → Q x) → Ψ[ xs ⦂ 𝒦 A ] ↦ (Any𝒦 P xs → Any𝒦 Q xs)
alg f .snd = prop-coh λ xs → isProp→ (isProp-Any Q xs)
alg f .fst ⟅ _ ⟆ = ∥map∥ f
alg f .fst (_ ⟨ P⟨xs⟩ ⟩∪ _ ⟨ P⟨ys⟩ ⟩) = ∥map∥ (map-⊎ P⟨xs⟩ P⟨ys⟩)
module _ {A : Type a} {B : Type b} where
open import HITs.PropositionalTruncation
𝒦-map-with-∈ : (xs : 𝒦 A) → (∀ x → x 𝒦∈ xs → B) → 𝒦 B
𝒦-map-with-∈ = ⟦ alg ⟧
where
alg : Ψ[ xs ⦂ 𝒦 A ] ↦ ((∀ x → x 𝒦∈ xs → B) → 𝒦 B)
alg .fst ∅ _ = ∅
alg .fst ⟅ x ⟆ f = ⟅ f x ∣ refl ∣ ⟆
alg .fst (xs ⟨ P⟨xs⟩ ⟩∪ ys ⟨ P⟨ys⟩ ⟩) f = P⟨xs⟩ (λ x x∈p → f x ∣ inl x∈p ∣) ∪ P⟨ys⟩ λ x x∈p → f x ∣ inr x∈p ∣
alg .snd .c-trunc _ = isSetΠ λ _ → trunc
alg .snd .c-comm xs P⟨xs⟩ ys P⟨ys⟩ =
J
(λ zs xs∪ys≡zs → (l∈ : ∀ {z} → z 𝒦∈ xs → z 𝒦∈ zs) → (r∈ : ∀ {z} → z 𝒦∈ ys → z 𝒦∈ zs) →
PathP
(λ i → ((x : A) → x 𝒦∈ xs∪ys≡zs i → B) → 𝒦 B)
(λ f → P⟨xs⟩ (λ x x∈p → f x ∣ inl x∈p ∣) ∪ P⟨ys⟩ (λ x x∈p → f x ∣ inr x∈p ∣)) (λ f → P⟨ys⟩ (λ x x∈ → f x (r∈ x∈)) ∪ P⟨xs⟩ λ x x∈ → f x (l∈ x∈)))
(λ l∈ r∈ → funExt λ f → comm (P⟨xs⟩ _) (P⟨ys⟩ _) ⨾ cong₂ _∪_ (cong P⟨ys⟩ (funExt λ x → funExt λ x∈p → cong (f x) (squash _ _))) ((cong P⟨xs⟩ (funExt λ x → funExt λ x∈p → cong (f x) (squash _ _)))))
(comm xs ys)
(∣_∣ ∘ inr)
(∣_∣ ∘ inl)
alg .snd .c-ident xs P⟨xs⟩ =
J (λ zs ∅∪xs≡zs → (xs∈ : ∀ {z} → z 𝒦∈ xs → z 𝒦∈ zs) →
PathP
(λ i → ((x : A) → x 𝒦∈ ∅∪xs≡zs i → B) → 𝒦 B)
(λ f → ∅ ∪ P⟨xs⟩ λ x x∈ → f x ∣ inr x∈ ∣)
(λ f → P⟨xs⟩ λ x x∈ → f x (xs∈ x∈)))
(λ xs∈ → funExt λ f → ident _ ⨾ cong P⟨xs⟩ (funExt λ x → funExt λ x∈ → cong (f x) (squash _ _)))
(ident xs)
id
alg .snd .c-idem xs P⟨xs⟩ =
J
(λ zs xs∪xs≡zs → (xs∈ : ∀ {z} → z 𝒦∈ xs → z 𝒦∈ zs) →
PathP
(λ i → ((x : A) → x 𝒦∈ xs∪xs≡zs i → B) → 𝒦 B)
(λ f → P⟨xs⟩ (λ x x∈ → f x ∣ inl x∈ ∣) ∪ P⟨xs⟩ λ x x∈ → f x ∣ inr x∈ ∣)
λ f → P⟨xs⟩ λ x x∈ → f x (xs∈ x∈))
(λ xs∈ → funExt λ f → cong₂ _∪_ (cong P⟨xs⟩ (funExt (λ x → funExt λ x∈ → cong (f x) (squash _ _)))) ((cong P⟨xs⟩ (funExt (λ x → funExt λ x∈ → cong (f x) (squash _ _))))) ⨾ idem (P⟨xs⟩ (λ x x∈ → f x (xs∈ x∈))))
(idem xs)
id
alg .snd .c-assoc xs P⟨xs⟩ ys P⟨ys⟩ zs P⟨zs⟩ =
J
(λ rs xs∪ys∪zs≡rs → (xs∈ : ∀ {z} → z 𝒦∈ xs → z 𝒦∈ rs) → (ys∈ : ∀ {z} → z 𝒦∈ ys → z 𝒦∈ rs) → (zs∈ : ∀ {z} → z 𝒦∈ zs → z 𝒦∈ rs) →
PathP
(λ i → ((x : A) → x 𝒦∈ xs∪ys∪zs≡rs i → B) → 𝒦 B)
(λ f → (P⟨xs⟩ (λ x x∈ → f x ∣ inl ∣ inl x∈ ∣ ∣) ∪ P⟨ys⟩ λ x x∈ → f x ∣ inl ∣ inr x∈ ∣ ∣) ∪ P⟨zs⟩ λ x x∈ → f x ∣ inr x∈ ∣)
(λ f → P⟨xs⟩ (λ x x∈ → f x (xs∈ x∈)) ∪ (P⟨ys⟩ (λ x x∈ → f x (ys∈ x∈)) ∪ P⟨zs⟩ λ x x∈ → f x (zs∈ x∈)))
)
(λ xs∈ ys∈ zs∈ → funExt λ f → assoc (P⟨xs⟩ _) (P⟨ys⟩ _) (P⟨zs⟩ _)
⨾ cong₂ _∪_ (cong P⟨xs⟩ (funExt λ x → funExt λ x∈ → cong (f x) (squash _ _)))
(cong₂ _∪_ (cong P⟨ys⟩ (funExt λ x → funExt λ x∈ → cong (f x) (squash _ _)))
(cong P⟨zs⟩ (funExt λ x → funExt λ x∈ → cong (f x) (squash _ _)))))
(assoc xs ys zs)
(∣_∣ ∘ inl)
(∣_∣ ∘ inr ∘ ∣_∣ ∘ inl)
(∣_∣ ∘ inr ∘ ∣_∣ ∘ inr)
𝒦-map-with-∈-map : ∀ (f : A → B) xs → 𝒦-map-with-∈ xs (λ x x∈xs → f x) ≡ 𝒦-map f xs
𝒦-map-with-∈-map f = ⟦ alg f ⟧
where
alg : (f : A → B) → Ψ[ xs ⦂ 𝒦 A ] ↦ (𝒦-map-with-∈ xs (λ x x∈xs → f x) ≡ 𝒦-map f xs)
alg f .snd = eq-coh
alg f .fst ∅ = refl
alg f .fst ⟅ x ⟆ = refl
alg f .fst (xs ⟨ P⟨xs⟩ ⟩∪ ys ⟨ P⟨ys⟩ ⟩) = cong₂ _∪_ P⟨xs⟩ P⟨ys⟩
𝒦->>=-with-∈ : (xs : 𝒦 A) → (∀ x → x 𝒦∈ xs → 𝒦 B) → 𝒦 B
𝒦->>=-with-∈ xs f = 𝒦-map-with-∈ xs f >>= id
𝒦->>=-with-∈->>= : (f : A → 𝒦 B) (xs : 𝒦 A) → 𝒦->>=-with-∈ xs (const ∘′ f) ≡ (xs >>= f)
𝒦->>=-with-∈->>= f xs =
𝒦->>=-with-∈ xs (const ∘′ f) ≡⟨⟩
𝒦-map-with-∈ xs (const ∘′ f) >>= id ≡⟨ cong (_>>= id) (𝒦-map-with-∈-map f xs) ⟩
𝒦-map f xs >>= id ≡⟨ >>=-assoc xs _ _ ⟩
(xs >>= f) ∎
open import Data.Bool.Properties
𝒦-empty : 𝒦 A → Bool
𝒦-empty = ⟦ alg ⟧
where
alg : Ψ[ p ⦂ 𝒦 A ] ↦ Bool
alg .fst ∅ = true
alg .fst ⟅ x ⟆ = false
alg .fst (xs ⟨ l ⟩∪ ys ⟨ r ⟩) = l && r
alg .snd .c-trunc _ = isSetBool
alg .snd .c-comm _ l _ r = &&-comm l r
alg .snd .c-idem _ = &&-idem
alg .snd .c-ident _ P⟨xs⟩ = refl
alg .snd .c-assoc _ x _ y _ z = &&-assoc x y z
∅≢⟅⟆ : (x : A) → (∅ ⦂ 𝒦 A) ≢ ⟅ x ⟆
∅≢⟅⟆ x = true≢false ∘ cong 𝒦-empty