open import Cat.Prelude

import Cat.Reasoning

module Cat.Groupoid where

Groupoids🔗

A category $\mathcal{C}$ is a (pre)groupoid if every morphism of $\mathcal{C}$ 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