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
- 2023-06-08. Fredrik Bakke. Remove empty
foundation
modules and replace them by their core counterparts (#644). - 2023-05-09. Fredrik Bakke and Egbert Rijke. Some half-finished additions to modalities (#606).
- 2023-03-14. Fredrik Bakke. Remove all unused imports (#502).
- 2023-03-13. Jonathan Prieto-Cubides. More maintenance (#506).
- 2023-03-07. Fredrik Bakke. Add blank lines between
<details>
tags and markdown syntax (#490).