Definition dagger_law_idemp {C : category} (dag : dagger_structure C) : UU := ∏ (x y : C) (f : C⟦x,y⟧), dag y x (dag x y f) = f.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories.