Proposition bloom_coupling_conditional_2_ase {x y : C} (p : I_{C} --> x) (f : x --> y) : (bloom_coupling p f)|2 =_{p · f} bayesian_inverse p f. Proof. unfold equal_almost_surely. assert(e : p · f · ⟨ identity y, (bloom_coupling p f) |2 ⟩ = bloom_coupling p f · proj2 · ⟨ identity y, (bloom_coupling p f) |2 ⟩). { rewrite bloom_coupling_cod. reflexivity. } rewrite e. clear e. apply cancel_braiding. rewrite !assoc', !pairing_sym_mon_braiding, !assoc. rewrite <- conditional_distribution_2_eq. rewrite bayesian_inverse_eq_l. 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.