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