open import Algebra.Monoid open import Cat.Displayed.Univalence.Thin open import Cat.Functor.Adjoint 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 , i.e., a lattice 1 having the property that , where on the right we have ordinary functions from to the (underlying set of) . Weβll actually construct in two different ways: first impredicatively, then higher-inductively.
Impredicativelyπ
The impredicative construction of is as follows: is the object of Kuratowski-finite subsets of , i.e., of predicates such that the total space merely admits a surjection from some finite ordinal .
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 into a semilattice is subset union. This is because, under subset union, the universal property of a free semilattice holds βalmost for freeβ: -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 is assumed to have decidable equality, we can not compute the cardinality of the union β and we have placed no such assumption on . Thatβs why weβre using -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 -finite subset expresses a possible upper bound on the size of , and in that case, we do not need decidable equality: the size of is bounded above by , where we will abusively write 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 , and we know how to cover and by and respectively, we can define an epimorphism
by2 showing that (resp. ) is associated with an element in (resp. ).
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 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 . In fact, a different characterisation of is as the smallest sub-semilattice of containing the singletons and closed under union.
We shall refer to the singleton-assigning map as , since it will play the role of our adjunction unit when we establish the universal property of .
Ξ·ββ : β£ 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 -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 and a semilattice structure on , we can extend this to a semilattice homomorphism3 by first expressing as for some , , then computing .
Normally this would only let us compute a map into the support of , since we had to choose an expression for , but it turns out that the diagram is not only a glb for the , but also for the family
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 to a meet of , 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.β€β¨ h.glbβ€fam ix β©B.β€ fam (g ix) B.=β¨ ap fam p β©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.β€β¨ y.β©β€l β©y.β€ g1 .fst y.β€β¨ g1.glbβ€fam (x , w) β©y.β€ _ y.β€β (inr w) β pure $ g1 .fst y.β© g2 .fst y.β€β¨ y.β©β€r β©y.β€ g2 .fst y.β€β¨ g2.glbβ€fam (x , w) β©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 β‘β¨ ap (fβ² #_) path β©β‘ fβ² # KA.β (Ξ» i β Ξ·ββ x (diagram i)) β‘β¨ slat-pres-β (K[ x ] .snd) (y .snd) _ (fβ² .preserves) {card} _ β©β‘ y.β (Ξ» i β fβ² # Ξ·ββ x (diagram i)) β‘β¨ ap (y.β {card}) (funext Ξ» i β y.β©-idr) β©β‘ y.β (Ξ» i β f (diagram i)) β‘β¨ ap (y.β {card}) (funext Ξ» i β happly w (diagram i)) β©β‘ y.β {card} (Ξ» i β g # Ξ·ββ x (diagram i)) β‘Λβ¨ slat-pres-β (K[ x ] .snd) (y .snd) _ (g .preserves) {card} _ β©β‘Λ g # KA.β (Ξ» i β Ξ·ββ x (diagram i)) β‘Λβ¨ ap (g #_) path β©β‘Λ g # arg β where module y = Semilattice y module KA = Semilattice K[ x ] module go = fold-K x y f