Lemma dagger_category_equality (C1 C2 : dagger_category) : ∏ p : precategory_data_from_precategory C1 = precategory_data_from_precategory C2, (∏ x y : C2, ∏ f : C2⟦x,y⟧, pr1 (transportf dagger (category_eq C1 C2 p) C1) x y f = {f}_C2^†) -> C1 = C2. Proof. intros p q. use total2_paths_f. - exact (category_eq _ _ p). - use subtypePath. + intro ; apply isaprop_dagger_laws. + do 3 (apply funextsec ; intro). apply q. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories.