Mathlib Map

Structures · Category theory

CategoryTheory.Enriched.HasConicalLimit

HasConicalLimit F represents the mere existence of a conical limit for F.

Defined in
Mathlib.CategoryTheory.Enriched.Limits.HasConicalLimits
Shape
2 explicit arguments · adds preservesLimit_eCoyoneda

Extends1

Extended by1

Forgetful instances

Concrete types that are instances0

No instance on a concrete type; it is reached through other classes.

How is a type an instance?

Loading the hierarchy index…

Assumed by5

Ancestors1