Mathlib Map

Structures · Category theory

CategoryTheory.CategoryStruct

A preliminary structure on the way to defining a category, containing the data, but none of the axioms.

Defined in
Mathlib.CategoryTheory.Category.Basic
Shape
One type argument · adds id, comp
Open in Mathlib docs

Extends1

Extended by2

Concrete types that are instances24

  • Quiver.Hom
  • CategoryTheory.Pairwise
  • CategoryTheory.Bicone
  • CategoryTheory.Comonad.Coalgebra
  • CategoryTheory.Monad.Algebra
  • CategoryTheory.SingleObj
  • CategoryTheory.Endofunctor.Coalgebra
  • CategoryTheory.Endofunctor.Algebra
  • CategoryTheory.CatEnriched
  • CategoryTheory.KleisliCat
  • SSet.Truncated.HomotopyCategory₂
  • CategoryTheory.Pseudofunctor.Grothendieck
  • CategoryTheory.Pseudofunctor.CoGrothendieck
  • CategoryTheory.SimplicialThickening
  • CategoryTheory.Limits.WidePullbackShape
  • CategoryTheory.Limits.WidePushoutShape
  • CategoryTheory.LocallyDiscrete
  • CategoryTheory.Bicategory.Pith
  • CategoryTheory.Bicategory.InducedBicategory
  • CategoryTheory.Bicategory.Adj
  • CategoryTheory.FreeBicategory
  • Prod
  • Opposite
  • Sigma

How is a type an instance?

Loading the hierarchy index…

Assumed by127

Ancestors1