Lemma isaset_dagger_structure (C : category) : isaset (dagger_structure C). Proof. do 2 (apply impred_isaset ; intro). apply funspace_isaset. apply homset_property. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories.