Proposition positive_implies_all_isos_deterministic (C : markov_category) : is_positive C -> all_isos_deterministic C. Proof. intros pos x y f. unfold is_deterministic. pose (g := inv_from_z_iso f). transitivity (f · ⟨identity _ , identity _⟩). { rewrite pairing_id. reflexivity. } transitivity (f · ⟨identity _, g · f⟩). { unfold g. rewrite z_iso_after_z_iso_inv. reflexivity. } etrans. { rewrite <- pairing_tensor_r. rewrite !assoc. rewrite positivity_r. { rewrite pairing_tensor_r. unfold g. rewrite z_iso_inv_after_z_iso, id_left. reflexivity. } - exact pos. - rewrite z_iso_inv_after_z_iso. apply is_deterministic_identity. } reflexivity. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Limits.Terminal. 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.AlmostSurely. Require Import UniMath.CategoryTheory.MarkovCategories.Univalence. Import MonoidalNotations.