Transport along homotopies

Content created by Fredrik Bakke and Egbert Rijke.

Created on 2023-10-22.
Last modified on 2024-02-06.

module foundation.transport-along-homotopies where
open import foundation.action-on-identifications-functions
open import foundation.function-extensionality
open import foundation.homotopy-induction
open import foundation.transport-along-higher-identifications
open import foundation.universe-levels

open import foundation-core.homotopies
open import foundation-core.identity-types
open import foundation-core.transport-along-identifications


If C : (x : A) → B x → 𝒰 is a type family, and H : f ~ g is a homotopy between functions f g : (x : A) → B x, then there is a natural transport operation that transports an element z : C x (f x) along the homotopy H to an element of type C x (g x).


Transporting along homotopies

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

  tr-htpy :
    (f ~ g)  ((x : A)  C x (f x))  ((x : A)  C x (g x))
  tr-htpy H f' x = tr (C x) (H x) (f' x)

  tr-htpy² :
    {H K : f ~ g} (L : H ~ K) (f' : (x : A)  C x (f x)) 
    tr-htpy H f' ~ tr-htpy K f'
  tr-htpy² L f' x = tr² (C x) (L x) (f' x)


Transport along a homotopy H is homotopic to transport along the identification eq-htpy H

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

  statement-compute-tr-htpy :
    {f g : (x : A)  B x} (H : f ~ g)  UU (l1  l3)
  statement-compute-tr-htpy H =
    tr  u  (x : A)  C x (u x)) (eq-htpy H) ~ tr-htpy C H

  base-case-compute-tr-htpy :
    {f : (x : A)  B x}  statement-compute-tr-htpy (refl-htpy' f)
  base-case-compute-tr-htpy =
    htpy-eq (ap (tr  u  (x : A)  C x (u x))) (eq-htpy-refl-htpy _))

    compute-tr-htpy :
      {f g : (x : A)  B x} (H : f ~ g)  statement-compute-tr-htpy H
    compute-tr-htpy {f} {g} =
      ind-htpy f
        ( λ _  statement-compute-tr-htpy)
        ( base-case-compute-tr-htpy)

    compute-tr-htpy-refl-htpy :
      {f : (x : A)  B x} 
      compute-tr-htpy (refl-htpy' f)  base-case-compute-tr-htpy
    compute-tr-htpy-refl-htpy {f} =
      compute-ind-htpy f
        ( λ _  statement-compute-tr-htpy)
        ( base-case-compute-tr-htpy)

Recent changes