proposition: Proposition pair_eq_pr2 {a b c : V} (φ : a --> b ⊸ w) (h : c --> b) : φ #⊗ h · internal_eval b w · BinProductPr2 V prod = pair_fun_pr2 φ #⊗ h · internal_eval _ _.
proof: Proof. unfold pair_fun_pr2 ; cbn. rewrite self_enrichment_postcomp. rewrite tensor_comp_r_id_r. rewrite !assoc'. apply maponpaths. rewrite internal_beta. apply maponpaths. unfold internal_to_arr. unfold self_enrichment_binary_product_pr2. rewrite !assoc'. rewrite internal_beta. rewrite !assoc. rewrite mon_linvunitor_lunitor. rewrite id_left. apply idpath. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.EnrichedCats.Enrichment UniMath.CategoryTheory.EnrichedCats.Examples.SelfEnriched UniMath.CategoryTheory.EnrichedCats.Limits.EnrichedTerminal UniMath.CategoryTheory.EnrichedCats.Limits.EnrichedBinaryProducts UniMath.CategoryTheory.EnrichedCats.Limits.EnrichedProducts UniMath.CategoryTheory.EnrichedCats.Limits.EnrichedEqualizers UniMath.CategoryTheory.EnrichedCats.Limits.EnrichedPowers UniMath.CategoryTheory.Monoidal.Categories UniMath.CategoryTheory.Monoidal.Structure.Symmetric UniMath.CategoryTheory.Monoidal.Structure.Closed UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.Equalizers UniMath.CategoryTheory.Limits.Products