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