17
$\begingroup$

I have recently been working with polynomial functors and monads based mostly on Gambino-Kock. There they define polynomial functors in a Locally Cartesian Closed Category (LCCC) and extensively use dependent type theory to define constructions on polynomials because working in the internal language is much easier than the diagrammtic language.

However, I am interested in polynomial monads for their application to defining flavors of multi-category and for that I need to use polynomals in Cat and similar categories, which have pullbacks, but are not locally closed. There you instead require in the polynomial diagrams

$$I \leftarrow E \to B \to J$$

that the middle arrow $E \to B$ is exponentiable, since that is the only $\Pi$ you use. The only paper I know of that does this is this which doesn't use the internal language at all and is much more difficult for me at least because of it.

Is there some kind of restriction I can put on dependent type theory so that I can use it as an internal language for a category with pullbacks rather than an LCCC? Specifically I want to be able to manipulate exponentiable morphisms as dependent types that I can take $\Pi$ of, but not every dependent type should be exponentiable. Then hopefully the usual proofs using dependent type theory would still be valid, because every use of $\Pi$ would be modeled by an exponentiable morphism.

My own idea would be to have dependent types interpreted as exponentiable morphisms and other terms interpreted as arbitrary morphisms, but since you can define from any $x : A \vdash t : B$ (where $\cdot \vdash B$) the dependent type: $$b : B \vdash \sum_{x:A} t = b$$ it seems like the type theory would make every morphism exponentiable.

Improve this question
$\endgroup$
4
  • $\begingroup$ Do you mean $x = b$, rather than $t = b$? $\endgroup$
    – Neel Krishnaswami
    Feb 23, 2018 at 15:44
  • $\begingroup$ No, I think it's right. $t$ has x as a free variable. It's supposed to be the fiber of $t$ over $b$. $\endgroup$
    – Max New
    Feb 23, 2018 at 15:57
  • 1
    $\begingroup$ Well, Cat is a 2-topos, so maybe a form of directed type theory? And if you don't need Pi-types, then Sigma and Id-types can be modeled in any lex category (addressing the question in the title), but that's probably not so helpful for the polynomial stuff. $\endgroup$
    – Ulrik Buchholtz
    Feb 28, 2018 at 21:33
  • $\begingroup$ FWIW there are comprehension categories which models pi types differently (comparing to LCCC) $\endgroup$
    – ice1000
    May 17, 2021 at 1:34

0

Reset to default

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.