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. idtoiso_t. Qed.
Require Import Category.Core Functor.Core. Require Import HoTT.Tactics Basics.Trunc Basics.Tactics Types.Sigma Equivalences.