Definition constant_functor_enrichment (E : cat_with_enrichment V) (x : E) : functor_enrichment (constant_functor unit_cat_with_enrichment E x) unit_cat_with_enrichment E. Proof. simple refine (_ ,, _). - exact (λ _ _, enriched_id _ _). - repeat split. + abstract (intros y ; cbn ; apply id_left). + abstract (intros y₁ y₂ y₃ ; cbn ; rewrite tensor_split ; rewrite assoc' ; rewrite <- enrichment_id_left ; rewrite tensor_lunitor ; apply idpath). + abstract (intros y₁ y₂ f ; cbn ; rewrite enriched_from_arr_id ; rewrite id_left ; apply idpath). 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.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Categories.StandardCategories. Require Import UniMath.CategoryTheory.EnrichedCats.Enrichment. Require Import UniMath.CategoryTheory.EnrichedCats.EnrichmentFunctor. Require Import UniMath.CategoryTheory.EnrichedCats.EnrichmentTransformation. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.Monoidal.Structure.Cartesian. Require Import UniMath.CategoryTheory.Limits.Terminal. Import MonoidalNotations.