Definition make_enriched_precat_data (C : UU) (mor : ∏ x y : C, ob Mon_V) (ids : ∏ x : C, I --> mor x x) (assoc : ∏ x y z : C, mor y z ⊗ mor x y --> mor x z) : enriched_precat_data. Proof. unfold enriched_precat_data. use tpair; [|use tpair; [|use make_dirprod]]. - exact C. - exact mor. - exact ids. - exact assoc. Defined.
Require Import UniMath.Foundations.PartA. Require Import UniMath.Foundations.Propositions. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.Core.Isos. Import MonoidalNotations.