proposition: Proposition functor_data_eq_alt {C C' : category} {F F' : functor_data C C'} (p : F ~ F') (q : ∏ (x y : C) (f : x --> y), #F f · idtoiso (p y) = idtoiso (p x) · #F' f) : F = F'.
proof: Proof. use functor_data_eq. - exact p. - intros x y f. specialize (q x y f). unfold double_transport. rewrite <- idtoiso_postcompose. rewrite <- idtoiso_precompose. rewrite !assoc'. etrans. { apply maponpaths. exact q. } rewrite !assoc. etrans. { apply maponpaths_2. refine (!_). apply pr1_idtoiso_concat. } rewrite pathsinv0l. cbn. apply id_left. Qed.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Univalence UniMath.MoreFoundations.Tactics UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.TransportMorphisms UniMath.CategoryTheory.Core.Univalence