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