open import 1Lab.Path.IdentitySystem open import 1Lab.Reflection.HLevel open import 1Lab.HLevel.Retracts open import 1Lab.HLevel.Universe open import 1Lab.Reflection using (arg ; typeError) open import 1Lab.Univalence open import 1Lab.HLevel open import 1Lab.Equiv open import 1Lab.Path open import 1Lab.Type open import Data.List.Base open import Meta.Idiom open import Meta.Bind 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.
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