proposition: Lemma idtoiso_comp4 (C : PreCategory) (s d d' d'' d''' : C) (m0 : d'' = d''') (m1 : d' = d'') (m2 : d = d') (m3 : s = d) : idtoiso _ m0 o (idtoiso _ m1 o (idtoiso _ m2 o idtoiso _ m3)) = idtoiso _ (((m3 @ m2) @ m1) @ m0)%path.
proof: Proof. idtoiso_t. Qed.
imports: Category.Core Functor.Core HoTT.Tactics Basics.Trunc Basics.Tactics Types.Sigma Equivalences