Definition make_dagger_laws {C : category} {d : dagger_structure C} (lid : dagger_law_id d) (lcomp : dagger_law_comp d) (lidemp : dagger_law_idemp d) : dagger_laws d := lid ,, lcomp ,, lidemp.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories.