The action on homotopies of functions

Content created by Fredrik Bakke and Egbert Rijke.

Created on 2023-12-21.
Last modified on 2024-02-19.

module foundation.action-on-homotopies-functions where
open import foundation.action-on-higher-identifications-functions
open import foundation.action-on-identifications-functions
open import foundation.dependent-pair-types
open import foundation.function-extensionality
open import foundation.homotopy-induction
open import foundation.universe-levels

open import foundation-core.constant-maps
open import foundation-core.contractible-types
open import foundation-core.function-types
open import foundation-core.homotopies
open import foundation-core.identity-types


Applying the action on identifications to identifications arising from the function extensionality axiom gives us the action on homotopies. For arbitrary functions of type

  F : ((x : A) → B x) → C.

We thus get an action of type

  f ~ g → F f = F g.


The unique functorial action of functions on homotopies

There is a unique action of functions on homotopies. Namely, by homotopy induction, function homotopies satisfy the dependent universal property of being an identity system on (dependent) function types. This means that for every type family

  C : (g : (x : A) → B x) → f ~ g → 𝒰

the map ev-refl-htpy C is an equivalence equivalence

  ev-refl-htpy C : ((g : (x : A) → B x) (H : f ~ g) → C g H) ≃ (C f refl-htpy).

In particular, applying this to type families of the form

  g H ↦ F f = F g

with the mapping

  f refl-htpy ↦ refl

shows that our action on homotopies is unique.

module _
  {l1 l2 l3 : Level}
  {A : UU l1} {B : A  UU l2} {C : UU l3}
  (F : ((x : A)  B x)  C)

    unique-action-htpy-function :
      (f : (x : A)  B x) 
        ( Σ ( (g : (x : A)  B x)  f ~ g  F f  F g)
            ( λ α  α f refl-htpy  refl))
    unique-action-htpy-function f =
      is-contr-map-ev-refl-htpy  g _  F f  F g) refl

  action-htpy-function :
    {f g : (x : A)  B x}  f ~ g  F f  F g
  action-htpy-function H = ap F (eq-htpy H)

  compute-action-htpy-function-refl-htpy :
    (f : (x : A)  B x)  action-htpy-function refl-htpy  refl
  compute-action-htpy-function-refl-htpy f =
    ap² F (eq-htpy-refl-htpy f)


The action on homotopies preserves concatenation

module _
  {l1 l2 l3 : Level}
  {A : UU l1} {B : A  UU l2} {C : UU l3}
  (F : ((x : A)  B x)  C)
  {f g h : (x : A)  B x}

  distributive-action-htpy-function-concat-htpy :
    (H : f ~ g) (H' : g ~ h) 
    action-htpy-function F (H ∙h H') 
    action-htpy-function F H  action-htpy-function F H'
  distributive-action-htpy-function-concat-htpy H H' =
    ap² F (eq-htpy-concat-htpy H H')  ap-concat F (eq-htpy H) (eq-htpy H')

The action on homotopies preserves inverses

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

  compute-action-htpy-function-inv-htpy :
    (H : f ~ g) 
    action-htpy-function F (inv-htpy H)  inv (action-htpy-function F H)
  compute-action-htpy-function-inv-htpy H =
    ap² F (compute-inv-eq-htpy H)  ap-inv F (eq-htpy H)

Recent changes