Proposition pairing_proj1 {a x y : C} (f : a --> x) (g : a --> y) : ⟨f,g⟩ · proj1 = f. Proof. unfold proj1. rewrite assoc. rewrite pairing_tensor. rewrite id_right, del_natural. etrans. { rewrite <- (id_left f). rewrite <- (id_right (del a)). unfold pairing. rewrite tensor_comp_mor. rewrite assoc. rewrite copy_del_r_ex. rewrite <- assoc. rewrite tensor_runitor. rewrite assoc. rewrite mon_rinvunitor_runitor. rewrite id_left. reflexivity. } reflexivity. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.Monoidal.Structure.Cartesian. Require Import UniMath.CategoryTheory.Monoidal.Structure.Symmetric. Require Import UniMath.CategoryTheory.Monoidal.Structure.SymmetricDiagonal. Import MonoidalNotations.