# 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

## Discussion Tag Cloud

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

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

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

• 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

• CommentRowNumber17.
• CommentAuthorspitters
• CommentTimeApr 19th 2019