Discussion of Homotopy Type Theory and Univalent Foundations
 help / color / mirror / Atom feed
From: Alexander Kurz <axhkrz@gmail.com>
To: Thorsten Altenkirch <Thorsten.Altenkirch@nottingham.ac.uk>
Cc: Michael Shulman <shulman@sandiego.edu>,
	Matt Oliveri <atmacen@gmail.com>,
	Homotopy Type Theory <homotopytypetheory@googlegroups.com>
Subject: Re: [HoTT] Re: Why do we need judgmental equality?
Date: Mon, 11 Feb 2019 10:45:20 -0800	[thread overview]
Message-ID: <6E2EB19D-DD82-4D32-A5DF-0DF6B914CAB3@gmail.com> (raw)
In-Reply-To: <2CD19190-1CC2-4B74-AAEA-C0DCAB6B1019@exmail.nottingham.ac.uk>

Hi Thorsten,

"When we talk about mathematical objects we think about typed entities"

I agree, but does it follow that types and not objects come first?

For example, 0 can simultaneously be the empty set, a natural number, an integer, a boolean, etc etc

The importance of the "etc etc" is that this list is not fixed in advance. It can change during mathematical course.

This seems to indicate to me that objects come first and types later.

Another example happens when I say that the dual category has the same objects and arrows with domain and codomain reversed. The same object then belongs to different categories. 

Do you think that type theory provides enough flexibility to model this aspect of mathematical discourse conveniently?

All the best,

Alexander

> On 11 Feb 2019, at 10:17, Thorsten Altenkirch <Thorsten.Altenkirch@nottingham.ac.uk> wrote:
> 
> I have got something else against NuPRL. It explains Type Theory via untyped objects which are then typed. In  my view there is no reason why we need to explain typed things via untyped objects. When we talk about mathematical objects we think about typed entities, and the formalism of type theory should reflect this. It is not that we find an untyped object on the street and then try to find out which type it has. We are thinking of a type first and then we construct an element.
> 
> Thorsten
> 
> On 11/02/2019, 17:21, "homotopytypetheory@googlegroups.com on behalf of Michael Shulman" <homotopytypetheory@googlegroups.com on behalf of shulman@sandiego.edu> wrote:
> 
>    FWIW, I think the only thing I have against NuPRL "in principle" is
>    that it seems to be closely tied to one particular model, which is the
>    opposite of what I want my type theories to achieve.  I say "seems"
>    because then someone says something like Jon's "Nuprl's underlying
>    objects are untyped -- but that is not an essential part of the idea",
>    providing an instance of the problem I have with NuPRL "in practice",
>    which is that every time I think I understand it someone proves me
>    wrong.  (-:O
> 
>    Can you explain the difference between "definitional" (whatever that
>    means) and "strict" equality in Andromeda?  Of course there is the
>    technical difference between judgmental equality and the equality
>    type, but that doesn't seem to me to be a "real" difference in the
>    presence of equality reflection, particularly at the purely
>    philosophical level at which a phrase like "equality of sense" has to
>    be interpreted.  As far as I know, even beta-reduction has no
>    privileged status in the Andromeda core -- although I suppose
>    alpha-conversion probably does.
> 
> 
>    On Mon, Feb 11, 2019 at 7:09 AM Matt Oliveri <atmacen@gmail.com> wrote:
>> 
>> It looks like Jon is with you regarding definitional/substitutive equality, since he considers Nuprl's subtitutive equality to be alpha conversion. From the old discussion about it, I had figured Nuprl's substitutive equality was the equality type. I guess I'll avoid that term.
>> 
>> So I'll ask a more concrete question. You seem to be more open to Andromeda than Nuprl. It has a difference between definitional equality (in Jon's sense) and the (strict/exact) equality type for approximately the same reason as Nuprl. If the theory you're using is HTS, then there's also path types. So I gather path types are what you want to take as equality of reference. Which is equality of sense?
>> 
>> Regarding the paragraph I said was vague, my complaint really is that I don't know what you're getting at. I recommended strict or exact equality as possible (informal) interpretations. This doesn't mean there needs to be something called "strict equality" in the system definition, for example, it means you recognize a strict equality notion when you see one. I don't know how to recognize the kind of equality you were getting at in that paragraph.
>> 
>> On Monday, February 11, 2019 at 8:04:35 AM UTC-5, Michael Shulman wrote:
>>> 
>>> On Mon, Feb 11, 2019 at 4:17 AM Matt Oliveri <atm...@gmail.com> wrote:
>>>> As a form of extensional type theory without any "built-in" implementation proposal, it seems like HTS has no notion of "proof object" in Jon's sense, which seems to be formal, checkable proofs. It's not that you couldn't come up with one, it just isn't specified. So I don't think HTS has any "definitional equality", in Jon's sense. But it seems like HTS' exact equality was considered substitutive nonetheless. In fact, it seems to me like what Vladimir meant by "substitutional" was that it doesn't cause coercions. Either because it's definitional, or because it's subsumptive (my term, from another message in this thread).
>>>> 
>>>> So I think you're misusing those terms.
>>> 
>>> Well, after many years I still have not managed to figure out how
>>> NuPRLites use words, so it's possible that I misinterpreted what Jon
>>> meant by "proof object".  But if you interpret what I meant in ITT,
>>> where I know what I am talking about, then it makes sense.  In ITT the
>>> relevant sort of "witness of a proof" is just a term, so "not
>>> perturbing the proof object" means the same thing as "not causing
>>> coercions".
>>> 
>>>> You seem to be downplaying the differences between these notions. Why?
>>> 
>>> Maybe things are different in computer science, but in mathematics it
>>> often happens that there are things called "ideas" that are, in fact,
>>> vaguer than anything that can be written down precisely, and can be
>>> realized precisely by a variety of different formal definitions with
>>> different formal properties.  The differences -- even conceptual
>>> differences -- between these definitions are not unimportant or
>>> ignorable, but do not detract from the importance of the idea or our
>>> ability to think about it.  Indeed, the presence of multiple formal
>>> approaches to the idea with different connections to different
>>> subjects make it *more* important and provide us *more* options to
>>> work with it formally.  I am thinking of for instance all the
>>> different constructions of a highly structured category of spectra, or
>>> all the different definitions of (oo,1)-category.
>> 
>> --
>> 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.
>> 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.
>    For more options, visit https://groups.google.com/d/optout.
> 
> 
> 
> 
> 
> This message and any attachment are intended solely for the addressee
> and may contain confidential information. If you have received this
> message in error, please contact the sender and delete the email and
> attachment. 
> 
> Any views or opinions expressed by the author of this email do not
> necessarily reflect the views of the University of Nottingham. Email
> communications with the University of Nottingham may be monitored 
> where permitted by law.
> 
> 
> 
> 
> -- 
> 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.
> 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.
For more options, visit https://groups.google.com/d/optout.

  reply	other threads:[~2019-02-11 18:45 UTC|newest]

Thread overview: 71+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2019-01-30 11:54 [HoTT] " Felix Rech
2019-02-05 23:00 ` [HoTT] " Matt Oliveri
2019-02-06  4:13   ` Anders Mörtberg
2019-02-09 11:55     ` Felix Rech
2019-02-16 15:59     ` Thorsten Altenkirch
2019-02-17  1:25       ` Michael Shulman
2019-02-17  7:56         ` Thorsten Altenkirch
2019-02-17  9:14           ` Matt Oliveri
2019-02-17  9:18           ` Michael Shulman
2019-02-17 10:52             ` Thorsten Altenkirch
2019-02-17 11:35               ` streicher
2019-02-17 11:44                 ` Thorsten Altenkirch
2019-02-17 14:24                   ` Bas Spitters
2019-02-17 19:36                   ` Thomas Streicher
2019-02-17 21:41                     ` Thorsten Altenkirch
2019-02-17 12:08             ` Matt Oliveri
2019-02-17 12:13               ` Matt Oliveri
2019-02-20  0:22               ` Michael Shulman
2019-02-17 14:22           ` [Agda] " Andreas Abel
2019-02-17  9:05         ` Matt Oliveri
2019-02-17 13:29         ` Nicolai Kraus
2019-02-08 21:19 ` Martín Hötzel Escardó
2019-02-08 23:31   ` Valery Isaev
2019-02-09  1:41     ` Nicolai Kraus
2019-02-09  8:04       ` Valery Isaev
2019-02-09  1:58     ` Jon Sterling
2019-02-09  8:16       ` Valery Isaev
2019-02-09  1:30   ` Nicolai Kraus
2019-02-09 11:38   ` Thomas Streicher
2019-02-09 13:29     ` Thorsten Altenkirch
2019-02-09 13:40       ` Théo Winterhalter
2019-02-09 11:57   ` Felix Rech
2019-02-09 12:39     ` Martín Hötzel Escardó
2019-02-11  6:58     ` Matt Oliveri
2019-02-18 17:37   ` Martín Hötzel Escardó
2019-02-18 19:22     ` Licata, Dan
2019-02-18 20:23       ` Martín Hötzel Escardó
2019-02-09 11:53 ` Felix Rech
2019-02-09 14:04   ` Nicolai Kraus
2019-02-09 14:26     ` Gabriel Scherer
2019-02-09 14:44     ` Jon Sterling
2019-02-09 20:34       ` Michael Shulman
2019-02-11 12:17         ` Matt Oliveri
2019-02-11 13:04           ` Michael Shulman
2019-02-11 15:09             ` Matt Oliveri
2019-02-11 17:20               ` Michael Shulman
2019-02-11 18:17                 ` Thorsten Altenkirch
2019-02-11 18:45                   ` Alexander Kurz [this message]
2019-02-11 22:58                     ` Thorsten Altenkirch
2019-02-12  2:09                       ` Jacques Carette
2019-02-12 11:03                   ` Matt Oliveri
2019-02-12 15:36                     ` Thorsten Altenkirch
2019-02-12 15:59                       ` Matt Oliveri
2019-02-11 19:27                 ` Matt Oliveri
2019-02-11 21:49                   ` Michael Shulman
2019-02-12  9:01                     ` Matt Oliveri
2019-02-12 17:54                       ` Michael Shulman
2019-02-13  6:37                         ` Matt Oliveri
2019-02-13 10:01                           ` Ansten Mørch Klev
2019-02-11 20:11                 ` Matt Oliveri
2019-02-11  8:23       ` Matt Oliveri
2019-02-11 13:03         ` Jon Sterling
2019-02-11 13:22           ` Matt Oliveri
2019-02-11 13:37             ` Jon Sterling
2019-02-11  6:51   ` Matt Oliveri
2019-02-09 12:30 ` [HoTT] " Thorsten Altenkirch
2019-02-11  7:01   ` Matt Oliveri
2019-02-11  8:04     ` Valery Isaev
2019-02-11  8:28       ` Matt Oliveri
2019-02-11  8:37         ` Matt Oliveri
2019-02-11  9:32           ` Rafaël Bocquet

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=6E2EB19D-DD82-4D32-A5DF-0DF6B914CAB3@gmail.com \
    --to=axhkrz@gmail.com \
    --cc=Thorsten.Altenkirch@nottingham.ac.uk \
    --cc=atmacen@gmail.com \
    --cc=homotopytypetheory@googlegroups.com \
    --cc=shulman@sandiego.edu \
    /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).