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 $A$, i.e., a lattice $K(A)$¹ having the property that ${\mathbf{Hom}}_{{\mathrm{SLat}}}(K(A), B) \cong (A \to B)$, where on the right we have ordinary functions from $A$ to the (underlying set of) $B$. We’ll actually construct $K$ in two different ways: first impredicatively, then higher-inductively.

Impredicatively🔗

The impredicative construction of $K(A)$ is as follows: $K(A)$ is the object of Kuratowski-finite subsets of $A$, i.e., of predicates $P : A \to \Omega$ such that the total space $\sum S$ merely admits a surjection from some finite ordinal $[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)$ into a semilattice is subset union. This is because, under subset union, the universal property of a free semilattice holds “almost for free”: $K$-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 $A$ is assumed to have decidable equality, we can not compute the cardinality of the union $P \cup Q$ — and we have placed no such assumption on $A$. That’s why we’re using $K$-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 $K$-finite subset $S$ expresses a possible upper bound on the size of $S$, and in that case, we do not need decidable equality: the size of $P \cup Q$ is bounded above by $s(P) + s(Q)$, where we will abusively write $s$ 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] \uplus [k]$, and we know how to cover $P$ and $Q$ by $[n]$ and $[k]$ respectively, we can define an epimorphism

$$[n + k] \simeq [n] \uplus [k] {\twoheadrightarrow}P \cup Q\text{,}$$

by² showing that ${\mathrm{inl}}(x)$ (resp. ${\mathrm{inr}}(x)$) is associated with an element in $[n]$ (resp. $[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)$ 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 $A$. In fact, a different characterisation of $K(A)$ is as the smallest sub-semilattice of $K(A)$ containing the singletons and closed under union.

We shall refer to the singleton-assigning map $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)$.

  ηₛₗ : ∣ A ∣ → K-finite-subset
  ηₛₗ x = (λ y → elΩ (x ≡ y)) , inc ( , (λ _ → 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 $K$-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 \to B$ and a semilattice structure on $B$, we can extend this to a semilattice homomorphism³ $K(A) \to B$ by first expressing $S : K(A)$ as $\bigcup_{i:[n]} \eta(a_i)$ for some $n$, $a_i$, then computing $\bigcap_{i:[n]} f(a_i)$.

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

$$(\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] {\twoheadrightarrow}P \to B$ to a meet of $P \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