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 standard finite set .
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 = (λ _ → ⊥Ω) , 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 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) = Glb.glb ε' 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 ∥) → Glb B.po fam ε (card , g , surj) = glb where module h = is-glb (B.⋂-is-glb (λ x → fam (g x))) glb : Glb B.po fam glb .Glb.glb = B.⋂ (λ x → fam (g x)) glb .Glb.has-glb .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) glb .Glb.has-glb .is-glb.greatest lb' lb'<subset = h.greatest lb' λ i → lb'<subset (g i) ε' : Glb B.po fam ε' = ∥-∥-rec (Glb-is-prop B.po) ε 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) = glb-unique y.po (Glb.has-glb (go.ε' (_∪_ x (A , af) (B , bf) .fst) (_∪_ x (A , af) (B , bf) .snd))) (λ where .glb≤fam (x , w) → ∥-∥-proj! $ w >>= λ where (inl w) → pure $ Glb.glb g1 y.∩ Glb.glb g2 y.≤⟨ y.∩≤l ⟩y.≤ Glb.glb g1 y.≤⟨ g1.glb≤fam (x , w) ⟩y.≤ _ y.≤∎ (inr w) → pure $ Glb.glb g1 y.∩ Glb.glb g2 y.≤⟨ y.∩≤r ⟩y.≤ Glb.glb g2 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 (Glb.has-glb g1) module g2 = is-glb (Glb.has-glb g2) 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 (y.Ob-is-set _ _) do (card , diagram , glb) ← K-reduce x arg let path : arg ≡ KA.⋂ λ i → ηₛₗ x (diagram i) path = 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