module 1Lab.Resizing where

Propositional ResizingπŸ”—

Ordinarily, the collection of all ΞΊ\kappa-small predicates on ΞΊ\kappa-small types lives in the next universe up, ΞΊ+\kappa^+. 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 TT is a proposition in any universe, β–‘T\Box 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 β„“β€²}
  β†’ {@(tactic hlevel-tactic-worker) pa : is-prop B}
  β†’ (A β†’ B) β†’ β–‘ A β†’ B
β–‘-rec! {pa = pa} f (inc x) = f x
β–‘-rec! {pa = pa} f (squash x y i) =
  pa (β–‘-rec! {pa = pa} f x) (β–‘-rec! {pa = pa} f y) i

out! : βˆ€ {β„“} {A : Type β„“}
     β†’ {@(tactic hlevel-tactic-worker) pa : is-prop A}
     β†’ β–‘ A β†’ A
out! {pa = pa} = β–‘-rec! {pa = pa} (Ξ» x β†’ x)

elΞ© : βˆ€ {β„“} (T : Type β„“) β†’ Ξ©
∣ elΞ© T ∣ = β–‘ T
elΞ© T .is-tr = squash
β–‘-elim
  : βˆ€ {β„“ β„“β€²} {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

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

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

β–‘-ap
  : βˆ€ {β„“ β„“β€²} {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

β–‘-bind
  : βˆ€ {β„“ β„“β€²} {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

instance
  Map-β–‘ : Map (eff β–‘)
  Map-β–‘ .Map._<$>_ = β–‘-map

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

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

_∈_ : βˆ€ {β„“} {A : Type β„“} β†’ A β†’ (A β†’ Ξ©) β†’ Type
x ∈ P = ∣ P x ∣

is-set→locally-small
  : βˆ€ {β„“} {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 = out! {pa = a-set _ _}
is-set→locally-small a-set .to-path-over p = is-prop→pathp (λ _ → squash) _ _