Content created by Fredrik Bakke, Egbert Rijke, Jonathan Prieto-Cubides, Daniel Gratzer and Elisabeth Stenholm.

Created on 2022-01-26.
Last modified on 2024-04-11.

module foundation.propositions where

open import foundation-core.propositions public
open import foundation.contractible-types
open import foundation.dependent-pair-types
open import foundation.logical-equivalences
open import foundation.retracts-of-types
open import foundation.universe-levels

open import foundation-core.embeddings
open import foundation-core.equivalences
open import foundation-core.truncated-types
open import foundation-core.truncation-levels


Propositions are k+1-truncated for any k

  is-trunc-is-prop :
    {l : Level} (k : 𝕋) {A : UU l}  is-prop A  is-trunc (succ-𝕋 k) A
  is-trunc-is-prop k is-prop-A x y = is-trunc-is-contr k (is-prop-A x y)

truncated-type-Prop : {l : Level} (k : 𝕋)  Prop l  Truncated-Type l (succ-𝕋 k)
pr1 (truncated-type-Prop k P) = type-Prop P
pr2 (truncated-type-Prop k P) = is-trunc-is-prop k (is-prop-type-Prop P)

Propositions are closed under retracts

module _
  {l1 l2 : Level} {A : UU l1} (B : UU l2)

  is-prop-retract-of : A retract-of B  is-prop B  is-prop A
  is-prop-retract-of = is-trunc-retract-of

If a type embeds into a proposition, then it is a proposition

  is-prop-is-emb :
    {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A  B) 
    is-emb f  is-prop B  is-prop A
  is-prop-is-emb = is-trunc-is-emb neg-two-𝕋

  is-prop-emb :
    {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A  B)  is-prop B  is-prop A
  is-prop-emb = is-trunc-emb neg-two-𝕋

Two equivalent types are equivalently propositions

equiv-is-prop-equiv : {l1 l2 : Level} {A : UU l1} {B : UU l2} 
  A  B  is-prop A  is-prop B
equiv-is-prop-equiv {A = A} {B = B} e =
    ( is-prop-is-prop A)
    ( is-prop-is-prop B)
    ( is-prop-equiv' e)
    ( is-prop-equiv e)

See also

Operations on propositions

There is a wide range of operations on propositions due to the rich structure of intuitionistic logic. Below we give a structured overview of a notable selection of such operations and their notation in the library.

The list is split into two sections, the first consists of operations that generalize to arbitrary types and even sufficiently nice subuniverses, such as -types.

NameOperator on typesOperator on propositions/subtypes
Dependent sumΣΣ-Prop
Dependent productΠΠ-Prop
Logical equivalence
Exclusive sumexclusive-sumexclusive-sum-Prop

Note that for many operations in the second section, there is an equivalent operation on propositions in the first.

NameOperator on typesOperator on propositions/subtypes
Initial objectemptyempty-Prop
Terminal objectunitunit-Prop
Existential quantificationexists-structure
Unique existential quantificationuniquely-exists-structure∃!
Universal quantification∀' (equivalent to Π-Prop)
Conjunction (equivalent to product-Prop)
Disjunctiondisjunction-type (equivalent to join-Prop)
Exclusive disjunctionxor-type (equivalent to exclusive-sum-Prop)
Double negation¬¬¬¬'

We can also organize these operations by indexed and binary variants, giving us the following table:

Constructive existence+Σ
Unique existence∃!

Table of files about propositional logic

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

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
Exclusive disjunctionfoundation.exclusive-disjunction
Existential quantificationfoundation.existential-quantification
Uniqueness quantificationfoundation.uniqueness-quantification
Universal quantificationfoundation.universal-quantification
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

Recent changes