Proposition is_deterministic_mon_runitor (x : C) : is_deterministic (mon_runitor x). Proof. unfold is_deterministic. rewrite <- copy_tensor. rewrite <- precompose_inner_swap_with_lunitors_and_runitor. refine (!_). etrans. { rewrite !assoc'. apply maponpaths. rewrite !assoc. rewrite inner_swap_inv. rewrite id_left. apply idpath. } rewrite tensor_mor_left. rewrite <- tensor_runitor. rewrite !assoc. apply maponpaths_2. etrans. { refine (!_). apply tensor_comp_mor. } rewrite id_right. apply maponpaths. apply markov_category_unit_eq. 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.Monoidal.Structure.SymmetricDiagonal. Require Import UniMath.CategoryTheory.MarkovCategories.MarkovCategory. Require Import UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors. Import MonoidalNotations. Import BifunctorNotations.