# Homotopy algebra

Content created by Fredrik Bakke, Egbert Rijke and Raymond Baker.

Created on 2024-02-06.

module foundation.homotopy-algebra where

Imports
open import foundation.universe-levels
open import foundation.whiskering-homotopies-composition

open import foundation-core.function-types
open import foundation-core.homotopies
open import foundation-core.whiskering-homotopies-concatenation


## Idea

This file has been created to collect operations on and facts about higher homotopies. The scope of this file is analogous to the scope of the file path algebra, which is about higher identifications.

## Definitions

### Horizontal concatenation of homotopies

module _
{l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} {C : A → UU l3}
{f f' : (x : A) → B x} {g g' : {x : A} → B x → C x}
where

horizontal-concat-htpy : ({x : A} → g {x} ~ g' {x}) → f ~ f' → g ∘ f ~ g' ∘ f'
horizontal-concat-htpy G F = (g ·l F) ∙h (G ·r f')

horizontal-concat-htpy' :
({x : A} → g {x} ~ g' {x}) → f ~ f' → g ∘ f ~ g' ∘ f'
horizontal-concat-htpy' G F = (G ·r f) ∙h (g' ·l F)


## Properties

### The two definitions of horizontal concatenation of homotopies agree

module _
{l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} {C : A → UU l3}
where

coh-right-unit-horizontal-concat-htpy :
{f : (x : A) → B x} {g g' : {x : A} → B x → C x}
(G : {x : A} → g {x} ~ g' {x}) →
horizontal-concat-htpy G (refl-htpy' f) ~
horizontal-concat-htpy' G (refl-htpy' f)
coh-right-unit-horizontal-concat-htpy G = inv-htpy-right-unit-htpy

coh-left-unit-horizontal-concat-htpy :
{f f' : (x : A) → B x} {g : {x : A} → B x → C x}
(F : f ~ f') →
horizontal-concat-htpy (refl-htpy' g) F ~
horizontal-concat-htpy' (refl-htpy' g) F
coh-left-unit-horizontal-concat-htpy F = right-unit-htpy


For the general case, we must construct a coherence of the square

            g ·r F
gf -------> gf'
|          |
G ·r f |          | G ·r f'
∨          ∨
g'f ------> g'f'
g' ·r F


but this is an instance of naturality of G applied to F.

module _
{l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} {C : A → UU l3}
{f f' : (x : A) → B x} {g g' : {x : A} → B x → C x}
(G : {x : A} → g {x} ~ g' {x}) (F : f ~ f')
where

coh-horizontal-concat-htpy :
horizontal-concat-htpy' G F ~ horizontal-concat-htpy G F
coh-horizontal-concat-htpy = nat-htpy G ·r F


### Eckmann-Hilton for homotopies

module _
{l1 l2 l3 : Level} {X : UU l1} {Y : UU l2} {Z : UU l3}
{f g : X → Y} {f' g' : Y → Z}
where

commutative-right-whisker-left-whisker-htpy :
(H' : f' ~ g') (H : f ~ g) →
(H' ·r f) ∙h (g' ·l H) ~
(f' ·l H) ∙h (H' ·r g)
commutative-right-whisker-left-whisker-htpy H' H x =
coh-horizontal-concat-htpy H' H x

module _
{l : Level} {X : UU l}
where

eckmann-hilton-htpy :
(H K : id {A = X} ~ id) →
(H ∙h K) ~ (K ∙h H)
eckmann-hilton-htpy H K =
( inv-htpy
( left-whisker-concat-htpy H (left-unit-law-left-whisker-comp K))) ∙h
( commutative-right-whisker-left-whisker-htpy H K) ∙h
( right-whisker-concat-htpy (left-unit-law-left-whisker-comp K) H)