Propositional resizing

Content created by Fredrik Bakke, Jonathan Prieto-Cubides and Egbert Rijke.

Created on 2022-05-27.
Last modified on 2023-06-08.

module foundation.propositional-resizing where
Imports 
open import foundation.dependent-pair-types
open import foundation.universe-levels

open import foundation-core.propositions
open import foundation-core.subtypes

Idea

We say that there is propositional resizing for propositions of universe levels l1 and l2 if there is a type Ω : UU l1 equipped with a subtype Q such that for each proposition P of universe level l2 there is an element u : Ω such that Q u ≃ P.

Definition

propositional-resizing : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2)
propositional-resizing l1 l2 =
  Σ ( Σ (UU l1) (subtype l1))
    ( λ Ω → (P : Prop l2) → Σ (pr1 Ω) (λ u → type-equiv-Prop (pr2 Ω u) P))

Recent changes