proposition: 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: 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.
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