Smallness

The previous chapter ended on a warning about universes: V ℓ is a large type built from small indexing data, and its truth values live in hProp (ℓ-suc ℓ), one level up. The warning matters because every set-forming device the library offers, sett first among them, accepts only small input: a small index type, a small predicate. To build a set out of a property, the property's truth value must first be brought down a universe. This chapter builds the toolkit for exactly that, and its payoff is the part's first theorem worth framing: separation for Δ₀ formulas costs no axiom at all.

{-# OPTIONS --cubical --safe --guardedness #-}

open import Base.Prelude
open import Base.Truth

module V.Smallness {ℓ : Level} where

open import Base.Impredicativity using ( isSmall )
open import FOL.ZFStructure using ( ZFStructure; _↾_ )
open import FOL.Syntax
  using ( Formula; _∈̇_; _≐_; _∧̇_; _∨̇_; _⇒̇_; ¬̇_; ⊤̇; ⊥̇; ∃̇_; ∀̇_; ∀̇∈; ∃̇∈ )
open import FOL.LevyHierarchy
  using ( Δ₀; δ-∈; δ-≐; δ-∧; δ-∨; δ-⇒; δ-¬; δ-⊤; δ-⊥; δ-∀∈; δ-∃∈ )
import FOL.Semantics
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )

open import Cubical.Foundations.Equiv
  using ( _≃_; equivFun; invEq; invEquiv; secEq; propBiimpl→Equiv )
import Cubical.Functions.Logic as Logic
open import Cubical.Functions.Logic using ( ⇔toPath )
import Cubical.Data.Sum as Sum
open import Cubical.Data.Unit using ( tt* )
import Cubical.HITs.PropositionalTruncation as PT
open import Cubical.HITs.CumulativeHierarchy.Properties
  using ( _∼_; identityPrinciple; _∈ₛ_; ∈∈ₛ; ⟪_⟫; ⟪_⟫↪; ∈ₛ⟪_⟫↪_; ∈-asFiber )
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( module SeparationSet )

open TruthAlgebra (hPropAlgebra (ℓ-suc ℓ))
open ZFStructure 𝒮ᵥ

Being small

A proposition one universe up is small when it is equivalent to some proposition one universe down: the definition (isSmall) was minted in Part 0, where the resizing interface asserts it of every proposition wholesale. This chapter assumes no such thing. It earns instances, one atom at a time, and the whole chapter is an exercise in passing the earned witnesses around.

The atoms are small straight from the library. This is the local-smallness apparatus the previous chapter glimpsed: membership has a small twin ∈ₛ (∈∈ₛ converts back and forth), and equality of sets compresses to the bisimilarity ∼ through identityPrinciple.

small-∈ : (a b : S) → isSmall (a ∈ˢ b)
small-∈ a b = (a ∈ₛ b) ,
  propBiimpl→Equiv (snd (a ∈ˢ b)) (snd (a ∈ₛ b))
    (∈∈ₛ {a = a} {b = b} .fst) (∈∈ₛ {a = a} {b = b} .snd)

small-≡ : (a b : S) → isSmall (a ≈ˢ b)
small-≡ a b = (a ∼ b) , invEquiv identityPrinciple

The connectives preserve smallness

Each of the six propositional operations passes smallness witnesses through; each proof is the mechanical transport of a bi-implication. (The qualified

Logic names are the library's connectives at the lower level, the codomain of the compression.)

small⊓ : {P Q : hProp (ℓ-suc ℓ)} → isSmall P → isSmall Q → isSmall (P ⊓ Q)
small⊓ {P} {Q} (P' , eP) (Q' , eQ) = (P' Logic.⊓ Q') ,
  propBiimpl→Equiv (snd (P ⊓ Q)) (snd (P' Logic.⊓ Q'))
    (λ pq → equivFun eP (pq .fst) , equivFun eQ (pq .snd))
    (λ pq → invEq eP (pq .fst) , invEq eQ (pq .snd))

small⊔ : {P Q : hProp (ℓ-suc ℓ)} → isSmall P → isSmall Q → isSmall (P ⊔ Q)
small⊔ {P} {Q} (P' , eP) (Q' , eQ) = (P' Logic.⊔ Q') ,
  propBiimpl→Equiv (snd (P ⊔ Q)) (snd (P' Logic.⊔ Q'))
    (PT.map (Sum.map (equivFun eP) (equivFun eQ)))
    (PT.map (Sum.map (invEq eP) (invEq eQ)))

small⇒ : {P Q : hProp (ℓ-suc ℓ)} → isSmall P → isSmall Q → isSmall (P ⇒ Q)
small⇒ {P} {Q} (P' , eP) (Q' , eQ) = (P' Logic.⇒ Q') ,
  propBiimpl→Equiv (snd (P ⇒ Q)) (snd (P' Logic.⇒ Q'))
    (λ f p' → equivFun eQ (f (invEq eP p')))
    (λ g p → invEq eQ (g (equivFun eP p)))

small¬ : {P : hProp (ℓ-suc ℓ)} → isSmall P → isSmall (¬ P)
small¬ {P} (P' , eP) = (Logic.¬ P') ,
  propBiimpl→Equiv (snd (¬ P)) (snd (Logic.¬ P'))
    (λ np p' → np (invEq eP p'))
    (λ np' p → np' (equivFun eP p))

small⊤ : isSmall ⊤
small⊤ = Logic.⊤ ,
  propBiimpl→Equiv (⊤ .snd) (snd (Logic.⊤ {ℓ}))
    (λ _ → tt*) (λ _ → tt*)

small⊥ : isSmall ⊥
small⊥ = (⊥* , isProp⊥*) ,
  propBiimpl→Equiv isProp⊥* isProp⊥* (λ ()) (λ ())

Bounded quantifiers preserve smallness

Here is the load-bearing step, and the point where the syntax chapter's oldest promise pays off in the currency of universes. A quantifier over all of V ℓ ranges over a large type and has no reason to be small. A quantifier bounded by a set a can instead range over the library's small member type ⟪ a ⟫, the index type of a's family, and smallness survives. The two directions travel along ∈-asFiber, whose fibers are untruncated because ⟪ a ⟫↪ is an embedding: passing from "a member of a" back to "an index of ⟪ a ⟫" is a function, not a choice.

small-∀∈ : (a : S) {B : S → hProp (ℓ-suc ℓ)}
         → (∀ x → isSmall (B x))
         → isSmall (⋀ S (λ x → (x ∈ˢ a) ⇒ B x))
small-∀∈ a {B} sm = Qsm , propBiimpl→Equiv (snd big) (snd Qsm) fwd bwd
  where
  big = ⋀ S (λ x → (x ∈ˢ a) ⇒ B x)
  Qsm = Logic.∀[]-syntax (λ (m : ⟪ a ⟫) → sm (⟪ a ⟫↪ m) .fst)
  fwd : ⟨ big ⟩ → ⟨ Qsm ⟩
  fwd f m = equivFun (sm (⟪ a ⟫↪ m) .snd)
                     (f (⟪ a ⟫↪ m) (∈∈ₛ {a = ⟪ a ⟫↪ m} {b = a} .snd (∈ₛ⟪ a ⟫↪ m)))
  bwd : ⟨ Qsm ⟩ → ⟨ big ⟩
  bwd g x x∈a =
    subst (λ v → ⟨ B v ⟩) (mf .snd)
          (invEq (sm (⟪ a ⟫↪ (mf .fst)) .snd) (g (mf .fst)))
    where mf = ∈-asFiber {a = x} {b = a} x∈a

small-∃∈ : (a : S) {B : S → hProp (ℓ-suc ℓ)}
         → (∀ x → isSmall (B x))
         → isSmall (⋁ S (λ x → (x ∈ˢ a) ⊓ B x))
small-∃∈ a {B} sm = Qsm , propBiimpl→Equiv (snd big) (snd Qsm) fwd bwd
  where
  big = ⋁ S (λ x → (x ∈ˢ a) ⊓ B x)
  Qsm = Logic.∃[]-syntax (λ (m : ⟪ a ⟫) → sm (⟪ a ⟫↪ m) .fst)
  fwd : ⟨ big ⟩ → ⟨ Qsm ⟩
  fwd = PT.map λ where
    (x , x∈a , bx) →
      let mf = ∈-asFiber {a = x} {b = a} x∈a
      in mf .fst ,
         equivFun (sm (⟪ a ⟫↪ (mf .fst)) .snd)
                  (subst (λ v → ⟨ B v ⟩) (sym (mf .snd)) bx)
  bwd : ⟨ Qsm ⟩ → ⟨ big ⟩
  bwd = PT.map λ where
    (m , q) → ⟪ a ⟫↪ m , ∈∈ₛ {a = ⟪ a ⟫↪ m} {b = a} .snd (∈ₛ⟪ a ⟫↪ m)
            , invEq (sm (⟪ a ⟫↪ m) .snd) q

The separation pipe

What smallness buys: a pointwise-small predicate can be separated. The library's

SeparationSet accepts only small predicates, and a smallness witness is exactly the ticket in; the specification comes back in the model record's field shape. Every separation this part performs, whatever pays for the smallness, flows through this one pipe.

separateFromSmall : (a : S) (P : S → hProp (ℓ-suc ℓ))
                  → (∀ y → isSmall (P y))
                  → Σ[ s ∈ S ] (∀ y → (y ∈ˢ s) ≡ ((y ∈ˢ a) ⊓ P y))
separateFromSmall a P sm = Sep.SEPAREE , λ y → ⇔toPath (fwd y) (bwd y)
  where
  ϕₛ : S → hProp ℓ
  ϕₛ y = sm y .fst
  module Sep = SeparationSet a ϕₛ
  fwd : ∀ y → ⟨ y ∈ˢ Sep.SEPAREE ⟩ → ⟨ (y ∈ˢ a) ⊓ P y ⟩
  fwd y y∈s = ∈∈ₛ {a = y} {b = a} .snd (Sep.separation-ax y .fst y∈ₛs .fst)
            , invEq (sm y .snd) (Sep.separation-ax y .fst y∈ₛs .snd)
    where y∈ₛs = ∈∈ₛ {a = y} {b = Sep.SEPAREE} .fst y∈s
  bwd : ∀ y → ⟨ (y ∈ˢ a) ⊓ P y ⟩ → ⟨ y ∈ˢ Sep.SEPAREE ⟩
  bwd y yp = ∈∈ₛ {a = y} {b = Sep.SEPAREE} .snd (Sep.separation-ax y .snd
               (∈∈ₛ {a = y} {b = a} .fst (yp .fst) , equivFun (sm y .snd) (yp .snd)))

Δ₀ formulas evaluate small

Now the Δ₀ witnesses earn a second salary. One induction over the Δ₀ witness shows that the witnessed formula's truth value at any environment is small: the two atoms are the library compressions, the eight connective cases are the closure lemmas, and the two bounded-quantifier cases consume

small-∀∈ and small-∃∈. There is no case for the unbounded quantifiers, because the witness has no such constructors: absence is the classification. This is the second load-bearing induction over Δ₀ witnesses (absoluteness was the first), and it is why the Levy hierarchy doubles as a cost accounting: Δ₀ means free, in the precise sense of universe levels.

module SemanticsV = FOL.Semantics (hPropAlgebra (ℓ-suc ℓ)) 𝒮ᵥ
open SemanticsV using ( _^_ )

module Δ₀Small {ℓc} {K : Type ℓc} (ι : K → S) where

  open SemanticsV.At K ι

  Δ₀-small : ∀ {n} {φ : Formula K n} → Δ₀ φ → (γ : S ^ n) → isSmall (γ ⊨ φ)
  Δ₀-small (δ-∈ {t = t} {u}) γ = small-∈ (⟦ t ⟧ γ) (⟦ u ⟧ γ)
  Δ₀-small (δ-≐ {t = t} {u}) γ = small-≡ (⟦ t ⟧ γ) (⟦ u ⟧ γ)
  Δ₀-small (δ-∧ {φ = φ} {ψ} c d) γ =
    small⊓ {P = γ ⊨ φ} {Q = γ ⊨ ψ} (Δ₀-small c γ) (Δ₀-small d γ)
  Δ₀-small (δ-∨ {φ = φ} {ψ} c d) γ =
    small⊔ {P = γ ⊨ φ} {Q = γ ⊨ ψ} (Δ₀-small c γ) (Δ₀-small d γ)
  Δ₀-small (δ-⇒ {φ = φ} {ψ} c d) γ =
    small⇒ {P = γ ⊨ φ} {Q = γ ⊨ ψ} (Δ₀-small c γ) (Δ₀-small d γ)
  Δ₀-small (δ-¬ {φ = φ} c) γ = small¬ {P = γ ⊨ φ} (Δ₀-small c γ)
  Δ₀-small δ-⊤ γ = small⊤
  Δ₀-small δ-⊥ γ = small⊥
  Δ₀-small (δ-∀∈ {t = t} {φ = φ} c) γ =
    small-∀∈ (⟦ t ⟧ γ) {B = λ x → (x ∷ γ) ⊨ φ} (λ x → Δ₀-small c (x ∷ γ))
  Δ₀-small (δ-∃∈ {t = t} {φ = φ} c) γ =
    small-∃∈ (⟦ t ⟧ γ) {B = λ x → (x ∷ γ) ⊨ φ} (λ x → Δ₀-small c (x ∷ γ))

The theorem: Δ₀ separation is free

Compose the induction with the pipe, at the canonical constant interpretation, and the flagship falls out: a formula carrying a Δ₀ witness can be separated with no resizing and no axiom, --safe all the way down. The model chapter will still owe full separation, but this theorem is the first hard evidence for a running theme: the Δ₀ witnesses are portable assets, and carrying them pays.

open Δ₀Small id
open SemanticsV.At S id using ( _⊨_ )

separateΔ₀ : (a : S) (φ : Formula S ) → Δ₀ φ
           → Σ[ s ∈ S ] (∀ y → (y ∈ˢ s) ≡ ((y ∈ˢ a) ⊓ ((y ∷ []) ⊨ φ)))
separateΔ₀ a φ c = separateFromSmall a (λ y → (y ∷ []) ⊨ φ) (λ y → Δ₀-small c (y ∷ []))

Essentially small worlds

One more register of smallness, bought not by Δ₀ witnesses but by location. When the quantification range is itself equivalent to a small type, even the unbounded quantifiers preserve smallness: quantify along the equivalence. This does not contradict the cost accounting above, which priced quantifiers ranging over all of V ℓ; here the range is the carrier of a restricted structure 𝒮ᵥ ↾ M, and smallness is exactly what the restriction buys.

small-⋀ : {A : Type (ℓ-suc ℓ)} {X : Type ℓ} (e : X ≃ A) {B : A → hProp (ℓ-suc ℓ)}
        → (∀ a → isSmall (B a))
        → isSmall (⋀ A B)
small-⋀ {A} {X} e {B} sm = Qsm , propBiimpl→Equiv (snd big) (snd Qsm) fwd bwd
  where
  big = ⋀ A B
  Qsm = Logic.∀[]-syntax (λ (m : X) → sm (equivFun e m) .fst)
  fwd : ⟨ big ⟩ → ⟨ Qsm ⟩
  fwd f m = equivFun (sm (equivFun e m) .snd) (f (equivFun e m))
  bwd : ⟨ Qsm ⟩ → ⟨ big ⟩
  bwd g a = subst (λ v → ⟨ B v ⟩) (secEq e a)
                  (invEq (sm (equivFun e (invEq e a)) .snd) (g (invEq e a)))

small-⋁ : {A : Type (ℓ-suc ℓ)} {X : Type ℓ} (e : X ≃ A) {B : A → hProp (ℓ-suc ℓ)}
        → (∀ a → isSmall (B a))
        → isSmall (⋁ A B)
small-⋁ {A} {X} e {B} sm = Qsm , propBiimpl→Equiv (snd big) (snd Qsm) fwd bwd
  where
  big = ⋁ A B
  Qsm = Logic.∃[]-syntax (λ (m : X) → sm (equivFun e m) .fst)
  fwd : ⟨ big ⟩ → ⟨ Qsm ⟩
  fwd = PT.map λ where
    (a , ba) → invEq e a ,
               equivFun (sm (equivFun e (invEq e a)) .snd)
                        (subst (λ v → ⟨ B v ⟩) (sym (secEq e a)) ba)
  bwd : ⟨ Qsm ⟩ → ⟨ big ⟩
  bwd = PT.map λ where
    (m , q) → equivFun e m , invEq (sm (equivFun e m) .snd) q

The consequence: over an essentially small restricted structure, every formula evaluates small, no Δ₀ witness required. The quantifier clauses walk along the equivalence, the atoms drop back to V's atomic smallness through the first projection. This is "spoken inside a small world, everything said is small", and it is the engine of Part 4's single construction step.

module InnerSmall (M : S → hProp (ℓ-suc ℓ))
                  (X : Type ℓ) (e : X ≃ (Σ[ x ∈ S ] (x ∈ᶜ M)))
                  {ℓc} {K : Type ℓc}
                  (ι : K → Σ[ x ∈ S ] (x ∈ᶜ M)) where

  SM : Type (ℓ-suc ℓ)
  SM = Σ[ x ∈ S ] (x ∈ᶜ M)

  𝒮M : ZFStructure (hPropAlgebra (ℓ-suc ℓ))
  𝒮M = 𝒮ᵥ ↾ M

  module SemanticsM = FOL.Semantics (hPropAlgebra (ℓ-suc ℓ)) 𝒮M
  open SemanticsM.At K ι renaming ( _⊨_ to _⊨ᵐ_ ; ⟦_⟧ to ⟦_⟧ᵐ ) public

  ⊨ᵐ-small : ∀ {n} (φ : Formula K n) (δ : SM ^ n) → isSmall (δ ⊨ᵐ φ)
  ⊨ᵐ-small (t ∈̇ u)  δ = small-∈ (fst (⟦ t ⟧ᵐ δ)) (fst (⟦ u ⟧ᵐ δ))
  ⊨ᵐ-small (t ≐ u)  δ = small-≡ (fst (⟦ t ⟧ᵐ δ)) (fst (⟦ u ⟧ᵐ δ))
  ⊨ᵐ-small (φ ∧̇ ψ)  δ =
    small⊓ {P = δ ⊨ᵐ φ} {Q = δ ⊨ᵐ ψ} (⊨ᵐ-small φ δ) (⊨ᵐ-small ψ δ)
  ⊨ᵐ-small (φ ∨̇ ψ)  δ =
    small⊔ {P = δ ⊨ᵐ φ} {Q = δ ⊨ᵐ ψ} (⊨ᵐ-small φ δ) (⊨ᵐ-small ψ δ)
  ⊨ᵐ-small (φ ⇒̇ ψ)  δ =
    small⇒ {P = δ ⊨ᵐ φ} {Q = δ ⊨ᵐ ψ} (⊨ᵐ-small φ δ) (⊨ᵐ-small ψ δ)
  ⊨ᵐ-small (¬̇ φ)    δ = small¬ {P = δ ⊨ᵐ φ} (⊨ᵐ-small φ δ)
  ⊨ᵐ-small ⊤̇        δ = small⊤
  ⊨ᵐ-small ⊥̇        δ = small⊥
  ⊨ᵐ-small (∃̇ φ)    δ =
    small-⋁ e {B = λ xm → (xm ∷ δ) ⊨ᵐ φ} (λ xm → ⊨ᵐ-small φ (xm ∷ δ))
  ⊨ᵐ-small (∀̇ φ)    δ =
    small-⋀ e {B = λ xm → (xm ∷ δ) ⊨ᵐ φ} (λ xm → ⊨ᵐ-small φ (xm ∷ δ))
  ⊨ᵐ-small (∀̇∈ t φ) δ =
    small-⋀ e {B = λ xm → (fst xm ∈ˢ fst (⟦ t ⟧ᵐ δ)) ⇒ ((xm ∷ δ) ⊨ᵐ φ)} (λ xm →
      small⇒ {P = fst xm ∈ˢ fst (⟦ t ⟧ᵐ δ)} {Q = (xm ∷ δ) ⊨ᵐ φ}
        (small-∈ (fst xm) (fst (⟦ t ⟧ᵐ δ))) (⊨ᵐ-small φ (xm ∷ δ)))
  ⊨ᵐ-small (∃̇∈ t φ) δ =
    small-⋁ e {B = λ xm → (fst xm ∈ˢ fst (⟦ t ⟧ᵐ δ)) ⊓ ((xm ∷ δ) ⊨ᵐ φ)} (λ xm →
      small⊓ {P = fst xm ∈ˢ fst (⟦ t ⟧ᵐ δ)} {Q = (xm ∷ δ) ⊨ᵐ φ}
        (small-∈ (fst xm) (fst (⟦ t ⟧ᵐ δ))) (⊨ᵐ-small φ (xm ∷ δ)))

Recap

Smallness is equivalence to a proposition one universe down (isSmall); the atoms compress through the library, the connectives and the bounded quantifiers pass smallness witnesses along, and separateFromSmall is the one pipe from small predicates to sets. The induction Δ₀-small then makes the Levy hierarchy a cost accounting, with separateΔ₀ as the free tier. What Δ₀ cannot reach is priced in the model chapter, and the price has a name: resizing.