# Propositional resizing

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

Created on 2022-05-27.

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 a universe 𝒱 satisfies 𝒰-small propositional resizing if there is a type Ω in 𝒰 equipped with a subtype Q such that for each proposition P in 𝒱 there is an element u : Ω such that Q u ≃ P. Such a type Ω is called an 𝒰-small classifier of 𝒱-small subobjects.

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


## Table of files about propositional logic

The following table gives an overview of basic constructions in propositional logic and related considerations.

ConceptFile
Propositions (foundation-core)foundation-core.propositions
Propositions (foundation)foundation.propositions
Subterminal typesfoundation.subterminal-types
Subsingleton inductionfoundation.subsingleton-induction
Empty types (foundation-core)foundation-core.empty-types
Empty types (foundation)foundation.empty-types
Unit typefoundation.unit-type
Logical equivalencesfoundation.logical-equivalences
Propositional extensionalityfoundation.propositional-extensionality
Mere logical equivalencesfoundation.mere-logical-equivalences
Conjunctionfoundation.conjunction
Disjunctionfoundation.disjunction
Exclusive disjunctionfoundation.exclusive-disjunction
Existential quantificationfoundation.existential-quantification
Uniqueness quantificationfoundation.uniqueness-quantification
Universal quantificationfoundation.universal-quantification
Negationfoundation.negation
Double negationfoundation.double-negation
Propositional truncationsfoundation.propositional-truncations
Universal property of propositional truncationsfoundation.universal-property-propositional-truncation
The induction principle of propositional truncationsfoundation.induction-principle-propositional-truncation
Functoriality of propositional truncationsfoundation.functoriality-propositional-truncations
Propositional resizingfoundation.propositional-resizing
Impredicative encodings of the logical operationsfoundation.impredicative-encodings