module Order.Semilattice.Free where

Free (semi)lattices🔗

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


The impredicative construction of K(A)K(A) is as follows: K(A)K(A) is the object of Kuratowski-finite subsets of AA, i.e., of predicates P:A→ΩP : A \to \Omega such that the total space ∑S\sum S merely admits a surjection from some standard finite set [n]↠∑S[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)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”: KK-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 AA is assumed to have decidable equality, we can not compute the cardinality of the union PâˆȘQP \cup Q — and we have placed no such assumption on AA. That’s why we’re using KK-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 KK-finite subset SS expresses a possible upper bound on the size of SS, and in that case, we do not need decidable equality: the size of PâˆȘQP \cup Q is bounded above by s(P)+s(Q)s(P) + s(Q), where we will abusively write ss 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.

      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]⊎[k][n + k] = [n] \uplus [k], and we know how to cover PP and QQ by [n][n] and [k][k] respectively, we can define an epimorphism

[n+k]≃[n]⊎[k]↠PâˆȘQ, [n + k] \simeq [n] \uplus [k] \twoheadrightarrow P \cup Q\text{,}

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

      $ 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 ( 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 ( Finite-coproduct (inr qix)
               , ap cover (Equiv.η Finite-coproduct _)
               ∙ Σ-prop-path hlevel! (ap fst path))

Since K(A)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 AA. In fact, a different characterisation of K(A)K(A) is as the smallest sub-semilattice of K(A)K(A) 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[_]
    : ∀ {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 })

    : ∀ {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 A→K(A)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)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)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 KK-finiteness condition, but it will be very useful!

    : (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→Bf : A \to B and a semilattice structure on BB, we can extend this to a semilattice homomorphism3 K(A)→BK(A) \to B by first expressing S:K(A)S : K(A) as ⋃i:[n]η(ai)\bigcup_{i:[n]} \eta(a_i) for some nn, aia_i, then computing ⋂i:[n]f(ai)\bigcap_{i:[n]} f(a_i).

Normally this would only let us compute a map K(A)→∄B∄K(A) \to \| B \| into the support of BB, since we had to choose an expression for SS, but it turns out that the diagram ⋂i:[n]f(ai)\bigcap_{i:[n]} f(a_i) is not only a glb for the f(ai)f(a_i), but also for the family

(∑x:AP(x))→π1A→fB, (\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.

    : ∀ {ℓ'} (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 [n]↠P→B[n] \twoheadrightarrow P \to B to a meet of P→BP \to B, 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
        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 ( (K[ x ] .snd)) ( (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))))))
      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
      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                                  ∎
    module y = Semilattice y
    module KA = Semilattice K[ x ]
    module go = fold-K x y f

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

  2. Since we’re merely showing that fibres are inhabited, we can treat PâˆȘQP \cup Q as P⊎QP \uplus Q↩

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