1. Presheaves are a CCC

The category of presheaves on a small category is cartesian closed

@[reducible, inline]

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

Equations

• CategoryTheory.Psh C = CategoryTheory.Functor Cᵒᵖ (Type u_2)

def CategoryTheory.diagCCC {C : Type u_1} [CategoryTheory.Category.{u_1, u_1} C] : CategoryTheory.CartesianClosed (CategoryTheory.Psh C)

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.presheafCCC {C : Type v₁} [CategoryTheory.SmallCategory C] : CategoryTheory.CartesianClosed (CategoryTheory.Psh C)

Equations

• CategoryTheory.presheafCCC = CategoryTheory.diagCCC

2. The category of elements

The category of elements of a contravariant functor P : Cᵒᵖ ⥤ Type is the opposite of the category of elements of P regarded as a covariant functor P : Cᵒᵖ ⥤ Type. Thus an object of (Elements P)ᵒᵖ is a pair (X : C, x : P.obj X) and a morphism (X, x) ⟶ (Y, y) is a morphism f : X ⟶ Y in C for which P.map f takes y back to x. We have an equivalence (Elements P)ᵒᵖ ≌ (yoneda, P). In MathLib the comma category is called the ``costructured arrow category''.

def CategoryTheory.CategoryOfElements.equivPsh {C : Type u_2} {D : Type u_3} [CategoryTheory.Category.{u_4, u_2} C] [CategoryTheory.Category.{u_4, u_3} D] (e : C ≌ D) : CategoryTheory.Psh C ≌ CategoryTheory.Psh D

Equations

• CategoryTheory.CategoryOfElements.equivPsh e = e.op.congrLeft

def CategoryTheory.CategoryOfElements.presheafElementsOpIsPshCostructuredArrow {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (P : CategoryTheory.Psh C) : CategoryTheory.Psh (CategoryTheory.Functor.Elements P)ᵒᵖ ≌ CategoryTheory.Psh (CategoryTheory.CostructuredArrow CategoryTheory.yoneda P)

Equations

• CategoryTheory.CategoryOfElements.presheafElementsOpIsPshCostructuredArrow P = CategoryTheory.CategoryOfElements.equivPsh (CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalence P)

3. The slice category of presheaves

The slice category (Psh C)/P is called the "over category" in MathLib and written "Over P".

def CategoryTheory.CategoryOfElements.overPshIsPshElementsOp {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {P : CategoryTheory.Psh C} : CategoryTheory.Over P ≌ CategoryTheory.Psh (CategoryTheory.Functor.Elements P)ᵒᵖ

Equations

• One or more equations did not get rendered due to their size.

4. The slice category Psh(C)/P is a CCC

We transfer the CCC structure across the equivalence (Psh C)/P ≃ Psh((Elements P)ᵒᵖ) using the following: def cartesianClosedOfEquiv (e : C ≌ D) [CartesianClosed C] : CartesianClosed D := MonoidalClosed.ofEquiv (e.inverse.toMonoidalFunctorOfHasFiniteProducts) e.symm.toAdjunction

def CategoryTheory.CategoryOfElements.presheafOverCCC {C : Type u_1} [CategoryTheory.Category.{max u_1 u_2, u_1} C] (P : CategoryTheory.Psh C) : CategoryTheory.CartesianClosed (CategoryTheory.Over P)

Equations

• CategoryTheory.CategoryOfElements.presheafOverCCC P = CategoryTheory.cartesianClosedOfEquiv CategoryTheory.CategoryOfElements.overPshIsPshElementsOp.symm

def CategoryTheory.CategoryOfElements.allPresheafOverCCC {C : Type u_1} [CategoryTheory.Category.{max u_1 u_2, u_1} C] (P : CategoryTheory.Psh C) : CategoryTheory.CartesianClosed (CategoryTheory.Over P)

Equations

• CategoryTheory.CategoryOfElements.allPresheafOverCCC P = CategoryTheory.CategoryOfElements.presheafOverCCC P

5. Presheaves is an LCCC

Use results in the file on locally cartesian closed categories.

Some references

1. Wellfounded trees and dependent polynomial functors.Gambino, Nicola; Hyland, Martin. Types for proofs and programs. International workshop, TYPES 2003, Torino, Italy, 2003. Revised selected papers.. Springer Berlin, 2004. p. 210-225.

2. Tamara Von Glehn. Polynomials and models of type theory. PhD thesis, University of Cambridge, 2015.

3. Joachim Kock. Data types with symmetries and polynomial functors over groupoids. Electronic Notes in Theoretical Computer Science, 286:351–365, 2012. Proceedings of the 28th Conference on the Mathematical Foundations of Programming Semantics (MFPS XXVIII).

4. Jean-Yves Girard. Normal functors, power series and λ-calculus. Ann. Pure Appl. Logic, 37(2):129–177, 1988. doi:10.1016/0168-0072(88)90025-5.

5. David Gepner, Rune Haugseng, and Joachim Kock. 8-Operads as analytic monads. Interna- tional Mathematics Research Notices, 2021.

6. Nicola Gambino and Joachim Kock. Polynomial functors and polynomial monads. Mathematical Proceedings of the Cambridge Philosophical Society, 154(1):153–192, 2013.

7. Marcelo Fiore, Nicola Gambino, Martin Hyland, and Glynn Winskel. The cartesian closed bicategory of generalised species of structures. J. Lond. Math. Soc. (2), 77(1):203–220, 2008.

8. M. Fiore, N. Gambino, M. Hyland, and G. Winskel. Relative pseudomonads, Kleisli bicategories, and substitution monoidal structures. Selecta Mathematica, 24(3):2791–2830, 2018.

9. Steve Awodey and Clive Newstead. Polynomial pseudomonads and dependent type theory, 2018.

10. Steve Awodey, Natural models of homotopy type theory, Mathematical Structures in Computer Science, 28 2 (2016) 241-286, arXiv:1406.3219.