Lemma unitary_inv_to_left {a b c : C} (f : C⟦ a, b ⟧) (g : C⟦b, c⟧) (h : C⟦ a, c ⟧) : is_unitary dag f -> dag _ _ f · h = g → h = f · g. Proof. exact (λ u p, z_iso_inv_to_left _ _ _ (make_z_iso _ _ (_,,pr2 u)) _ _ p). Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.DaggerCategories.Categories.