Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

• Username
• Password
• Remember me

• Sign in using OpenID
• Remember me

• Forgot your password?
• Apply for membership

(0 1)-category-theory 2-category 2-category-theory 2-monad abelian-categories accessible adjoint algebra algebraic algebraic-geometry analysis arithmetic beauty book bug bundle categories category category-theory chern-simons-theory cohesion cohesive-homotopy-type-theory cohomology combinatorics complex-geometry conference connection constructive constructive-mathematics cosmology database deformation-theory descent differential differential-cohomology differential-geometry duality enriched enriched-category-theory enrichment examples factorization-system fiber fibration forms foundation foundations functional-analysis functor galois-theory gauge-theory gebra general topology geometric geometric-quantization geometry gravity group-theory higher higher-algebra higher-category-theory higher-geometry higher-lie-theory higher-topos-theory history homological homological-algebra homotopy homotopy-theory homotopy-type-theory homtopy-type-theory infinity-groupoid integration-theory internal-categories kan lie lie-algebras lie-theory limit limits linear linear-algebra locale localization localization-theory logic manifolds mathematics measure measure-theory mechanics meta modal-logic model model-category-theory monoidal monoidal-category monoidal-category-theory morphism n-groups newpage noncommutative noncommutative-geometry object operator operator-algebra order-theory philosophy physics predicative pretopology pro-object probability-theory quantum quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry set set-theory sheaf simplicial site space stable-homotopy-theory stack string string-theory subobject supergeometry symplectic-geometry tannaka tensor terminology theory topologica-quantum-field-theory topology topos topos-theory torsor tqft type type-theory universal weighted-limit

1. • CommentRowNumber1.
   • CommentAuthorUrs
   • CommentTimeMay 15th 2012
   • PermaLink
   Author: Urs
   Format: MarkdownItexnow I have finally the time to come back to this, as announced, and so I am now starting an entry: _[[relation between type theory and category theory]]_ . So far there is just some literature collected. I now plan to extract the essence of Seely's artice into the entry in some technical detail.

   now I have finally the time to come back to this, as announced, and so I am now starting an entry:

   relation between type theory and category theory .

   So far there is just some literature collected. I now plan to extract the essence of Seely’s artice into the entry in some technical detail.

2. • CommentRowNumber2.
   • CommentAuthorUrs
   • CommentTimeMay 15th 2012
   • (edited May 15th 2012)
   • PermaLink
   Author: Urs
   Format: MarkdownItexit won't come as a surprise to you that I am [creating a table](http://ncatlab.org/nlab/show/relation+between+type+theory+and+category+theory#Overview). Currently it looks like this: | flavor of type theory | $\;$equivalent to$\;$ | flavor of category theory | | |--|--|--|--| |[[first-order logic]] | | [[hyperdoctrine]] | ([Seely 1984a](#SeelyA)) | |[[dependent type theory]]| | [[locally cartesian closed category]] | ([Seely 1984b](#Seely)) | |[[intensional type theory]] with [[identity types]] | | [[locally cartesian closed (∞,1)-category]] | (conjectural) | |[[homotopy type theory]] with [[higher inductive types]] | | [[elementary (∞,1)-topos]] | (conjectural) | But that made me wonder: what's the best terminology for the entries on the left? What should be the canonical term for that part of homotopy type theory which does _not_ assume univalence and hence is supposedly the language of locally cartesian closed $(\infty,1)$-categories?

   it won’t come as a surprise to you that I am creating a table.

   Currently it looks like this:

   flavor of type theory	$$equivalent to$$	flavor of category theory
   first-order logic		hyperdoctrine	(Seely 1984a)
   dependent type theory		locally cartesian closed category	(Seely 1984b)
   intensional type theory with identity types		locally cartesian closed (∞,1)-category	(conjectural)
   homotopy type theory with higher inductive types		elementary (∞,1)-topos	(conjectural)

   But that made me wonder: what’s the best terminology for the entries on the left? What should be the canonical term for that part of homotopy type theory which does not assume univalence and hence is supposedly the language of locally cartesian closed $(\mathrm{\infty }\mathrm{,1})$-categories?

3. • CommentRowNumber3.
   • CommentAuthorMike Shulman
   • CommentTimeMay 15th 2012
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexI dunno. Just "homotopy type theory" maybe? I think there's also an equivalence between some kind of type theory and elementary 1-toposes somewhere in the literature...

   I dunno. Just “homotopy type theory” maybe?

   I think there’s also an equivalence between some kind of type theory and elementary 1-toposes somewhere in the literature…

4. • CommentRowNumber4.
   • CommentAuthorStephan A Spahn
   • CommentTimeMay 15th 2012
   • PermaLink
   Author: Stephan A Spahn
   Format: MarkdownItexOne could add in the entry that the morphisms in the categories in the left column of the table are what Seely calls ''derivations''.

   One could add in the entry that the morphisms in the categories in the left column of the table are what Seely calls ”derivations”.

5. • CommentRowNumber5.
   • CommentAuthorUrs
   • CommentTimeMay 16th 2012
   • (edited May 16th 2012)
   • PermaLink
   Author: Urs
   Format: MarkdownItexhave been working on [[HoTT methods for homotopy theorists]]. Mainly added a bunch of translation tables, also reorganized a bit. Still far from what it should eventually be, but at least it is beginning to look like an entry. A point to be amplified more, also with respect to the $n$Café-discussion, is how in the internal HoTT language statements about fibers simplify, in that the naive external statements which are generally wrong become true internally: "A morphism is $n$-truncated/$n$-connected if all fibers are so."

   have been working on HoTT methods for homotopy theorists. Mainly added a bunch of translation tables, also reorganized a bit. Still far from what it should eventually be, but at least it is beginning to look like an entry.

   A point to be amplified more, also with respect to the $n$Café-discussion, is how in the internal HoTT language statements about fibers simplify, in that the naive external statements which are generally wrong become true internally: “A morphism is $n$-truncated/$n$-connected if all fibers are so.”

6. • CommentRowNumber6.
   • CommentAuthorMike Shulman
   • CommentTimeMay 16th 2012
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItex> the morphisms in the categories in the left column of the table are what Seely calls ''derivations''. That seems like a weird name to me; I'd be more inclined to call them something like "translations".

   the morphisms in the categories in the left column of the table are what Seely calls ”derivations”.

   That seems like a weird name to me; I’d be more inclined to call them something like “translations”.

7. • CommentRowNumber7.
   • CommentAuthorStephan A Spahn
   • CommentTimeMay 16th 2012
   • PermaLink
   Author: Stephan A Spahn
   Format: MarkdownItex> it won't come as a surprise to you that I am [creating a table](http://ncatlab.org/nlab/show/relation+between+type+theory+and+category+theory#Overview). I like the encyclopedic flavor of your tables! > have been working on [[HoTT methods for homotopy theorists]]. Mainly added a bunch of translation tables, In the basic dictionary table I missed that a morphism $f:X\to Y$ which is not necessarily a fibration corresponds to a typing judgement $x:X\vdash f(x):Y$. Is this omission intended? > I'd be more inclined to call them something like "translations". This sounds fairly descriptive. Can you explain why this is a good name?

   it won’t come as a surprise to you that I am creating a table.

   I like the encyclopedic flavor of your tables!

   have been working on HoTT methods for homotopy theorists. Mainly added a bunch of translation tables,

   In the basic dictionary table I missed that a morphism $f:X\to Y$ which is not necessarily a fibration corresponds to a typing judgement $x:X⊢f(x):Y$. Is this omission intended?

   I’d be more inclined to call them something like “translations”.

   This sounds fairly descriptive. Can you explain why this is a good name?

8. • CommentRowNumber8.
   • CommentAuthorUrs
   • CommentTimeMay 16th 2012
   • PermaLink
   Author: Urs
   Format: MarkdownItexMike writes: > I dunno. Just "homotopy type theory" maybe? It's just that eventually we need two terms, one for the internal language of locally cartesian closed $(\infty,1)$-catgegories in general, and one for that of elementary $(\infty,1)$-toposes. > I think there's also an equivalence between some kind of type theory and elementary 1-toposes somewhere in the literature... Scott and Lambek in their section II have an adjunction between toposes with NNO and type theories with product types and natural numbers. Is that maybe what you have in mind? If not, I'd be very interested in finding the reference that you do have in mind.

   Mike writes:

   I dunno. Just “homotopy type theory” maybe?

   It’s just that eventually we need two terms, one for the internal language of locally cartesian closed $(\mathrm{\infty }\mathrm{,1})$-catgegories in general, and one for that of elementary $(\mathrm{\infty }\mathrm{,1})$-toposes.

   I think there’s also an equivalence between some kind of type theory and elementary 1-toposes somewhere in the literature…

   Scott and Lambek in their section II have an adjunction between toposes with NNO and type theories with product types and natural numbers. Is that maybe what you have in mind? If not, I’d be very interested in finding the reference that you do have in mind.

9. • CommentRowNumber9.
   • CommentAuthorUrs
   • CommentTimeMay 16th 2012
   • (edited May 16th 2012)
   • PermaLink
   Author: Urs
   Format: MarkdownItexConcerning "derivations" and "translations": I think you are maybe talking about different tables each? Seely calls a term of a type a "derivation", because it can be regarded a proof of a proposition. What should be called "translations" are the morphisms in the category of type theories, since they translate one internal language into another)

   Concerning “derivations” and “translations”: I think you are maybe talking about different tables each?

   Seely calls a term of a type a “derivation”, because it can be regarded a proof of a proposition. What should be called “translations” are the morphisms in the category of type theories, since they translate one internal language into another)

10. • CommentRowNumber10.
    • CommentAuthorUrs
    • CommentTimeMay 16th 2012
    • (edited May 16th 2012)
    • PermaLink
    Author: Urs
    Format: MarkdownItexStephan writes: > I like the encyclopedic flavor of your tables! Thanks for letting me know. I am certainly benefitting from making such tables explicit. It helps me organize my thoughts and see clearly. > In the basic dictionary table I missed that a morphism f:X→Y which is not necessarily a fibration corresponds to a typing judgement x:X⊢f(x):Y. Is this omission intended? It's not really omitted, as this is a special case of the clause for a _term_ (forth item in [the table](http://www.ncatlab.org/nlab/show/HoTT+methods+for+homotopy+theorists#BasicDictionary)). There also the type $Y$ may depend on $x$. Your typing judgement is obtained from this by assuming that $Y$ does not in fact depend on $X$, hence by assuming that the fibration in question is the projection $Y \times X \to X$. Maybe I should add a remark about that (as soon as the $n$Lab reacts again).

    Stephan writes:

    I like the encyclopedic flavor of your tables!

    Thanks for letting me know. I am certainly benefitting from making such tables explicit. It helps me organize my thoughts and see clearly.

    In the basic dictionary table I missed that a morphism f:X→Y which is not necessarily a fibration corresponds to a typing judgement x:X⊢f(x):Y. Is this omission intended?

    It’s not really omitted, as this is a special case of the clause for a term (forth item in the table). There also the type $Y$ may depend on $x$. Your typing judgement is obtained from this by assuming that $Y$ does not in fact depend on $X$, hence by assuming that the fibration in question is the projection $Y\times X\to X$.

    Maybe I should add a remark about that (as soon as the $n$Lab reacts again).

11. • CommentRowNumber11.
    • CommentAuthorDavid_Corfield
    • CommentTimeMay 16th 2012
    • PermaLink
    Author: David_Corfield
    Format: MarkdownItexIs the relationship between the hyperdoctrine approach and the syntactic category approach to logic known? We were talking about it [here](http://golem.ph.utexas.edu/category/2011/04/category_theoretic_modal_logic.html#c037350).

    Is the relationship between the hyperdoctrine approach and the syntactic category approach to logic known? We were talking about it here.

12. • CommentRowNumber12.
    • CommentAuthorUrs
    • CommentTimeMay 16th 2012
    • PermaLink
    Author: Urs
    Format: MarkdownItex> We were talking about it [here](http://golem.ph.utexas.edu/category/2011/04/category_theoretic_modal_logic.html#c037350). Hm, interesting that [slide 96](www.lama.univ-savoie.fr/~hirschowitz/talks/cours.pdf#page=96) of Hirschowitz. I guess the devil is in the details somewhere, but Seely seems to have made this kind of adjunction an equivalence $$ FirstOrderTheories \simeq Hyperdoctrines $$ already in 1987 (references at [[relation between type theory and category theory]]). I haven't looked through all the details. One thing that seems noteworthy is that in his proof Seely in fact considers hyperdoctrines whose fibers are not required to be posets. Maybe that makes the difference. But I'd say the equivalence proven justifies whatever fine-tuning on $Hyperdoctrines$ made it work.

    We were talking about it here.

    Hm, interesting that slide 96 of Hirschowitz.

    I guess the devil is in the details somewhere, but Seely seems to have made this kind of adjunction an equivalence

    $$\mathrm{FirstOrderTheories}\simeq \mathrm{Hyperdoctrines}$$

    already in 1987 (references at relation between type theory and category theory).

    I haven’t looked through all the details. One thing that seems noteworthy is that in his proof Seely in fact considers hyperdoctrines whose fibers are not required to be posets. Maybe that makes the difference. But I’d say the equivalence proven justifies whatever fine-tuning on $\mathrm{Hyperdoctrines}$ made it work.

13. • CommentRowNumber13.
    • CommentAuthorUrs
    • CommentTimeMay 16th 2012
    • PermaLink
    Author: Urs
    Format: MarkdownItexHm, Seely's article contains a mistake, in that it is not dealing with the non-uniqueness of pullbacks in the category correctly. In * Hofmann, _[On the interpretation of type theory in locally cartesian closed categories](http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.54.4410)_ there is at least a partial fix. Though I need to figure out if that fix retains the equivalence of categories $DependentTypeTheories \simeq LocallyCartesianClosedCategories$ that Seely claimed.

    Hm, Seely’s article contains a mistake, in that it is not dealing with the non-uniqueness of pullbacks in the category correctly.

    In

    • Hofmann, On the interpretation of type theory in locally cartesian closed categories

    there is at least a partial fix. Though I need to figure out if that fix retains the equivalence of categories $\mathrm{DependentTypeTheories}\simeq \mathrm{LocallyCartesianClosedCategories}$ that Seely claimed.

14. • CommentRowNumber14.
    • CommentAuthorMike Shulman
    • CommentTimeMay 16th 2012
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexWhat about [this paper](http://arxiv.org/abs/1112.3456)?

    What about this paper?

15. • CommentRowNumber15.
    • CommentAuthorMike Shulman
    • CommentTimeMay 16th 2012
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItex> I think you are maybe talking about different tables each? Ah, indeed we were! I misinterpreted Stephan's remark #4. But in that case, I think the morphisms should just be called "terms".

    I think you are maybe talking about different tables each?

    Ah, indeed we were! I misinterpreted Stephan’s remark #4. But in that case, I think the morphisms should just be called “terms”.

16. • CommentRowNumber16.
    • CommentAuthorMike Shulman
    • CommentTimeMay 16th 2012
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItex> It's just that eventually we need two terms, one for the internal language of locally cartesian closed (∞,1)-catgegories in general, and one for that of elementary (∞,1)-toposes. "homotopy type theory" and "univalent (homotopy) type theory"?

    It’s just that eventually we need two terms, one for the internal language of locally cartesian closed (∞,1)-catgegories in general, and one for that of elementary (∞,1)-toposes.

    “homotopy type theory” and “univalent (homotopy) type theory”?

17. • CommentRowNumber17.
    • CommentAuthorUrs
    • CommentTimeMay 16th 2012
    • PermaLink
    Author: Urs
    Format: MarkdownItex> "homotopy type theory" and "univalent (homotopy) type theory"? But what about the higher inductive types? Currently in the entry I have (I think) "homotopy type theory" for the language of LCC $\infty$-categories and "homotopy type theory with higher inductive types and univalence" for the language of elementary $\infty$-toposes.

    “homotopy type theory” and “univalent (homotopy) type theory”?

    But what about the higher inductive types?

    Currently in the entry I have (I think) “homotopy type theory” for the language of LCC $\mathrm{\infty }$-categories and “homotopy type theory with higher inductive types and univalence” for the language of elementary $\mathrm{\infty }$-toposes.

18. • CommentRowNumber18.
    • CommentAuthorUrs
    • CommentTimeMay 16th 2012
    • PermaLink
    Author: Urs
    Format: MarkdownItex> What about [this paper](http://arxiv.org/abs/1112.3456)? Ah, great! Thanks, Mike. And what a coincidence that we posted #13 and #14 in the very same minute! :-)

    What about this paper?

    Ah, great! Thanks, Mike. And what a coincidence that we posted #13 and #14 in the very same minute! :-)

19. • CommentRowNumber19.
    • CommentAuthorTobyBartels
    • CommentTimeMay 16th 2012
    • PermaLink
    Author: TobyBartels
    Format: MarkdownItex@Mike #15: Whether morphisms should be called ‘terms’ depends on whether objects are called ‘types’. Are the objects here types or contexts?

    @Mike #15: Whether morphisms should be called ‘terms’ depends on whether objects are called ‘types’. Are the objects here types or contexts?

20. • CommentRowNumber20.
    • CommentAuthorUrs
    • CommentTimeMay 16th 2012
    • PermaLink
    Author: Urs
    Format: MarkdownItexToby: types. The article under discussion is [this one](http://www.math.mcgill.ca/rags/LCCC/LCCC.pdf).

    Toby: types.

    The article under discussion is this one.

21. • CommentRowNumber21.
    • CommentAuthorUrs
    • CommentTimeMay 16th 2012
    • (edited May 16th 2012)
    • PermaLink
    Author: Urs
    Format: MarkdownItexre 18: I have worked this and related references into [[the relation between type theory and category theory|the entry]]. When I started this quest, I had no idea that what I am after was still not settled by December last year! I thought this is ancient stuff. Interesting to see that it is not only in physics that some statements become so much folk lore that people forget that they haven't proven them yet ;-)

    re 18: I have worked this and related references into the entry.

    When I started this quest, I had no idea that what I am after was still not settled by December last year! I thought this is ancient stuff. Interesting to see that it is not only in physics that some statements become so much folk lore that people forget that they haven’t proven them yet ;-)

22. • CommentRowNumber22.
    • CommentAuthorMike Shulman
    • CommentTimeMay 17th 2012
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexI think we can be flexible with terminology and not demand a concise term for every possible variation on a theme.

    I think we can be flexible with terminology and not demand a concise term for every possible variation on a theme.

23. • CommentRowNumber23.
    • CommentAuthorMike Shulman
    • CommentTimeMay 24th 2012
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexIs it really a good idea to include the detailed constructions of the functors $Con$ and $Lan$ in the particular case of DTT vs LCCCs on the page [[relation between type theory and category theory]]? The construction of $Con$ is already described at (now) [[syntactic category]]; why duplicate it elsewhere? If we want to include the proof that $Con(T)$ is LCCC when $T$ is a DTT, it seems more natural to me to put it at [[syntactic category]] or at [[dependent type theory]]. Similarly for $Lan$.

    Is it really a good idea to include the detailed constructions of the functors $\mathrm{Con}$ and $\mathrm{Lan}$ in the particular case of DTT vs LCCCs on the page relation between type theory and category theory? The construction of $\mathrm{Con}$ is already described at (now) syntactic category; why duplicate it elsewhere? If we want to include the proof that $\mathrm{Con}(T)$ is LCCC when $T$ is a DTT, it seems more natural to me to put it at syntactic category or at dependent type theory. Similarly for $\mathrm{Lan}$.

24. • CommentRowNumber24.
    • CommentAuthorUrs
    • CommentTimeMay 24th 2012
    • PermaLink
    Author: Urs
    Format: MarkdownItexThat sounds reasonable. I didn't finish what had planned to write there anyway. Right now I don't have the time to look into this. But if you have a second to do so, feel free. Otherwise I can try to look into it later.

    That sounds reasonable. I didn’t finish what had planned to write there anyway.

    Right now I don’t have the time to look into this. But if you have a second to do so, feel free. Otherwise I can try to look into it later.

25. • CommentRowNumber25.
    • CommentAuthorMike Shulman
    • CommentTimeMay 24th 2012
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexI think there is a lot of duplication and confusing organization right now. (Nobody's fault, surely, it just happened organically.) The page [[internal logic]] discusses, for first-order theories, exactly the sort of thing that [[categorical semantics]] currently does for dependent type theories. A lot of the same thing is also at the introductory section on categorical semantics at [[type theory]], as well as at [[relation between type theory and category theory]]. I suppose it makes sense to keep an intuitive discussion at [[type theory]] for people who are just stumbling on that page. But maybe the rest of it can be unified and better organized. What about merging [[relation between type theory and category theory]] with [[categorical semantics]]? Maybe a descriptive pagename would be [[categorical semantics of type theory]]. Then we can try to centralize constructions of the functor $Lang$ on the page [[internal logic]], construction of the functor $Syn$ on the page [[syntactic category]], and discussion of the adjunction/equivalence between them at the merged page.

    I think there is a lot of duplication and confusing organization right now. (Nobody’s fault, surely, it just happened organically.) The page internal logic discusses, for first-order theories, exactly the sort of thing that categorical semantics currently does for dependent type theories. A lot of the same thing is also at the introductory section on categorical semantics at type theory, as well as at relation between type theory and category theory.

    I suppose it makes sense to keep an intuitive discussion at type theory for people who are just stumbling on that page. But maybe the rest of it can be unified and better organized. What about merging relation between type theory and category theory with categorical semantics? Maybe a descriptive pagename would be categorical semantics of type theory. Then we can try to centralize constructions of the functor $\mathrm{Lang}$ on the page internal logic, construction of the functor $\mathrm{Syn}$ on the page syntactic category, and discussion of the adjunction/equivalence between them at the merged page.

26. • CommentRowNumber26.
    • CommentAuthorUrs
    • CommentTimeMay 25th 2012
    • PermaLink
    Author: Urs
    Format: MarkdownItexYes, I feel precisely the same way. The current status of the pages is the result of several attempts to start with the same topic, each of them unfinished. I'd certainly have no objections against merging pages.

    Yes, I feel precisely the same way. The current status of the pages is the result of several attempts to start with the same topic, each of them unfinished.

    I’d certainly have no objections against merging pages.