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