Definition functor_eq_eq_from_functor_ob_eq (C C' : precategory_data) (hs: has_homsets C') (F G : functor C C') (p q : F = G) (H : base_paths _ _ (base_paths _ _ p) = base_paths _ _ (base_paths _ _ q)) : p = q. Proof. apply (invmaponpathsweq (total2_paths_equiv _ _ _ )); simpl. assert (H' : base_paths _ _ p = base_paths _ _ q). { apply (invmaponpathsweq (total2_paths_equiv _ _ _ )); simpl. apply (two_arg_paths_f H), uip. apply impred_isaset; intro a; apply impred_isaset; intro b; apply impred_isaset; intro f. apply hs. } apply (two_arg_paths_f H'), uip, isasetaprop, isaprop_is_functor, hs. Defined.
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.