Proposition coupling_composition_assoc {x y z w : C} (β : I_{C} --> x ⊗ y) (γ : I_{C} --> y ⊗ z) (δ : I_{C} --> z ⊗ w) (e1 : β · proj2 = γ · proj1) (e2 : γ · proj2 = δ · proj1) : coupling_composition (coupling_composition β γ) δ = coupling_composition β (coupling_composition γ δ). Proof. assert (coupling_composition β γ · proj2 = δ · proj1) as e3. { rewrite coupling_composition_cod ; assumption. } assert (β · proj2 = coupling_composition γ δ · proj1) as e4. { rewrite coupling_composition_dom ; assumption. } etrans. { repeat (rewrite coupling_composition_eq_2 ; [ | assumption ]). etrans. { do 2 apply maponpaths_2. exact (conditional_distribution_1_eq β). } do 2 refine (assoc' _ _ _ @ _). rewrite <- tensor_comp_id_l. rewrite pairing_tensor_r. rewrite conditional_distribution_1_to_2. rewrite e1. rewrite conditional_distribution_1_to_2. rewrite e2. rewrite <- (id_right (δ |1)). rewrite conditional_distribution_1_to_2. rewrite id_right. rewrite <- pairing_tensor_l. refine (assoc _ _ _ @ _). apply maponpaths_2. exact (!(conditional_distribution_2_eq δ)). } repeat (rewrite coupling_composition_eq_3 ; [ | assumption ]). rewrite tensor_comp_id_r. rewrite assoc'. reflexivity. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.coslicecat. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Categories.Quotient. 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.State. Require Import UniMath.CategoryTheory.MarkovCategories.InformationFlowAxioms. Require Import UniMath.CategoryTheory.MarkovCategories.AlmostSurely. Require Import UniMath.CategoryTheory.MarkovCategories.Conditionals. Import MonoidalNotations.