Definition make_dagger_category {C : category} {d : dagger_structure C} (dl : dagger_laws d) : dagger_category := C ,, d ,, dl.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories.