# The action of functions on higher identifications

Content created by Fredrik Bakke and Egbert Rijke.

Created on 2024-02-06.
Last modified on 2024-04-11.

module foundation.action-on-higher-identifications-functions where

Imports
open import foundation.action-on-identifications-functions
open import foundation.path-algebra
open import foundation.universe-levels

open import foundation-core.commuting-squares-of-identifications
open import foundation-core.constant-maps
open import foundation-core.function-types
open import foundation-core.homotopies
open import foundation-core.identity-types


## Idea

Any map f : A → B has an action on higher identifications, which is a map

  ap² f : (p ＝ q) → (ap f p ＝ ap f q)


Here p q : x ＝ y are identifications in the type A. The action of f on higher identifications is defined by

  ap² f := ap (ap f).


## Definitions

### The action of functions on higher identifications

module _
{l1 l2 : Level} {A : UU l1} {B : UU l2} {x y : A}
{p q : x ＝ y} (f : A → B) (α : p ＝ q)
where

ap² : ap f p ＝ ap f q
ap² = ap (ap f) α


## Properties

### The inverse law of the action of functions on higher identifications

Consider an identification α : p ＝ q between two identifications p q : x ＝ y in a type A, and consider a map f : A → B. Then the square of identifications

                      ap² f (horizontal-inv-Id² α)
ap f (inv p) ------------------------------> ap f (inv q)
|                                            |
ap-inv f p |                                            | ap-inv f q
∨                                            ∨
inv (ap f p) ------------------------------> inv (ap f q)
horizontal-inv-Id² (ap² f α)

module _
{l1 l2 : Level} {A : UU l1} {B : UU l2} {x y : A}
{p q : x ＝ y} (f : A → B) (α : p ＝ q)
where

compute-inv-ap² :
coherence-square-identifications
( ap² f (horizontal-inv-Id² α))
( ap-inv f p)
( ap-inv f q)
( horizontal-inv-Id² (ap² f α))
compute-inv-ap² =
( ( inv (horizontal-concat-Id² refl (ap-comp inv (ap f) α))) ∙
( nat-htpy (ap-inv f) α)) ∙
( horizontal-concat-Id² (ap-comp (ap f) inv α) refl)


### The action of the identity function on higher identifications is trivial

Consider an identification α : p ＝ q between two identifications p q : x ＝ y in a type A. Then the square of identifications

                ap² id α
ap id p ----------> ap id q
|                    |
ap-id p |                    | ap-id q
∨                    ∨
p -----------------> q
α


commutes.

module _
{l1 l2 : Level} {A : UU l1} {B : UU l2} {x y : A}
{p q : x ＝ y} (α : p ＝ q)
where

compute-id-ap² :
coherence-square-identifications (ap² id α) (ap-id p) (ap-id q) α
compute-id-ap² =
horizontal-concat-Id² refl (inv (ap-id α)) ∙ nat-htpy ap-id α


### The action of a composite function on higher identifications

Consider an identification α : p ＝ q between two identifications p q : x ＝ y in a type A and consider two functions f : A → B and g : B → C. Then the square of identifications

                         ap² (g ∘ f) α
ap (g ∘ f) p -----------------> ap (g ∘ f) q
|                               |
ap-comp g f p |                               | ap-comp g f q
∨                               ∨
ap g (ap f p) ----------------> ap g (ap f q)
ap² g (ap² f α)


commutes.

module _
{l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : UU l3}
{x y : A} {p q : x ＝ y} (g : B → C) (f : A → B) (α : p ＝ q)
where

compute-comp-ap² :
coherence-square-identifications
( ap² (g ∘ f) α)
( ap-comp g f p)
( ap-comp g f q)
( (ap² g ∘ ap² f) α)
compute-comp-ap² =
(horizontal-concat-Id² refl (inv (ap-comp (ap g) (ap f) α)) ∙
(nat-htpy (ap-comp g f) α))


### The action of a constant function on higher identifications is constant

Consider an identification α : p ＝ q between two identifications p q : x ＝ y in a type A and consider an element b : B. Then the triangle of identifications

                 ap² (const b) α
ap (const b) p ---------------> ap (const b) q
\              /
ap-const b p \          / ap-const b q
∨      ∨
refl

module _
{l1 l2 : Level} {A : UU l1} {B : UU l2} {x y : A}
{p q : x ＝ y} (α : p ＝ q)
where

compute-const-ap² :
(b : B) →
coherence-square-identifications
( ap² (const A b) α)
( ap-const b p)
( ap-const b q)
( refl)
compute-const-ap² b =
( inv (horizontal-concat-Id² refl (ap-const refl α))) ∙
( nat-htpy (ap-const b) α)