Definition functor_enrichment_disp_cat_id_comp : disp_cat_id_comp [C₁, C₂] functor_enrichment_disp_cat_ob_mor. Proof. simple refine (_ ,, _). - exact (λ F FE, id_trans_enrichment FE). - exact (λ F₁ F₂ F₃ τ θ FE₁ FE₂ FE₃ τE θE, comp_trans_enrichment τE θE). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.EnrichedCats.Enrichment. Require Import UniMath.CategoryTheory.EnrichedCats.EnrichmentFunctor. Require Import UniMath.CategoryTheory.EnrichedCats.EnrichmentTransformation. Require Import UniMath.CategoryTheory.EnrichedCats.Examples.HomFunctor. Require Import UniMath.CategoryTheory.EnrichedCats.Examples.OppositeEnriched. Require Import UniMath.CategoryTheory.EnrichedCats.Examples.SelfEnriched. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.Monoidal.Structure.Symmetric. Require Import UniMath.CategoryTheory.Monoidal.Structure.Closed. Require Import UniMath.CategoryTheory.OppositeCategory.Core. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.Limits.Equalizers. Require Import UniMath.CategoryTheory.Limits.Products. Import MonoidalNotations. Section EnrichmentFromArr. End EnrichmentFromArr.