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 α)

commutes.

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

commutes.

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) α)

See also

Recent changes