Discussion of Homotopy Type Theory and Univalent Foundations
 help / color / mirror / Atom feed
* [HoTT] my first 3 questions about HoTT
@ 2019-06-20 16:16 Nathan Carter
  2019-06-20 16:37 ` Cory Knapp
                   ` (2 more replies)
  0 siblings, 3 replies; 7+ messages in thread
From: Nathan Carter @ 2019-06-20 16:16 UTC (permalink / raw)
  To: Homotopy Type Theory

[-- Attachment #1.1: Type: text/plain, Size: 3184 bytes --]

Hello, HoTT community.

I've learned a bit about HoTT in bits of spare time over the past few 
years, and have come up with some questions I can't answer on my own.  It 
was suggested that I ask them on this list.  I will start with a few small 
questions, and if anyone in the community here has time to answer them, 
then I'll continue with others as needed.  Thank you in advance for any 
help you can give.

(Where I'm coming from:  I'm a mathematician; my dissertation was on 
intermediate logics, but I haven't focused on logic much for the past 15 
years, instead doing mathematical software and some applied mathematics.  I 
have a passion for clear exposition, so as I learn about HoTT, I process it 
by writing detailed notes to myself, explaining it as clearly as I can.  
When I can't explain something clearly, I flag it as a question.  I'm 
bringing those questions here.)

Here are three to start.

   1. Very early in the HoTT book, it talks about the difference between 
   types and sets, and says that HoTT encourages us to see sets as spaces.  
   Yet in a set of lecture videos Robert Harper did that I watched on YouTube 
   (which also seem to have disappeared, so I cannot link to them here), he 
   said that Extensional Type Theory takes Intuitionistic Type Theory in a 
   different direction than HoTT does, formalizing the idea that types are 
   sets.  Why does the HoTT book not mention this possibility?  Why does ETT 
   not seem to get as much press as HoTT?
   2. When that same text introduces judgmental equality, it claims that it 
   is a decidable relation.  It does not seem to prove this, and so I 
   suspected that perhaps the evidence was in Appendix A, where things are 
   done more formally (twice, even).  The first of these two formalisms places 
   some restrictions on how one can introduce new judgmental equalities, which 
   seem sufficient to guarantee its decidability, but at no point is an 
   algorithm for deciding it given.  Is the algorithm simply to apply the only 
   applicable rule over and over to reduce each side, and then compare for 
   exact syntactic equality?
   3. One of my favorite things about HoTT as a foundation for mathematics 
   actually comes just from DTT:  Once you've formalized pi types, you can 
   define all of logic and (lots of) mathematics.  But then the hierarchy of 
   type universes seem to require that we understand the natural numbers, 
   which is way more complicated than just pi types, and thus highly 
   disappointing to have to bring in at a foundational level.  Am I right to 
   be disappointed about that or am I missing something?

Thanks in advance for any help you have time and interest to provide!

Nathan Carter

You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/d62ccb9e-10d7-4884-bb09-aa1cce32bcb2%40googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[-- Attachment #1.2: Type: text/html, Size: 3666 bytes --]

^ permalink raw reply	[flat|nested] 7+ messages in thread

end of thread, other threads:[~2019-06-21  1:05 UTC | newest]

Thread overview: 7+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2019-06-20 16:16 [HoTT] my first 3 questions about HoTT Nathan Carter
2019-06-20 16:37 ` Cory Knapp
2019-06-20 16:39 ` Thorsten Altenkirch
2019-06-20 16:56   ` Michael Shulman
2019-06-20 23:11     ` Nathan Carter
2019-06-21  1:04       ` Michael Shulman
2019-06-20 16:48 ` Ali Caglayan

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).