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