open import 1Lab.Path.IdentitySystem
open import 1Lab.Reflection.HLevel
open import 1Lab.HLevel.Retracts
open import 1Lab.HLevel.Universe
open import 1Lab.HIT.Truncation
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 ΞΊ\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.

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 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) _ _