Definition iso_weq_det_iso_all_deterministic {C : markov_category} (H : all_isos_deterministic C) (x y : C) : z_iso x y ≃ deterministic_iso x y. Proof. use weq_iso. - intro f. refine (f ,, _). apply H. - intro f. exact (pr1 f). - abstract (intro f ; reflexivity). - abstract (intro f ; use subtypePath ; [ intro ; apply isaprop_is_deterministic | ] ; reflexivity). Defined.
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. Import MonoidalNotations. Require Import UniMath.CategoryTheory.MarkovCategories.Determinism.