Lemma catiso_to_precategory_mor_path {A B : precategory_data} (F : catiso A B) : forall a a', (precategory_morphisms (C:=A)) a a' = transportb (λ T, T -> T -> UU) (catiso_to_precategory_ob_path F) (precategory_morphisms (C:=B)) a a'. Proof. intros a. intros a'. eapply pathscomp0. apply (catiso_fully_faithful_path F). eapply pathscomp0. apply correct_hom. eapply pathscomp0. apply transport_mor. 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.