# Composition algebra

Content created by Fredrik Bakke and Egbert Rijke.

Created on 2024-01-14.

module foundation.composition-algebra where

Imports
open import foundation.action-on-identifications-functions
open import foundation.function-extensionality
open import foundation.homotopy-induction
open import foundation.postcomposition-functions
open import foundation.precomposition-functions
open import foundation.universe-levels
open import foundation.whiskering-higher-homotopies-composition
open import foundation.whiskering-homotopies-composition

open import foundation-core.function-types
open import foundation-core.homotopies
open import foundation-core.identity-types


## Idea

Given a homotopy of maps H : f ~ g, there are standard witnesses

  htpy-precomp H S : precomp f S ~ precomp g S


and

  htpy-postcomp S H : postcomp S f ~ postcomp S g.


This file records their interactions with eachother and different operations on homotopies.

## Properties

### Precomposition distributes over whiskerings of homotopies

The operation htpy-precomp distributes over whiskerings of homotopies contravariantly. Given a homotopy H : f ~ g and a suitable map h the homotopy constructed as the whiskering

               - ∘ f
----------------->         - ∘ h
(B → S)  htpy-precomp H S  (A → S) -----> (C → S)
----------------->
- ∘ g


is homotopic to the homotopy

                    - ∘ (f ∘ h)
-------------------------->
(B → S)   htpy-precomp (H ·r h) S   (C → S).
-------------------------->
- ∘ (g ∘ h)

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

inv-distributive-htpy-precomp-right-whisker :
(h : C → A) (H : f ~ g) (S : UU l4) →
precomp h S ·l htpy-precomp H S ~ htpy-precomp (H ·r h) S
inv-distributive-htpy-precomp-right-whisker h H S i =
compute-eq-htpy-ap-precomp h (i ·l H)

distributive-htpy-precomp-right-whisker :
(h : C → A) (H : f ~ g) (S : UU l4) →
htpy-precomp (H ·r h) S ~ precomp h S ·l htpy-precomp H S
distributive-htpy-precomp-right-whisker h H S =
inv-htpy (inv-distributive-htpy-precomp-right-whisker h H S)


Similarly, the homotopy given by the whiskering

                               - ∘ f
- ∘ h          ----------------->
(C → S) -----> (B → S)  htpy-precomp H S  (A → S)
----------------->
- ∘ g


is homotopic to the homotopy

                    - ∘ (h ∘ f)
-------------------------->
(C → S)   htpy-precomp (h · l H) S   (A → S).
-------------------------->
- ∘ (h ∘ g)

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

inv-distributive-htpy-precomp-left-whisker :
(h : B → C) (H : f ~ g) (S : UU l4) →
htpy-precomp H S ·r precomp h S ~ htpy-precomp (h ·l H) S
inv-distributive-htpy-precomp-left-whisker h H S i =
ap eq-htpy (eq-htpy (ap-comp i h ∘ H))

distributive-htpy-precomp-left-whisker :
(h : B → C) (H : f ~ g) (S : UU l4) →
htpy-precomp (h ·l H) S ~ htpy-precomp H S ·r precomp h S
distributive-htpy-precomp-left-whisker h H S =
inv-htpy (inv-distributive-htpy-precomp-left-whisker h H S)


### Precomposition distributes over concatenations of homotopies

module _
{l1 l2 l3 : Level} {A : UU l1} {B : UU l2}
{f g h : A → B}
where

distributive-htpy-precomp-concat-htpy :
(H : f ~ g) (K : g ~ h) (S : UU l3) →
htpy-precomp (H ∙h K) S ~ htpy-precomp H S ∙h htpy-precomp K S
distributive-htpy-precomp-concat-htpy H K S i =
( ap eq-htpy (eq-htpy (distributive-left-whisker-comp-concat i H K))) ∙
( eq-htpy-concat-htpy (i ·l H) (i ·l K))


### Postcomposition distributes over whiskerings of homotopies

Given a homotopy H : f ~ g and a suitable map h the homotopy given by the whiskering

                               f ∘ –
h ∘ -          ------------------>
(S → C) -----> (S → B)  htpy-postcomp S H  (S → A)
------------------>
g ∘ -


is homotopic to the homotopy

                    (f ∘ h) ∘ -
-------------------------->
(S → C)   htpy-postcomp S (H ·r h)   (S → A).
-------------------------->
(g ∘ h) ∘ -


In fact, they are syntactically equal.

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

inv-distributive-htpy-postcomp-right-whisker :
(h : C → A) (H : f ~ g) (S : UU l4) →
htpy-postcomp S (H ·r h) ~ htpy-postcomp S H ·r postcomp S h
inv-distributive-htpy-postcomp-right-whisker h H S = refl-htpy

distributive-htpy-postcomp-right-whisker :
(h : C → A) (H : f ~ g) (S : UU l4) →
htpy-postcomp S H ·r postcomp S h ~ htpy-postcomp S (H ·r h)
distributive-htpy-postcomp-right-whisker h H S = refl-htpy


Similarly, the homotopy given by the whiskering

                f ∘ -
----------------->          h ∘ -
(S → A)  htpy-postcomp S H  (S → B) -----> (S → C)
----------------->
g ∘ -


is homotopic to the homotopy

                    (h ∘ f) ∘ -
-------------------------->
(S → A)   htpy-postcomp S (h ·l H)   (S → C).
-------------------------->
(h ∘ g) ∘ -

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

inv-distributive-htpy-postcomp-left-whisker :
(h : B → C) (H : f ~ g) (S : UU l4) →
postcomp S h ·l htpy-postcomp S H ~ htpy-postcomp S (h ·l H)
inv-distributive-htpy-postcomp-left-whisker h H S i =
compute-eq-htpy-ap-postcomp h (H ·r i)

distributive-htpy-postcomp-left-whisker :
(h : B → C) (H : f ~ g) (S : UU l4) →
htpy-postcomp S (h ·l H) ~ postcomp S h ·l htpy-postcomp S H
distributive-htpy-postcomp-left-whisker h H S =
inv-htpy (inv-distributive-htpy-postcomp-left-whisker h H S)


### Postcomposition distributes over concatenations of homotopies

module _
{l1 l2 l3 : Level} {A : UU l1} {B : UU l2}
{f g h : A → B}
where

distributive-htpy-postcomp-concat-htpy :
(H : f ~ g) (K : g ~ h) (S : UU l3) →
htpy-postcomp S (H ∙h K) ~ htpy-postcomp S H ∙h htpy-postcomp S K
distributive-htpy-postcomp-concat-htpy H K S i =
( ap eq-htpy (eq-htpy (distributive-right-whisker-comp-concat i H K))) ∙
( eq-htpy-concat-htpy (H ·r i) (K ·r i))


### The actions of precomposition and postcomposition on homotopies commute

Given homotopies F : f ~ f' and G : g ~ g', we have a commuting square of homotopies

                        postcomp A g ·l htpy-precomp F X
(g ∘ - ∘ f) ---------------------------------> (g ∘ - ∘ f')
|                                              |
|                                              |
|                                              |
precomp f Y ·l htpy-postcomp B G            htpy-postcomp A G ·r precomp f' X
|                                              |
|                                              |
∨                                              ∨
(g' ∘ - ∘ f) --------------------------------> (g' ∘ - ∘ f').
htpy-precomp F Y ·r postcomp B g'

module _
{l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4}
where

commutative-postcomp-htpy-precomp :
{f f' : A → B} (g : X → Y) (F : f ~ f') →
htpy-precomp F Y ·r postcomp B g ~ postcomp A g ·l htpy-precomp F X
commutative-postcomp-htpy-precomp {f} g =
ind-htpy f
( λ f' F →
htpy-precomp F Y ·r postcomp B g ~ postcomp A g ·l htpy-precomp F X)
( ( right-whisker-comp²
( compute-htpy-precomp-refl-htpy f Y)
( postcomp B g)) ∙h
( inv-htpy
( left-whisker-comp²
( postcomp A g)
( compute-htpy-precomp-refl-htpy f X))))

commutative-precomp-htpy-postcomp :
(f : A → B) {g g' : X → Y} (G : g ~ g') →
htpy-postcomp A G ·r precomp f X ~ precomp f Y ·l htpy-postcomp B G
commutative-precomp-htpy-postcomp f {g} =
ind-htpy g
( λ g' G →
htpy-postcomp A G ·r precomp f X ~ precomp f Y ·l htpy-postcomp B G)
( ( right-whisker-comp²
( compute-htpy-postcomp-refl-htpy A g)
( precomp f X)) ∙h
( inv-htpy
( left-whisker-comp²
( precomp f Y)
( compute-htpy-postcomp-refl-htpy B g))))

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

commutative-htpy-postcomp-htpy-precomp :
(F : f ~ f') (G : g ~ g') →
( postcomp A g ·l htpy-precomp F X ∙h htpy-postcomp A G ·r precomp f' X) ~
( precomp f Y ·l htpy-postcomp B G ∙h htpy-precomp F Y ·r postcomp B g')
commutative-htpy-postcomp-htpy-precomp F =
ind-htpy g
( λ g' G →
( postcomp A g ·l htpy-precomp F X ∙h
htpy-postcomp A G ·r precomp f' X) ~
( precomp f Y ·l htpy-postcomp B G ∙h
htpy-precomp F Y ·r postcomp B g'))
( ( ap-concat-htpy
( postcomp A g ·l htpy-precomp F X)
( right-whisker-comp²
( compute-htpy-postcomp-refl-htpy A g)
( precomp f' X))) ∙h
( right-unit-htpy) ∙h
( inv-htpy (commutative-postcomp-htpy-precomp g F)) ∙h
( ap-concat-htpy'
( htpy-precomp F Y ·r postcomp B g)
( left-whisker-comp²
( precomp f Y)
( inv-htpy (compute-htpy-postcomp-refl-htpy B g)))))