Add link to ’natural numbers object’ page.

]]>Adding quotient types

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

Steve Vickers

]]>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

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

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

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

]]>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

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

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

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.

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

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

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.

]]>@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.

]]>What is wrong with “type theory internal to topos” ? Too self-explainable and too little of insider slang ?? Proliferation of terminology in $n$Lab 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”.

]]>Fixed the PDF link at geometric type theory.

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