Transport

module foundations.transport where

open import foundations.universe
open import foundations.identity-type
open import foundations.functions-are-functors
open import foundations.groupoid-laws
open import foundations.function

private variable
  ℓ : Level
  A B C : Type ℓ
  x y : A

transport : A ＝ B → A → B
transport refl x = x

subst : ∀ (P : A → Type ℓ) → x ＝ y → P x → P y
subst P p = transport (ap P p)

transport∙ : ∀ (p : A ＝ B) (q : B ＝ C)
  → transport (p ∙ q) x ＝ transport q (transport p x)
transport∙ {x = x} p refl =
  ap (λ w → transport w x) (runitId p)

substConst : ∀ (p : x ＝ y) (b : B)
  → subst (λ _ → B) p b ＝ b
substConst refl b = refl

private variable
  P Q : B → Type ℓ

subst∘ : ∀ (f : A → B) (p : x ＝ y) (v : P (f x))
  → subst (P ∘ f) p v ＝ subst P (ap f p) v
subst∘ f refl v = refl

substFiberwise : ∀ (f : (a : A) → P a → Q a) (p : x ＝ y) (v : P x)
  → subst Q p (f x v) ＝ f y (subst P p v)
substFiberwise f refl v = refl