FreeSupLattice

Tom de Jong, 8 & 15 January 2021

We construct the free π“₯-sup-lattice on a set X : π“₯ as the (π“₯-)powerset of X.


{-# OPTIONS --safe --without-K #-}

open import MLTT.Spartan

open import UF.FunExt
open import UF.Lower-FunExt
open import UF.Powerset
open import UF.PropTrunc
open import UF.Sets
open import UF.Subsingletons
open import UF.Subsingletons-FunExt

module OrderedTypes.FreeSupLattice
        (pt : propositional-truncations-exist)
       where

open PropositionalTruncation pt


We define sup-lattices using a record. We also introduce convenient helpers
and syntax for reasoning about the order βŠ‘.


record SupLattice (π“₯ 𝓀 𝓣 : Universe) : 𝓀ω where
  constructor
    lattice
  field
    L : 𝓀 Μ‡
    L-is-set : is-set L
    _βŠ‘_ : L β†’ L β†’ 𝓣 Μ‡
    βŠ‘-is-prop-valued : (x y : L) β†’ is-prop (x βŠ‘ y)
    βŠ‘-is-reflexive : (x : L) β†’ x βŠ‘ x
    βŠ‘-is-transitive : (x y z : L) β†’ x βŠ‘ y β†’ y βŠ‘ z β†’ x βŠ‘ z
    βŠ‘-is-antisymmetric : (x y : L) β†’ x βŠ‘ y β†’ y βŠ‘ x β†’ x ＝ y
    ⋁ : {I : π“₯ Μ‡ } β†’ (I β†’ L) β†’ L
    ⋁-is-upperbound : {I : π“₯ Μ‡ } (Ξ± : I β†’ L) (i : I) β†’ Ξ± i βŠ‘ ⋁ Ξ±
    ⋁-is-lowerbound-of-upperbounds : {I : π“₯ Μ‡ } (Ξ± : I β†’ L) (x : L)
                                   β†’ ((i : I) β†’ Ξ± i βŠ‘ x)
                                   β†’ ⋁ Ξ± βŠ‘ x

  transitivity' : (x : L) {y z : L}
                β†’ x βŠ‘ y β†’ y βŠ‘ z β†’ x βŠ‘ z
  transitivity' x {y} {z} = βŠ‘-is-transitive x y z

  syntax transitivity' x u v = x βŠ‘βŸ¨ u ⟩ v
  infixr 0 transitivity'

  reflexivity' : (x : L) β†’ x βŠ‘ x
  reflexivity' x = βŠ‘-is-reflexive x

  syntax reflexivity' x = x βŠ‘βˆŽ
  infix 1 reflexivity'

  ＝-to-βŠ‘ : {x y : L} β†’ x ＝ y β†’ x βŠ‘ y
  ＝-to-βŠ‘ {x} {x} refl = reflexivity' x

  ⋁-transport : {I : π“₯ Μ‡ } (Ξ± Ξ² : I β†’ L)
              β†’ Ξ± ∼ Ξ²
              β†’ ⋁ Ξ± ＝ ⋁ Ξ²
  ⋁-transport {I} Ξ± Ξ² H = βŠ‘-is-antisymmetric (⋁ Ξ±) (⋁ Ξ²) u v
   where
    u : ⋁ Ξ± βŠ‘ ⋁ Ξ²
    u = ⋁-is-lowerbound-of-upperbounds Ξ± (⋁ Ξ²) Ξ³
     where
      Ξ³ : (i : I) β†’ Ξ± i βŠ‘ ⋁ Ξ²
      Ξ³ i = Ξ± i  βŠ‘βŸ¨ ＝-to-βŠ‘ (H i) ⟩
             Ξ² i βŠ‘βŸ¨ ⋁-is-upperbound Ξ² i ⟩
             ⋁ Ξ² βŠ‘βˆŽ
    v : ⋁ Ξ² βŠ‘ ⋁ Ξ±
    v = ⋁-is-lowerbound-of-upperbounds Ξ² (⋁ Ξ±) Ξ³
     where
      Ξ³ : (i : I) β†’ Ξ² i βŠ‘ ⋁ Ξ±
      Ξ³ i = Ξ² i βŠ‘βŸ¨ ＝-to-βŠ‘ (H i ⁻¹) ⟩
            Ξ± i βŠ‘βŸ¨ ⋁-is-upperbound Ξ± i ⟩
            ⋁ Ξ± βŠ‘βˆŽ


The powerset of X is an example of a sup-lattice and every subset can be written
as a union of singletons (this will come in useful later).


module _
        (pe : propext π“₯)
        (fe : funext π“₯ (π“₯ ⁺))
        (X : π“₯ Μ‡ )
        (X-is-set : is-set X)
       where

 open unions-of-small-families pt π“₯ π“₯ X

 π“Ÿ-lattice : SupLattice π“₯ (π“₯ ⁺) π“₯
 SupLattice.L π“Ÿ-lattice                              = π“Ÿ X
 SupLattice.L-is-set π“Ÿ-lattice                       = powersets-are-sets fe pe
 SupLattice._βŠ‘_ π“Ÿ-lattice                            = _βŠ†_
 SupLattice.βŠ‘-is-prop-valued π“Ÿ-lattice               = βŠ†-is-prop (lower-funext π“₯ (π“₯ ⁺) fe)
 SupLattice.βŠ‘-is-reflexive π“Ÿ-lattice                 = βŠ†-refl
 SupLattice.βŠ‘-is-transitive π“Ÿ-lattice                = βŠ†-trans
 SupLattice.βŠ‘-is-antisymmetric π“Ÿ-lattice             = (Ξ» A B β†’ subset-extensionality pe fe)
 SupLattice.⋁ π“Ÿ-lattice                              = ⋃
 SupLattice.⋁-is-upperbound π“Ÿ-lattice                = ⋃-is-upperbound
 SupLattice.⋁-is-lowerbound-of-upperbounds π“Ÿ-lattice = ⋃-is-lowerbound-of-upperbounds

 open singleton-subsets X-is-set

 express-subset-as-union-of-singletons :
  (A : π“Ÿ X) β†’ A ＝ ⋃ (❴_❡ ∘ (𝕋-to-carrier A))
 express-subset-as-union-of-singletons A = subset-extensionality pe fe u v
  where
   u : A βŠ† ⋃ (❴_❡ ∘ (𝕋-to-carrier A))
   u x a = ∣ (x , a) , refl ∣
   v : ⋃ (❴_❡ ∘ (𝕋-to-carrier A)) βŠ† A
   v x = βˆ₯βˆ₯-rec (∈-is-prop A x) Ξ³
    where
     Ξ³ : (Ξ£ i κž‰ 𝕋 A , x ∈ (❴_❡ ∘ 𝕋-to-carrier A) i)
       β†’ x ∈ A
     Ξ³ ((x , a) , refl) = a


Finally we will show that π“Ÿ X is the free π“₯-sup-lattice on a set X : π“₯.
Concretely, if L is a π“₯-sup-lattice and f : X β†’ L is any function,
then there is a *unique* mediating map fβ™­ : π“Ÿ X β†’ L such that:
(i)  fβ™­ is a sup-lattice homomorphism, i.e.
     - fβ™­ preserves joins (of families indexed by types in π“₯)
(ii) the diagram
           f
     X ---------> L
      \          ^
       \        /
      Ξ· \      / βˆƒ! fβ™­
         \    /
          v  /
          π“Ÿ X
     commutes.

(The map Ξ· : X β†’ π“Ÿ X is of course given by x ↦ ❴ x ❡.)


module _
        (𝓛 : SupLattice π“₯ 𝓀 𝓣)
       where

 open SupLattice 𝓛

 module _
         (X : π“₯ Μ‡ )
         (X-is-set : is-set X)
         (f : X β†’ L)
        where

  open singleton-subsets X-is-set

  open unions-of-small-families pt π“₯ π“₯ X

  fΜƒ : (A : π“Ÿ X) β†’ 𝕋 A β†’ L
  fΜƒ A = f ∘ (𝕋-to-carrier A)

  fβ™­ : π“Ÿ X β†’ L
  fβ™­ A = ⋁ {𝕋 A} (fΜƒ A)

  Ξ· : X β†’ π“Ÿ X
  η = ❴_❡

  fβ™­-after-Ξ·-is-f : fβ™­ ∘ Ξ· ∼ f
  fβ™­-after-Ξ·-is-f x = βŠ‘-is-antisymmetric ((fβ™­ ∘ Ξ·) x) (f x) u v
   where
    u : (fβ™­ ∘ Ξ·) x βŠ‘ f x
    u = ⋁-is-lowerbound-of-upperbounds (fΜƒ (Ξ· x)) (f x) Ξ³
     where
      Ξ³ : (i : 𝕋 (Ξ· x)) β†’ (fΜƒ (Ξ· x)) i βŠ‘ f x
      Ξ³ (x , refl) = βŠ‘-is-reflexive (f x)
    v : f x βŠ‘ (fβ™­ ∘ Ξ·) x
    v = ⋁-is-upperbound (Ξ» (x , _) β†’ f x) (x , refl)

  fβ™­-is-monotone : (A B : π“Ÿ X) β†’ A βŠ† B β†’ fβ™­ A βŠ‘ fβ™­ B
  fβ™­-is-monotone A B s = ⋁-is-lowerbound-of-upperbounds (fΜƒ A) (fβ™­ B) Ξ³
   where
    Ξ³ : (i : Ξ£ x κž‰ X , x ∈ A) β†’ fΜƒ A i βŠ‘ ⋁ (fΜƒ B)
    Ξ³ (x , a) = ⋁-is-upperbound (fΜƒ B) (x , s x a)

  fβ™­-preserves-joins : (I : π“₯ Μ‡ ) (Ξ± : I β†’ π“Ÿ X)
                     β†’ fβ™­ (⋃ Ξ±) ＝ ⋁ (fβ™­ ∘ Ξ±)
  fβ™­-preserves-joins I Ξ± = βŠ‘-is-antisymmetric (fβ™­ (⋃ Ξ±)) (⋁ (fβ™­ ∘ Ξ±)) u v
   where
    u : ⋁ (fΜƒ (⋃ Ξ±)) βŠ‘ ⋁ (Ξ» (i : I) β†’ ⋁ (fΜƒ (Ξ± i)))
    u = ⋁-is-lowerbound-of-upperbounds (fΜƒ (⋃ Ξ±)) (⋁ (Ξ» (i : I) β†’ ⋁ (fΜƒ (Ξ± i)))) Ξ³
     where
      Ξ³ : (p : (Ξ£ x κž‰ X , x ∈ ⋃ Ξ±))
        β†’ fΜƒ (⋃ Ξ±) p βŠ‘ ⋁ (Ξ» (i : I) β†’ ⋁ (fΜƒ (Ξ± i)))
      Ξ³ (x , a) = βˆ₯βˆ₯-rec (βŠ‘-is-prop-valued _ _) ψ a
       where
        ψ : (Ξ£ i κž‰ I , x ∈ Ξ± i) β†’ f x βŠ‘ ⋁ (Ξ» (i : I) β†’ ⋁ (fΜƒ (Ξ± i)))
        ψ (i , a') = f x                         βŠ‘βŸ¨ u₁ ⟩
                     ⋁ (fΜƒ (Ξ± i))                 βŠ‘βŸ¨ uβ‚‚ ⟩
                     ⋁ (Ξ» (i : I) β†’ ⋁ (fΜƒ (Ξ± i))) βŠ‘βˆŽ
         where
          u₁ = ⋁-is-upperbound (fΜƒ (Ξ± i)) (x , a')
          uβ‚‚ = ⋁-is-upperbound (Ξ» i' β†’ ⋁ (fΜƒ (Ξ± i'))) i
    v : ⋁ (Ξ» (i : I) β†’ ⋁ (fΜƒ (Ξ± i))) βŠ‘ ⋁ (fΜƒ (⋃ Ξ±))
    v = ⋁-is-lowerbound-of-upperbounds (Ξ» i β†’ ⋁ (fΜƒ (Ξ± i))) (⋁ (fΜƒ (⋃ Ξ±))) Ξ³
     where
      Ξ³ : (i : I)
        β†’ ⋁ (fΜƒ (Ξ± i)) βŠ‘ ⋁ (fΜƒ (⋃ Ξ±))
      Ξ³ i = ⋁-is-lowerbound-of-upperbounds (fΜƒ (Ξ± i)) (⋁ (fΜƒ (⋃ Ξ±))) ψ
       where
        ψ : (p : Ξ£ x κž‰ X , x ∈ Ξ± i)
          β†’ fΜƒ (Ξ± i) p βŠ‘ ⋁ (fΜƒ (⋃ Ξ±))
        ψ (x , a) = ⋁-is-upperbound (fΜƒ (⋃ Ξ±)) (x , ∣ i , a ∣)


Finally we prove that fβ™­ is the unique map with the above properties (i) & (ii).


  module _
          (pe : propext π“₯)
          (fe : funext π“₯ (π“₯ ⁺))
         where

   fβ™­-is-unique : (h : π“Ÿ X β†’ L)
                β†’ ((I : π“₯ Μ‡ ) (Ξ± : I β†’ π“Ÿ X) β†’ h (⋃ Ξ±) ＝ ⋁ (h ∘ Ξ±))
                β†’ (h ∘ Ξ· ∼ f)
                β†’ h ∼ fβ™­
   fβ™­-is-unique h p₁ pβ‚‚ A =
    h A               ＝⟨ ap h (express-subset-as-union-of-singletons pe fe X X-is-set A) ⟩
    h (⋃ (Ξ· ∘ pr₁))   ＝⟨ p₁ (𝕋 A) (Ξ· ∘ pr₁) ⟩
    ⋁ (h ∘ Ξ· ∘ pr₁)   ＝⟨ ⋁-transport (h ∘ Ξ· ∘ pr₁) (f ∘ pr₁) (Ξ» p β†’ pβ‚‚ (pr₁ p)) ⟩
    ⋁ (f ∘ pr₁)       ＝⟨refl⟩
    fβ™­ A ∎


Assuming some more function extensionality axioms, we can prove "homotopy
uniqueness", i.e. the tuple consisting of fβ™­ together with the proofs of (i) and
(ii) is unique. This follows easily from the above, because (i) and (ii) are
subsingletons (as L is a set).


  module _
          (pe : propext π“₯)
          (fe : funext (π“₯ ⁺) (π“₯ ⁺ βŠ” 𝓀))
         where

   homotopy-uniqueness-of-fβ™­ :
    βˆƒ! h κž‰ (π“Ÿ X β†’ L) , (((I : π“₯ Μ‡ ) (Ξ± : I β†’ π“Ÿ X) β†’ h (⋃ Ξ±) ＝ ⋁ (h ∘ Ξ±)))
                     Γ— (h ∘ Ξ· ∼ f)
   homotopy-uniqueness-of-fβ™­ =
    (fβ™­ , fβ™­-preserves-joins , fβ™­-after-Ξ·-is-f) , Ξ³
     where
      Ξ³ : (t : (Ξ£ h κž‰ (π“Ÿ X β†’ L) ,
                   (((I : π“₯ Μ‡ ) (Ξ± : I β†’ π“Ÿ X) β†’ h (⋃ Ξ±) ＝ ⋁ (h ∘ Ξ±)))
                 Γ— (h ∘ Ξ· ∼ f)))
        β†’ (fβ™­ , fβ™­-preserves-joins , fβ™­-after-Ξ·-is-f) ＝ t
      Ξ³ (h , p₁ , pβ‚‚) = to-subtype-＝ ψ
                        (dfunext (lower-funext (π“₯ ⁺) (π“₯ ⁺) fe)
                          (Ξ» A β†’ (fβ™­-is-unique
                                   pe
                                   (lower-funext (π“₯ ⁺) 𝓀 fe)
                                   h p₁ pβ‚‚ A) ⁻¹))
       where
        ψ : (k : π“Ÿ X β†’ L)
          β†’ is-prop (((I : π“₯ Μ‡ ) (Ξ± : I β†’ π“Ÿ X) β†’ k (⋃ Ξ±) ＝ ⋁ (k ∘ Ξ±))
                    Γ— k ∘ Ξ· ∼ f)
        ψ k = Γ—-is-prop (Ξ -is-prop fe
                              (Ξ» _ β†’ Ξ -is-prop (lower-funext (π“₯ ⁺) (π“₯ ⁺) fe)
                              (Ξ» _ β†’ L-is-set)))
                            (Ξ -is-prop (lower-funext (π“₯ ⁺) (π“₯ ⁺) fe)
                              (Ξ» _ β†’ L-is-set))