Definition iso_between_terminal_enriched {x y : C} (Hx : is_terminal_enriched x) (Hy : is_terminal_enriched y) : z_iso x y. Proof. use make_z_iso. - exact (enriched_to_arr E (is_terminal_enriched_arrow Hy x)). - exact (enriched_to_arr E (is_terminal_enriched_arrow Hx y)). - split. + abstract (refine (enriched_to_arr_comp E _ _ @ _ @ enriched_to_arr_id E _) ; apply maponpaths ; apply (is_terminal_enriched_eq Hx)). + abstract (refine (enriched_to_arr_comp E _ _ @ _ @ enriched_to_arr_id E _) ; apply maponpaths ; apply (is_terminal_enriched_eq Hy)). Defined.
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.Monoidal.Categories. Require Import UniMath.CategoryTheory.EnrichedCats.Enrichment. Require Import UniMath.CategoryTheory.Limits.Terminal. Import MonoidalNotations.