This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.

The action on homotopies of functions

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

Idea

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.

Definition

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

  abstract
    unique-action-htpy-function :
      (f : (x : A) → B x) →
      is-contr
        ( Σ ( (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)

Properties

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}
  where

  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}
  where

  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)