The involutive type of H-space structures on a pointed type

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

Created on 2023-02-09.
Last modified on 2024-04-11.

module structured-types.involutive-type-of-h-space-structures where

Imports
open import foundation.action-on-identifications-functions
open import foundation.binary-transport
open import foundation.constant-maps
open import foundation.contractible-types
open import foundation.dependent-pair-types
open import foundation.equality-dependent-function-types
open import foundation.equivalences
open import foundation.functoriality-dependent-pair-types
open import foundation.fundamental-theorem-of-identity-types
open import foundation.homotopies
open import foundation.homotopy-induction
open import foundation.identity-types
open import foundation.structure-identity-principle
open import foundation.symmetric-identity-types
open import foundation.torsorial-type-families
open import foundation.universe-levels

open import structured-types.constant-pointed-maps
open import structured-types.pointed-types

open import univalent-combinatorics.2-element-types


Idea

We construct the involutive type of H-space structures on a pointed type.

Definition

The involutive type of H-space structures on a pointed type

h-space-Involutive-Type :
{l1 : Level} (A : Pointed-Type l1) (X : 2-Element-Type lzero) → UU l1
h-space-Involutive-Type A X =
Σ ( (type-2-Element-Type X → type-Pointed-Type A) → type-Pointed-Type A)
( λ μ →
Σ ( ( f : type-2-Element-Type X → type-Pointed-Type A) →
( x : type-2-Element-Type X) →
( p : f x ＝ point-Pointed-Type A) →
μ f ＝ f (map-swap-2-Element-Type X x))
( λ ν →
symmetric-Id
( ( X) ,
( λ x →
ν ( map-constant-pointed-map (type-2-Element-Type X , x) A)
( x)
( refl)))))


Properties

Characterization of equality in the involutive type of H-space structures on a pointed type

module _
{l1 : Level} (A : Pointed-Type l1) (X : 2-Element-Type lzero)
where

htpy-h-space-Involutive-Type :
(μ μ' : h-space-Involutive-Type A X) → UU l1
htpy-h-space-Involutive-Type μ μ' =
Σ ( (f : type-2-Element-Type X → type-Pointed-Type A) → pr1 μ f ＝ pr1 μ' f)
( λ H →
Σ ( ( f : type-2-Element-Type X → type-Pointed-Type A) →
( x : type-2-Element-Type X) →
( p : f x ＝ point-Pointed-Type A) →
pr1 (pr2 μ) f x p ＝ (H f ∙ pr1 (pr2 μ') f x p))
( λ K →
Eq-symmetric-Id
( ( X) ,
( λ x →
( H ( map-constant-pointed-map
( type-2-Element-Type X , x)
( A))) ∙
( pr1
( pr2 μ')
( map-constant-pointed-map (type-2-Element-Type X , x) A)
( x)
( refl))))
( tr-symmetric-Id
( ( X) ,
( λ x →
pr1
( pr2 μ)
( map-constant-pointed-map (type-2-Element-Type X , x) A)
( x)
( refl)))
( ( X) ,
( λ x →
( H ( map-constant-pointed-map
( type-2-Element-Type X , x)
( A))) ∙
( pr1
( pr2 μ')
( map-constant-pointed-map (type-2-Element-Type X , x) A)
( x)
( refl))))
( id-equiv)
( λ x →
K ( map-constant-pointed-map (type-2-Element-Type X , x) A)
( x)
( refl))
( pr2 (pr2 μ)))
( map-equiv-symmetric-Id
( equiv-concat
( H ( const
( type-2-Element-Type X)
( point-Pointed-Type A)))
( point-Pointed-Type A))
( ( X) ,
( λ x →
pr1
( pr2 μ')
( map-constant-pointed-map (type-2-Element-Type X , x) A)
( x)
( refl)))
( pr2 (pr2 μ')))))

refl-htpy-h-space-Involutive-Type :
(μ : h-space-Involutive-Type A X) → htpy-h-space-Involutive-Type μ μ
pr1 (refl-htpy-h-space-Involutive-Type (μ , unit-laws-μ , coh-μ)) f = refl
pr1
( pr2 (refl-htpy-h-space-Involutive-Type (μ , unit-laws-μ , coh-μ))) f x p =
refl
pr1
( pr2 (pr2 (refl-htpy-h-space-Involutive-Type (μ , unit-laws-μ , coh-μ)))) =
refl
pr2
( pr2
( pr2 (refl-htpy-h-space-Involutive-Type (μ , unit-laws-μ , coh-μ)))) x =
( ( compute-pr2-tr-symmetric-Id
( ( X) ,
( λ x →
unit-laws-μ
( map-constant-pointed-map (type-2-Element-Type X , x) A)
( x)
( refl)))
( ( X) ,
( λ x →
unit-laws-μ
( map-constant-pointed-map (type-2-Element-Type X , x) A)
( x)
( refl)))
( id-equiv)
( λ y → refl)
( λ y → pr2 coh-μ y)
( x)) ∙
( right-unit)) ∙
( inv (ap-id (pr2 coh-μ x)))

is-torsorial-htpy-h-space-Involutive-Type :
( μ : h-space-Involutive-Type A X) →
is-torsorial (htpy-h-space-Involutive-Type μ)
is-torsorial-htpy-h-space-Involutive-Type (μ , ν , ρ) =
is-torsorial-Eq-structure
( is-torsorial-htpy μ)
( μ , refl-htpy)
( is-torsorial-Eq-structure
( is-torsorial-Eq-Π
( λ f → is-torsorial-Eq-Π (λ x → is-torsorial-htpy (ν f x))))
( ν , (λ f x p → refl))
( is-contr-equiv
( Σ ( symmetric-Id
( ( X) ,
( λ x →
ν ( map-constant-pointed-map (type-2-Element-Type X , x) A)
( x)
( refl))))
( Eq-symmetric-Id
( ( X) ,
( λ x →
ν ( map-constant-pointed-map (type-2-Element-Type X , x) A)
( x)
( refl)))
( ρ)))
( equiv-tot
( λ α →
equiv-binary-tr
( Eq-symmetric-Id
( ( X) ,
( λ x →
ν ( map-constant-pointed-map
( type-2-Element-Type X , x)
( A))
( x)
( refl))))
( refl-Eq-unordered-pair-tr-symmetric-Id
( ( X) ,
( λ x →
ν ( map-constant-pointed-map
( type-2-Element-Type X , x)
( A))
( x)
( refl)))
( ρ))
( id-equiv-symmetric-Id
( ( X) ,
( λ x →
ν ( map-constant-pointed-map
( type-2-Element-Type X , x)
( A))
( x)
( refl)))
( α))))
( is-torsorial-Eq-symmetric-Id
( ( X) ,
( λ x →
ν ( map-constant-pointed-map (type-2-Element-Type X , x) A)
( x)
( refl)))
( ρ))))

htpy-eq-h-space-Involutive-Type :
(μ μ' : h-space-Involutive-Type A X) →
(μ ＝ μ') → htpy-h-space-Involutive-Type μ μ'
htpy-eq-h-space-Involutive-Type μ .μ refl =
refl-htpy-h-space-Involutive-Type μ

is-equiv-htpy-eq-h-space-Involutive-Type :
(μ μ' : h-space-Involutive-Type A X) →
is-equiv (htpy-eq-h-space-Involutive-Type μ μ')
is-equiv-htpy-eq-h-space-Involutive-Type μ =
fundamental-theorem-id
( is-torsorial-htpy-h-space-Involutive-Type μ)
( htpy-eq-h-space-Involutive-Type μ)

extensionality-h-space-Involutive-Type :
(μ μ' : h-space-Involutive-Type A X) →
(μ ＝ μ') ≃ htpy-h-space-Involutive-Type μ μ'
pr1 (extensionality-h-space-Involutive-Type μ μ') =
htpy-eq-h-space-Involutive-Type μ μ'
pr2 (extensionality-h-space-Involutive-Type μ μ') =
is-equiv-htpy-eq-h-space-Involutive-Type μ μ'

eq-htpy-h-space-Involutive-Type :
(μ μ' : h-space-Involutive-Type A X) →
htpy-h-space-Involutive-Type μ μ' → μ ＝ μ'
eq-htpy-h-space-Involutive-Type μ μ' =
map-inv-equiv (extensionality-h-space-Involutive-Type μ μ')