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