Lemma iso_between_conical_lim_enriched_inv (a b : conical_lim_enriched) : map_between_conical_lim_enriched a b · map_between_conical_lim_enriched b a = identity _. Proof. unfold map_between_conical_lim_enriched. use (is_conical_lim_enriched_arrow_eq a). intro j. rewrite !assoc'. rewrite !is_conical_lim_enriched_map_pr. rewrite id_left. apply idpath. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.Limits.Graphs.Limits. Require Import UniMath.CategoryTheory.Limits.Equalizers. Require Import UniMath.CategoryTheory.Limits.Products. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.EnrichedCats.Enrichment. Require Import UniMath.CategoryTheory.EnrichedCats.Limits.EnrichedProducts. Require Import UniMath.CategoryTheory.EnrichedCats.Limits.EnrichedEqualizers. Import MonoidalNotations.