🔍

Equations Inline Footnotes

open import Cat.Morphism.Duality
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

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)

module _ {o ℓ} (C : Precategory o ℓ) (gpd : is-pregroupoid C) where

Of course, the opposite of a groupoid is a groupoid.

  ^op-pregroupoid : is-pregroupoid (C ^op)
  ^op-pregroupoid f = invertible→co-invertible C (gpd f)