Lemma dagger_equality {C : category} (dag1 dag2 : dagger C) : dagger_to_struct dag1 = dagger_to_struct dag2 -> dag1 = dag2. Proof. intro p. apply (total2_paths_f p). apply isaprop_dagger_laws. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories.