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