Proposition dagger_coupling_composition {x y z : C} (β : I_{C} --> x ⊗ y) (γ : I_{C} --> y ⊗ z) (e : β · proj2 = γ · proj1) : coupling_composition (coupling_dagger γ) (coupling_dagger β) = coupling_dagger (coupling_composition β γ). Proof. assert(compat : coupling_dagger γ · proj2 = coupling_dagger β · proj1). { rewrite coupling_dagger_dom, coupling_dagger_cod, e. reflexivity. } assert(def_cond : (β · sym_mon_braiding C x y)|1 = β|2). { reflexivity. } etrans. { rewrite coupling_composition_eq_2; [ | assumption ]. unfold coupling_dagger. rewrite assoc'. rewrite <- tensor_sym_mon_braiding. rewrite def_cond. rewrite assoc. reflexivity. } symmetry. etrans. { rewrite coupling_composition_eq_2; [ | assumption ]. unfold coupling_dagger. reflexivity. } apply maponpaths_2. rewrite <- coupling_composition_eq_2; [ | assumption ]. rewrite <- coupling_composition_eq_3; [ | assumption ]. 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.