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