module 1Lab.Resizing where

Propositional resizing🔗

Ordinarily, the collection of all $\kappa \text{-small}$ predicates on $\kappa \text{-small}$ types lives in the next universe up, ${\kappa }^{+}\text{.}$ This is because predicates are not special in type theory: they are ordinary type families, that just so happen to be valued in propositions. For most purposes we can work with this limitation: this is called predicative mathematics. But, for a few classes of theorems, predicativity is too restrictive: Even if we don’t have a single universe of propositions that can accommodate all predicates, we would still like for universes to be closed under power-sets.

Using some of Agda’s more suspicious features, we can achieve this in a way which does not break computation too much. Specifically, we’ll use a combination of NO_UNIVERSE_CHECK, postulates, and rewrite rules.

We start with the NO_UNIVERSE_CHECK part: We define the small type of propositions, Ω, to be a record containing a Type (together with an irrelevant proof that this type is a proposition), but contrary to the universe checker, which would like us to put Ω : Type₁, we instead force Ω : Type.

{-# NO_UNIVERSE_CHECK #-}
record Ω : Type where
  constructor el
  field
    ∣_∣   : Type
    is-tr : is-prop ∣_∣
open Ω public

This type, a priori, only contains the propositions whose underlying type lives in the first universe. However, we can populate it using a NO_UNIVERSE_CHECK-powered higher inductive type, the “small propositional truncation”:

{-# NO_UNIVERSE_CHECK #-}
data □ {ℓ} (A : Type ℓ) : Type where
  inc    : A → □ A
  squash : (x y : □ A) → x ≡ y

Just like the ordinary propositional truncation, every type can be squashed, but unlike the ordinary propositional truncation, the □-squashing of a type always lives in the lowest universe. If $T$ is a proposition in any universe, $\square T$ is its name in the zeroth universe.

We can also prove a univalence principle for Ω:

Ω-ua : {A B : Ω} → (∣ A ∣ → ∣ B ∣) → (∣ B ∣ → ∣ A ∣) → A ≡ B
Ω-ua {A} {B} f g i .∣_∣ = ua (prop-ext! f g) i
Ω-ua {A} {B} f g i .is-tr =
  is-prop→pathp (λ i → is-prop-is-prop {A = ua (prop-ext! f g) i})
    (A .is-tr) (B .is-tr) i

instance abstract
  H-Level-Ω : ∀ {n} → H-Level Ω (2 + n)
  H-Level-Ω = basic-instance 2 $ retract→is-hlevel 2
    (λ r → el ∣ r ∣ (r .is-tr))
    (λ r → el ∣ r ∣ (r .is-tr))
    (λ x → Ω-ua (λ x → x) λ x → x)
    (n-Type-is-hlevel {lzero} 1)

The □ type former is a functor (in the handwavy sense that it supports a “map” operation), and can be projected from into propositions of any universe. These functions compute on incs, as usual.

□-map : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'}
      → (A → B) → □ A → □ B
□-map f (inc x) = inc (f x)
□-map f (squash x y i) = squash (□-map f x) (□-map f y) i

□-rec : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} → is-prop B → (A → B) → □ A → B
□-rec bp f (inc x)        = f x
□-rec bp f (squash x y i) = bp (□-rec bp f x) (□-rec bp f y) i

elΩ : ∀ {ℓ} (T : Type ℓ) → Ω
elΩ T .∣_∣ = □ T
elΩ T .is-tr = squash

Connectives🔗

The universe of small propositions contains true, false, conjunctions, disjunctions, and implications.

⊤Ω : Ω
∣ ⊤Ω ∣ = ⊤
⊤Ω .is-tr = hlevel 1

⊥Ω : Ω
∣ ⊥Ω ∣ = ⊥
⊥Ω .is-tr = hlevel 1

_∧Ω_ : Ω → Ω → Ω
∣ P ∧Ω Q ∣ = ∣ P ∣ × ∣ Q ∣
(P ∧Ω Q) .is-tr = hlevel 1

_∨Ω_ : Ω → Ω → Ω
∣ P ∨Ω Q ∣ = ∥ ∣ P ∣ ⊎ ∣ Q ∣ ∥
(P ∨Ω Q) .is-tr = hlevel 1

_→Ω_ : Ω → Ω → Ω
∣ P →Ω Q ∣ = ∣ P ∣ → ∣ Q ∣
(P →Ω Q) .is-tr = hlevel 1

¬Ω_ : Ω → Ω
¬Ω P = P →Ω ⊥Ω

Furthermore, we can quantify over types of arbitrary size and still land in Ω.

∃Ω : ∀ {ℓ} (A : Type ℓ) → (A → Ω) → Ω
∣ ∃Ω A P ∣ = □ (Σ[ x ∈ A ] ∣ P x ∣)
∃Ω A P .is-tr = squash

∀Ω : ∀ {ℓ} (A : Type ℓ) → (A → Ω) → Ω
∣ ∀Ω A P ∣ = □ (∀ (x : A) → ∣ P x ∣)
∀Ω A P .is-tr = squash

syntax ∃Ω A (λ x → B) = ∃Ω[ x ∈ A ] B
syntax ∀Ω A (λ x → B) = ∀Ω[ x ∈ A ] B

These connectives and quantifiers are only provided for completeness; if you find yourself building nested propositions, it is generally a good idea to construct the large proposition by hand, and then use truncation to turn it into a small proposition.