Not signed in (Sign In)

Start a new discussion

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

Discussion Tag Cloud

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
    • CommentTimeSep 26th 2013
    • (edited Sep 26th 2013)

    I came to think that the term geometric type theory for the type theory internal toi sheaf toposes should exists. Thanks to Bas Spitter for pointing out that Steve Vickers had already had the same idea (now linked to at the above entry).

    Also created geometric homotopy type theory in this vein, with some evident comments.

    • CommentRowNumber2.
    • CommentAuthorZhen Lin
    • CommentTimeSep 26th 2013

    Fixed the PDF link at geometric type theory.

    • CommentRowNumber3.
    • CommentAuthorzskoda
    • CommentTimeSep 26th 2013

    What is wrong with “type theory internal to topos” ? Too self-explainable and too little of insider slang ?? Proliferation of terminology in nnLab is the main complaint of most of people whom I personally tried to persuade to join us so far. Terminology is good when there is no obvious short phrase for it. But “geometric type theory” is not much shorter than self-evident “type theory internal to topos”.

    • CommentRowNumber4.
    • CommentAuthorUrs
    • CommentTimeSep 26th 2013

    @Zhen Lin: thanks!

    @Zoran: not in a topos. In a sheaf topos. And “geometric logic” already exists and is used instead of the equivalent to “logic internal to a sheaf topos” for good reason, I think.

    In any case, what I really wanted here is to highlight that “geometric homotopy type” is effectively an already agreed-up good term that nicely helps to make the (important) point that HoTT is not just about “bare” homotopy types.

    • CommentRowNumber5.
    • CommentAuthorzskoda
    • CommentTimeSep 26th 2013
    • (edited Sep 26th 2013)

    here is to highlight that “geometric homotopy type” is effectively an already agreed-up good term

    OK, forget about us normal people who are not encyclopaedias of all possible terms agreed upon in small communities of insider experts. More argot abbreviations the better.

    I am not saying that the terminology is not good. I know about geometric logic. I am just saying it makes the communication barrier between you and the rest of us larger.

    • CommentRowNumber6.
    • CommentAuthorTodd_Trimble
    • CommentTimeSep 26th 2013

    When you say “type theory internal to a sheaf topos”, my first thought is that you mean type theory with extensional equality, since in fact equality is interpreted extensionally in a sheaf 1-topos. Is that what you mean?

    • CommentRowNumber7.
    • CommentAuthorUrs
    • CommentTimeSep 26th 2013
    • (edited Sep 26th 2013)

    @Todd: yes, the extensional dependent type theory, as given by a sheaf topos under the equivalence at relation betwen category theory and type theory. I have expanded a tad in the entry to make this clearer.

    @Zoran: I think this is actually a really good term especially helpful for people without all the technical background, as it is nicely evocative of what it describes.

    • CommentRowNumber8.
    • CommentAuthorMike Shulman
    • CommentTimeSep 26th 2013

    geometric logic does not mean just “logic internal to a sheaf topos”; it refers only to the fragment of that logic which is preserved by geometric morphisms.

    • CommentRowNumber9.
    • CommentAuthorRodMcGuire
    • CommentTimeSep 26th 2013
    • (edited Sep 26th 2013)

    Arrgh, I tried to fix a bad link in geometric theory but it is now bad in a different way. It is also bad in here in nForum. What did I do wrong?

    [[Steve Vickers]], _Geometric logic in computer science_ ([pdf](http://www.cs.bham.ac.uk/~sjv/GLiCS.pdf‎))

    Steve Vickers, Geometric logic in computer science (pdf)

    (the pdf link becomes http://www.cs.bham.ac.uk/~sjv/GLiCS.pdf%E2%80%8E)

    This reference there works fine:

    [[Steve Vickers]], _Locales and toposes as spaces_ ([pdf](http://www.cs.bham.ac.uk/~sjv/LocTopSpaces.pdf))

    Steve Vickers, Locales and toposes as spaces (pdf)

    • CommentRowNumber10.
    • CommentAuthorZhen Lin
    • CommentTimeSep 26th 2013

    There’s an invisible character at the end of the URL (U+200E LEFT TO RIGHT MARK, if you’re interested).

    • CommentRowNumber11.
    • CommentAuthorRodMcGuire
    • CommentTimeSep 26th 2013
    • (edited Oct 1st 2013)

    Thanks. nLab fixed. Deleting and retyping the URL end makes it work, though how that char got there and how to see it is a mystery. Urs seems to have added it in #22 maybe as an artifact of copy and pasting.

    Steve Vickers, Geometric logic in computer science (pdf)

    Edit: I made this bug and some complications a separate issue in the nForum: Make visible or surpress invisible characters

    • CommentRowNumber12.
    • CommentAuthorMike Shulman
    • CommentTimeApr 17th 2018

    Clarified that “geometric type theory” is not yet a precisely specified type theory.

    diff, v6, current

    • CommentRowNumber13.
    • CommentAuthorspitters
    • CommentTimeApr 17th 2018

    Mike, shouldn’t we be a little more positive. Steve shows how many type formers constructions can be defined.

    • CommentRowNumber14.
    • CommentAuthorMike Shulman
    • CommentTimeApr 17th 2018

    If you can say something precise that is more positive, feel free!

    • CommentRowNumber15.
    • CommentAuthorUrs
    • CommentTimeApr 22nd 2018

    Mike, it seems to me that to make better sense both of the original intent of the entry as well as your complaint about it, we could use your recently proposed fine-grained terminology of “n-theories”.

    What I had in mind seems to be what you might call geometric type 0-theory. What you complain about not having been constructed yet might be some higher theory level version of this. I suppose you are talking about geometric type 1-theory not having been fully described yet

  1. Updated with illustrative example and reference to new papers on “arithmetic” type theory.

    Steve Vickers

    diff, v7, current

    • CommentRowNumber17.
    • CommentAuthorspitters
    • CommentTimeApr 19th 2019

    Adding quotient types

    diff, v9, current

    • CommentRowNumber18.
    • CommentAuthorAlexisHazell
    • CommentTime4 days ago

    Add link to ’natural numbers object’ page.

    diff, v10, current

Add your comments
  • Please log in or leave your comment as a "guest post". If commenting as a "guest", please include your name in the message as a courtesy. Note: only certain categories allow guest posts.
  • To produce a hyperlink to an nLab entry, simply put double square brackets around its name, e.g. [[category]]. To use (La)TeX mathematics in your post, make sure Markdown+Itex is selected below and put your mathematics between dollar signs as usual. Only a subset of the usual TeX math commands are accepted: see here for a list.

  • (Help)