Discussion of Homotopy Type Theory and Univalent Foundations
 help / color / mirror / Atom feed
From: Thorsten Altenkirch <Thorsten.Altenkirch@nottingham.ac.uk>
To: "Anders Mörtberg" <andersmortberg@gmail.com>,
	"Homotopy Type Theory" <homotopytypetheory@googlegroups.com>
Subject: Re: [HoTT] Re: Why do we need judgmental equality?
Date: Sat, 16 Feb 2019 15:59:13 +0000	[thread overview]
Message-ID: <D0B540BF-4D8C-4507-AD4F-FF5B6B335D44@nottingham.ac.uk> (raw)
In-Reply-To: <26028d40-d53c-48d0-a889-4b57fdb77e42@googlegroups.com>

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

Hi,

I have already written on this topic but I had some thoughts, actually this is related to my explanation of judgemental equality when teaching type theory.

In Set Theory we have the element relation and equality and both are propositions, so in some sense dynamic. Eg whether a element relation holds may depend on some assumptions you have made and the same goes for equality. In type theory as in statically typed programming languages typing is a judgement, i.e. it is static (Actually I think there is a nice anology of set theory vs type theory = python vs Haskell). The reason is that we only talk about typed objects and as a consequence a phrase in our language refers to an object whose type is known statically. In particular the type doesn’t depend on some assumptions. If I say that x is a natural number then this is not dependent on some other assumptions I have made. Once I have dependent types this static reasoning needs to be extended. If I define n = 3 and I am checking that (1,2,3) is a vector of size n I need to unfold the definition of n. Actually I am already unfolding the definition of Vec anyway. Hence I am introducing a static equality judgement accompanying my static element judgement. Now what exactly are equalities that are known statically. It seems very natural to include beta equalities and the unfolding of recursive definitions. It is less obvious whether we should include eta equalities because we can only do this for some types and not for all. Hence one of the issues with definitional / judgemental equality is that it is not clear what exactly should be included and what not.

With the introduction of HoTT another important aspect of judgemental equality became apparent: it is a universal strict equality. As I have argued it may be a good idea to have a stronger universal strict equality, in particular one which is not a static judgement. However, now we end up with 3 equalities: judgemental, strict and propositional equality (I stick to this term even if propositional equality may not be a proposition). This may make it difficult to convince the non type theorists that type theory is cool. Hence maybe we can only have 2 or 1 equality and reduce judgemental equality to a mere convenience but not a fundamental feature of type theory.

Thorsten



From: <homotopytypetheory@googlegroups.com> on behalf of Anders Mörtberg <andersmortberg@gmail.com>
Date: Wednesday, 6 February 2019 at 04:13
To: Homotopy Type Theory <homotopytypetheory@googlegroups.com>
Subject: [HoTT] Re: Why do we need judgmental equality?

Note that judgmental equality is not only a convenience, but it also affects what is provable in your type theory. Consider the interval HIT, it is contractible and hence equivalent to Unit. But it also lets you prove function extensionallity which you definitely don't get from the Unit type.

--
Anders

On Tuesday, February 5, 2019 at 6:00:24 PM UTC-5, Matt Oliveri wrote:
The type checking rules are nonlinear (reuses metavariables). For example, for function application, the type of the argument needs to "equal" the domain of the function. What equality is that? It gets called judgmental equality. It's there in some sense even if it's just syntactic equality. But it seems really really hard to have judgmental equality be just syntactic equality, in a dependent type system. It would also be unnatural, from a computational perspective; the judgmental equations are saying something about the computational behavior of the system.

On Wednesday, January 30, 2019 at 6:54:07 AM UTC-5, Felix Rech wrote:
In section 1.1 of the HoTT book it says "In type theory there is also a need for an equality judgment." Currently it seems to me like one could, in principle, replace substitution along judgmental equality with explicit transports if one added a few sensible rules to the type theory. Is there a fundamental reason why the equality judgment is still necessary?

Thanks,
Felix Rech
--
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<mailto: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.

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

  parent reply	other threads:[~2019-02-16 15:59 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 [this message]
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
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=D0B540BF-4D8C-4507-AD4F-FF5B6B335D44@nottingham.ac.uk \
    --to=thorsten.altenkirch@nottingham.ac.uk \
    --cc=andersmortberg@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
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).