Transport along identifications

Content created by Egbert Rijke, Fredrik Bakke and Raymond Baker.

Created on 2023-09-11.
Last modified on 2023-11-24.

module foundation.transport-along-identifications where

open import foundation-core.transport-along-identifications public
open import foundation.action-on-identifications-functions
open import foundation.dependent-pair-types
open import foundation.universe-levels

open import foundation-core.equivalences
open import foundation-core.function-types
open import foundation-core.homotopies
open import foundation-core.identity-types


Given a type family B over A, an identification p : x = y in A and an element b : B x, we can transport the element b along the identification p to obtain an element tr B p b : B y.

The fact that tr B p is an equivalence is recorded in this file.


Transport is an equivalence

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

  inv-tr : x  y  B y  B x
  inv-tr p = tr B (inv p)

  is-retraction-inv-tr : (p : x  y)  (inv-tr p  tr B p) ~ id
  is-retraction-inv-tr refl b = refl

  is-section-inv-tr : (p : x  y)  (tr B p  inv-tr p) ~ id
  is-section-inv-tr refl b = refl

  is-equiv-tr : (p : x  y)  is-equiv (tr B p)
  is-equiv-tr p =
      ( inv-tr p)
      ( is-section-inv-tr p)
      ( is-retraction-inv-tr p)

  equiv-tr : x  y  (B x)  (B y)
  pr1 (equiv-tr p) = tr B p
  pr2 (equiv-tr p) = is-equiv-tr p

Transporting along refl is the identity equivalence

equiv-tr-refl :
  {l1 l2 : Level} {A : UU l1} (B : A  UU l2) {x : A} 
  equiv-tr B refl  id-equiv {A = B x}
equiv-tr-refl B = refl

Computing transport of loops

tr-loop :
  {l1 : Level} {A : UU l1} {a0 a1 : A} (p : a0  a1) (l : a0  a0) 
  (tr  y  y  y) p l)  ((inv p  l)  p)
tr-loop refl l = inv right-unit

Recent changes