Cat.Groupoid

1Lab
  • GroupoidsπŸ”—


back to index
view all pages
link to source

Written by AmΓ©lia Liao and Reed Mullanix

back to index
open import Cat.Prelude

import Cat.Reasoning
module Cat.Groupoid where

GroupoidsπŸ”—

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