Proposition bloom_coupling_composition {x y z : C} (p : I_{C} --> x) (f : x --> y) (g : y --> z) : coupling_composition (bloom_coupling p f) (bloom_coupling (p · f) g) = bloom_coupling p (f · g). Proof. assert(compat : bloom_coupling p f · proj2 = bloom_coupling (p · f) g · proj1). { rewrite bloom_coupling_dom, bloom_coupling_cod. reflexivity. } rewrite coupling_composition_eq_2; [ | assumption ]. unfold bloom_coupling. rewrite assoc'. rewrite pairing_tensor. rewrite id_left. assert(target : f · (p · f · ⟨ identity y, g ⟩) |1 =_{p} f · g). { use ase_comp. - apply conditionals_imply_causality. - apply bloom_coupling_conditional_1_ase. } exact target. 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.