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