Contractible pointed types

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

Created on 2022-05-16.
Last modified on 2023-03-10.

module structured-types.contractible-pointed-types where
Imports 
open import foundation.contractible-types
open import foundation.propositions
open import foundation.universe-levels

open import structured-types.pointed-types

Definition

is-contr-pointed-type-Prop : {l : Level} → Pointed-Type l → Prop l
is-contr-pointed-type-Prop A = is-contr-Prop (type-Pointed-Type A)

is-contr-Pointed-Type : {l : Level} → Pointed-Type l → UU l
is-contr-Pointed-Type A = type-Prop (is-contr-pointed-type-Prop A)

is-prop-is-contr-Pointed-Type :
  {l : Level} (A : Pointed-Type l) → is-prop (is-contr-Pointed-Type A)
is-prop-is-contr-Pointed-Type A =
  is-prop-type-Prop (is-contr-pointed-type-Prop A)

Recent changes