Transport along identifications

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

Created on 2023-09-11.
Last modified on 2025-11-06.

module foundation.transport-along-identifications where

open import foundation-core.transport-along-identifications public
Imports 
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
open import foundation-core.retractions
open import foundation-core.sections

Idea

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 on this page.

Properties

Transport is an equivalence

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

  is-retraction-inv-tr : (p : x ＝ y) → is-retraction (tr B p) (inv-tr B p)
  is-retraction-inv-tr refl b = refl

  is-section-inv-tr : (p : x ＝ y) → is-section (tr B p) (inv-tr B p)
  is-section-inv-tr refl b = refl

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

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

  equiv-tr : x ＝ y → B x ≃ B y
  equiv-tr p = (tr B p , is-equiv-tr p)

  equiv-inv-tr : x ＝ y → B y ≃ B x
  equiv-inv-tr p = (inv-tr B p , is-equiv-inv-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) (q : a0 ＝ a0) →
  tr (λ y → y ＝ y) p q ＝ (inv p ∙ q) ∙ p
tr-loop refl q = inv right-unit

tr-loop-self :
  {l1 : Level} {A : UU l1} {a : A} (p : a ＝ a) →
  tr (λ y → y ＝ y) p p ＝ p
tr-loop-self p = tr-loop p p ∙ ap (_∙ p) (left-inv p)

Recent changes