module 1Lab.Resizing where
Propositional Resizingπ
Ordinarily, the collection of all -small predicates on -small 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
.
{-# 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
is a proposition in any universe,
is its name in the zeroth universe.
instance H-Level-β‘ : β {β} {T : Type β} {n} β H-Level (β‘ T) (suc n) H-Level-β‘ = prop-instance squash open hlevel-projection Ξ©-hlevel-proj : hlevel-projection (quote Ξ©.β£_β£) Ξ©-hlevel-proj .has-level = quote Ξ©.is-tr Ξ©-hlevel-proj .get-level x = pure (quoteTerm (suc zero)) Ξ©-hlevel-proj .get-argument (arg _ t β· _) = pure t Ξ©-hlevel-proj .get-argument _ = typeError []
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 inc
s, 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) _ _