proposition: Lemma isstrict_groupoid_category X `{IsHSet X} : IsStrictCategory (groupoid_category X).
proof: Proof. typeclasses eauto. Defined.
imports: Category.Morphisms Category.Strict Trunc Types.Forall PathGroupoids Basics.Tactics