Lemma correct_hom_on_id {A B : precategory} (F : catiso A B) : forall a, identity ((eqweqmap (catiso_to_precategory_ob_path F)) a) = (eqweqmap (correct_hom F a a)) (identity (F a)). Proof. intros a. apply pathsinv0. eapply pathscomp0. apply eqweq_correct_hom_is_comp. induction (eqweq_ob_path_is_functor_app F a). simpl. rewrite 2 id_right. reflexivity. Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.Foundations.UnivalenceAxiom. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Setcategories. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Equivalences.Core. Require Import UniMath.CategoryTheory.Equivalences.FullyFaithful.