Lemma unitary_inv_is_unitary {C : category} {dag : dagger C} {x y : C} {f : C⟦x,y⟧} (ff : is_unitary dag f) : is_unitary dag (pr1 dag x y f). Proof. split. - refine (! dagger_to_law_comp dag y x y (pr1 dag x y f) f @ _). etrans. { apply maponpaths, ff. } apply dagger_to_law_id. - refine (! dagger_to_law_comp dag x y x f (pr1 dag x y f) @ _). etrans. { apply maponpaths, ff. } apply dagger_to_law_id. 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.