# Transport along identifications

Content created by Fredrik Bakke and Egbert Rijke.

Created on 2023-09-11.

module foundation-core.transport-along-identifications where

Imports
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