Proposition is_deterministic_tensor {x1 x2 y1 y2 : C} {f1 : x1 --> y1} {f2 : x2 --> y2} (d1 : is_deterministic f1) (d2 : is_deterministic f2) : is_deterministic (f1 #⊗ f2). Proof. unfold is_deterministic in *. rewrite <- !copy_tensor. etrans. { rewrite assoc. rewrite <- tensor_comp_mor. rewrite d1, d2. rewrite tensor_comp_mor. apply idpath. } rewrite !assoc'. apply maponpaths. rewrite naturality_inner_swap. apply idpath. 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.