proposition: 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: 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.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.Foundations.UnivalenceAxiom UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.Setcategories UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.Adjunctions.Core UniMath.CategoryTheory.Equivalences.Core UniMath.CategoryTheory.Equivalences.FullyFaithful