Lemma isaprop_is_functor (C C' : precategory_data) (hs: has_homsets C') (F : functor_data C C') : isaprop (is_functor F). Proof. apply isofhleveldirprod. apply impred; intro. apply hs. do 5 (apply impred; intro). apply hs. 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.