Non-coherent H-spaces

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-09-13.
Last modified on 2024-02-06.

module structured-types.noncoherent-h-spaces where
open import foundation.dependent-pair-types
open import foundation.identity-types
open import foundation.unital-binary-operations
open import foundation.universe-levels

open import structured-types.pointed-types


A noncoherent H-space is a pointed type A equipped with a binary operation μ and homotopies (λ x → μ point x) ~ id and λ x → μ x point ~ id. If A is a connected H-space, then λ x → μ a x and λ x → μ x a are equivalences for each a : A.


Unital binary operations on pointed types

unit-laws-mul-Pointed-Type :
  {l : Level} (A : Pointed-Type l)
  (μ : (x y : type-Pointed-Type A)  type-Pointed-Type A)  UU l
unit-laws-mul-Pointed-Type A μ = unit-laws μ (point-Pointed-Type A)

unital-mul-Pointed-Type :
  {l : Level}  Pointed-Type l  UU l
unital-mul-Pointed-Type A =
  Σ ( type-Pointed-Type A  type-Pointed-Type A  type-Pointed-Type A)
    ( unit-laws-mul-Pointed-Type A)

Non-coherent Noncoherent-H-Spaces

noncoherent-h-space-structure :
  {l : Level} (A : Pointed-Type l)  UU l
noncoherent-h-space-structure A =
  Σ ( (x y : type-Pointed-Type A)  type-Pointed-Type A)
    ( λ μ  unit-laws μ (point-Pointed-Type A))

Noncoherent-H-Space : (l : Level)  UU (lsuc l)
Noncoherent-H-Space l = Σ (Pointed-Type l) (noncoherent-h-space-structure)

module _
  {l : Level} (A : Noncoherent-H-Space l)

  pointed-type-Noncoherent-H-Space : Pointed-Type l
  pointed-type-Noncoherent-H-Space = pr1 A

  type-Noncoherent-H-Space : UU l
  type-Noncoherent-H-Space = type-Pointed-Type pointed-type-Noncoherent-H-Space

  point-Noncoherent-H-Space : type-Noncoherent-H-Space
  point-Noncoherent-H-Space =
    point-Pointed-Type pointed-type-Noncoherent-H-Space

  mul-Noncoherent-H-Space :
  mul-Noncoherent-H-Space = pr1 (pr2 A)

  unit-laws-mul-Noncoherent-H-Space :
    unit-laws mul-Noncoherent-H-Space point-Noncoherent-H-Space
  unit-laws-mul-Noncoherent-H-Space = pr2 (pr2 A)

  left-unit-law-mul-Noncoherent-H-Space :
    (x : type-Noncoherent-H-Space) 
    mul-Noncoherent-H-Space point-Noncoherent-H-Space x  x
  left-unit-law-mul-Noncoherent-H-Space = pr1 unit-laws-mul-Noncoherent-H-Space

  right-unit-law-mul-Noncoherent-H-Space :
    (x : type-Noncoherent-H-Space) 
    mul-Noncoherent-H-Space x point-Noncoherent-H-Space  x
  right-unit-law-mul-Noncoherent-H-Space = pr2 unit-laws-mul-Noncoherent-H-Space

Recent changes