open import 1Lab.Function.Surjection
open import 1Lab.Path.IdentitySystem
open import 1Lab.Reflection.HLevel
open import 1Lab.HLevel.Universe
open import 1Lab.Extensionality
open import 1Lab.HLevel.Closure
open import 1Lab.Reflection using (arg ; typeError)
open import 1Lab.Truncation
open import 1Lab.Univalence
open import 1Lab.Inductive
open import 1Lab.HLevel
open import 1Lab.Equiv
open import 1Lab.Path
open import 1Lab.Type

open import Data.List.Base
open import Data.Sum.Base

open import Meta.Idiom
open import Meta.Bind
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 closed computation too much. Specifically, we can use the evil NO_UNIVERSE_CHECK pragma: 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 second NO_UNIVERSE_CHECK pragma, this time forcing the propositional truncation of an arbitrary type into the first universe.

{-# 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. Thus 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 Ξ©: if are logically equivalent, then they are equal.

Ξ©-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 id id)
    (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
β–‘-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

instance
  Inductive-β–‘
    : βˆ€ {β„“ β„“' β„“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)

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

β–‘-out-rec : βˆ€ {β„“ β„“'} {A : Type β„“} {X : Type β„“'} β†’ is-prop A β†’ (A β†’ X) β†’ β–‘ A β†’ X
β–‘-out-rec A-prop go x = go (β–‘-out A-prop x)

β–‘-out-elim
  : βˆ€ {β„“ β„“'} {A : Type β„“} {P : β–‘ A β†’ Type β„“'}
  β†’ is-prop A
  β†’ (βˆ€ x β†’ P (inc x))
  β†’ βˆ€ x β†’ P x
β–‘-out-elim {P = P} A-prop go x =
  subst P prop! (go (β–‘-out A-prop x))

β–‘-rec-set
  : βˆ€ {β„“ β„“'} {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))
    a

β–‘-idempotent : βˆ€ {β„“} {A : Type β„“} β†’ is-prop A β†’ β–‘ A ≃ A
β–‘-idempotent aprop = prop-ext squash aprop (β–‘-out 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 = β–‘-map

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

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

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 = ░-rec (a-set _ _) id
is-set→locally-small a-set .to-path-over p = is-prop→pathp (λ _ → squash) _ _

to-is-true
  : βˆ€ {P Q : Ξ©} ⦃ _ : H-Level ∣ Q ∣ 0 ⦄
  β†’ ∣ P ∣
  β†’ P ≑ Q
to-is-true prf = Ξ©-ua (Ξ» _ β†’ hlevel!) Ξ» _ β†’ 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

ConnectivesπŸ”—

The universe of small propositions contains true, false, conjunctions, disjunctions, and (bi)implications.

infixr 10 _∧Ω_
infixr 9 _∨Ω_
infixr 8 _β†’Ξ©_
⊀Ω : Ω
∣ ⊀Ω ∣ = ⊀
⊀Ω .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
instance
  Extensional-Ξ£-β–‘
    : βˆ€ {β„“ β„“' β„“r} {A : Type β„“} {B : A β†’ Type β„“'}
    β†’ ⦃ ea : Extensional A β„“r ⦄ β†’ Extensional (Ξ£ A Ξ» x β†’ β–‘ (B x)) β„“r
  Extensional-Ξ£-β–‘ ⦃ ea ⦄ = Ξ£-prop-extensional (Ξ» x β†’ hlevel 1) ea

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.

module _ {β„“ β„“'} {A : Type β„“} {B : Type β„“'} (f : A β†’ B) where
  Ξ©-image : Type β„“'
  Ξ©-image = Ξ£[ b ∈ B ] β–‘ (fibre f b)

  Ξ©-corestriction : A β†’ Ξ©-image
  Ξ©-corestriction a = f a , inc (a , refl)

  opaque
    Ξ©-corestriction-is-surjective : is-surjective Ξ©-corestriction
    Ξ©-corestriction-is-surjective = elim! Ξ» y x fx=y β†’ pure (x , Ξ£-prop-path! fx=y)