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.

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

    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]β† 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]).

    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 = (Ξ» _ β†’ 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 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!
  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: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.

  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 [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 (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

  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β†©οΈŽ