Central H-spaces

Content created by Fredrik Bakke, Jonathan Prieto-Cubides and Egbert Rijke.

Created on 2022-09-21.
Last modified on 2024-03-12.

module structured-types.central-h-spaces where
Imports 
open import foundation.equivalences
open import foundation.universe-levels

open import structured-types.pointed-types

Idea

In structured-types.h-spaces we saw that the type of H-space structures on a pointed type A is equivalently described as the type of pointed sections of the pointed evaluation map (A → A) →∗ A. If the type A is connected, then the section maps to the connected component of (A ≃ A) at the identity equivalence. An evaluative H-space is a pointed type such that the map ev_pt : (A ≃ A)_{(id)} → A is an equivalence.

Definition

is-central-h-space :
  {l : Level} (A : Pointed-Type l) → UU l
is-central-h-space A =
  is-equiv
    { A = type-Pointed-Type A → type-Pointed-Type A}
    ( ev-point-Pointed-Type A)

References

[BCFR23]
Ulrik Buchholtz, J. Daniel Christensen, Jarl G. Taxerås Flaten, and Egbert Rijke. Central H-spaces and banded types. 02 2023. arXiv:2301.02636.

Recent changes