proposition: 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: 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.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.DaggerCategories.Categories