{A : Type} {P Q : A -> Type} {a a' : A} (p : a = a') (z : P a + Q a) : transport (fun a => P a + Q a) p z = match z with | inl z' => inl (p # z') | inr z' => inr (p # z') end := match p with idpath => match z with inl _ => 1 | inr _ => 1 end end.
Require Import HoTT.Basics. Require Import Types.Empty Types.Unit Types.Prod Types.Sigma. Require Import Types.Bool.