proposition: Lemma isaset_dagger (C : category) : isaset (dagger C).
proof: Proof. apply isaset_total2. - apply isaset_dagger_structure. - intro ; apply isasetaprop ; apply isaprop_dagger_laws. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories