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.

See also

Recent changes