fact: Definition isotoid (s d : groupoid_category X) : s <~=~> d -> s = d := fun f => f : morphism _ _ _.
imports: Category.Core Category.Morphisms Category.Univalent GroupoidCategory.Core Trunc Equivalences HoTT.Tactics