@[reducible, inline]

abbrev CategoryTheory.Psh (C : Type u) [Category.{v, u} C] : Type (max u (v + 1))

Equations

• CategoryTheory.Psh C = CategoryTheory.Functor Cᵒᵖ (Type ?u.10)

instance CategoryTheory.cartesianClosedOver {C : Type u} [Category.{max u v, u} C] (P : Psh C) : CartesianClosed (Over P)

Equations

• CategoryTheory.cartesianClosedOver P = CategoryTheory.cartesianClosedOfEquiv (CategoryTheory.overEquivPresheafCostructuredArrow P).symm

instance CategoryTheory.locallyCartesianClosed {C : Type u_1} [SmallCategory C] : LocallyCartesianClosed (Psh C)

Equations

• CategoryTheory.locallyCartesianClosed = inferInstance

instance CategoryTheory.instExponentiableMorphismPsh {C : Type u_1} [SmallCategory C] {X Y : Psh C} (f : X ⟶ Y) : ExponentiableMorphism f