Proposition presheaf_enrichment_id_laws (F : C ⟶ V) : presheaf_enrichment_id_data F · presheaf_enrichment_hom_eq_left F F = presheaf_enrichment_id_data F · presheaf_enrichment_hom_eq_right F F. Proof. use ProductArrow_eq. intros xyf. induction xyf as [ x [ y f ]]. unfold presheaf_enrichment_hom_eq_left, presheaf_enrichment_hom_eq_right. rewrite !assoc'. etrans. { apply maponpaths. exact (ProductPrCommutes (∑ (x y : C), x --> y) V _ _ _ _ _). } rewrite !assoc. etrans. { do 3 apply maponpaths_2. exact (ProductPrCommutes C V _ _ _ _ _). } refine (!_). etrans. { refine (assoc' _ _ _ @ _). apply maponpaths. exact (ProductPrCommutes (∑ (x y : C), x --> y) V _ _ _ _ _). } rewrite !assoc. etrans. { do 3 apply maponpaths_2. exact (ProductPrCommutes C V _ _ _ _ _). } cbn. use internal_funext. intros a h. rewrite !tensor_comp_r_id_r. rewrite !assoc'. unfold internal_comp. rewrite !internal_beta. etrans. { do 2 apply maponpaths. rewrite !assoc. rewrite tensor_lassociator. rewrite !assoc'. apply maponpaths. rewrite !assoc. apply maponpaths_2. rewrite <- tensor_comp_id_l. unfold internal_from_arr. rewrite internal_beta. apply idpath. } etrans. { apply maponpaths. rewrite tensor_comp_id_l. rewrite !assoc. do 2 apply maponpaths_2. rewrite !assoc'. rewrite <- mon_triangle. rewrite <- tensor_comp_id_r. rewrite mon_rinvunitor_runitor. apply tensor_id_id. } rewrite id_left. etrans. { rewrite !assoc. rewrite <- tensor_comp_mor. rewrite id_right. rewrite tensor_split. rewrite !assoc'. unfold internal_id. rewrite internal_beta. apply idpath. } refine (!_). etrans. { do 2 apply maponpaths. rewrite !assoc. rewrite tensor_lassociator. rewrite !assoc'. apply maponpaths. rewrite tensor_id_id. rewrite !assoc. rewrite <- tensor_split'. rewrite tensor_split. rewrite !assoc'. unfold internal_from_arr. rewrite internal_beta. rewrite !assoc. rewrite tensor_lunitor. apply idpath. } etrans. { apply maponpaths. rewrite !assoc. do 2 apply maponpaths_2. rewrite !assoc'. rewrite mon_lunitor_triangle. rewrite <- tensor_comp_id_r. rewrite mon_linvunitor_lunitor. apply tensor_id_id. } rewrite id_left. rewrite !assoc. rewrite tensor_split. unfold internal_id. rewrite !assoc'. etrans. { apply maponpaths. rewrite !assoc. rewrite internal_beta. apply idpath. } rewrite <- tensor_lunitor. rewrite !assoc. rewrite <- tensor_comp_id_l. apply idpath. Qed.
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.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.