(C : PreCategory) (s d d' : C) (m1 : d = d') (m2 : s = d) : idtoiso _ m1 o idtoiso _ m2 = idtoiso _ (m2 @ m1)%path. Proof. idtoiso_t. Qed.
Require Import Category.Core Functor.Core. Require Import HoTT.Tactics Basics.Trunc Basics.Tactics Types.Sigma Equivalences.