Lemma correct_hom {A B : precategory_data} (F : catiso A B) : forall a a' : A, F a --> F a' = (eqweqmap (catiso_to_precategory_ob_path F) a) --> (eqweqmap (catiso_to_precategory_ob_path F) a'). Proof. intros a a'. assert (W := (!(homotweqinvweq (univalence _ _)) (catiso_ob_weq F))). exact (maponpaths (λ T, (pr1weq T) a --> (pr1weq T) a') W ). 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.