# Acyclic types

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

Created on 2023-04-26.

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


ConceptFile
Acyclic mapssynthetic-homotopy-theory.acyclic-maps
Acyclic typessynthetic-homotopy-theory.acyclic-types
Acyclic undirected graphsgraph-theory.acyclic-undirected-graphs
Braceletsunivalent-combinatorics.bracelets
The category of cyclic ringsring-theory.category-of-cyclic-rings
The circlesynthetic-homotopy-theory.circle
Connected set bundles over the circlesynthetic-homotopy-theory.connected-set-bundles-circle
Cyclic finite typesunivalent-combinatorics.cyclic-finite-types
Cyclic groupsgroup-theory.cyclic-groups
Cyclic higher groupshigher-group-theory.cyclic-higher-groups
Cyclic ringsring-theory.cyclic-rings
Cyclic typesstructured-types.cyclic-types
Euler's totient functionelementary-number-theory.eulers-totient-function
Finitely cyclic mapselementary-number-theory.finitely-cyclic-maps
Generating elements of groupsgroup-theory.generating-elements-groups
Hatcher's acyclic typesynthetic-homotopy-theory.hatchers-acyclic-type
Homomorphisms of cyclic ringsring-theory.homomorphisms-cyclic-rings
Infinite cyclic typessynthetic-homotopy-theory.infinite-cyclic-types
Multiplicative units in the standard cyclic ringselementary-number-theory.multiplicative-units-standard-cyclic-rings
Necklacesunivalent-combinatorics.necklaces
Polygonsgraph-theory.polygons
The poset of cyclic ringsring-theory.poset-of-cyclic-rings
Standard cyclic groups (ℤ/k)elementary-number-theory.standard-cyclic-groups
Standard cyclic rings (ℤ/k)elementary-number-theory.standard-cyclic-rings