proposition: Lemma idtoiso_of_transport (C D : PreCategory) s d (m1 m2 : morphism C s d) (p : m1 = m2) (s' d' : morphism C s d -> D) u : @transport _ (fun m => morphism D (s' m) (d' m)) _ _ p u = idtoiso _ (ap d' p) o u o (idtoiso _ (ap s' p))^-1.
proof: Proof. idtoiso_t. Qed.
imports: Category.Core Functor.Core HoTT.Tactics Basics.Trunc Basics.Tactics Types.Sigma Equivalences