Lemma catiso_to_precategory_mor_path_funext {A B : precategory_data} (F : catiso A B) : (precategory_morphisms (C:=A)) = transportb (λ T, T -> T -> UU) (catiso_to_precategory_ob_path F) (precategory_morphisms (C:=B)). Proof. apply (pr1 (weqfunextsec _ _ _)). intros a. apply (pr1 (weqfunextsec _ _ _)). intros a'. apply (catiso_to_precategory_mor_path F). 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.