Proposition coupling_id_left {x y : C} (p : I_{C} --> x) (β : I_{C} --> x ⊗ y) (e : identity_coupling p · proj2 = β · proj1) : coupling_composition (identity_coupling p) β = β. Proof. assert (e2 : p = β · proj1). { rewrite <- e. rewrite identity_coupling_cod. reflexivity. } rewrite coupling_composition_eq_2 ; [ | assumption ]. unfold identity_coupling. rewrite <- assoc. rewrite e2. rewrite conditional_distribution_1_eq. 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.