Discussion of Homotopy Type Theory and Univalent Foundations
 help / color / mirror / Atom feed
From: Jon Sterling <j...@jonmsterling.com>
To: "\"Joyal, André\"" <"joyal..."@uqam.ca>
Cc: 'Martin Escardo' via Homotopy Type Theory
	<HomotopyT...@googlegroups.com>
Subject: Re: [HoTT] Identity versus equality
Date: Sat, 9 May 2020 23:04:08 -0400	[thread overview]
Message-ID: <BA7FD9AF-9A62-4DB0-8B2E-13DFBFE4B828@jonmsterling.com> (raw)
In-Reply-To: <8C57894C7413F04A98DDF5629FEC90B1652F5693@Pli.gst.uqam.ca>

Dear André,

I don’t want to accidentally say the wrong thing, I think your intuition about the quillen model category is correct. Let me just say that the strict equality of the type theory is interpreted as the mathematical equality of a 1-categorical presentation of an infinity category, for instance mathematical equality of cells in a simplicial set. The “homotopical semantics” of type theory currently always factor through some 1-categorical presentation of an infinity category (some may wish to change this! I welcome it); judgmental equality is at present always “about” the 1-categorical presentation, whereas path equality is intended to only make distinctions that makes sense at the level of the infinity-categorical localization.

I am somewhat familiar with Vladimir’s HTS (Homotopy Type System) — the arrangement is that you have judgmental equality, a “strict equality” type, and a path type. Some types are distinguished as fibrant and others are not — for instance, the fibrant types are closed under path types but not strict equality types. A rule is added to ensure that the judgmental equality coincides with the (inhabitedness of the) strict equality type — this rule is called “equality reflection” by the logicians and type theorists. The rules are arranged to ensure that strict equality implies path equality but not the other way around. This ensured by having a notion of non-fibrant type (rather than having all types be fibrant).

This may sound very confusing, but for intuitions it is helpful to think of what it means in the context of an “intended model” (for instance, Vladimir’s model in simplicial sets). In that case, there is an object that weakly classifies *all* small simplicial sets, and there is also an object that weakly classifies just the Kan-fibrant small simplicial sets. The HTS formalism is then a (very strict) language to capture the general-abstract aspects of this semantic situation.

Vladimir’s HTS can be thought of as extending Martin-L\”of’s Extensional Type Theory with homotopical notions; this is particularly natural from a mathematical point of view, considering that a quillen model category usually has finite limits. Other authors have considered realizations of this idea that are more like extending Martin-L\”of’s Intensional Type Theory + Streicher’s Axiom K with homotopical notions (where Axiom K is something to ensure that there can, up to identity, be only one proof of a given identity); this style is preferred for implementation or computational purposes. The differences between these points of view are more syntactic than semantic — I would call them “subjective” in deference to Thomas.

Best,
Jon





> On May 9, 2020, at 10:19 PM, Joyal, André <joyal...@uqam.ca> wrote:
> 
> Dear Jon,
> 
> You wrote:
> 
> <<The coherence problems involved in formulating everyday notions like simplicial types (what an amazing world we live in to be able to call this everyday!) can be resolved by extending Homotopy Type Theory with a "sub-homotopical" layer, a second equality type that is meant to capture the strict mathematical equality instead of paths.>>
> 
> That is interesting.
> Is the "strict" equality like the equality relation between the maps of a Quillen model structure?
> I am curious to see the description of such a formal system.
> 
> Is it related to Vladimir's theory with 3 levels of equality (which I never understood)?
> 
> Best,
> André
> 
> ________________________________________
> From: homotopyt...@googlegroups.com [homotopyt...@googlegroups.com] on behalf of Jon Sterling [j...@jonmsterling.com]
> Sent: Saturday, May 09, 2020 5:27 PM
> To: 'Martin Escardo' via Homotopy Type Theory
> Subject: Re: [HoTT] Identity versus equality
> 
> Dear André,
> 
> The coherence problems involved in formulating everyday notions like simplicial types (what an amazing world we live in to be able to call this everyday!) can be resolved by extending Homotopy Type Theory with a "sub-homotopical" layer, a second equality type that is meant to capture the strict mathematical equality instead of paths. This is sometimes called Two Level Type Theory. In this case, it is possible to define simplicial types, using the strict equality to sidestep the problem of defining homotopy coherent structures in HoTT.
> 
> There are a number of ways to achieve this, and they have different tradeoffs depending on what your goals are. The space of possible realizations of this idea corresponds to what Thomas has referred to as the "subjectivity" of judgmental equality.
> 
> Best,
> Jon
> 
> 
> On Sat, May 9, 2020, at 4:18 PM, Joyal, André wrote:
>> Dear Thomas,
>> 
>> You wrote
>> 
>> <<In my opinion the currenrly implemented type theories are essentially
>> for proving and not for computing.
>> But if you haven't mechanized PART of equational reasoning it would be
>> much much more painful than it still is.
>> But that is "only" a pragmatic issue.>>
>> 
>> Type  theory has very nice features. I wish they could be preserved and
>> developped further.
>> 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;
>> (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;
>> (5) Let SType be the category of simplical types.
>> (6) Let Map(X,Y) be the simplicial types of maps X--->Y
>> between two simplicial types X and Y.
>> 
>> It is crucial to have (1)
>> For example, a group could be defined to
>> be a simplicial object satisfying the Segal conditions.
>> The classifying space of a group is the colimit of this simplicial object.
>> The category of groups can be defined to be
>> a simplicial objects satisfiying the Rezk conditions (a complete Segal space).
>> 
>> Is there some aspects of type theory that we may give up as a price
>> for solving these problems ?
>> 
>> 
>> Best,
>> André
>> 
>> ________________________________________
>> From: Thomas Streicher [stre...@mathematik.tu-darmstadt.de]
>> Sent: Saturday, May 09, 2020 2:43 PM
>> To: Joyal, André
>> Cc: David Roberts; Thorsten Altenkirch; Michael Shulman; Steve Awodey;
>> homotopyt...@googlegroups.com
>> Subject: Re: [HoTT] Identity versus equality
>> 
>> Dear Andr'e,
>> 
>>> By the way, if type theory is not very effective in practice, why do we insist that it should always compute?
>>> The dream of a formal system in which every proof leads to an actual computation may be far off.
>>> Not that we should abandon it, new discoveries are always possible.
>>> Is there a version of type theory for proving and verifying, less
>>> for computing?
>> 
>> In my opinion the currenrly implemented type theories are essentially
>> for proving and not for computing.
>> But if you haven't mechanized PART of equational reasoning it would be
>> much much more painful than it still is.
>> But that is "only" a pragmatic issue.
>> 
>>> The notations of type theory are very useful in homotopy theory.
>>> But the absence of simplicial types is a serious obstacle to applications.
>> 
>> In cubical type theory they sort of live well with cubes not being
>> fibrant... They have them as pretypes. But maybe I misunderstand...
>> 
>> Thomas
>> 
>> --
>> 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 HomotopyT...@googlegroups.com.
>> To view this discussion on the web visit
>> https://groups.google.com/d/msgid/HomotopyTypeTheory/8C57894C7413F04A98DDF5629FEC90B1652F563A%40Pli.gst.uqam.ca.
>> 
> 
> --
> 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 HomotopyT...@googlegroups.com.
> To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/b1d32ac0-e364-4405-9e48-e0e1e0b37732%40www.fastmail.com.


  reply	other threads:[~2020-05-10  3:04 UTC|newest]

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 [this message]
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
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=BA7FD9AF-9A62-4DB0-8B2E-13DFBFE4B828@jonmsterling.com \
    --to="j..."@jonmsterling.com \
    --cc="HomotopyT..."@googlegroups.com \
    --cc="joyal..."@uqam.ca \
    /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
Be sure your reply has a Subject: header at the top and a blank line before the message body.
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).