Documentation

Poly.ForMathlib.CategoryTheory.LocallyCartesianClosed.Presheaf

@[reducible, inline]
abbrev CategoryTheory.Psh (C : Type u) [Category.{v, u} C] :
Type (max u (v + 1))
Equations
Instances For