proposition: Lemma idtoiso_functor (C D : PreCategory) (s d : C) (m : s = d) (F : Functor C D) : F _1 (idtoiso _ m) = idtoiso _ (ap (object_of F) m).
proof: Proof. path_induction; simpl; apply identity_of. Defined.
imports: Category.Core Functor.Core HoTT.Tactics Basics.Trunc Basics.Tactics Types.Sigma Equivalences