Propositions
Content created by Fredrik Bakke, Egbert Rijke and Jonathan Prieto-Cubides.
Created on 2022-01-26.
Last modified on 2023-09-28.
module foundation.propositions where open import foundation-core.propositions public
Imports
open import foundation.contractible-types open import foundation.dependent-pair-types open import foundation.universe-levels open import foundation-core.retractions open import foundation-core.truncated-types open import foundation-core.truncation-levels
Properties
Propositions are k+1
-truncated for any k
abstract 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) where is-prop-retract-of : A retract-of B → is-prop B → is-prop A is-prop-retract-of = is-trunc-retract-of
Recent changes
- 2023-09-28. Egbert Rijke and Fredrik Bakke. The Regensburg extension of the fundamental theorem (#803).
- 2023-06-08. Fredrik Bakke. Remove empty
foundation
modules and replace them by their core counterparts (#644). - 2023-06-07. Fredrik Bakke. Move public imports before "Imports" block (#642).
- 2023-05-01. Fredrik Bakke. Refactor 2, the sequel to refactor (#581).
- 2023-03-14. Fredrik Bakke. Remove all unused imports (#502).