open import Algebra.Monoid

open import Cat.Displayed.Univalence.Thin
open import Cat.Prelude

open import Data.Nat.Properties
open import Data.Fin.Closure
open import Data.Nat.Order
open import Data.Fin.Base
open import Data.Sum.Base

open import Order.Diagram.Glb
open import Order.Semilattice

module Order.Semilattice.Free where

# Free (semi)lattices🔗

We construct the free semilattice on a type $A$, i.e., a lattice $K(A)$1 having the property that ${\mathbf{Hom}}_{{\mathrm{SLat}}}(K(A), B) \cong (A \to B)$, where on the right we have ordinary functions from $A$ to the (underlying set of) $B$. We’ll actually construct $K$ in two different ways: first impredicatively, then higher-inductively.

## Impredicatively🔗

The impredicative construction of $K(A)$ is as follows: $K(A)$ is the object of Kuratowski-finite subsets of $A$, i.e., of predicates $P : A \to \Omega$ such that the total space $\sum S$ merely admits a surjection from some finite ordinal $[n] {\twoheadrightarrow}\sum S$.

module _ {} (A : Set ) where
K-finite-subset : Type
K-finite-subset =
Σ ( A   Ω) λ P
Nat λ n
Σ (Fin n  (Σ  A  λ x  x  P)) λ f
x   fibre f x

The operator we’ll choose to make $K(A)$ into a semilattice is subset union. This is because, under subset union, the universal property of a free semilattice holds “almost for free”: $K$-finite subsets admit a reduction theorem (which we will prove after we have defined the semilattice) into a join of singletons, and this theorem will be necessary to prove the universal property.

{- TODO [Amy 2022-12-27] Refactor Data.Power.Lattice so we can "just" use that instead -}
_∪_ : K-finite-subset  K-finite-subset  K-finite-subset
(P , pf)  (Q , qf) =  x  el  x  P  x  Q  squash) , do
(Pn , Pf , Ps)  pf
(Qn , Qf , Qs)  qf

Now, the astute reader has probably noticed that, unless $A$ is assumed to have decidable equality, we can not compute the cardinality of the union $P \cup Q$ — and we have placed no such assumption on $A$. That’s why we’re using $K$-finite, rather than just “finite”, subsets: since all we have to do is cover the subset with a finite ordinal, it’s not a problem to have duplicated elements.

Put another way, the “size field” of a $K$-finite subset $S$ expresses a possible upper bound on the size of $S$, and in that case, we do not need decidable equality: the size of $P \cup Q$ is bounded above by $s(P) + s(Q)$, where we will abusively write $s$ for “an arbitrary upper bound”. Note that this definition does not require choice to.. choose.. an upper bound, because we’re really computing a proposition.

let
cover : Fin Pn  Fin Qn  Σ  A   x   x  P  x  Q )
cover = λ where
(inl x)  Pf x .fst , inc (inl (Pf x .snd))
(inr x)  Qf x .fst , inc (inr (Qf x .snd))

Since $[n + k] = [n] \uplus [k]$, and we know how to cover $P$ and $Q$ by $[n]$ and $[k]$ respectively, we can define an epimorphism

$[n + k] \simeq [n] \uplus [k] {\twoheadrightarrow}P \cup Q\text{,}$

by2 showing that ${\mathrm{inl}}(x)$ (resp. ${\mathrm{inr}}(x)$) is associated with an element in $[n]$ (resp. $[k]$).

pure
$Pn + Qn , x cover (Equiv.from Finite-coproduct x)) , λ (elt , elt∈P∪Q) elt∈P∪Q >>= λ where (inl elt∈P) do (pix , path) Ps (elt , elt∈P) pure ( Equiv.to Finite-coproduct (inl pix) , ap cover (Equiv.η Finite-coproduct _) Σ-prop-path hlevel! (ap fst path)) (inr elt∈Q) do (qix , path) Qs (elt , elt∈Q) pure ( Equiv.to Finite-coproduct (inr qix) , ap cover (Equiv.η Finite-coproduct _) Σ-prop-path hlevel! (ap fst path)) Since $K(A)$ is closed under unions (and contains the least element), it follows that it’s a semilattice, being a sub-semilattice of the power set of $A$. In fact, a different characterisation of $K(A)$ is as the smallest sub-semilattice of $K(A)$ containing the singletons and closed under union. We shall refer to the singleton-assigning map $A \to K(A)$ as $\eta$, since it will play the role of our adjunction unit when we establish the universal property of $K(A)$. ηₛₗ : A K-finite-subset ηₛₗ x = y elΩ (x y)) , inc (1 , _ x , inc refl) , λ (y , p) inc (fzero , Σ-prop-path _ squash) (out! p))) We can now prove the aforementioned reduction theorem: Every element$S
K(A)$can be expressed (in a noncanonical way) as the finite union of a diagram of singletons. This is almost a pure restatement of the $K$-finiteness condition, but it will be very useful! K-reduce : (x : K-finite-subset) Nat λ n Σ (Fin n A ) λ f is-glb KA.po i ηₛₗ (f i)) x K-reduce (P , P-fin) = ∥-∥-map reduce P-fin where open is-glb reduce : Σ Nat n Σ (Fin n Σ A λ x x P) λ f x fibre f x ) Σ Nat λ n Σ (Fin n A ) λ f is-glb KA.po i ηₛₗ (f i)) (P , P-fin) reduce (card , cover , surj) = card , x cover x .fst) , λ where .glb≤fam i K-fin-lt {P , P-fin} {ηₛₗ (cover i .fst)} λ j i=j subst e P e ) (out! i=j) (cover i .snd) .greatest lb′ wit K-fin-lt {lb′} {P , P-fin} λ i i∈p ∥-∥-proj do (idx , path) surj (i , i∈p) pure (K-fin-lt′ {lb′} {ηₛₗ (cover idx .fst)} (wit idx) i (inc (ap fst path))) In a similar vein, given a map $f : A \to B$ and a semilattice structure on $B$, we can extend this to a semilattice homomorphism3 $K(A) \to B$ by first expressing $S : K(A)$ as $\bigcup_{i:[n]} \eta(a_i)$ for some $n$, $a_i$, then computing $\bigcap_{i:[n]} f(a_i)$. Normally this would only let us compute a map $K(A) \to \| B \|$ into the support of $B$, since we had to choose an expression for $S$, but it turns out that the diagram $\bigcap_{i:[n]} f(a_i)$ is not only a glb for the $f(a_i)$, but also for the family $(\sum_{x : A} P(x)) {\xrightarrow{\pi_1}} A {\xrightarrow{f}} B\text{,}$ and since glbs are unique, we can get our computed value out from under the truncation. fold-K : {ℓ′} (B : Semilattice ℓ′) ( A B ) K-finite-subset B fold-K B f (P , P-fin) = ε′ .fst module fold-K where module B = Semilattice B fam : (Σ A λ x P x ) B fam (x , _) = f x We need to do a slight bit of symbol pushing to “pull back”, so to speak, the meet of our family $[n] {\twoheadrightarrow}P \to B$ to a meet of $P \to B$, using surjectivity of the first map. ε : Σ Nat n Σ (Fin n Σ A λ x x P) λ f x fibre f x ) Σ B (is-glb B.po fam) ε (card , g , surj) = B.⋂ x fam (g x)) , λ where .is-glb.glb≤fam elt ∥-∥-rec B.≤-thin { (ix , p) B.⋂ x fam (g x)) B.≤ fam (g ix) B.= fam elt B.≤∎ }) (surj elt) .is-glb.greatest lb′ lb′<subset h.greatest lb′ λ i lb′<subset (g i) where module h = is-glb (B.⋂-is-glb x fam (g x))) ε′ : Σ B (is-glb B.po fam) ε′ = ∥-∥-rec (glb-unique _) ε P-fin open is-glb open make-left-adjoint make-free-slat : {} make-left-adjoint (Forget-structure (Semilattice-structure )) make-free-slat .free A = K[ A ] make-free-slat .unit x = ηₛₗ x make-free-slat .universal {x} {y} f = total-hom go pres where module y = Semilattice y open Monoid-hom go = fold-K x y f module go = fold-K x y f pres : Monoid-hom (Semilattice-on.to-monoid (K[ x ] .snd)) (Semilattice-on.to-monoid (y .snd)) _ pres .pres-id = refl pres .pres-⋆ (A , af) (B , bf) = ap fst$
glb-unique y.po (go.ε′ (_∪_ x (A , af) (B , bf) .fst) (_∪_ x (A , af) (B , bf) .snd)) $_ , λ where .glb≤fam (x , w) ∥-∥-proj$ w >>= λ where
(inl w)  pure $g1 .fst y.∩ g2 .fst y.≤ g1 .fst y.≤ _ y.≤∎ (inr w) pure$
g1 .fst y.∩ g2 .fst y.≤
g2 .fst             y.≤
_                   y.≤∎
.greatest lb′ f  y.∩-univ _
(g1.greatest lb′  i  f (_ , inc (inl (i .snd)))))
(g2.greatest lb′  i  f (_ , inc (inr (i .snd)))))
where
g1 = go.ε′ A af
g2 = go.ε′ B bf
module g1 = is-glb (g1 .snd)
module g2 = is-glb (g2 .snd)
make-free-slat .commutes {y = y} f = funext λ x  sym y.∩-idr
where module y = Semilattice y
make-free-slat .unique {x = x} {y = y} {f = f} {g = g} w =
Homomorphism-path λ arg  ∥-∥-proj {ap = y.has-is-set _ _} do
(card , diagram , glb)  K-reduce x arg
let
path : arg  KA.⋂ λ i  ηₛₗ x (diagram i)
path = ap fst $glb-unique KA.po (_ , glb) (_ , KA.⋂-is-glb λ i ηₛₗ x (diagram i)) f′ = make-free-slat .universal {x = x} {y = y} f pure$
f′ # arg
f′ # KA.⋂  i  ηₛₗ x (diagram i))
y.⋂  i  f′ # ηₛₗ x (diagram i))
y.⋂  i  f (diagram i))
y.⋂ {card}  i  g # ηₛₗ x (diagram i)) ≡˘
g # KA.⋂  i  ηₛₗ x (diagram i))       ≡˘
g # arg
where
module y = Semilattice y
module KA = Semilattice K[ x ]
module go = fold-K x y f

1. The reason for the name $K(A)$ will become clear soon!↩︎

2. Since we’re merely showing that fibres are inhabited, we can treat $P \cup Q$ as $P \uplus Q$↩︎

3. Here we construct the underlying map first, the proof that it’s a semilattice homomorphism follows↩︎