Definition unitary_id {C : category} (dag : dagger C) (x : C) : unitary dag x x. Proof. exists (identity_z_iso x). abstract (apply make_is_inverse_in_precat ; [ refine (id_left _ @ _) ; apply dagger_to_law_id | refine (id_right _ @ _) ; apply dagger_to_law_id ]). Defined.
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.