open import Cat.Prelude

import Cat.Reasoning
module Cat.Groupoid where

Groupoids🔗

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 C
module is-pregroupoid {o â„“} {C : Precategory o â„“} (gpd : is-pregroupoid C) where
  open Cat.Reasoning C

  hom→iso : ∀ {x y} → Hom x y → x ≅ y
  hom→iso f = invertible→iso f (gpd f)