@[reducible, inline]
Equations
- CategoryTheory.Psh C = CategoryTheory.Functor Cᵒᵖ (Type ?u.10)
Instances For
instance
CategoryTheory.cartesianClosedOver
{C : Type u}
[Category.{max u v, u} C]
(P : Psh C)
:
CartesianClosed (Over P)
instance
CategoryTheory.instExponentiableMorphismPsh
{C : Type u_1}
[SmallCategory C]
{X Y : Psh C}
(f : X ⟶ Y)
: