<p>I have recently been working with polynomial functors and monads based mostly on <a href="https://arxiv.org/abs/0906.4931" rel="noreferrer">Gambino-Kock</a>. 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.</p>

<p>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</p>

<p>$$I \leftarrow E \to B \to J$$</p>

<p>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 <a href="https://arxiv.org/abs/1106.1983" rel="noreferrer">this</a> which doesn't use the internal language at all and is much more difficult for me at least because of it.</p>

<p>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.</p>

<p>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.</p>

CC BY-SA 3.0
2018-02-23T15:44:53.723Z
Do you mean $x = b$, rather than $t = b$?
Neel Krishnaswami
CC BY-SA 3.0
2018-02-23T15:57:08.133Z
No, I think it's right. $t$ has x as a free variable. It's supposed to be the fiber of $t$ over $b$.
Max New
CC BY-SA 3.0
2018-02-28T21:33:37.427Z
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.
Ulrik Buchholtz
CC BY-SA 4.0
2021-05-17T01:34:12.143Z
FWIW there are comprehension categories which models pi types differently (comparing to LCCC)
ice1000
<type-theory><ct.category-theory><dependent-type>
Using Dependent Type Theory for Categories that are not LCCC
Max New
# Using Dependent Type Theory for Categories that are not LCCC

(Asked by: username_0 on 2018-02-23)

I have recently been working with polynomial functors and monads based mostly on [Gambino-Kock](https://arxiv.org/abs/0906.4931). 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](https://arxiv.org/abs/1106.1983) 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.

**Tags:** type-theory, ct.category-theory, dependent-type

> **Comments:**
> **username_1**: Do you mean $x = b$, rather than $t = b$?  
> **username_0**: No, I think it's right. $t$ has x as a free variable. It's supposed to be the fiber of $t$ over $b$.  
> **username_2**: 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.  
> **username_3**: FWIW there are comprehension categories which models pi types differently (comparing to LCCC)  

---

## 0 answers

