Lemma copy_tensor_x_I_mor_comp {C : markov_category} {x y : C} (f : I_{C} --> x ⊗ x) (g : x ⊗ I_{C} --> y) : ⟨f, identity _⟩ · mon_lassociator _ _ _ · (identity _ #⊗ g) = f · (identity _ #⊗ (mon_rinvunitor _ · g)). Proof. unfold pairing. rewrite copy_I_mon_rinvunitor. rewrite <- tensor_rinvunitor. rewrite <- !assoc. apply maponpaths. rewrite <- mon_rinvunitor_triangle. etrans. { rewrite !assoc'. apply maponpaths. rewrite assoc. rewrite mon_rassociator_lassociator. apply id_left. } rewrite <- tensor_comp_l_id_r. apply idpath. 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.MarkovCategories.MarkovCategory. Require Import UniMath.CategoryTheory.MarkovCategories.Determinism. Require Import UniMath.CategoryTheory.MarkovCategories.InformationFlowAxioms. Require Import UniMath.CategoryTheory.MarkovCategories.AlmostSurely. Import MonoidalNotations.