proposition: 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: 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.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories