Mathlib Map

Structures · Category theory

CategoryTheory.Groupoid

A Groupoid is a category such that all morphisms are isomorphisms.

Defined in
Mathlib.CategoryTheory.Groupoid
Shape
One type argument · adds inv, inv_comp, comp_inv
Open in Mathlib docs

Extends1

Extended by0

Nothing extends this class yet.

Concrete types that are instances15

  • Quiver.Hom
  • CategoryTheory.Discrete
  • FundamentalGroupoid
  • CategoryTheory.Quotient
  • CategoryTheory.InducedCategory
  • CategoryTheory.Bundled.α
  • CategoryTheory.SingleObj
  • CategoryTheory.FreeMonoidalCategory
  • CategoryTheory.Functor.Elements
  • CategoryTheory.ActionCategory
  • CategoryTheory.Core
  • Quiver.FreeGroupoid
  • CategoryTheory.FreeGroupoid
  • Prod
  • Set.Elem

How is a type an instance?

Loading the hierarchy index…

Assumed by233

Ancestors41