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.

  • $\begingroup$ Do you mean $x = b$, rather than $t = b$? $\endgroup$ – Neel Krishnaswami Feb 23 '18 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 '18 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 '18 at 21:33
  • $\begingroup$ FWIW there are comprehension categories which models pi types differently (comparing to LCCC) $\endgroup$ – ice1000 May 17 at 1:34

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.