Lemma functor_eq (C C' : precategory_data) (hs: has_homsets C') (F F': functor C C'): pr1 F = pr1 F' -> F = F'. Proof. intro H. apply (total2_paths_f H). apply proofirrelevance. apply isaprop_is_functor. apply 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.