(s d : groupoid_category X) : s <~=~> d -> s = d := fun f => f : morphism _ _ _. Global Instance iscategory_groupoid_category : IsCategory (groupoid_category X). Proof. repeat intro. apply (isequiv_adjointify (@idtoiso (groupoid_category X) _ _) (@ _ _)); repeat intro; destruct_head @Isomorphic; destruct_head @IsIsomorphism; compute in *; path_induction_hammer. Qed.
Require Import Category.Core Category.Morphisms Category.Univalent GroupoidCategory.Core. Require Import Trunc Equivalences HoTT.Tactics.