proposition: Lemma mor_to_el_mor_comp {I J K} (ρ : pr1 (pr1 X I)) (f : C^op⟦I,J⟧) (g : C^op⟦J,K⟧) : mor_to_el_mor (f · g) ρ = transportb (λ Z, ∫ X⟦Z,_⟧) (make_ob_comp_eq ρ f g) (mor_to_el_mor g (# (pr1 X) f ρ) · mor_to_el_mor f ρ).
proof: Proof. apply (@transportf_transpose_right _ (λ Z : ∫ X, ∫ X ⟦Z,_⟧)), cat_of_elems_mor_eq; simpl. unfold transportb; rewrite pathsinv0inv0. rewrite transportf_total2; simpl; rewrite transportf_make_ob_eq. now unfold make_ob_comp_eq; rewrite base_paths_maponpaths_make_ob, idpath_transportf. Qed.
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.Categories.HSET.Core UniMath.CategoryTheory.opp_precat UniMath.CategoryTheory.Presheaf