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.
K[_] : Semilattice β K[_] = to-semilattice make-ka where open make-semilattice make-ka : make-semilattice K-finite-subset make-ka .has-is-set = hlevel! make-ka .top = (Ξ» _ β el β₯ (Ξ» x β absurd x)) , inc (0 , (Ξ» { () }) , Ξ» { () }) make-ka .op = _βͺ_ make-ka .idl = Ξ£-prop-path! $ funext Ξ» i β Ξ©-ua (β₯-β₯-rec! (Ξ» { (inr x) β x ; (inl ()) })) (Ξ» x β inc (inr x)) make-ka .idempotent = Ξ£-prop-path! $ funext Ξ» i β Ξ©-ua (β₯-β₯-rec! (Ξ» { (inl x) β x ; (inr x) β x })) (Ξ» x β inc (inl x)) make-ka .commutative = Ξ£-prop-path! $ funext Ξ» i β Ξ©-ua (β₯-β₯-rec squash Ξ» { (inl x) β inc (inr x) ; (inr x) β inc (inl x) }) (β₯-β₯-rec squash Ξ» { (inl x) β inc (inr x) ; (inr x) β inc (inl x) }) make-ka .associative = Ξ£-prop-path! $ funext Ξ» i β Ξ©-ua (β₯-β₯-rec squash Ξ» where (inl x) β inc (inl (inc (inl x))) (inr x) β β₯-β₯-rec squash (Ξ» where (inl x) β inc (inl (inc (inr x))) (inr x) β inc (inr x)) x) (β₯-β₯-rec squash Ξ» where (inl x) β β₯-β₯-rec squash (Ξ» where (inl x) β inc (inl x) (inr x) β inc (inr (inc (inl x)))) x (inr x) β inc (inr (inc (inr x)))) private module KA = Semilattice K[_] K-fin-lt : β {x y : K-finite-subset} β (β i β i β y .fst β i β x .fst) β x KA.β€ y K-fin-lt wit = Ξ£-prop-path! $ funext Ξ» i β Ξ©-ua (Ξ» x β inc (inl x)) (β₯-β₯-rec! Ξ» { (inl x) β x ; (inr y) β wit _ y }) K-fin-ltβ² : β {x y : K-finite-subset} β x KA.β€ y β β i β i β y .fst β i β x .fst K-fin-ltβ² wit idx yβ² = transport (Ξ» i β idx β wit (~ i) .fst) (inc (inr yβ²))
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