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)(AB)\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.

Impredicatively🔗

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 PQP \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 PQP \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.

    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 [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]PQ, [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]).

    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 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[_]
  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 AK(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!

  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 f:ABf : 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)BK(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))π1AfB, (\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.

  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 [n]PB[n] \twoheadrightarrow P \to B to a meet of PBP \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
      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

  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 PQP \cup Q as PQP \uplus Q↩︎

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