This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.
Acyclic types
module synthetic-homotopy-theory.acyclic-types where
Imports
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
Idea
A type A is said to be acyclic if its
suspension is
contractible.
Definition
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)
Properties
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} where 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
- Acyclic maps
k-acyclic types- Dependent epimorphisms
- Epimorphisms
- Epimorphisms with respect to sets
- Epimorphisms with respect to truncated types