Discussion of Homotopy Type Theory and Univalent Foundations
 help / Atom feed
From: Cory Knapp <cory.m.knapp@gmail.com>
Cc: Homotopy Type Theory <HomotopyTypeTheory@googlegroups.com>
Subject: Re: [HoTT] my first 3 questions about HoTT
Date: Thu, 20 Jun 2019 17:37:33 +0100
Message-ID: <CADzYOhd-tHN0XO_c+-rW_JSU1=Q6CmGE3L8aSHCEW32oX+KttA@mail.gmail.com> (raw)
In-Reply-To: <d62ccb9e-10d7-4884-bb09-aa1cce32bcb2@googlegroups.com>

[-- Attachment #1: Type: text/plain, Size: 4860 bytes --]

Hi Nathan,

I'm a bit rusty and don't want to say potentially misleading things on a
public forum, so I'm messaging offlist. Hopefully someone else gives more
thorough answers:

1. ETT provides little (if any) technical value over set theory, at the
cost of more bureaucracy, so it's main draw is the philosophical
underpinnings. Since it also seems to conflict with computational
intuitions, it alienates not only the classical mathematician, but also the
computer scientist--this leaves a small audience.

2. I believe you are correct

3. Without *any* type universes, you only get the types of System T---So
you get a system that corresponds to higher-typed Heyting arithmetic. So we
need at least one universe. The HoTT book doesn't *really* use the natural
numbers, only successor and a (binary) least upper bound operator. I guess
this corresponds roughly to Robinson's Arithmetic?

Best,
Cory

On Thu, Jun 20, 2019 at 5:16 PM Nathan Carter <nathancarter5@gmail.com>
wrote:

>
> 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
> <https://groups.google.com/d/msgid/HomotopyTypeTheory/d62ccb9e-10d7-4884-bb09-aa1cce32bcb2%40googlegroups.com?utm_medium=email&utm_source=footer>
> .
> For more options, visit https://groups.google.com/d/optout.
>

-- 
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/CADzYOhd-tHN0XO_c%2B-rW_JSU1%3DQ6CmGE3L8aSHCEW32oX%2BKttA%40mail.gmail.com.
For more options, visit https://groups.google.com/d/optout.

[-- Attachment #2: Type: text/html, Size: 5953 bytes --]

  reply index

Thread overview: 7+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2019-06-20 16:16 Nathan Carter
2019-06-20 16:37 ` Cory Knapp [this message]
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

Reply instructions:

You may reply publically to this message via plain-text email
using any one of the following methods:

* Save the following mbox file, import it into your mail client,
  and reply-to-all from there: mbox

  Avoid top-posting and favor interleaved quoting:
  https://en.wikipedia.org/wiki/Posting_style#Interleaved_style

* Reply using the --to, --cc, and --in-reply-to
  switches of git-send-email(1):

  git send-email \
    --in-reply-to='CADzYOhd-tHN0XO_c+-rW_JSU1=Q6CmGE3L8aSHCEW32oX+KttA@mail.gmail.com' \
    --to=cory.m.knapp@gmail.com \
    --cc=HomotopyTypeTheory@googlegroups.com \
    /path/to/YOUR_REPLY

  https://kernel.org/pub/software/scm/git/docs/git-send-email.html

* If your mail client supports setting the In-Reply-To header
  via mailto: links, try the mailto: link

Discussion of Homotopy Type Theory and Univalent Foundations

Archives are clonable: git clone --mirror http://inbox.vuxu.org/hott

Newsgroup available over NNTP:
	nntp://inbox.vuxu.org/vuxu.archive.hott


AGPL code for this site: git clone https://public-inbox.org/ public-inbox