Proposition univalence_weq_markov_univalence {C : markov_category} (H : all_isos_deterministic C) : is_univalent C ≃ is_markov_univalent C. Proof. use weqimplimpl. - intros HC x y. use weqhomot. + refine (iso_weq_det_iso_all_deterministic H x y ∘ _)%weq. use make_weq. * apply idtoiso. * apply HC. + intro p. induction p. use subtypePath. { intro. apply isaprop_is_deterministic. } cbn. reflexivity. - intros HC x y. use weqhomot. + refine (invweq (iso_weq_det_iso_all_deterministic H x y) ∘ _)%weq. use make_weq. * apply idtodet_iso. * apply HC. + intro p. induction p. cbn. reflexivity. - apply isaprop_is_univalent. - apply isaprop_is_markov_univalent. 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. Import MonoidalNotations. Require Import UniMath.CategoryTheory.MarkovCategories.Determinism.