Proposition ase_congruence {x y z : C} {f f' : x --> y} {g g' : y --> z} {p : I_{C} --> x} {q : I_{C} --> y} (e1 : f =_{p} f') (e2 : g =_{q} g') (e3 : q = p · f) : f · g =_{p} f' · g'. Proof. use ase_trans. - exact (f · g'). - apply ase_comp. rewrite <- e3. exact e2. - apply ase_postcomp. exact e1. 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.