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. 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.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Univalence. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.TransportMorphisms. Require Import UniMath.CategoryTheory.Core.Univalence.