Mathlib Map

Structures · Category theory

CategoryTheory.IsCofiltered

A category IsCofiltered if 1. for every pair of objects there exists another object "to the left", 2. for every pair of parallel morphisms there exists a morphism to the left so the compositions are equal, and 3. there exists some object.

Defined in
Mathlib.CategoryTheory.Filtered.Basic
Shape
One type argument · adds nonempty
Open in Mathlib docs

Extends1

Extended by1

Forgetful instances

Provided automatically by

Concrete types that are instances14

  • CategoryTheory.Over
  • CategoryTheory.Discrete
  • CategoryTheory.WithTerminal
  • CategoryTheory.CostructuredArrow
  • CategoryTheory.StructuredArrow
  • CategoryTheory.ULiftHom
  • CategoryTheory.Functor.Elements
  • CategoryTheory.InitiallySmall.CofilteredInitialModel
  • CategoryTheory.AsSmall
  • CategoryTheory.IsCofiltered.SmallCofilteredIntermediate
  • CategoryTheory.GrothendieckTopology.HOneHypercover
  • Prod
  • ULift
  • Opposite

How is a type an instance?

Loading the hierarchy index…

Assumed by166

Ancestors1