Lemma catiso_to_precategory_id_path {A B : precategory} (F : catiso A B) : forall a : A, (transportb (X := total2 (λ T, T -> T -> UU)) (λ T, forall a, (pr2 T) a a) (total2_paths2_b (catiso_to_precategory_ob_path F) (catiso_to_precategory_mor_path_funext F)) identity) a = identity a. Proof. intros a. eapply pathscomp0. apply transport_id. unfold catiso_to_precategory_mor_path_funext. unfold catiso_to_precategory_mor_path. unfold weqfunextsec. simpl (pr1 _). rewrite !(homotweqinvweq (weqtoforallpaths _ _ _)). rewrite pathscomp_inv. rewrite pathscomp_inv. rewrite path_assoc. rewrite path_assoc. rewrite pathscomp0rid. rewrite pathsinv0r. simpl. apply pathsweq1'. rewrite <- pathscomp_inv. rewrite eqweqmap_pathsinv0. rewrite invinv. rewrite <- eqweqmap_pathscomp0. rewrite (eqweq_fully_faithful_is_functor_app F a a). simpl. rewrite functor_id. apply correct_hom_on_id. 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.