Lemma catiso_to_precategory_comp_path {A B : precategory} (F : catiso A B) : forall a a' a'' : A, (transportb (X := total2 (λ T, T -> T -> UU)) (λ T, forall a b c : (pr1 T), (pr2 T) a b -> (pr2 T) b c -> (pr2 T) a c) (total2_paths2_b (catiso_to_precategory_ob_path F) (catiso_to_precategory_mor_path_funext F)) (@compose B)) a a' a'' = (@compose A a a' a''). Proof. intros a a' a''. eapply pathscomp0. apply transport_comp. apply funextsec. intros f. apply funextsec. intros g. unfold transport_comp_target. unfold catiso_to_precategory_mor_path_funext. simpl. set (W := homotweqinvweq (weqtoforallpaths (λ _ : A, A -> UU) precategory_morphisms (transportb (λ T, T -> T -> UU) (catiso_to_precategory_ob_path F) precategory_morphisms))). simpl in W. rewrite !W. clear W. set (W := homotweqinvweq (weqtoforallpaths (λ _ : A, UU) (precategory_morphisms a) (transportb (λ T, T -> T -> UU) (catiso_to_precategory_ob_path F) precategory_morphisms a))). simpl in W. rewrite !W. clear W. set (W := homotweqinvweq (weqtoforallpaths (λ _ : A, UU) (precategory_morphisms a') (transportb (λ T, T -> T -> UU) (catiso_to_precategory_ob_path F) precategory_morphisms a'))). simpl in W. rewrite !W. clear W. unfold catiso_to_precategory_mor_path. rewrite !pathscomp0rid. rewrite !pathscomp_inv. rewrite !pathsinv0inv0. rewrite path_assoc. rewrite path_assoc. rewrite pathsinv0r. simpl. rewrite <- path_assoc. rewrite <- path_assoc. rewrite pathsinv0r. rewrite pathscomp0rid. rewrite <- path_assoc. rewrite <- path_assoc. rewrite pathsinv0r. rewrite pathscomp0rid. rewrite <- pathscomp_inv. apply pathsweq1'. rewrite eqweqmap_pathsinv0. rewrite invinv. rewrite <- !eqweqmap_pathscomp0. rewrite !eqweq_fully_faithful_is_functor_app. simpl. rewrite functor_comp. apply (correct_hom_on_comp 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.