\begin{code} {-# OPTIONS --cubical --safe --postfix-projections #-} module Algebra.Construct.Free.Semilattice.Direct where open import Algebra open import Prelude open import Path.Reasoning infixl 6 _∪_ \end{code} %<*direct-def> \begin{code} data 𝒦 (A : Type a) : Type a where η : A → 𝒦 A _∪_ : 𝒦 A → 𝒦 A → 𝒦 A ∅ : 𝒦 A ∪-assoc : ∀ xs ys zs → (xs ∪ ys) ∪ zs ≡ xs ∪ (ys ∪ zs) ∪-commutative : ∀ xs ys → xs ∪ ys ≡ ys ∪ xs ∪-idempotent : ∀ xs → xs ∪ xs ≡ xs ∪-identity : ∀ xs → xs ∪ ∅ ≡ xs trunc : isSet (𝒦 A) \end{code} %</direct-def> \begin{code} module _ (semiLattice : Semilattice b) where open Semilattice semiLattice module _ (sIsSet : isSet 𝑆) (h : A → 𝑆) where μ : 𝒦 A → 𝑆 μ (η x) = h x μ (xs ∪ ys) = μ xs ∙ μ ys μ ∅ = ε μ (∪-assoc xs ys zs i) = assoc (μ xs) (μ ys) (μ zs) i μ (∪-commutative xs ys i) = comm (μ xs) (μ ys) i μ (∪-idempotent xs i) = idem (μ xs) i μ (∪-identity xs i) = ∙ε (μ xs) i μ (trunc xs ys x y i j) = sIsSet (μ xs) (μ ys) (cong μ x) (cong μ y) i j module Eliminators where record _⇘_ {a p} (A : Type a) (P : 𝒦 A → Type p) : Type (a ℓ⊔ p) where constructor elim field ⟦_⟧-set : ∀ {xs} → isSet (P xs) ⟦_⟧∅ : P ∅ ⟦_⟧_∪_⟨_∪_⟩ : ∀ xs ys → P xs → P ys → P (xs ∪ ys) ⟦_⟧η : ∀ x → P (η x) private z = ⟦_⟧∅; f = ⟦_⟧_∪_⟨_∪_⟩ field ⟦_⟧-assoc : ∀ xs ys zs pxs pys pzs → f (xs ∪ ys) zs (f xs ys pxs pys) pzs ≡[ i ≔ P (∪-assoc xs ys zs i ) ]≡ f xs (ys ∪ zs) pxs (f ys zs pys pzs) ⟦_⟧-commutative : ∀ xs ys pxs pys → f xs ys pxs pys ≡[ i ≔ P (∪-commutative xs ys i) ]≡ f ys xs pys pxs ⟦_⟧-idempotent : ∀ xs pxs → f xs xs pxs pxs ≡[ i ≔ P (∪-idempotent xs i) ]≡ pxs ⟦_⟧-identity : ∀ xs pxs → f xs ∅ pxs z ≡[ i ≔ P (∪-identity xs i) ]≡ pxs ⟦_⟧⇓ : ∀ xs → P xs ⟦ η x ⟧⇓ = ⟦_⟧η x ⟦ xs ∪ ys ⟧⇓ = f xs ys ⟦ xs ⟧⇓ ⟦ ys ⟧⇓ ⟦ ∅ ⟧⇓ = z ⟦ ∪-assoc xs ys zs i ⟧⇓ = ⟦_⟧-assoc xs ys zs ⟦ xs ⟧⇓ ⟦ ys ⟧⇓ ⟦ zs ⟧⇓ i ⟦ ∪-commutative xs ys i ⟧⇓ = ⟦_⟧-commutative xs ys ⟦ xs ⟧⇓ ⟦ ys ⟧⇓ i ⟦ ∪-idempotent xs i ⟧⇓ = ⟦_⟧-idempotent xs ⟦ xs ⟧⇓ i ⟦ ∪-identity xs i ⟧⇓ = ⟦_⟧-identity xs ⟦ xs ⟧⇓ i ⟦ trunc xs ys x y i j ⟧⇓ = isOfHLevel→isOfHLevelDep 2 (λ xs → ⟦_⟧-set {xs}) ⟦ xs ⟧⇓ ⟦ ys ⟧⇓ (cong ⟦_⟧⇓ x) (cong ⟦_⟧⇓ y) (trunc xs ys x y) i j open _⇘_ public infixr 0 ⇘-syntax ⇘-syntax = _⇘_ syntax ⇘-syntax A (λ xs → Pxs) = xs ∈𝒦 A ⇒ Pxs record _⇲_ {a p} (A : Type a) (P : 𝒦 A → Type p) : Type (a ℓ⊔ p) where constructor elim-prop field ∥_∥-prop : ∀ {xs} → isProp (P xs) ∥_∥∅ : P ∅ ∥_∥_∪_⟨_∪_⟩ : ∀ xs ys → P xs → P ys → P (xs ∪ ys) ∥_∥η : ∀ x → P (η x) private z = ∥_∥∅; f = ∥_∥_∪_⟨_∪_⟩ ∥_∥⇑ = elim (λ {xs} → isProp→isSet (∥_∥-prop {xs})) z f ∥_∥η (λ xs ys zs pxs pys pzs → toPathP (∥_∥-prop (transp (λ i → P (∪-assoc xs ys zs i)) i0 (f (xs ∪ ys) zs (f xs ys pxs pys) pzs)) (f xs (ys ∪ zs) pxs (f ys zs pys pzs) ))) (λ xs ys pxs pys → toPathP (∥_∥-prop (transp (λ i → P (∪-commutative xs ys i)) i0 (f xs ys pxs pys)) (f ys xs pys pxs) )) (λ xs pxs → toPathP (∥_∥-prop (transp (λ i → P (∪-idempotent xs i)) i0 (f xs xs pxs pxs)) pxs)) (λ xs pxs → toPathP (∥_∥-prop (transp (λ i → P (∪-identity xs i)) i0 (f xs ∅ pxs z)) pxs)) ∥_∥⇓ = ⟦ ∥_∥⇑ ⟧⇓ open _⇲_ public elim-prop-syntax : ∀ {a p} → (A : Type a) → (𝒦 A → Type p) → Type (a ℓ⊔ p) elim-prop-syntax = _⇲_ syntax elim-prop-syntax A (λ xs → Pxs) = xs ∈𝒦 A ⇒∥ Pxs ∥ module _ {a} {A : Type a} where open Semilattice open CommutativeMonoid open Monoid 𝒦-semilattice : Semilattice a 𝒦-semilattice .commutativeMonoid .monoid .𝑆 = 𝒦 A 𝒦-semilattice .commutativeMonoid .monoid ._∙_ = _∪_ 𝒦-semilattice .commutativeMonoid .monoid .ε = ∅ 𝒦-semilattice .commutativeMonoid .monoid .assoc = ∪-assoc 𝒦-semilattice .commutativeMonoid .monoid .ε∙ x = ∪-commutative ∅ x ; ∪-identity x 𝒦-semilattice .commutativeMonoid .monoid .∙ε = ∪-identity 𝒦-semilattice .commutativeMonoid .comm = ∪-commutative 𝒦-semilattice .idem = ∪-idempotent import Algebra.Construct.Free.Semilattice as Listed Listed→Direct : Listed.𝒦 A → 𝒦 A Listed→Direct = Listed.μ 𝒦-semilattice trunc η Direct→Listed : 𝒦 A → Listed.𝒦 A Direct→Listed = μ Listed.𝒦-semilattice Listed.trunc (Listed._∷ Listed.[]) Listed→Direct→Listed : (xs : Listed.𝒦 A) → Direct→Listed (Listed→Direct xs) ≡ xs Listed→Direct→Listed = ∥ ldl ∥⇓ where open Listed using (_⇲_; elim-prop-syntax) open _⇲_ ldl : xs ∈𝒦 A ⇒∥ Direct→Listed (Listed→Direct xs) ≡ xs ∥ ∥ ldl ∥-prop = Listed.trunc _ _ ∥ ldl ∥[] = refl ∥ ldl ∥ x ∷ xs ⟨ Pxs ⟩ = cong (x Listed.∷_) Pxs open Eliminators Direct→Listed→Direct : (xs : 𝒦 A) → Listed→Direct (Direct→Listed xs) ≡ xs Direct→Listed→Direct = ∥ dld ∥⇓ where dld : xs ∈𝒦 A ⇒∥ Listed→Direct (Direct→Listed xs) ≡ xs ∥ ∥ dld ∥-prop = trunc _ _ ∥ dld ∥∅ = refl ∥ dld ∥η x = ∪-identity (η x) ∥ dld ∥ xs ∪ ys ⟨ Pxs ∪ Pys ⟩ = sym (Listed.∙-hom 𝒦-semilattice trunc η (Direct→Listed xs) (Direct→Listed ys)) ; cong₂ _∪_ Pxs Pys Direct⇔Listed : 𝒦 A ⇔ Listed.𝒦 A Direct⇔Listed .fun = Direct→Listed Direct⇔Listed .inv = Listed→Direct Direct⇔Listed .rightInv = Listed→Direct→Listed Direct⇔Listed .leftInv = Direct→Listed→Direct \end{code}