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