Lemma GRP_dagger_laws : dagger_laws GRP_dagger_structure. Proof. repeat split ; intro ; intros ; use inverse_unique_precat. - exact (identity x). - apply groupoid_is_pregroupoid. - apply is_inverse_in_precat_identity. - exact (f · g). - apply groupoid_is_pregroupoid. - apply is_inverse_in_precat_comp ; apply groupoid_is_pregroupoid. - apply groupoid_is_pregroupoid ; exact f. - apply groupoid_is_pregroupoid. - apply is_inverse_in_precat_inv ; apply groupoid_is_pregroupoid. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Groupoids. Require Import UniMath.CategoryTheory.DaggerCategories.Categories. Require Import UniMath.CategoryTheory.DaggerCategories.Unitary. Require Import UniMath.CategoryTheory.DaggerCategories.Univalence.