Proposition is_precategory_couplings : is_precategory couplings_precategory_data. Proof. use make_is_precategory_one_assoc. - intros p q β. apply coupling_ext. apply coupling_id_left. rewrite identity_coupling_cod. rewrite coupling_dom. reflexivity. - intros p q β. apply coupling_ext. apply coupling_id_right. rewrite identity_coupling_dom. rewrite coupling_cod. reflexivity. - intros p q r s β γ δ. apply coupling_ext. cbn. rewrite coupling_composition_assoc. + reflexivity. + apply couplings_composable. + apply couplings_composable. 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.