Acyclic types

Content created by Egbert Rijke, Tom de Jong and Fredrik Bakke.

Created on 2023-04-26.
Last modified on 2023-12-01.

module synthetic-homotopy-theory.acyclic-types where
open import foundation.contractible-types
open import foundation.equivalences
open import foundation.propositions
open import foundation.retracts-of-types
open import foundation.unit-type
open import foundation.universe-levels

open import synthetic-homotopy-theory.functoriality-suspensions
open import synthetic-homotopy-theory.suspensions-of-types


A type A is said to be acyclic if its suspension is contractible.


is-acyclic-Prop : {l : Level}  UU l  Prop l
is-acyclic-Prop A = is-contr-Prop (suspension A)

is-acyclic : {l : Level}  UU l  UU l
is-acyclic A = type-Prop (is-acyclic-Prop A)

is-prop-is-acyclic : {l : Level} (A : UU l)  is-prop (is-acyclic A)
is-prop-is-acyclic A = is-prop-type-Prop (is-acyclic-Prop A)


Being acyclic is invariant under equivalence

is-acyclic-equiv :
  {l1 l2 : Level} {A : UU l1} {B : UU l2} 
  A  B  is-acyclic B  is-acyclic A
is-acyclic-equiv {B = B} e ac =
  is-contr-equiv (suspension B) (equiv-suspension e) ac

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

Acyclic types are closed under retracts

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

  is-acyclic-retract-of : A retract-of B  is-acyclic B  is-acyclic A
  is-acyclic-retract-of R ac =
    is-contr-retract-of (suspension B) (retract-of-suspension-retract-of R) ac

Contractible types are acyclic

is-acyclic-is-contr : {l : Level} (A : UU l)  is-contr A  is-acyclic A
is-acyclic-is-contr A = is-contr-suspension-is-contr

is-acyclic-unit : is-acyclic unit
is-acyclic-unit = is-acyclic-is-contr unit is-contr-unit

See also

Recent changes