proposition: Lemma mor_to_el_mor_id {I : C} (ρ : pr1 (pr1 X I)) : mor_to_el_mor (identity I) ρ = transportb (λ Z, ∫ X⟦Z, make_ob I ρ⟧) (make_ob_identity_eq ρ) (identity _).
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_identity_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