|
Given a locally cartesian closed category E with a strict initial object, we define a negation operator on E and show that this yields a dense-closed orthogonal factorization system on E. Using this negation operator (and now assuming E has disjoint finite sums) we define both terms and derivatives of polynomial functors. Moreover, we show that the localization of E by the class W of dense monomorphisms E[W-1] remains locally cartesian closed, and that in E[W-1] all derivatives of polynomial functors exist. This generalizes Abbott-Altenkirch-Ghani-McBride's definition of derivatives by giving a context in which all derivatives exist. All results are shown categorically using distributivity pullbacks. Note that some parts are a work in progress.
|
