Home

同一視のtransport

module foundations.transport-identity where
Imports 
open import foundations.universe
open import foundations.identity-type
open import foundations.transport
open import foundations.groupoid-laws
open import foundations.identity-type-reasoning

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

substDom : ∀ (p : x ＝ x′) (q : x ＝ y)
  → subst (_＝ y) p q ＝ sym p ∙ q
substDom refl q = sym (lelimId (sym refl) q symRefl)

substCod : ∀ (p : y ＝ y′) (q : x ＝ y)
  → subst (x ＝_) p q ＝ q ∙ p
substCod refl q = sym (runitId q)

substBoth : ∀ (p : x ＝ x′) (q : x ＝ x)
  → subst (λ w → w ＝ w) p q ＝ sym p ∙ (q ∙ p)
substBoth refl q = sym (lelimId _ _ symRefl ∙ runitId q)