Acyclic types

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

Created on 2023-04-26.
Last modified on 2026-07-29.

module synthetic-homotopy-theory.acyclic-types where

open import foundation.action-on-identifications-functions
open import foundation.contractible-types
open import foundation.dependent-pair-types
open import foundation.dependent-products-contractible-types
open import foundation.dependent-products-propositions
open import foundation.equivalences
open import foundation.equivalences-contractible-types
open import foundation.evaluation-functions
open import foundation.propositions
open import foundation.retracts-of-types
open import foundation.subuniverse-of-contractible-types
open import foundation.unit-type
open import foundation.universe-levels

open import foundation-core.function-types
open import foundation-core.identity-types

open import structured-types.constant-pointed-maps
open import structured-types.pointed-maps
open import structured-types.pointed-types
open import structured-types.pointed-universal-property-contractible-types

open import synthetic-homotopy-theory.functoriality-suspensions
open import synthetic-homotopy-theory.loop-spaces
open import synthetic-homotopy-theory.suspensions-of-pointed-types
open import synthetic-homotopy-theory.suspensions-of-types
open import synthetic-homotopy-theory.universal-property-suspensions-of-pointed-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

Acyclic loop spaces are contractible

module _
  {l : Level} {A : Pointed-Type l}
  (ac : is-acyclic (type-Pointed-Type (Ω A)))
  where

  is-contr-pointed-endomaps-loop-space-is-acyclic-loop-space :
    is-contr (Ω A →∗ Ω A)
  is-contr-pointed-endomaps-loop-space-is-acyclic-loop-space =
    is-contr-equiv
      ( suspension-Pointed-Type (Ω A) →∗ A)
      ( inv-equiv (equiv-transpose-suspension-loop-adjunction (Ω A) A))
      ( universal-property-contr-is-contr-Pointed-Type'
        ( point-Pointed-Type (suspension-Pointed-Type (Ω A)))
        ( ac)
        ( A))

  is-null-homotopic-pointed-endomap-loop-space-is-acyclic-loop-space :
    (f : Ω A →∗ Ω A) → (p : type-Pointed-Type (Ω A)) →
    map-pointed-map f p ＝ refl
  is-null-homotopic-pointed-endomap-loop-space-is-acyclic-loop-space f p =
    ap
      ( ev p ∘ map-pointed-map)
      ( eq-is-contr
        ( is-contr-pointed-endomaps-loop-space-is-acyclic-loop-space)
        { f}
        { constant-pointed-map (Ω A) (Ω A)})

  is-contr-is-acyclic-loop-space : is-contr (type-Pointed-Type (Ω A))
  is-contr-is-acyclic-loop-space =
    point-Pointed-Type (Ω A) ,
    (λ p →
      inv
        ( is-null-homotopic-pointed-endomap-loop-space-is-acyclic-loop-space
            ( id-pointed-map)
            ( p)))

Acyclic types are inhabited

TODO

See also

• Acyclic maps
• k-acyclic types
• Dependent epimorphisms
• Epimorphisms
• Epimorphisms with respect to sets
• Epimorphisms with respect to truncated types

Table of files related to cyclic types, groups, and rings

Recent changes

• 2026-07-29. Tom de Jong. Acyclic loop spaces are contractible (#1998).
• 2026-05-02. Fredrik Bakke and Egbert Rijke. Remove dependency between BUILTIN and postulates (#1373).
• 2025-08-14. Fredrik Bakke. Dedekind finiteness of various notions of finite type (#1422).
• 2023-12-01. Tom de Jong. Closure properties of acyclic maps and types (#960).
• 2023-11-27. Tom de Jong. k-acyclic types (#948).