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. 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.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.Categories.HSET.Core. Require Import UniMath.CategoryTheory.opp_precat. Require Import UniMath.CategoryTheory.Presheaf.