Definition product_enrichment_data : enrichment_data (category_binproduct C₁ C₂) V. Proof. simple refine (_ ,, _ ,, _ ,, _ ,, _). - exact (λ xy₁ xy₂, product_enrichment_hom (pr1 xy₁) (pr1 xy₂) (pr2 xy₁) (pr2 xy₂)). - exact (λ xy, product_enrichment_id (pr1 xy) (pr2 xy)). - exact (λ xy₁ xy₂ xy₃, product_enrichment_comp _ _ _ _ _ _). - exact (λ xy₁ xy₂ fg, product_enrichment_from_arr (pr1 fg) (pr2 fg)). - exact (λ xy₁ xy₂ fg, product_enrichment_to_arr fg). 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.opp_precat. Require Import UniMath.CategoryTheory.Core. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. 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. Require Import UniMath.CategoryTheory.Limits.BinProducts. Import MonoidalNotations.