proposition: Proposition product_enrichment_laws : enrichment_laws product_enrichment_data.
proof: Proof. repeat split. - intros xy₁ xy₂. use (BinProductArrowsEq _ _ _ (is_cartesian_BinProduct HV _ _)). + cbn. refine (mon_lunitor_pr1 _ _ _ @ _). rewrite enrichment_id_left. rewrite !assoc'. rewrite product_enrichment_comp_pr1. rewrite !assoc. apply maponpaths_2. use (BinProductArrowsEq _ _ _ (is_cartesian_BinProduct HV _ _)) ; cbn. * rewrite !assoc'. rewrite product_enrichment_pr1_comp_pr1. etrans. { apply maponpaths. apply cartesian_tensor_pr1. } refine (!_). rewrite !assoc. etrans. { apply maponpaths_2. apply cartesian_tensor_pr1. } rewrite !assoc'. etrans. { apply maponpaths. apply product_enrichment_id_pr1. } rewrite !assoc. apply maponpaths_2. rewrite cartesian_tensor_pr1. rewrite id_right. apply idpath. * rewrite !assoc'. rewrite product_enrichment_pr1_comp_pr2. etrans. { apply maponpaths. apply cartesian_tensor_pr2. } rewrite id_right. refine (!_). rewrite !assoc. etrans. { apply maponpaths_2. apply cartesian_tensor_pr2. } rewrite id_right. rewrite cartesian_tensor_pr2. apply idpath. + cbn. refine (mon_lunitor_pr2 _ _ _ @ _). rewrite enrichment_id_left. rewrite !assoc'. rewrite product_enrichment_comp_pr2. rewrite !assoc. apply maponpaths_2. use (BinProductArrowsEq _ _ _ (is_cartesian_BinProduct HV _ _)) ; cbn. * rewrite !assoc'. rewrite product_enrichment_pr2_comp_pr1. etrans. { apply maponpaths. apply cartesian_tensor_pr1. } refine (!_). rewrite !assoc. etrans. { apply maponpaths_2. apply cartesian_tensor_pr1. } rewrite !assoc'. etrans. { apply maponpaths. apply product_enrichment_id_pr2. } rewrite !assoc. apply maponpaths_2. rewrite cartesian_tensor_pr1. rewrite id_right. apply idpath. * rewrite !assoc'. rewrite product_enrichment_pr2_comp_pr2. etrans. { apply maponpaths. apply cartesian_tensor_pr2. } rewrite id_right. refine (!_). rewrite !assoc. etrans. { apply maponpaths_2. apply cartesian_tensor_pr2. } rewrite id_right. rewrite cartesian_tensor_pr2. apply idpath. - intros xy₁ xy₂. use (BinProductArrowsEq _ _ _ (is_cartesian_BinProduct HV _ _)). + cbn. refine (mon_runitor_pr1 _ _ _ @ _). rewrite enrichment_id_right. rewrite !assoc'. rewrite product_enrichment_comp_pr1. rewrite !assoc. apply maponpaths_2. use (BinProductArrowsEq _ _ _ (is_cartesian_BinProduct HV _ _)) ; cbn. * rewrite !assoc'. rewrite product_enrichment_pr1_comp_pr1. etrans. { apply maponpaths. apply cartesian_tensor_pr1. } refine (!_). rewrite !assoc. etrans. { apply maponpaths_2. apply cartesian_tensor_pr1. } rewrite !assoc'. rewrite id_left, id_right. rewrite cartesian_tensor_pr1. apply idpath. * rewrite !assoc'. rewrite product_enrichment_pr1_comp_pr2. etrans. { apply maponpaths. apply cartesian_tensor_pr2. } rewrite !assoc. rewrite !cartesian_tensor_pr2. rewrite id_right. rewrite !assoc'. apply maponpaths. refine (!_). apply product_enrichment_id_pr1. + cbn. refine (mon_runitor_pr2 _ _ _ @ _). rewrite enrichment_id_right. rewrite !assoc'. rewrite product_enrichment_comp_pr2. rewrite !assoc. apply maponpaths_2. use (BinProductArrowsEq _ _ _ (is_cartesian_BinProduct HV _ _)) ; cbn. * rewrite !assoc'. rewrite product_enrichment_pr2_comp_pr1. etrans. { apply maponpaths. apply cartesian_tensor_pr1. } refine (!_). rewrite !assoc. etrans. { apply maponpaths_2. apply cartesian_tensor_pr1. } rewrite !assoc'. rewrite id_left, id_right. rewrite cartesian_tensor_pr1. apply idpath. * rewrite !assoc'. rewrite product_enrichment_pr2_comp_pr2. etrans. { apply maponpaths. apply cartesian_tensor_pr2. } rewrite !assoc. rewrite !cartesian_tensor_pr2. rewrite id_right. rewrite !assoc'. apply maponpaths. refine (!_). apply product_enrichment_id_pr2. - intros w x y z. use (BinProductArrowsEq _ _ _ (is_cartesian_BinProduct HV _ _)) ; cbn. + rewrite !assoc'. rewrite !product_enrichment_comp_pr1. rewrite !assoc. rewrite triple_pr1_eq. rewrite !assoc'. rewrite enrichment_assoc. rewrite !assoc. apply maponpaths_2. use (BinProductArrowsEq _ _ _ (is_cartesian_BinProduct HV _ _)) ; cbn. * rewrite !assoc'. etrans. { do 2 apply maponpaths. apply cartesian_tensor_pr1. } rewrite id_right. rewrite mon_lassociator_pr1. rewrite product_enrichment_pr1_comp_pr1. refine (!_). etrans. { apply maponpaths. rewrite !assoc. apply maponpaths_2. apply cartesian_tensor_pr1. } rewrite id_right. rewrite !assoc. rewrite mon_lassociator_pr1. refine (!_). etrans. { apply maponpaths_2. apply (BinProductPr1Commutes _ _ _ (is_cartesian_BinProduct HV _ _)). } apply (BinProductPr1Commutes _ _ _ (is_cartesian_BinProduct HV _ _)). * rewrite !assoc'. etrans. { do 2 apply maponpaths. apply cartesian_tensor_pr2. } rewrite product_enrichment_pr1_comp_pr2. refine (!_). etrans. { apply maponpaths. rewrite !assoc. apply maponpaths_2. apply cartesian_tensor_pr2. } rewrite !assoc'. rewrite product_enrichment_comp_pr1. rewrite !assoc. apply maponpaths_2. rewrite !assoc'. rewrite mon_lassociator_pr2. use (BinProductArrowsEq _ _ _ (is_cartesian_BinProduct HV _ _)) ; cbn. ** rewrite !assoc'. rewrite product_enrichment_pr1_comp_pr1. rewrite !assoc. rewrite mon_lassociator_pr2. rewrite cartesian_tensor_pr1. refine (!_). rewrite !assoc'. etrans. { apply maponpaths. apply cartesian_tensor_pr1. } rewrite !assoc. etrans. { apply maponpaths_2. apply (BinProductPr1Commutes _ _ _ (is_cartesian_BinProduct HV _ _)). } apply (BinProductPr2Commutes _ _ _ (is_cartesian_BinProduct HV _ _)). ** rewrite !assoc'. rewrite product_enrichment_pr1_comp_pr2. rewrite !assoc. rewrite mon_lassociator_pr2. rewrite cartesian_tensor_pr2. refine (!_). rewrite !assoc'. etrans. { apply maponpaths. apply cartesian_tensor_pr2. } rewrite !assoc. etrans. { apply maponpaths_2. apply (BinProductPr2Commutes _ _ _ (is_cartesian_BinProduct HV _ _)). } rewrite !id_right. apply idpath. + rewrite !assoc'. rewrite !product_enrichment_comp_pr2. rewrite !assoc. rewrite triple_pr2_eq. rewrite !assoc'. rewrite enrichment_assoc. rewrite !assoc. apply maponpaths_2. use (BinProductArrowsEq _ _ _ (is_cartesian_BinProduct HV _ _)) ; cbn. * rewrite !assoc'. etrans. { do 2 apply maponpaths. apply cartesian_tensor_pr1. } rewrite id_right. rewrite mon_lassociator_pr1. rewrite product_enrichment_pr2_comp_pr1. refine (!_). etrans. { apply maponpaths. rewrite !assoc. apply maponpaths_2. apply cartesian_tensor_pr1. } rewrite id_right. rewrite !assoc. rewrite mon_lassociator_pr1. refine (!_). etrans. { apply maponpaths_2. apply (BinProductPr1Commutes _ _ _ (is_cartesian_BinProduct HV _ _)). } apply (BinProductPr1Commutes _ _ _ (is_cartesian_BinProduct HV _ _)). * rewrite !assoc'. etrans. { do 2 apply maponpaths. apply cartesian_tensor_pr2. } rewrite product_enrichment_pr2_comp_pr2. refine (!_). etrans. { apply maponpaths. rewrite !assoc. apply maponpaths_2. apply cartesian_tensor_pr2. } rewrite !assoc'. rewrite product_enrichment_comp_pr2. rewrite !assoc. apply maponpaths_2. rewrite !assoc'. rewrite mon_lassociator_pr2. use (BinProductArrowsEq _ _ _ (is_cartesian_BinProduct HV _ _)) ; cbn. ** rewrite !assoc'. rewrite product_enrichment_pr2_comp_pr1. rewrite !assoc. rewrite mon_lassociator_pr2. rewrite cartesian_tensor_pr1. refine (!_). rewrite !assoc'. etrans. { apply maponpaths. apply cartesian_tensor_pr1. } rewrite !assoc. etrans. { apply maponpaths_2. apply (BinProductPr1Commutes _ _ _ (is_cartesian_BinProduct HV _ _)). } apply (BinProductPr2Commutes _ _ _ (is_cartesian_BinProduct HV _ _)). ** rewrite !assoc'. rewrite product_enrichment_pr2_comp_pr2. rewrite !assoc. rewrite mon_lassociator_pr2. rewrite cartesian_tensor_pr2. refine (!_). rewrite !assoc'. etrans. { apply maponpaths. apply cartesian_tensor_pr2. } rewrite !assoc. etrans. { apply maponpaths_2. apply (BinProductPr2Commutes _ _ _ (is_cartesian_BinProduct HV _ _)). } rewrite !id_right. apply idpath. - intros x y f ; cbn. use pathsdirprod. + rewrite product_enrichment_from_arr_pr1. rewrite enriched_to_from_arr. apply idpath. + rewrite product_enrichment_from_arr_pr2. rewrite enriched_to_from_arr. apply idpath. - intros x y f ; cbn. use (BinProductArrowsEq _ _ _ (is_cartesian_BinProduct HV _ _)) ; cbn. + refine (product_enrichment_from_arr_pr1 _ _ @ _). apply enriched_from_to_arr. + refine (product_enrichment_from_arr_pr2 _ _ @ _). apply enriched_from_to_arr. - intros x ; cbn. use pathsdirprod. + rewrite product_enrichment_id_pr1. apply enriched_to_arr_id. + rewrite product_enrichment_id_pr2. apply enriched_to_arr_id. - intros x y z f g ; cbn. use pathsdirprod. + rewrite (enriched_to_arr_comp E₁). apply maponpaths. rewrite !assoc'. apply maponpaths. rewrite product_enrichment_comp_pr1. rewrite !assoc. apply maponpaths_2. use (BinProductArrowsEq _ _ _ (is_cartesian_BinProduct HV _ _)) ; cbn. * rewrite !assoc'. rewrite product_enrichment_pr1_comp_pr1. rewrite !assoc. rewrite !cartesian_tensor_pr1. rewrite !assoc'. refine (cartesian_tensor_pr1 _ _ _ @ _). apply maponpaths. refine (!_). apply product_enrichment_from_arr_pr1. * rewrite !assoc'. rewrite product_enrichment_pr1_comp_pr2. rewrite !assoc. rewrite !cartesian_tensor_pr2. rewrite !assoc'. refine (cartesian_tensor_pr2 _ _ _ @ _). apply maponpaths. refine (!_). apply product_enrichment_from_arr_pr1. + rewrite (enriched_to_arr_comp E₂). apply maponpaths. rewrite !assoc'. apply maponpaths. rewrite product_enrichment_comp_pr2. rewrite !assoc. apply maponpaths_2. use (BinProductArrowsEq _ _ _ (is_cartesian_BinProduct HV _ _)) ; cbn. * rewrite !assoc'. rewrite product_enrichment_pr2_comp_pr1. rewrite !assoc. rewrite !cartesian_tensor_pr1. rewrite !assoc'. refine (cartesian_tensor_pr1 _ _ _ @ _). apply maponpaths. refine (!_). apply product_enrichment_from_arr_pr2. * rewrite !assoc'. rewrite product_enrichment_pr2_comp_pr2. rewrite !assoc. rewrite !cartesian_tensor_pr2. rewrite !assoc'. refine (cartesian_tensor_pr2 _ _ _ @ _). apply maponpaths. refine (!_). apply product_enrichment_from_arr_pr2. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.opp_precat UniMath.CategoryTheory.Core UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.EnrichedCats.Enrichment UniMath.CategoryTheory.EnrichedCats.EnrichmentFunctor UniMath.CategoryTheory.EnrichedCats.EnrichmentTransformation UniMath.CategoryTheory.Monoidal.Categories UniMath.CategoryTheory.Monoidal.Structure.Cartesian UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.Limits.BinProducts