# 0-acyclic types

Content created by Fredrik Bakke and Tom de Jong.

Created on 2023-12-01.

module synthetic-homotopy-theory.0-acyclic-types where

Imports
open import foundation.contractible-types
open import foundation.dependent-pair-types
open import foundation.functoriality-propositional-truncation
open import foundation.inhabited-types
open import foundation.propositional-truncations
open import foundation.propositions
open import foundation.truncation-levels
open import foundation.unit-type
open import foundation.universe-levels

open import synthetic-homotopy-theory.0-acyclic-maps
open import synthetic-homotopy-theory.truncated-acyclic-maps
open import synthetic-homotopy-theory.truncated-acyclic-types


## Idea

A type is 0-acyclic if its suspension is 0-connected.

We can characterize the 0-acyclic types as the inhabited types.

## Definition

### The predicate of being a 0-acyclic type

module _
{l : Level} (A : UU l)
where

is-0-acyclic-Prop : Prop l
is-0-acyclic-Prop = is-truncated-acyclic-Prop zero-𝕋 A

is-0-acyclic : UU l
is-0-acyclic = type-Prop is-0-acyclic-Prop

is-prop-is-0-acyclic : is-prop is-0-acyclic
is-prop-is-0-acyclic = is-prop-type-Prop is-0-acyclic-Prop


## Properties

### A type is 0-acyclic if and only if it is inhabited

module _
{l : Level} {A : UU l}
where

is-inhabited-is-0-acyclic : is-0-acyclic A → is-inhabited A
is-inhabited-is-0-acyclic ac =
map-trunc-Prop
( pr1)
( is-surjective-is-0-acyclic-map
( terminal-map A)
( is-truncated-acyclic-map-terminal-map-is-truncated-acyclic A ac)
( star))

is-0-acyclic-is-inhabited : is-inhabited A → is-0-acyclic A
is-0-acyclic-is-inhabited h =
is-truncated-acyclic-is-truncated-acyclic-map-terminal-map A
( is-0-acyclic-map-is-surjective
( terminal-map A)
( λ u →
map-trunc-Prop
(λ a → (a , (contraction is-contr-unit u)))
( h)))