module 1Lab.Resizing where

Propositional resizingπŸ”—

Ordinarily, the collection of all predicates on types lives in the next universe up, 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.

record Ξ© : Type where
  constructor el
    ∣_∣   : 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”:

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 is a proposition in any universe, 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
  : βˆ€ {β„“ β„“'} {A : Type β„“} {P : β–‘ A β†’ Type β„“'}
  β†’ (βˆ€ x β†’ is-prop (P x))
  β†’ (βˆ€ x β†’ P (inc x))
  β†’ βˆ€ x β†’ P x
β–‘-elim pprop go (inc x) = go x
β–‘-elim pprop go (squash x y i) =
  is-prop→pathp (λ i → pprop (squash x y i)) (░-elim pprop go x) (░-elim pprop go y) i

    : βˆ€ {β„“ β„“' β„“m} {A : Type β„“} {P : β–‘ A β†’ Type β„“'} ⦃ i : Inductive (βˆ€ x β†’ P (inc x)) β„“m ⦄
    β†’ ⦃ _ : βˆ€ {x} β†’ H-Level (P x) 1 ⦄
    β†’ Inductive (βˆ€ x β†’ P x) β„“m
  Inductive-β–‘ ⦃ i ⦄ = record
    { methods = i .Inductive.methods
    ; from    = Ξ» f β†’ β–‘-elim (Ξ» x β†’ hlevel 1) (i .Inductive.from f)

β–‘-out : βˆ€ {β„“} {A : Type β„“} β†’ is-prop A β†’ β–‘ A β†’ A
β–‘-out ap = β–‘-rec ap (Ξ» x β†’ x)

  : βˆ€ {β„“} {A : Type β„“}
  β†’ ⦃ _ : H-Level A 1 ⦄
  β†’ β–‘ A β†’ A
β–‘-out! = rec! Ξ» x β†’ x

  : βˆ€ {β„“ β„“'} {A : Type β„“} {B : Type β„“'}
  β†’ is-set B
  β†’ (f : A β†’ B)
  β†’ (βˆ€ x y β†’ f x ≑ f y)
  β†’ β–‘ A β†’ B
β–‘-rec-set B-set f f-const a =
  fst $ β–‘-elim
    (λ _ → is-constant→image-is-prop B-set f f-const)
    (Ξ» a β†’ f a , inc (a , refl))

β–‘-idempotent : βˆ€ {β„“} {A : Type β„“} β†’ is-prop A β†’ β–‘ A ≃ A
β–‘-idempotent aprop = prop-ext squash aprop (β–‘-out aprop) inc

  : βˆ€ {β„“ β„“'} {A : Type β„“} {B : Type β„“'}
  β†’ β–‘ (A β†’ B) β†’ β–‘ A β†’ β–‘ B
β–‘-ap (inc f) (inc g) = inc (f g)
β–‘-ap (inc f) (squash g g' i) = squash (β–‘-ap (inc f) g) (β–‘-ap (inc f) g') i
β–‘-ap (squash f f' i) g = squash (β–‘-ap f g) (β–‘-ap f' g) i

  : βˆ€ {β„“ β„“'} {A : Type β„“} {B : Type β„“'}
  β†’ β–‘ A β†’ (A β†’ β–‘ B) β†’ β–‘ B
β–‘-bind (inc x) f = f x
β–‘-bind (squash x x' i) f = squash (β–‘-bind x f) (β–‘-bind x' f) i

  Map-β–‘ : Map (eff β–‘)
  Map-β–‘ = β–‘-map

  Idiom-β–‘ : Idiom (eff β–‘)
  Idiom-β–‘ .Idiom.pure = inc
  Idiom-β–‘ .Idiom._<*>_ = β–‘-ap

  Bind-β–‘ : Bind (eff β–‘)
  Bind-β–‘ .Bind._>>=_ = β–‘-bind

  : βˆ€ {β„“} {A : Type β„“}
  β†’ is-set A
  β†’ is-identity-system {A = A} (Ξ» x y β†’ β–‘ (x ≑ y)) (Ξ» x β†’ inc refl)
is-set→locally-small a-set .to-path = ░-rec (a-set _ _) id
is-set→locally-small a-set .to-path-over p = is-prop→pathp (λ _ → squash) _ _

  : βˆ€ {P Q : Ξ©} ⦃ _ : H-Level ∣ Q ∣ 0 ⦄
  β†’ ∣ P ∣
  β†’ P ≑ Q
to-is-true prf = Ξ©-ua (Ξ» _ β†’ hlevel 0 .centre) (Ξ» _ β†’ prf)

tr-β–‘ : βˆ€ {β„“} {A : Type β„“} β†’ βˆ₯ A βˆ₯ β†’ β–‘ A
tr-β–‘ (inc x) = inc x
tr-β–‘ (squash x y i) = squash (tr-β–‘ x) (tr-β–‘ y) i

β–‘-tr : βˆ€ {β„“} {A : Type β„“} β†’ β–‘ A β†’ βˆ₯ A βˆ₯
β–‘-tr (inc x) = inc x
β–‘-tr (squash x y i) = squash (β–‘-tr x) (β–‘-tr y) i


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.