# 1-acyclic types

Content created by Tom de Jong and Fredrik Bakke.

Created on 2023-12-01.
Last modified on 2024-04-11.

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

Imports
open import foundation.0-connected-types
open import foundation.binary-transport
open import foundation.constant-maps
open import foundation.contractible-types
open import foundation.dependent-pair-types
open import foundation.diagonal-maps-of-types
open import foundation.equivalences
open import foundation.function-extensionality
open import foundation.identity-types
open import foundation.inhabited-types
open import foundation.injective-maps
open import foundation.propositions
open import foundation.set-truncations
open import foundation.sets
open import foundation.truncated-types
open import foundation.truncation-levels
open import foundation.universe-levels

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


## Idea

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

We can characterize the 1-acyclic types as the 0-connected types.

In one direction, our proof relies on the following group-theoretic fact: the map of generators from a set X to the free group on X is injective. This is proved constructively in [MRR88] by Mines, Richman and Ruitenburg, and carried out in HoTT/UF and formalized in Agda in [BCDE21] by Bezem, Coquand, Dybjer, and Escardó.

Translated to concrete groups this means that for every set X, we have a pointed 1-type pt : BG together with an injection gen : X → pt ＝ pt. (Actually, BG is 0-connected as well, but we don't use this in our proof below.)

A construction on the level of concrete groups can be found in the recent preprint by David Wärn [War23].

For the time being, we haven't formalized this group-theoretic fact; instead we label it as an explicit assumption of our proof.

## Definition

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

is-1-acyclic-Prop : Prop l
is-1-acyclic-Prop = is-truncated-acyclic-Prop (one-𝕋) A

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

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


## Properties

### Every 0-connected type is 1-acyclic

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

is-1-acyclic-is-0-connected : is-0-connected A → is-1-acyclic A
is-1-acyclic-is-0-connected = is-truncated-acyclic-succ-is-connected


### Every 1-acyclic type is 0-connected

As explained at the top "Idea" section, we turn the necessary group-theoretic fact into an explicit assumption of our proof.

private
record
concrete-group-assumption' {l : Level} (A : UU l) : UU (lsuc l)
where
field
BG : Truncated-Type l (one-𝕋)
pt : type-Truncated-Type BG
gen : A → type-Ω (pair (type-Truncated-Type BG) pt)
is-injective-gen : is-injective gen

concrete-group-assumption : UUω
concrete-group-assumption =
{l : Level} (A : UU l) → concrete-group-assumption' A

module _
(cga : concrete-group-assumption)
where

is-contr-is-1-acyclic-is-set :
{l : Level} (A : UU l) →
is-set A → is-1-acyclic A → is-contr A
is-contr-is-1-acyclic-is-set A s ac =
let open concrete-group-assumption' (cga A) in
is-contr-is-inhabited-is-prop
( is-prop-all-elements-equal
( λ x y →
is-injective-gen
( binary-tr
( Id)
( htpy-eq
( is-section-map-inv-equiv
( ( diagonal-exponential
( type-Ω (type-Truncated-Type BG , pt))
( A)) ,
( is-equiv-diagonal-exponential-Id-is-acyclic-Truncated-Type
( A)
( ac)
( BG)
( pt)
( pt)))
( gen))
( x))
( htpy-eq
( is-section-map-inv-equiv
( ( diagonal-exponential
( type-Ω (type-Truncated-Type BG , pt))
( A)) ,
( is-equiv-diagonal-exponential-Id-is-acyclic-Truncated-Type
( A)
( ac)
( BG)
( pt)
( pt)))
( gen))
( y))
( refl))))
( is-inhabited-is-0-acyclic
( is-truncated-acyclic-is-truncated-acyclic-succ ac))

is-0-connected-is-1-acyclic :
{l : Level} (A : UU l) →
is-1-acyclic A → is-0-connected A
is-0-connected-is-1-acyclic A ac =
is-contr-is-1-acyclic-is-set
( type-trunc-Set A)
( is-set-type-trunc-Set)
( is-truncated-acyclic-succ-type-trunc-is-truncated-acyclic-succ A ac)


## References

[BCDE21]
Marc Bezem, Thierry Coquand, Peter Dybjer, and Martín Escardó. Free groups in hott/uf in agda. 2021. URL: https://www.cs.bham.ac.uk/~mhe/TypeTopology/Groups.Free.html.
[MRR88]
Ray Mines, Fred Richman, and Wim Ruitenburg. A Course in Constructive Algebra. Universitext. Springer New York, 1988. ISBN 978-0-387-96640-3 978-1-4419-8640-5. URL: http://link.springer.com/10.1007/978-1-4419-8640-5, doi:10.1007/978-1-4419-8640-5.
[War23]
David Wärn. Path spaces of pushouts. E-mail, 04 2023. URL: https://dwarn.se/po-paths.pdf.