module Cat.Groupoid whereGroupoids🔗
A category is a (pre)groupoid if every morphism of is invertible.
is-pregroupoid : ∀ {o ℓ} → Precategory o ℓ → Type (o ⊔ ℓ)
is-pregroupoid C = ∀ {x y} (f : Hom x y) → is-invertible f
where open Cat.Reasoning Cmodule Cat.Groupoid whereA category is a (pre)groupoid if every morphism of is invertible.
is-pregroupoid : ∀ {o ℓ} → Precategory o ℓ → Type (o ⊔ ℓ)
is-pregroupoid C = ∀ {x y} (f : Hom x y) → is-invertible f
where open Cat.Reasoning C