Transport along identifications

Content created by Fredrik Bakke

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

module foundation-core.transport-along-identifications where
Imports 
open import foundation.universe-levels

open import foundation-core.identity-types

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 in foundation.transport-along-identifications.

Definition

Transport

tr :
  {l1 l2 : Level} {A : UU l1} (B : A → UU l2) {x y : A} (p : x ＝ y) → B x → B y
tr B refl b = b

Properties

Transport preserves concatenation of identifications

module _
  {l1 l2 : Level} {A : UU l1} {B : A → UU l2}
  where

  tr-concat :
    {x y z : A} (p : x ＝ y) (q : y ＝ z) (b : B x) →
    tr B (p ∙ q) b ＝ tr B q (tr B p b)
  tr-concat refl q b = refl

Transposing transport along the inverse of an identification

module _
  {l1 l2 : Level} {A : UU l1} {B : A → UU l2}
  where

  eq-transpose-tr :
    {x y : A} (p : x ＝ y) {u : B x} {v : B y} →
    v ＝ tr B p u → tr B (inv p) v ＝ u
  eq-transpose-tr refl q = q

  eq-transpose-tr' :
    {x y : A} (p : x ＝ y) {u : B x} {v : B y} →
    tr B p u ＝ v → u ＝ tr B (inv p) v
  eq-transpose-tr' refl q = q

Every family of maps preserves transport

preserves-tr :
  {l1 l2 l3 : Level} {I : UU l1} {A : I → UU l2} {B : I → UU l3}
  (f : (i : I) → A i → B i)
  {i j : I} (p : i ＝ j) (x : A i) →
  f j (tr A p x) ＝ tr B p (f i x)
preserves-tr f refl x = refl

Recent changes