Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
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.
Fixed the PDF link at geometric type theory.
What is wrong with “type theory internal to topos” ? Too self-explainable and too little of insider slang ?? Proliferation of terminology in 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”.
@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.
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.
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?
@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.
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.
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)
There’s an invisible character at the end of the URL (U+200E LEFT TO RIGHT MARK, if you’re interested).
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
Mike, shouldn’t we be a little more positive. Steve shows how many type formers constructions can be defined.
If you can say something precise that is more positive, feel free!
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 to 18 of 18