Not signed in (Sign In)

Not signed in

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

  • Sign in using OpenID

Site Tag Cloud

(0 2-category 2-category-theory abelian-categories accessible adjoint algebra algebraic algebraic-geometry algebraic-topology analysis applications arithmetic beauty book bundle calculus categories category category-theory chern-simons-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology cohomolohy combinatorics comma complex-geometry computable-mathematics computer-science connection constructive constructive-mathematics cosmology deformation-theory descent differential differential-cohomology differential-geometry dold fibration duality elliptic-cohomology enriched factorization-system fibration forms 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-theory homtopy-type-theory index-theory integration-theory internal-categories k-theory kan lie-algebras lie-theory limit limits linear linear-algebra locale localization logic manifolds mathematics measure measure-theory meta modal-logic model model-category-theory monoidal-category monoidal-category-theory morphism motives motivic-cohomology n-groups newpage nforum nonassociative noncommutative noncommutative-geometry number-theory operator operator-algebra order-theory philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme set set-theory sheaf simplicial space spin-geometry stable-homotopy-theory stack string string-theory subobject supergeometry symplectic-geometry tannaka terminology theory topology topos topos-theory torsor tqft type type-theory

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • CommentRowNumber1.
    • CommentAuthorUrs
    • CommentTimeMay 15th 2012

    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.

    • CommentRowNumber2.
    • CommentAuthorUrs
    • CommentTimeMay 15th 2012
    • (edited May 15th 2012)

    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 (,1)(\infty,1)-categories?

    • CommentRowNumber3.
    • CommentAuthorMike Shulman
    • CommentTimeMay 15th 2012

    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…

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

    • CommentRowNumber5.
    • CommentAuthorUrs
    • CommentTimeMay 16th 2012
    • (edited May 16th 2012)

    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 nnCafé-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 nn-truncated/nn-connected if all fibers are so.”

    • CommentRowNumber6.
    • CommentAuthorMike Shulman
    • CommentTimeMay 16th 2012

    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”.

  2. 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:XYf:X\to Y which is not necessarily a fibration corresponds to a typing judgement x:Xf(x):Yx: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?

    • CommentRowNumber8.
    • CommentAuthorUrs
    • CommentTimeMay 16th 2012

    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 (,1)(\infty,1)-catgegories in general, and one for that of elementary (,1)(\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.

    • CommentRowNumber9.
    • CommentAuthorUrs
    • CommentTimeMay 16th 2012
    • (edited May 16th 2012)

    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)

    • CommentRowNumber10.
    • CommentAuthorUrs
    • CommentTimeMay 16th 2012
    • (edited May 16th 2012)

    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 YY may depend on xx. Your typing judgement is obtained from this by assuming that YY does not in fact depend on XX, hence by assuming that the fibration in question is the projection Y×XXY \times X \to X.

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

    • CommentRowNumber11.
    • CommentAuthorDavid_Corfield
    • CommentTimeMay 16th 2012

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

    • CommentRowNumber12.
    • CommentAuthorUrs
    • CommentTimeMay 16th 2012

    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

    FirstOrderTheoriesHyperdoctrines 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 HyperdoctrinesHyperdoctrines made it work.

    • CommentRowNumber13.
    • CommentAuthorUrs
    • CommentTimeMay 16th 2012

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

    In

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

    • CommentRowNumber14.
    • CommentAuthorMike Shulman
    • CommentTimeMay 16th 2012

    What about this paper?

    • CommentRowNumber15.
    • CommentAuthorMike Shulman
    • CommentTimeMay 16th 2012

    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”.

    • CommentRowNumber16.
    • CommentAuthorMike Shulman
    • CommentTimeMay 16th 2012

    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”?

    • CommentRowNumber17.
    • CommentAuthorUrs
    • CommentTimeMay 16th 2012

    “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.

    • CommentRowNumber18.
    • CommentAuthorUrs
    • CommentTimeMay 16th 2012

    What about this paper?

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

    • CommentRowNumber19.
    • CommentAuthorTobyBartels
    • CommentTimeMay 16th 2012

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

    • CommentRowNumber20.
    • CommentAuthorUrs
    • CommentTimeMay 16th 2012

    Toby: types.

    The article under discussion is this one.

    • CommentRowNumber21.
    • CommentAuthorUrs
    • CommentTimeMay 16th 2012
    • (edited May 16th 2012)

    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 ;-)

    • CommentRowNumber22.
    • CommentAuthorMike Shulman
    • CommentTimeMay 17th 2012

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

    • CommentRowNumber23.
    • CommentAuthorMike Shulman
    • CommentTimeMay 24th 2012

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

    • CommentRowNumber24.
    • CommentAuthorUrs
    • CommentTimeMay 24th 2012

    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.

    • CommentRowNumber25.
    • CommentAuthorMike Shulman
    • CommentTimeMay 24th 2012

    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 LangLang on the page internal logic, construction of the functor SynSyn on the page syntactic category, and discussion of the adjunction/equivalence between them at the merged page.

    • CommentRowNumber26.
    • CommentAuthorUrs
    • CommentTimeMay 25th 2012

    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.

    • CommentRowNumber27.
    • CommentAuthorUrs
    • CommentTimeSep 17th 2013

    Does anyone know if the Clairambault-Dybjer article on “The Biequivalence of Locally Cartesian Closed Categories and Martin-Löf Type Theories” has meanwhile been published in a journal?

    • CommentRowNumber28.
    • CommentAuthorUlrik
    • CommentTimeSep 17th 2013

    From MathSciNet:

    @incollection {MR2830789,
        AUTHOR = {Clairambault, Pierre and Dybjer, Peter},
         TITLE = {The biequivalence of locally {C}artesian closed categories and
                  {M}artin-{L}\"of type theories},
     BOOKTITLE = {Typed lambda calculi and applications},
        SERIES = {Lecture Notes in Comput. Sci.},
        VOLUME = {6690},
         PAGES = {91--106},
     PUBLISHER = {Springer},
       ADDRESS = {Heidelberg},
          YEAR = {2011},
       MRCLASS = {03B15 (18B99)},
      MRNUMBER = {2830789 (2012i:03029)},
           DOI = {10.1007/978-3-642-21691-6_10},
           URL = {http://dx.doi.org/10.1007/978-3-642-21691-6_10},
    }
    
    • CommentRowNumber29.
    • CommentAuthorUrs
    • CommentTimeSep 17th 2013

    Thanks! I have added that to the entry now.

    • CommentRowNumber30.
    • CommentAuthorUrs
    • CommentTimeDec 9th 2013

    At relation between type theory and category theory I made the table entry on linear logic come out right and link to

    (made the pdf appear here)

    Also highlighted this more at star-autonomous category and at linear logic.

    • CommentRowNumber31.
    • CommentAuthorUrs
    • CommentTimeMar 27th 2014

    Added a pointed to Joyal’s recent talk on categorical semantics of HoTT, and also added Mike’s notes that precede this by two years, so in total I added this to the References section at relation between type theory and category theory:


    Details on this higher categorical semantics of homotopy type theory are in

    with lecture notes in

    • Mike Shulman, Categorical models of homotopy type theory, April 13, 2012 (pdf)

    • Andre Joyal, Categorical homotopy type theory, March 17, 2014 (pdf)

    • CommentRowNumber32.
    • CommentAuthorZhen Lin
    • CommentTimeMar 27th 2014

    The Joyal link seems to point to Voevodsky’s slides.

    • CommentRowNumber33.
    • CommentAuthorUrs
    • CommentTimeMar 27th 2014
    • (edited Mar 27th 2014)

    Woops.

    Could somebody fix it for me, as i am just on my phone now.

    The link is: http://ncatlab.org/homotopytypetheory/files/Joyal.pdf

    (Unwise choice of file name, eh.)

    • CommentRowNumber34.
    • CommentAuthorZhen Lin
    • CommentTimeMar 28th 2014

    Fixed.

    • CommentRowNumber35.
    • CommentAuthorUrs
    • CommentTimeMar 28th 2014

    Thanks!

    • CommentRowNumber36.
    • CommentAuthorUrs
    • CommentTimeMar 31st 2014
    • (edited Mar 31st 2014)

    The entry long has a placeholder section On HoTT with Univalence interpreted in infinity-Toposes.

    Is there a precise version of the statement that involves mumbling “weakly Tarski universes”?

    I imagine at that point in the entry it could say the following, but I don’t know what the formal status of the second half of the statement is:

    Homotopy type theory with the univalence axiom added has interpretation in locally presentable and locally Cartesian closed \infty-categories which also satisfy the Giraud-Rezk-Lurie axioms. This is strictly so for those which have presentation by model structures of simplicial presheaves over elegant Reedy categories (Shulman), and is true generally if the univalent universes are interpreted “weakly a la Tarski”.

    • CommentRowNumber37.
    • CommentAuthorMike Shulman
    • CommentTimeMar 31st 2014

    I wrote a bit leading up to a more formal meaning of the statement in quotes at universe (homotopytypetheory).

    • CommentRowNumber38.
    • CommentAuthorUrs
    • CommentTimeApr 1st 2014
    • (edited Apr 1st 2014)

    Thanks for that.

    I have adapted the text that I found at that link to expand the nnLab entry type of types. There is now a section "Formalization" with essentially your text (enriched by some more hyperlinks), and then I have added a brief paragraph Properties – Categorical semantics with pointers to the articles that I am aware of.

    I tried to vaguely indicate that the discussion in Gepner-Kock would fit under the "weakly Tarskian" umbrella. But you may feel wanting to touch the text here and there.

    Then, finally, I have added a corresponding paragraph at relation between TT and CT – Univalent HoTT and Elementary infinity-toposes.

    Again I pointed to the pertinent references (or tried to). The paragraph currently ends with a brief remark on how, therefore, HoTT+UV+HIT is analogous to a homotopy theoretic version of ETCS.

    • CommentRowNumber39.
    • CommentAuthorMike Shulman
    • CommentTimeApr 1st 2014

    It makes me kind of sad to copy text from one wiki to another rather than linking, since then if it gets improved in one place, the improvement won’t be visible in the other place. I also wasn’t sure that it was really reasonable to call a Tarski universe a “type of types” rather than a “type of codes for types”.

    I tried to clarify some statements at “relation” that I thought were misleading or confusing.

    • CommentRowNumber40.
    • CommentAuthorUrs
    • CommentTimeApr 1st 2014
    • (edited Apr 1st 2014)

    Mike,

    regarding the “relations”-entry: thanks for the edits.

    Regarding duplicating material: that is in the end due to your decision, not mine. I am not supposed to edit over at homotopytheory, not to link back to the nLab, and you are duplicating keywords over there which we already have on the nLab. So that makes that wiki be an external resource from the point of view of the nLab.

    If I just linked to your entry over at homotopytypetheory then all the supplementary links that the nLab does offer are not abvailable, I can’t add links etc. That makes just linking to the entry less preferred than adapting its content to the nLab.

    • CommentRowNumber41.
    • CommentAuthorMike Shulman
    • CommentTimeApr 1st 2014

    I never said you weren’t supposed to edit at the HoTT wiki; just that the edits should be in its spirit, which is different from the nLab’s. Linking to the nLab is also fine from there if it’s for a topic that we probably won’t want a page on there, and otherwise one can just make a stub there which links to here, just as we sometimes do here linking to wikipedia.

    I also don’t think I agree that copying content from an external resource into the nLab is always preferable to linking to it. When the external resource is static, that makes some sense (apart from the duplication of effort involved), but when the external resource is liable to change and improve itself, I think it’s better to link. By analogy, I administer a database system for a nonprofit that I volunteer for, and if you want to see only some of the information in a database table, you don’t copy that data into a smaller table, but you make a “stored view” that essentially links to the original data.