Proposition pair_eq_pr1 {a b c : V} (φ : a --> b ⊸ w) (h : c --> b) : φ #⊗ h · internal_eval b w · BinProductPr1 V prod = pair_fun_pr1 φ #⊗ h · internal_eval _ _. Proof. unfold pair_fun_pr1 ; 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_pr1. rewrite !assoc'. rewrite internal_beta. rewrite !assoc. rewrite mon_linvunitor_lunitor. rewrite id_left. apply idpath. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.EnrichedCats.Enrichment. Require Import UniMath.CategoryTheory.EnrichedCats.Examples.SelfEnriched. Require Import UniMath.CategoryTheory.EnrichedCats.Limits.EnrichedTerminal. Require Import UniMath.CategoryTheory.EnrichedCats.Limits.EnrichedBinaryProducts. Require Import UniMath.CategoryTheory.EnrichedCats.Limits.EnrichedProducts. Require Import UniMath.CategoryTheory.EnrichedCats.Limits.EnrichedEqualizers. Require Import UniMath.CategoryTheory.EnrichedCats.Limits.EnrichedPowers. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.Monoidal.Structure.Symmetric. Require Import UniMath.CategoryTheory.Monoidal.Structure.Closed. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Equalizers. Require Import UniMath.CategoryTheory.Limits.Products. Import MonoidalNotations.