Discussion of Homotopy Type Theory and Univalent Foundations
 help / color / Atom feed
From: Ulrik Buchholtz <ulrikbu...@gmail.com>
To: Homotopy Type Theory <HomotopyT...@googlegroups.com>
Subject: Re: [HoTT] Identity versus equality
Date: Sun, 10 May 2020 05:53:21 -0700 (PDT)
Message-ID: <e47e6263-d0eb-4882-ab07-e31483095bd4@googlegroups.com> (raw)
In-Reply-To: <8C57894C7413F04A98DDF5629FEC90B1652F563A@Pli.gst.uqam.ca>

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

Dear André,

On Saturday, May 9, 2020 at 10:18:11 PM UTC+2, joyal wrote:

> But I find it frustrating that I cant do my everyday mathematics with it.
>
> For example, I cannot  say 
>
> (1) Let X:\Delta^{op}---->Type be a simplicial type;
>

Let me remind everyone that we don't have a proof that it's impossible to 
define simplicial types in book HoTT! As long as we haven't settled this 
question either way, the predicament we're in (and I agree it's a 
predicament) is more an indictment of type theorists than of type theory. 
(And I include myself as a type theorist here.)

Anyway, from your phrasing of (1), it looks like you're after a directed 
type theory. Several groups are working on type theories where your (1) is 
valid syntax, but you have to write Space (or Anima or ...) to indicate the 
covariant universe of homotopy types and maps, rather than the full 
universe.

(2) Let G be a type equipped with a group structure; 
>
(3) Let BG be the classifying space of a group G;
> (4) Let Gr be the category of groups;
>

Again, let me remind everyone, that groups are precisely one of the few 
structures we know how to handle (along with grouplike E_n-types, and 
connective/general spectra): To equip a type G with a group structure is to 
give a pointed connected type BG and an equivalence of G with the loop type 
of BG. The type of objects of Gr is the universe of pointed, connected 
types.

When you replace groups by monoids, it gets more embarrassing.

Earlier (on May 7) you wrote:

> At some level, all mathematics is based on some kind of set theory.
> Is it not obvious?
> We cannot escape Cantor's paradise!
>

That is exactly the question, isn't it?

What HoTT/UF offers us is another axis of foundational variation, besides 
the old classical/constructive, impredicative/predicative, 
infinitist/finitist, namely: everything is based on sets/general homotopy 
types are not reducible to sets.

I don't know of catchy names for these positions, but I think that working 
with HoTT has a tendency of making the latter position more plausible: Why 
should there for any type be a set that surjects onto it?

A question: Recall that if we assume the axiom of choice (AC) for sets, 
then there is a surjection from a set onto Set, namely the map that takes a 
cardinal (or ordinal) to the set of ordinals below it.
Is there (with AC for sets) also a surjection from a set to the type of 
1-types? To the full universe?

The 2-level type theories can be viewed as another way of making a type 
theory that is faithful to the idea that everything is based on sets. I 
like to think of the outer layer as an exoskeleton for type theory, giving 
it a bit of extra strength while we don't know how to use its own powers 
fully, or whether indeed it is strong enough to effect constructions like 
that of simplicial types. Every type (which for me is a fibrant type, since 
that's the mathematically meaningful ones) has a corresponding exotype 
(indeed an exoset), but there are more exotypes, such as the exonatural 
numbers, which are sometimes useful.

Best wishes,
Ulrik


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

  parent reply index

Thread overview: 61+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2020-05-05  8:47 Ansten Mørch Klev
2020-05-06 16:02 ` [HoTT] " Joyal, André
2020-05-06 19:01   ` Steve Awodey
2020-05-06 19:18     ` Michael Shulman
2020-05-06 19:31       ` Steve Awodey
2020-05-06 20:30         ` Joyal, André
2020-05-06 22:52         ` Thorsten Altenkirch
2020-05-06 22:54       ` Thorsten Altenkirch
2020-05-06 23:29         ` Joyal, André
2020-05-07  6:11           ` Egbert Rijke
2020-05-07  6:58           ` Thorsten Altenkirch
2020-05-07  9:04             ` Ansten Mørch Klev
2020-05-07 10:09             ` Thomas Streicher
2020-05-07 16:13               ` Joyal, André
2020-05-07 21:41                 ` David Roberts
2020-05-07 23:43                   ` Joyal, André
2020-05-07 23:56                     ` David Roberts
2020-05-08  6:40                       ` Thomas Streicher
2020-05-08 21:06                         ` Joyal, André
2020-05-08 23:44                           ` Steve Awodey
2020-05-09  2:46                             ` Joyal, André
2020-05-09  3:09                               ` Jon Sterling
     [not found]                             ` <CADZEZBY+3z6nrRwsx9p-HqYuTxAnwMUHv7JasHy8aoy1oaGPcw@mail.gmail.com>
2020-05-09  2:50                               ` Steve Awodey
2020-05-09  8:28                           ` Thomas Streicher
2020-05-09 15:53                             ` Joyal, André
2020-05-09 18:43                               ` Thomas Streicher
2020-05-09 20:18                                 ` Joyal, André
2020-05-09 21:27                                   ` Jon Sterling
2020-05-10  2:19                                     ` Joyal, André
2020-05-10  3:04                                       ` Jon Sterling
2020-05-10  9:09                                         ` Thomas Streicher
2020-05-10 11:59                                           ` Thorsten Altenkirch
2020-05-10 11:46                                     ` Thorsten Altenkirch
2020-05-10 14:01                                       ` Michael Shulman
2020-05-10 14:20                                         ` Nicolai Kraus
2020-05-10 14:34                                           ` Michael Shulman
2020-05-10 14:52                                             ` Nicolai Kraus
2020-05-10 15:16                                               ` Michael Shulman
2020-05-10 15:23                                                 ` Nicolai Kraus
2020-05-10 16:13                                                   ` Nicolai Kraus
2020-05-10 16:28                                                     ` Michael Shulman
2020-05-10 18:18                                                       ` Nicolai Kraus
2020-05-10 19:15                                             ` Thorsten Altenkirch
2020-05-10 19:20                                         ` Thorsten Altenkirch
2020-05-10 12:53                                   ` Ulrik Buchholtz [this message]
2020-05-10 14:01                                     ` Michael Shulman
2020-05-10 14:27                                       ` Nicolai Kraus
2020-05-10 15:35                                         ` Ulrik Buchholtz
2020-05-10 16:30                                           ` Michael Shulman
2020-05-10 18:56                                           ` Nicolai Kraus
2020-05-10 18:04                                     ` Joyal, André
2020-05-11  7:33                                       ` Thomas Streicher
2020-05-11 14:54                                         ` Joyal, André
2020-05-11 16:37                                           ` stre...
2020-05-11 16:42                                             ` Michael Shulman
2020-05-11 17:27                                               ` Thomas Streicher
2020-05-10 16:51                                   ` Nicolai Kraus
2020-05-10 18:57                                     ` Michael Shulman
2020-05-10 19:18                                     ` Nicolai Kraus
2020-05-10 20:22                                       ` Michael Shulman
2020-05-10 22:08                                         ` Joyal, André

Reply instructions:

You may reply publicly 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=e47e6263-d0eb-4882-ab07-e31483095bd4@googlegroups.com \
    --to="ulrikbu..."@gmail.com \
    --cc="HomotopyT..."@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

Example config snippet for mirrors

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


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