Propositional resizing

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

Created on 2022-05-27.
Last modified on 2024-04-11.

module foundation.propositional-resizing where

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

See also

• The large locale of propositions

Table of files about propositional logic

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

Recent changes

• 2024-04-11. Fredrik Bakke and Egbert Rijke. Propositional operations (#1008).
• 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).