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 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 finite ordinal [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.

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)$ 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) = ε′ .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]↠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 ∥)
      → Σ ⌞ 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 ( (K[ x ] .snd)) ( (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)))))
      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
      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                                  ∎
    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↩︎