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

Transport along identifications

module foundation-core.transport-along-identifications where

open import foundation.action-on-identifications-functions
open import foundation.universe-levels

open import foundation-core.function-types
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.

Definitions

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

Transporting along the action on identifications of a function

tr-ap :
  {l1 l2 l3 l4 : Level} {A : UU l1} {B : A → UU l2} {C : UU l3} {D : C → UU l4}
  (f : A → C) (g : (x : A) → B x → D (f x))
  {x y : A} (p : x ＝ y) (z : B x) →
  tr D (ap f p) (g x z) ＝ g y (tr B p z)
tr-ap f g refl z = refl

Computing maps out of identity types as transports

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

  compute-map-out-of-identity-type :
    (x : A) (p : a ＝ x) → f x p ＝ tr B p (f a refl)
  compute-map-out-of-identity-type x refl = refl

Computing transport in the type family of identifications with a fixed target

tr-Id-left :
  {l : Level} {A : UU l} {a b c : A} (q : b ＝ c) (p : b ＝ a) →
  tr (_＝ a) q p ＝ (inv q ∙ p)
tr-Id-left refl p = refl

Computing transport in the type family of identifications with a fixed source

tr-Id-right :
  {l : Level} {A : UU l} {a b c : A} (q : b ＝ c) (p : a ＝ b) →
  tr (a ＝_) q p ＝ (p ∙ q)
tr-Id-right refl p = inv right-unit

Substitution law for transport

substitution-law-tr :
  {l1 l2 l3 : Level} {X : UU l1} {A : UU l2} (B : A → UU l3) (f : X → A)
  {x y : X} (p : x ＝ y) {x' : B (f x)} →
  tr B (ap f p) x' ＝ tr (B ∘ f) p x'
substitution-law-tr B f refl = refl