Discussion of Homotopy Type Theory and Univalent Foundations
 help / color / mirror / Atom feed
* [HoTT] Why do we need judgmental equality?
@ 2019-01-30 11:54 Felix Rech
  2019-02-05 23:00 ` [HoTT] " Matt Oliveri
                   ` (3 more replies)
  0 siblings, 4 replies; 71+ messages in thread
From: Felix Rech @ 2019-01-30 11:54 UTC (permalink / raw)
  To: Homotopy Type Theory


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

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.
For more options, visit https://groups.google.com/d/optout.

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

^ permalink raw reply	[flat|nested] 71+ messages in thread

* [HoTT] Re: Why do we need judgmental equality?
  2019-01-30 11:54 [HoTT] Why do we need judgmental equality? Felix Rech
@ 2019-02-05 23:00 ` Matt Oliveri
  2019-02-06  4:13   ` Anders Mörtberg
  2019-02-08 21:19 ` Martín Hötzel Escardó
                   ` (2 subsequent siblings)
  3 siblings, 1 reply; 71+ messages in thread
From: Matt Oliveri @ 2019-02-05 23:00 UTC (permalink / raw)
  To: Homotopy Type Theory


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

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.
For more options, visit https://groups.google.com/d/optout.

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

^ permalink raw reply	[flat|nested] 71+ messages in thread

* [HoTT] Re: Why do we need judgmental equality?
  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
  0 siblings, 2 replies; 71+ messages in thread
From: Anders Mörtberg @ 2019-02-06  4:13 UTC (permalink / raw)
  To: Homotopy Type Theory


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

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.
For more options, visit https://groups.google.com/d/optout.

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

^ permalink raw reply	[flat|nested] 71+ messages in thread

* [HoTT] Re: Why do we need judgmental equality?
  2019-01-30 11:54 [HoTT] Why do we need judgmental equality? Felix Rech
  2019-02-05 23:00 ` [HoTT] " Matt Oliveri
@ 2019-02-08 21:19 ` Martín Hötzel Escardó
  2019-02-08 23:31   ` Valery Isaev
                     ` (4 more replies)
  2019-02-09 11:53 ` Felix Rech
  2019-02-09 12:30 ` [HoTT] " Thorsten Altenkirch
  3 siblings, 5 replies; 71+ messages in thread
From: Martín Hötzel Escardó @ 2019-02-08 21:19 UTC (permalink / raw)
  To: Homotopy Type Theory


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

I would also like to know an answer to this question. It is true that 
dependent type theories have been designed using definitional equality.

But why would anybody say that there is a *need* for that? Is it impossible 
to define a sensible dependent type theory (say for the purpose of serving 
as a foundation for univalent mathematics) that doesn't mention anything 
like definitional equality? If not, why not? And notice that I am not 
talking about *usability* of a proof assistant such as the *existing* ones 
(say Coq, Agda, Lean) were definitional equalities to be removed. I don't 
care if such hypothetical proof assistants would be impossibly difficult to 
use for a dependent type theory lacking definitional equalities (if such a 
thing exists).

The question asked by Felix is a very sensible one: why is it claimed that 
definitional equalities are essential to dependent type theories?

(I do understand that they are used to compute, and so if you are 
interested in constructive mathematics (like I am) then they are useful. 
But, again, in principle we can think of a dependent type theory with no 
definitional equalities and instead an existence property like e.g. in 
Lambek and Scott's "introduction to higher-order categorical logic". And 
like was discussed in a relatively recent message by Thierry Coquand in 
this list,)

Martin 


On Wednesday, 30 January 2019 11:54:07 UTC, 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.
For more options, visit https://groups.google.com/d/optout.

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

^ permalink raw reply	[flat|nested] 71+ messages in thread

* Re: [HoTT] Re: Why do we need judgmental equality?
  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  1:58     ` Jon Sterling
  2019-02-09  1:30   ` Nicolai Kraus
                     ` (3 subsequent siblings)
  4 siblings, 2 replies; 71+ messages in thread
From: Valery Isaev @ 2019-02-08 23:31 UTC (permalink / raw)
  To: Martín Hötzel Escardó; +Cc: Homotopy Type Theory

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

If you are not interested in computations and convenience of your type
theory, then the definitional equality is not essential in the sense that
every type theory T is equivalent to a type theory Q(T) with no
computational rules. Now, what do I mean when I say that type theories T
and Q(T) are equivalent? I won't give here the formal definition, but the
idea is that Q(T) can be interpreted in T and, for every type A of T, there
is a type in Q(T) equivalent to A in T and the same is true for terms. This
implies that every statement (i.e., type) of Q(T) is provable in Q(T) if
and only if it is provable in T and every statement of T has an equivalent
statement in Q(T), so the theories are "logically equivalent". Moreover,
equivalent theories have equivalent (in an appropriate homotopical sense)
categories of models.

Regards,
Valery Isaev


сб, 9 февр. 2019 г. в 00:19, Martín Hötzel Escardó <escardo.martin@gmail.com
>:

> I would also like to know an answer to this question. It is true that
> dependent type theories have been designed using definitional equality.
>
> But why would anybody say that there is a *need* for that? Is it
> impossible to define a sensible dependent type theory (say for the purpose
> of serving as a foundation for univalent mathematics) that doesn't mention
> anything like definitional equality? If not, why not? And notice that I am
> not talking about *usability* of a proof assistant such as the *existing*
> ones (say Coq, Agda, Lean) were definitional equalities to be removed. I
> don't care if such hypothetical proof assistants would be impossibly
> difficult to use for a dependent type theory lacking definitional
> equalities (if such a thing exists).
>
> The question asked by Felix is a very sensible one: why is it claimed that
> definitional equalities are essential to dependent type theories?
>
> (I do understand that they are used to compute, and so if you are
> interested in constructive mathematics (like I am) then they are useful.
> But, again, in principle we can think of a dependent type theory with no
> definitional equalities and instead an existence property like e.g. in
> Lambek and Scott's "introduction to higher-order categorical logic". And
> like was discussed in a relatively recent message by Thierry Coquand in
> this list,)
>
> Martin
>
>
> On Wednesday, 30 January 2019 11:54:07 UTC, 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.
> 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.

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

^ permalink raw reply	[flat|nested] 71+ messages in thread

* Re: [HoTT] Re: Why do we need judgmental equality?
  2019-02-08 21:19 ` Martín Hötzel Escardó
  2019-02-08 23:31   ` Valery Isaev
@ 2019-02-09  1:30   ` Nicolai Kraus
  2019-02-09 11:38   ` Thomas Streicher
                     ` (2 subsequent siblings)
  4 siblings, 0 replies; 71+ messages in thread
From: Nicolai Kraus @ 2019-02-09  1:30 UTC (permalink / raw)
  To: Martín Hötzel Escardó; +Cc: Homotopy Type Theory

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

I agree with everything Martin said below, but I want to go a step further
and argue that judgmental equality is potentially holding us back, in terms
of meta-theoretical results AND usability of the type theory.

I can understand that, for programming, we want built-in computation.
However, for a foundational system, I think we should strive for something
as minimalistic as possible without arbitrary additional features.

It might be a bit controversial to call judgmental equality an "arbitrary
additional feature", but there is certainly some arbitrariness involved
(why else would Sigma have judgmental eta in some systems and not in
others?). It seems to me that the cleanest, most minimalistic, and most
canonical choice would be a type theory without judgmental equalities *at
all*. This would also be much more in line with the approach of category
theory, and I expect that it could make the lives of those of us working
with models easier. Is there a deep theoretical reason for the necessity of
judgmental equality?

Of course, we want convenience and usability. I just fail to see why this
means that judgmental equality has to be a built-in thing (one could say:
why does it have to be part of the core). It's possible that, if we do
*not* insist on built-in judgmental equality, we could even get *more*
convenience. What I mean is this: Let's write WTT for a "weak type theory"
without any judgmental equalities (since we're doing HoTT, maybe with some
axioms such as univalence, but let's not specify this here). Let's say we
know that a certain set A of judgmental equalities does not change WTT,
i.e. that (WTT+A) is a conservative extension of WTT (conservative in a
constructive sense). We could now have a proof assistant which uses WTT as
core but which allows us to "load" the conservativity proof of A. Then, at
the beginning of a module, a user can tell the proof assistant that in this
module, they pretend that the type theory is (WTT+A); i.e. for the user, it
looks as if they are working in (WTT+A) but, in the background, the proof
assistant translates everything to WTT. In another module, the user can
pretend they are working in (WTT+B) instead, if (WTT+B) is conservative
over WTT as well. The idea here is that some proofs benefit more from one
set of judgmental equalities, while other proofs benefit more from others.
Being able to choose which equalities one wants could lead to increased
convenience. (I think WTT+A+B is not necessarily conservative over WTT, so
we cannot just always assume all equalities for maximum convenience.)

For example, let's consider a cubical type theory. I'm aware that we don't
really know many conservativity properties of cubical type theories yet,
but I would be interested in knowing some. Maybe some cubical type theory
gives us a set C which our WTT-based proof assistant can load. In other
words, instead of saying "hey, we have found a new cubical type theory with
amazing computational behaviour, an implementation is on GitHub", people
could say "hey, we have found a new set of judgmental equalities, on GitHub
is the conservativity proof that you can load into your proof assistant to
use it".

I don't think this is something that we will manage to get anytime soon,
and I find it very difficult in general to find conservativity results, but
is there a theoretical reason which makes this impossible?

Nicolai


On Fri, Feb 8, 2019 at 9:19 PM Martín Hötzel Escardó <
escardo.martin@gmail.com> wrote:

> I would also like to know an answer to this question. It is true that
> dependent type theories have been designed using definitional equality.
>
> But why would anybody say that there is a *need* for that? Is it
> impossible to define a sensible dependent type theory (say for the purpose
> of serving as a foundation for univalent mathematics) that doesn't mention
> anything like definitional equality? If not, why not? And notice that I am
> not talking about *usability* of a proof assistant such as the *existing*
> ones (say Coq, Agda, Lean) were definitional equalities to be removed. I
> don't care if such hypothetical proof assistants would be impossibly
> difficult to use for a dependent type theory lacking definitional
> equalities (if such a thing exists).
>
> The question asked by Felix is a very sensible one: why is it claimed that
> definitional equalities are essential to dependent type theories?
>
> (I do understand that they are used to compute, and so if you are
> interested in constructive mathematics (like I am) then they are useful.
> But, again, in principle we can think of a dependent type theory with no
> definitional equalities and instead an existence property like e.g. in
> Lambek and Scott's "introduction to higher-order categorical logic". And
> like was discussed in a relatively recent message by Thierry Coquand in
> this list,)
>
> Martin
>
>
> On Wednesday, 30 January 2019 11:54:07 UTC, 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.
> 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.

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

^ permalink raw reply	[flat|nested] 71+ messages in thread

* Re: [HoTT] Re: Why do we need judgmental equality?
  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
  1 sibling, 1 reply; 71+ messages in thread
From: Nicolai Kraus @ 2019-02-09  1:41 UTC (permalink / raw)
  To: Valery Isaev; +Cc: Homotopy Type Theory

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

Hi Valery,

On Fri, Feb 8, 2019 at 11:32 PM Valery Isaev <valery.isaev@gmail.com> wrote:

> Now, what do I mean when I say that type theories T and Q(T) are
> equivalent? I won't give here the formal definition
>

Would it be correct to say that T is a conservative extension of T, in the
sense of Martin Hofmann's thesis? Your description sounds a bit like this,
or do you have something different in mind?
Nicolai



> , but the idea is that Q(T) can be interpreted in T and, for every type A
> of T, there is a type in Q(T) equivalent to A in T and the same is true for
> terms. This implies that every statement (i.e., type) of Q(T) is provable
> in Q(T) if and only if it is provable in T and every statement of T has an
> equivalent statement in Q(T), so the theories are "logically equivalent".
> Moreover, equivalent theories have equivalent (in an appropriate
> homotopical sense) categories of models.
>
> Regards,
> Valery Isaev
>
>
> сб, 9 февр. 2019 г. в 00:19, Martín Hötzel Escardó <
> escardo.martin@gmail.com>:
>
>> I would also like to know an answer to this question. It is true that
>> dependent type theories have been designed using definitional equality.
>>
>> But why would anybody say that there is a *need* for that? Is it
>> impossible to define a sensible dependent type theory (say for the purpose
>> of serving as a foundation for univalent mathematics) that doesn't mention
>> anything like definitional equality? If not, why not? And notice that I am
>> not talking about *usability* of a proof assistant such as the *existing*
>> ones (say Coq, Agda, Lean) were definitional equalities to be removed. I
>> don't care if such hypothetical proof assistants would be impossibly
>> difficult to use for a dependent type theory lacking definitional
>> equalities (if such a thing exists).
>>
>> The question asked by Felix is a very sensible one: why is it claimed
>> that definitional equalities are essential to dependent type theories?
>>
>> (I do understand that they are used to compute, and so if you are
>> interested in constructive mathematics (like I am) then they are useful.
>> But, again, in principle we can think of a dependent type theory with no
>> definitional equalities and instead an existence property like e.g. in
>> Lambek and Scott's "introduction to higher-order categorical logic". And
>> like was discussed in a relatively recent message by Thierry Coquand in
>> this list,)
>>
>> Martin
>>
>>
>> On Wednesday, 30 January 2019 11:54:07 UTC, 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.
>> 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.
>

-- 
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: 5616 bytes --]

^ permalink raw reply	[flat|nested] 71+ messages in thread

* Re: [HoTT] Re: Why do we need judgmental equality?
  2019-02-08 23:31   ` Valery Isaev
  2019-02-09  1:41     ` Nicolai Kraus
@ 2019-02-09  1:58     ` Jon Sterling
  2019-02-09  8:16       ` Valery Isaev
  1 sibling, 1 reply; 71+ messages in thread
From: Jon Sterling @ 2019-02-09  1:58 UTC (permalink / raw)
  To: 'Martin Escardo' via Homotopy Type Theory

Hi Valery,

I'm trying to square what you said with what Anders said. Consider extending MLTT with an interval in two different ways:

1. With judgmental computation rules for the recursor
2. With propositional computation axioms for the recursor

I do not expect to obtain a conservativity result for the second version over the first version, since the first one derives function extensionality, and the second one does not (afaict).

Can you give a bit more detail about how this algebraic power move that you are describing works, and whether it applies in this case?

Thanks!
Jon

On Fri, Feb 8, 2019, at 6:32 PM, Valery Isaev wrote:
> If you are not interested in computations and convenience of your type 
> theory, then the definitional equality is not essential in the sense 
> that every type theory T is equivalent to a type theory Q(T) with no 
> computational rules. Now, what do I mean when I say that type theories 
> T and Q(T) are equivalent? I won't give here the formal definition, but 
> the idea is that Q(T) can be interpreted in T and, for every type A of 
> T, there is a type in Q(T) equivalent to A in T and the same is true 
> for terms. This implies that every statement (i.e., type) of Q(T) is 
> provable in Q(T) if and only if it is provable in T and every statement 
> of T has an equivalent statement in Q(T), so the theories are 
> "logically equivalent". Moreover, equivalent theories have equivalent 
> (in an appropriate homotopical sense) categories of models.
> 
> Regards,
> Valery Isaev
> 
> 
> сб, 9 февр. 2019 г. в 00:19, Martín Hötzel Escardó <escardo.martin@gmail.com>:
> > I would also like to know an answer to this question. It is true that dependent type theories have been designed using definitional equality.
> > 
> > But why would anybody say that there is a *need* for that? Is it impossible to define a sensible dependent type theory (say for the purpose of serving as a foundation for univalent mathematics) that doesn't mention anything like definitional equality? If not, why not? And notice that I am not talking about *usability* of a proof assistant such as the *existing* ones (say Coq, Agda, Lean) were definitional equalities to be removed. I don't care if such hypothetical proof assistants would be impossibly difficult to use for a dependent type theory lacking definitional equalities (if such a thing exists).
> > 
> > The question asked by Felix is a very sensible one: why is it claimed that definitional equalities are essential to dependent type theories?
> > 
> > (I do understand that they are used to compute, and so if you are interested in constructive mathematics (like I am) then they are useful. But, again, in principle we can think of a dependent type theory with no definitional equalities and instead an existence property like e.g. in Lambek and Scott's "introduction to higher-order categorical logic". And like was discussed in a relatively recent message by Thierry Coquand in this list,)
> > 
> > Martin 
> > 
> > 
> > On Wednesday, 30 January 2019 11:54:07 UTC, 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.
> >  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.
>

-- 
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.

^ permalink raw reply	[flat|nested] 71+ messages in thread

* Re: [HoTT] Re: Why do we need judgmental equality?
  2019-02-09  1:41     ` Nicolai Kraus
@ 2019-02-09  8:04       ` Valery Isaev
  0 siblings, 0 replies; 71+ messages in thread
From: Valery Isaev @ 2019-02-09  8:04 UTC (permalink / raw)
  To: Nicolai Kraus; +Cc: Homotopy Type Theory

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

Hi Nicolai,

The notion of a conservative extension is certainly related to the notion
of an equivalence of type theories that I'm referring to (I call it Morita
equivalence). Hofmann defines various properties of the interpretation |-|
: ITT -> ETT, which are weaker than Morita equivalence in general. The
statement of Theorem 3.2.5 is almost equivalent to the notion of Morita
equivalence. We just need to replace "|P'| = P" with "|P'| and P are
propositionally equivalent" and add the condition that, for every \Gamma
|-_I and every |\Gamma| |-_E A there is a type \Gamma |-_I A' such that
|A'| and A are equivalent in the sense of HoTT (the latter condition
follows from Theorem 3.2.5 for ITT and ETT, but not for general type
theories). Then we get precisely the notion of Morita equivalence between
type theories I and E.

Regards,
Valery Isaev


сб, 9 февр. 2019 г. в 04:41, Nicolai Kraus <nicolai.kraus@gmail.com>:

> Hi Valery,
>
> On Fri, Feb 8, 2019 at 11:32 PM Valery Isaev <valery.isaev@gmail.com>
> wrote:
>
>> Now, what do I mean when I say that type theories T and Q(T) are
>> equivalent? I won't give here the formal definition
>>
>
> Would it be correct to say that T is a conservative extension of T, in the
> sense of Martin Hofmann's thesis? Your description sounds a bit like this,
> or do you have something different in mind?
> Nicolai
>
>
>
>> , but the idea is that Q(T) can be interpreted in T and, for every type A
>> of T, there is a type in Q(T) equivalent to A in T and the same is true for
>> terms. This implies that every statement (i.e., type) of Q(T) is provable
>> in Q(T) if and only if it is provable in T and every statement of T has an
>> equivalent statement in Q(T), so the theories are "logically equivalent".
>> Moreover, equivalent theories have equivalent (in an appropriate
>> homotopical sense) categories of models.
>>
>> Regards,
>> Valery Isaev
>>
>>
>> сб, 9 февр. 2019 г. в 00:19, Martín Hötzel Escardó <
>> escardo.martin@gmail.com>:
>>
>>> I would also like to know an answer to this question. It is true that
>>> dependent type theories have been designed using definitional equality.
>>>
>>> But why would anybody say that there is a *need* for that? Is it
>>> impossible to define a sensible dependent type theory (say for the purpose
>>> of serving as a foundation for univalent mathematics) that doesn't mention
>>> anything like definitional equality? If not, why not? And notice that I am
>>> not talking about *usability* of a proof assistant such as the *existing*
>>> ones (say Coq, Agda, Lean) were definitional equalities to be removed. I
>>> don't care if such hypothetical proof assistants would be impossibly
>>> difficult to use for a dependent type theory lacking definitional
>>> equalities (if such a thing exists).
>>>
>>> The question asked by Felix is a very sensible one: why is it claimed
>>> that definitional equalities are essential to dependent type theories?
>>>
>>> (I do understand that they are used to compute, and so if you are
>>> interested in constructive mathematics (like I am) then they are useful.
>>> But, again, in principle we can think of a dependent type theory with no
>>> definitional equalities and instead an existence property like e.g. in
>>> Lambek and Scott's "introduction to higher-order categorical logic". And
>>> like was discussed in a relatively recent message by Thierry Coquand in
>>> this list,)
>>>
>>> Martin
>>>
>>>
>>> On Wednesday, 30 January 2019 11:54:07 UTC, 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.
>>> 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.
>>
>

-- 
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: 7187 bytes --]

^ permalink raw reply	[flat|nested] 71+ messages in thread

* Re: [HoTT] Re: Why do we need judgmental equality?
  2019-02-09  1:58     ` Jon Sterling
@ 2019-02-09  8:16       ` Valery Isaev
  0 siblings, 0 replies; 71+ messages in thread
From: Valery Isaev @ 2019-02-09  8:16 UTC (permalink / raw)
  To: Jon Sterling; +Cc: 'Martin Escardo' via Homotopy Type Theory

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

Hi Jon,

It is not true that Q(T) can be obtained from T simply by replacing
judgmental equalities with propositional ones (I think this should be true
for some theories, but certainly not for all).

So, if we denote the theory with an interval and judgmental rules by T_I
and the theory with propsoitional axioms by T_a, then Q(T_I) is equivalent
to T_I and Q(T_a) is equivalent to T_a, but Q(T_I) is not equivalent to
T_a. Theories T_a and Q(T_a) are actually equivalent to the ordinary MLTT
(since we simply add another contractible type to it).

Functional extensionality is provable in both T_I and Q(T_I). It follows
from the existence of the interval type in T_I and it can be added as an
axiom to Q(T_I). I believe that theories T_I and Q(T_I) are equivalent to
MLTT + functional extensionality, but I don't know how to prove this yet.

Regards,
Valery Isaev


сб, 9 февр. 2019 г. в 05:01, Jon Sterling <jon@jonmsterling.com>:

> Hi Valery,
>
> I'm trying to square what you said with what Anders said. Consider
> extending MLTT with an interval in two different ways:
>
> 1. With judgmental computation rules for the recursor
> 2. With propositional computation axioms for the recursor
>
> I do not expect to obtain a conservativity result for the second version
> over the first version, since the first one derives function
> extensionality, and the second one does not (afaict).
>
> Can you give a bit more detail about how this algebraic power move that
> you are describing works, and whether it applies in this case?
>
> Thanks!
> Jon
>
> On Fri, Feb 8, 2019, at 6:32 PM, Valery Isaev wrote:
> > If you are not interested in computations and convenience of your type
> > theory, then the definitional equality is not essential in the sense
> > that every type theory T is equivalent to a type theory Q(T) with no
> > computational rules. Now, what do I mean when I say that type theories
> > T and Q(T) are equivalent? I won't give here the formal definition, but
> > the idea is that Q(T) can be interpreted in T and, for every type A of
> > T, there is a type in Q(T) equivalent to A in T and the same is true
> > for terms. This implies that every statement (i.e., type) of Q(T) is
> > provable in Q(T) if and only if it is provable in T and every statement
> > of T has an equivalent statement in Q(T), so the theories are
> > "logically equivalent". Moreover, equivalent theories have equivalent
> > (in an appropriate homotopical sense) categories of models.
> >
> > Regards,
> > Valery Isaev
> >
> >
> > сб, 9 февр. 2019 г. в 00:19, Martín Hötzel Escardó <
> escardo.martin@gmail.com>:
> > > I would also like to know an answer to this question. It is true that
> dependent type theories have been designed using definitional equality.
> > >
> > > But why would anybody say that there is a *need* for that? Is it
> impossible to define a sensible dependent type theory (say for the purpose
> of serving as a foundation for univalent mathematics) that doesn't mention
> anything like definitional equality? If not, why not? And notice that I am
> not talking about *usability* of a proof assistant such as the *existing*
> ones (say Coq, Agda, Lean) were definitional equalities to be removed. I
> don't care if such hypothetical proof assistants would be impossibly
> difficult to use for a dependent type theory lacking definitional
> equalities (if such a thing exists).
> > >
> > > The question asked by Felix is a very sensible one: why is it claimed
> that definitional equalities are essential to dependent type theories?
> > >
> > > (I do understand that they are used to compute, and so if you are
> interested in constructive mathematics (like I am) then they are useful.
> But, again, in principle we can think of a dependent type theory with no
> definitional equalities and instead an existence property like e.g. in
> Lambek and Scott's "introduction to higher-order categorical logic". And
> like was discussed in a relatively recent message by Thierry Coquand in
> this list,)
> > >
> > > Martin
> > >
> > >
> > > On Wednesday, 30 January 2019 11:54:07 UTC, 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.
> > >  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.
> >
>
> --
> 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.

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

^ permalink raw reply	[flat|nested] 71+ messages in thread

* Re: [HoTT] Re: Why do we need judgmental equality?
  2019-02-08 21:19 ` Martín Hötzel Escardó
  2019-02-08 23:31   ` 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 11:57   ` Felix Rech
  2019-02-18 17:37   ` Martín Hötzel Escardó
  4 siblings, 1 reply; 71+ messages in thread
From: Thomas Streicher @ 2019-02-09 11:38 UTC (permalink / raw)
  To: Martín Hötzel Escardó; +Cc: Homotopy Type Theory

Working without any judgemental equality was the aim of the original
LF where elements of a type A correspond to formal derivations of A in
abstract syntax. Also Isabelle works a bit like that.

So with a modicum of judgemental equality one uses dependent types for
having a syntax for formal derivations. But, of course, this is
absolutely useless when you want to execute your proofs!

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 HomotopyTypeTheory+unsubscribe@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

^ permalink raw reply	[flat|nested] 71+ messages in thread

* [HoTT] Re: Why do we need judgmental equality?
  2019-01-30 11:54 [HoTT] Why do we need judgmental equality? Felix Rech
  2019-02-05 23:00 ` [HoTT] " Matt Oliveri
  2019-02-08 21:19 ` Martín Hötzel Escardó
@ 2019-02-09 11:53 ` Felix Rech
  2019-02-09 14:04   ` Nicolai Kraus
  2019-02-11  6:51   ` Matt Oliveri
  2019-02-09 12:30 ` [HoTT] " Thorsten Altenkirch
  3 siblings, 2 replies; 71+ messages in thread
From: Felix Rech @ 2019-02-09 11:53 UTC (permalink / raw)
  To: Homotopy Type Theory


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

Thank you all for the discussion!

One of the motivations for my question was that I actually expect usability 
benefits if one worked in a dependent type theory without judgmental 
equality that has good support by a proof assistant. There are primarily 
two reasons for this:

   1. Judgmental equality cannot be taken as assumptions. If one wants to 
   use judgmental equalities then one has to give concrete definitions that 
   satisfy those equalities and cannot hide the definition details. This makes 
   it impossible to change definitions later on without breaking constructions 
   that depend on them.
   2. In nontrivial definitions, judgmental equalities seem more arbitrary 
   than natural. If we define addition of natural numbers for example then we 
   can choose between x + 0 = x and 0 + x = x as judgmental equality but we 
   cannot have both. This makes it hard to find the right definitions and to 
   predict their behavior.

Another motivation was of course that it would simplify the implementation 
of proof checkers and parts of the metatheory.

I would appreciate any comments on this.

-- 
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 #1.2: Type: text/html, Size: 1664 bytes --]

^ permalink raw reply	[flat|nested] 71+ messages in thread

* [HoTT] Re: Why do we need judgmental equality?
  2019-02-06  4:13   ` Anders Mörtberg
@ 2019-02-09 11:55     ` Felix Rech
  2019-02-16 15:59     ` Thorsten Altenkirch
  1 sibling, 0 replies; 71+ messages in thread
From: Felix Rech @ 2019-02-09 11:55 UTC (permalink / raw)
  To: Homotopy Type Theory


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

On Wednesday, 6 February 2019 05:13:35 UTC+1, Anders Mörtberg wrote:
>
> 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.
>

I have the feeling that function extensionality is special in the sense 
that the proof that I know of, as well as that of function extensionality 
in ETT, relies on the fact that we can replace judgmentally equal terms 
under lambdas, which is like function extensionality for judgmental 
equality. 

-- 
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 #1.2: Type: text/html, Size: 1228 bytes --]

^ permalink raw reply	[flat|nested] 71+ messages in thread

* [HoTT] Re: Why do we need judgmental equality?
  2019-02-08 21:19 ` Martín Hötzel Escardó
                     ` (2 preceding siblings ...)
  2019-02-09 11:38   ` Thomas Streicher
@ 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ó
  4 siblings, 2 replies; 71+ messages in thread
From: Felix Rech @ 2019-02-09 11:57 UTC (permalink / raw)
  To: Homotopy Type Theory


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

On Friday, 8 February 2019 22:19:24 UTC+1, Martín Hötzel Escardó wrote:
>
> I do understand that they are used to compute, and so if you are 
> interested in constructive mathematics (like I am) then they are useful.
>

I agree that the ability to compute canonical forms for terms is essential 
but one does not need to integrate computation into the type system to do 
that. At least, one can alway interprete terms of a type theory without an 
equality judgment in a stronger type theory that has judgmental equalities 
and do the computations there. 

-- 
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 #1.2: Type: text/html, Size: 1222 bytes --]

^ permalink raw reply	[flat|nested] 71+ messages in thread

* Re: [HoTT] Why do we need judgmental equality?
  2019-01-30 11:54 [HoTT] Why do we need judgmental equality? Felix Rech
                   ` (2 preceding siblings ...)
  2019-02-09 11:53 ` Felix Rech
@ 2019-02-09 12:30 ` Thorsten Altenkirch
  2019-02-11  7:01   ` Matt Oliveri
  3 siblings, 1 reply; 71+ messages in thread
From: Thorsten Altenkirch @ 2019-02-09 12:30 UTC (permalink / raw)
  To: Felix Rech, Homotopy Type Theory

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

Hi,

what we need is a strict equality on all types. If we would state the laws of type theory just using the equality type we would also need to add coherence laws. Since I would include the laws for substitution (never understood why substitution is different from application) this would include the laws for infinity categories and this would make even basic type theory certainly much more complicated if not unusable. Instead one introduces a 2-level system with strict equality on one level and weak equality on another. For historic and pragmatic reasons this is combined with the computational aspects of type theory which is expressed as judgemental equality. However, there are reasons to separate these concerns, e.g. to work with higher dimensional constructions in type theory such as semi-simplicial types it is helpful to work with hypothetical strict equalities (see our paper (http://www.cs.nott.ac.uk/~psztxa/publ/csl16.pdf).

I do think that the computational behaviour of type theory is important too. However, this can be expressed by demandic a form of computational adequacy, that is for every term there is a strictly equal normal form. It is not necessary that strict equality in general is decidable (indeed different applications of type theory may demand different decision procedures).

Thorsten


From: <homotopytypetheory@googlegroups.com> on behalf of Felix Rech <s9ferech@gmail.com>
Date: Wednesday, 30 January 2019 at 11:55
To: Homotopy Type Theory <homotopytypetheory@googlegroups.com>
Subject: [HoTT] Why do we need judgmental equality?

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: 6179 bytes --]

^ permalink raw reply	[flat|nested] 71+ messages in thread

* [HoTT] Re: Why do we need judgmental equality?
  2019-02-09 11:57   ` Felix Rech
@ 2019-02-09 12:39     ` Martín Hötzel Escardó
  2019-02-11  6:58     ` Matt Oliveri
  1 sibling, 0 replies; 71+ messages in thread
From: Martín Hötzel Escardó @ 2019-02-09 12:39 UTC (permalink / raw)
  To: Homotopy Type Theory


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

On 09/02/2019 11:57, Felix Rech wrote:> On Friday, 8 February 2019 22:19:24 
UTC+1, Martín Hötzel Escardó wrote:
>
>     I do understand that they are used to compute, and so if you are
>     interested in constructive mathematics (like I am) then they are 
useful.
>
>
> I agree that the ability to compute canonical forms for terms is
> essential but one does not need to integrate computation into the type
> system to do that. At least, one can alway interprete terms of a type
> theory without an equality judgment in a stronger type theory that has
> judgmental equalities and do the computations there.

Yes, this is what I meant by the sentence that follows the one quoted
above, which I quote below. Also, you don't need to compute by
reducing equalities. In fact, most functional languages (e.g. Haskell)
when compiled *do not* compute by unfolding definitional equalities.

On 08/02/2019 21:19, Martín Hötzel Escardó wrote:> (I do understand that 
they are used to compute, and so if you are
> interested in constructive mathematics (like I am) then they are useful.
> But, again, in principle we can think of a dependent type theory with no
> definitional equalities and instead an existence property like e.g. in
> Lambek and Scott's "introduction to higher-order categorical logic". And
> like was discussed in a relatively recent message by Thierry Coquand in
> this list,)

Martin


-- 
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 #1.2: Type: text/html, Size: 2261 bytes --]

^ permalink raw reply	[flat|nested] 71+ messages in thread

* Re: [HoTT] Re: Why do we need judgmental equality?
  2019-02-09 11:38   ` Thomas Streicher
@ 2019-02-09 13:29     ` Thorsten Altenkirch
  2019-02-09 13:40       ` Théo Winterhalter
  0 siblings, 1 reply; 71+ messages in thread
From: Thorsten Altenkirch @ 2019-02-09 13:29 UTC (permalink / raw)
  To: Thomas Streicher, Martín Hötzel Escardó
  Cc: Homotopy Type Theory

Even LF included beta eta hence has a non-trivial judgemental equality. Not to mention the equations for substitution.

Thorsten

On 09/02/2019, 11:38, "homotopytypetheory@googlegroups.com on behalf of Thomas Streicher" <homotopytypetheory@googlegroups.com on behalf of streicher@mathematik.tu-darmstadt.de> wrote:

    Working without any judgemental equality was the aim of the original
    LF where elements of a type A correspond to formal derivations of A in
    abstract syntax. Also Isabelle works a bit like that.
    
    So with a modicum of judgemental equality one uses dependent types for
    having a syntax for formal derivations. But, of course, this is
    absolutely useless when you want to execute your proofs!
    
    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 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.

^ permalink raw reply	[flat|nested] 71+ messages in thread

* Re: [HoTT] Re: Why do we need judgmental equality?
  2019-02-09 13:29     ` Thorsten Altenkirch
@ 2019-02-09 13:40       ` Théo Winterhalter
  0 siblings, 0 replies; 71+ messages in thread
From: Théo Winterhalter @ 2019-02-09 13:40 UTC (permalink / raw)
  To: Homotopy Type Theory


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

Hi,

To follow on the idea of 2-level type theory. It indeed seems enough to 
have a strict equality (meaning with UIP and Funext) to pull off an 
interpretation of weakTT.
In fact, I have updated an formalised the work of Nicolas Oury of 
translating Extensional Type Theory into Intensional Type Theory, and 
extended the proof so that it can be an instance of a translation from an 
extensional 2-level type theory into an intensional one. In this work, the 
treatment of conversion in the target seems to be orthogonal to the result 
itself. With Simon Boulier we plan to tweak the formalisation a bit so that 
it allows to target weakTT (and we already conducted informal reasoning to 
justify it). You can thus give an interpretation to a theory into its weak 
version, provided you have UIP, funext and enough equalities to interpret 
for instance β-reduction.

I hope this is clear.

Théo

Le samedi 9 février 2019 14:29:28 UTC+1, Thorsten Altenkirch a écrit :
>
> Even LF included beta eta hence has a non-trivial judgemental equality. 
> Not to mention the equations for substitution. 
>
> Thorsten 
>
> On 09/02/2019, 11:38, "homotopyt...@googlegroups.com <javascript:> on 
> behalf of Thomas Streicher" <homotopyt...@googlegroups.com <javascript:> 
> on behalf of stre...@mathematik.tu-darmstadt.de <javascript:>> wrote: 
>
>     Working without any judgemental equality was the aim of the original 
>     LF where elements of a type A correspond to formal derivations of A in 
>     abstract syntax. Also Isabelle works a bit like that. 
>     
>     So with a modicum of judgemental equality one uses dependent types for 
>     having a syntax for formal derivations. But, of course, this is 
>     absolutely useless when you want to execute your proofs! 
>     
>     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 HomotopyTypeTheory+unsubscribe@googlegroups.com <javascript:>. 
>
>     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 #1.2: Type: text/html, Size: 4530 bytes --]

^ permalink raw reply	[flat|nested] 71+ messages in thread

* Re: [HoTT] Re: Why do we need judgmental equality?
  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-11  6:51   ` Matt Oliveri
  1 sibling, 2 replies; 71+ messages in thread
From: Nicolai Kraus @ 2019-02-09 14:04 UTC (permalink / raw)
  To: Felix Rech; +Cc: Homotopy Type Theory

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

On Sat, Feb 9, 2019 at 11:53 AM Felix Rech <s9ferech@gmail.com> wrote:

> One of the motivations for my question was that I actually expect
> usability benefits if one worked in a dependent type theory without
> judgmental equality that has good support by a proof assistant.
>

Yes, me too (but I think *a lot* of work needs to be done before we can
have a proof assistant based on this idea which provides better usability
than the current ones).
I agree with your points. But I think "x + 0 = x versus 0 + x = x" is an
example where I'd expect that one should be able to produce a
conservativity proof and use both at the same time instead of choosing one.
I think it's not necessary that we restrict ourselves to computation rules
that come from actual definitions; anything that is "constructively
conservative" over a weak theory should be allowed. In Agda, one can have
additional computation rules, but it's not a safe feature.
Nicolai



>    1. Judgmental equality cannot be taken as assumptions. If one wants to
>    use judgmental equalities then one has to give concrete definitions that
>    satisfy those equalities and cannot hide the definition details. This makes
>    it impossible to change definitions later on without breaking constructions
>    that depend on them.
>    2. In nontrivial definitions, judgmental equalities seem more
>    arbitrary than natural. If we define addition of natural numbers for
>    example then we can choose between x + 0 = x and 0 + x = x as judgmental
>    equality but we cannot have both. This makes it hard to find the right
>    definitions and to predict their behavior.
>
> Another motivation was of course that it would simplify the implementation
> of proof checkers and parts of the metatheory.
>
> I would appreciate any comments on this.
>
> --
> 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.

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

^ permalink raw reply	[flat|nested] 71+ messages in thread

* Re: [HoTT] Re: Why do we need judgmental equality?
  2019-02-09 14:04   ` Nicolai Kraus
@ 2019-02-09 14:26     ` Gabriel Scherer
  2019-02-09 14:44     ` Jon Sterling
  1 sibling, 0 replies; 71+ messages in thread
From: Gabriel Scherer @ 2019-02-09 14:26 UTC (permalink / raw)
  To: Nicolai Kraus; +Cc: Felix Rech, Homotopy Type Theory

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

A relevant citation for this line of thinking (if we reduce implicit
computation, can we gain usability some other way?) is the work on the
Zombie programming language, which tried to weaken beta-reduction in a
dependent language (restricting it to values only, as in F*) to obtain a
more automatic form of reasoning upto congruence (definitional equalities
can be put in the context and used from there).

  Programming up to Congruence
  Vilhelm Sjöberg and Stephanie Weirich, 2015
  http://www.cs.yale.edu/homes/vilhelm/papers/popl15congruence.pdf


On Sat, Feb 9, 2019 at 3:05 PM Nicolai Kraus <nicolai.kraus@gmail.com>
wrote:

> On Sat, Feb 9, 2019 at 11:53 AM Felix Rech <s9ferech@gmail.com> wrote:
>
>> One of the motivations for my question was that I actually expect
>> usability benefits if one worked in a dependent type theory without
>> judgmental equality that has good support by a proof assistant.
>>
>
> Yes, me too (but I think *a lot* of work needs to be done before we can
> have a proof assistant based on this idea which provides better usability
> than the current ones).
> I agree with your points. But I think "x + 0 = x versus 0 + x = x" is an
> example where I'd expect that one should be able to produce a
> conservativity proof and use both at the same time instead of choosing one.
> I think it's not necessary that we restrict ourselves to computation rules
> that come from actual definitions; anything that is "constructively
> conservative" over a weak theory should be allowed. In Agda, one can have
> additional computation rules, but it's not a safe feature.
> Nicolai
>
>
>
>>    1. Judgmental equality cannot be taken as assumptions. If one wants
>>    to use judgmental equalities then one has to give concrete definitions that
>>    satisfy those equalities and cannot hide the definition details. This makes
>>    it impossible to change definitions later on without breaking constructions
>>    that depend on them.
>>    2. In nontrivial definitions, judgmental equalities seem more
>>    arbitrary than natural. If we define addition of natural numbers for
>>    example then we can choose between x + 0 = x and 0 + x = x as judgmental
>>    equality but we cannot have both. This makes it hard to find the right
>>    definitions and to predict their behavior.
>>
>> Another motivation was of course that it would simplify the
>> implementation of proof checkers and parts of the metatheory.
>>
>> I would appreciate any comments on this.
>>
>> --
>> 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.
>

-- 
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: 4936 bytes --]

^ permalink raw reply	[flat|nested] 71+ messages in thread

* Re: [HoTT] Re: Why do we need judgmental equality?
  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  8:23       ` Matt Oliveri
  1 sibling, 2 replies; 71+ messages in thread
From: Jon Sterling @ 2019-02-09 14:44 UTC (permalink / raw)
  To: 'Martin Escardo' via Homotopy Type Theory

Hi all,

I think there's two different issues being conflated -- there is the question of whether definitional equalities can be removed, in order to obtain more direct interpretation into weaker models, and then there is the question of whether definitional equalities can be removed as a way to make a proof assistant more modular, exploiting conservativity results locally to add defintional equalities.

The first seems more interesting to me, and is indeed the topic of Curien's famous paper. Many interesting coherence theorems lurk underneath the definitional equalities that we take for granted, and we can only see them if we treat definitional equalities as defeasible.

The issue about proof assistants seems quite different to me -- the approach that seems to be proposed by some of the people in the room, to replace judgmental equality with a good enough equality *type* seems perfectly good for studying algebra and models (for instance, the discipline of QIITs in the presence of [semantically] extensional equality types seems like a good tool for dependently-sorted algebraic theories). But this approach is not likely to yield *proof assistants* that are more usable than existing systems which have replaced definitional equality with propositional equality.

I am referring to Nuprl -- usually Nuprl is characterized as using equality reflection, but this is not totally accurate (though there is a sense in which it is true). When I say "definitional equality" for a formalism, what I mean is that if I have a proof object D of a judgment J, if J is definitionally equal to J', then D is also already a proof of J'. Definitional equality is the silent equality. In most formalisms, definitional equality includes some combination of alpha/beta/eta/xi, but in Nuprl is included ONLY alpha. What I mean is that in a proof object for Nuprl, the biggest relation by which you can "purturb" a judgment without needing to update the proof object is alpha equivalence. Proof objects must NOT be confused with realizers, of course -- just like we do not confuse Coq proofs with the OCaml code that they could be extract to.

So how does Nuprl work? "Real" equality is captured purely using the equality type, and not using any judgment except membership in the equality type (a judgment whose derivations are crucially taken only up to alpha, rather than up to beta/eta/xi). When you want to reason using beta/eta/xi (and the much richer equations that are also available), you use the equality type and its elimination rules directly, essentially in the same way that Thorsten has advocated.

Nuprl is in essence what it looks like to remove all definitional equalities and replace them with internal equalities. The main difference between Nuprl and Thorsten's proposal is that Nuprl's underlying objects are untyped -- but that is not an essential part of the idea.

The reason I bring this up is that the question of whether such an idea can be made usable, namely using a formalism with only alpha equivalence regarded silently/definitionally, and all other equations mediated through the equality type, can be essentially reduced to the question of whether Nuprl is practical and usable, or whether it is possible to implement a version of that idea which is practical and usable.

As many of the people on this list are aware, in the years past I was very bullish on this idea, but now after having implemented two separate proof assistants based on this idea, I am not as optimistic about it as I was (but I don't rule it out). Today, I have changed my methodology and embraced strong definitional equality, in order to achieve my actual goals during the very finite historical period of my PhD -- to build usable proof assistants for formalizing mathematics.

Best,
Jon




On Sat, Feb 9, 2019, at 9:05 AM, Nicolai Kraus wrote:
> On Sat, Feb 9, 2019 at 11:53 AM Felix Rech <s9ferech@gmail.com> wrote:
> > One of the motivations for my question was that I actually expect usability benefits if one worked in a dependent type theory without judgmental equality that has good support by a proof assistant.
> 
> Yes, me too (but I think *a lot* of work needs to be done before we can 
> have a proof assistant based on this idea which provides better 
> usability than the current ones).
> I agree with your points. But I think "x + 0 = x versus 0 + x = x" is 
> an example where I'd expect that one should be able to produce a 
> conservativity proof and use both at the same time instead of choosing 
> one. I think it's not necessary that we restrict ourselves to 
> computation rules that come from actual definitions; anything that is 
> "constructively conservative" over a weak theory should be allowed. In 
> Agda, one can have additional computation rules, but it's not a safe 
> feature.
> Nicolai
> 
> 
> >  1. Judgmental equality cannot be taken as assumptions. If one wants to use judgmental equalities then one has to give concrete definitions that satisfy those equalities and cannot hide the definition details. This makes it impossible to change definitions later on without breaking constructions that depend on them.
> >  2. In nontrivial definitions, judgmental equalities seem more arbitrary than natural. If we define addition of natural numbers for example then we can choose between x + 0 = x and 0 + x = x as judgmental equality but we cannot have both. This makes it hard to find the right definitions and to predict their behavior.
> > Another motivation was of course that it would simplify the implementation of proof checkers and parts of the metatheory.
> > 
> > I would appreciate any comments on this.
> >  
> 
> 
> > -- 
> > 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.
>

-- 
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.

^ permalink raw reply	[flat|nested] 71+ messages in thread

* Re: [HoTT] Re: Why do we need judgmental equality?
  2019-02-09 14:44     ` Jon Sterling
@ 2019-02-09 20:34       ` Michael Shulman
  2019-02-11 12:17         ` Matt Oliveri
  2019-02-11  8:23       ` Matt Oliveri
  1 sibling, 1 reply; 71+ messages in thread
From: Michael Shulman @ 2019-02-09 20:34 UTC (permalink / raw)
  To: HomotopyTypeTheory@googlegroups.com

From a semantic point of view, I agree that judgmental equality is
about convenience and usability.  But that shouldn't be regarded as
making it any less important.  Indeed, the whole *point* of using type
theory as an internal language for a category, rather than simply
reasoning about the category directly, is... convenience and
usability.  Of course there are degrees of convenience, and even type
theory without judgmental equality might be slightly more convenient
than reasoning directly in categorical language.  But I think we need
judgmental equality if we really want to get some substantial benefit
out of type theory as an internal language.  The problem of course is
to bridge the gap between the type theory and the category theory, and
for that purpose intermediate structures may be useful: categories
that are more like type theory (such as tribes and contextual
categories) and type theories that are more like category theory (such
as ones with fewer judgmental equalities).  But I don't think I would
want to regard the intermediate structures as fundamental, rather than
tools to get from one side to another.

From an implementation point of view, I agree that in the long run we
should have proof assistants that don't hardcode a fixed set of
judgmental equalities.  But I don't think that means eliminating all
judgmental equalities; it just means making the logical framework more
flexible, such as Agda's ability to postulate new reductions or
Andromeda's framework with equality reflection.  In particular, the
new equalities that we postulate should still be *substitutive* (as
Jon says, allowing to perturb a judgment without altering the proof
object) rather than *transportive* (requiring the proof object to be
altered) -- I think Vladimir was the one who suggested words like
those.

From a computation point of view, of course some kind of reduction is
necessary, and it makes sense to consider an object to be "equal" in
some sense to the result of computing it.  This would presumably be a
stronger sense than typal equality inside the system, whether or not
it is actually substitutive.  Conversely, in order to implement a
substitutive equality it seems very useful to have some algorithm that
can at least go some part of the way towards deciding it, and
computation is likely to play an important role in such an algorithm.

From a philosophical point of view, I think definitional/substitutive
equality is very important: as Steve Awodey pointed out some time ago,
it represents the intensional "equality of sense" rather than the
extensional "equality of reference".  This explains why it is
substitutive: if two terms have the same sense, there is no
explanation necessary for why a statement about one also applies to
the other, while if they only have the same reference, then some
explanation may be required.  If I say "I saw the morning star this
morning" and you reply "yes, and I saw it last night", it sounds weird
because there is a transport necessary along the equality of reference
"morning star = evening star", in a way that doesn't happen if instead
you reply "yes, and I saw it yesterday morning".  Foundations for
mathematics based on first-order logic, like ZFC, have no ability to
talk about equality of sense; the only equality they know about is
reference.  A type theory without definitional equality would have the
same limitation.

Judgmental, definitional, substitutive, and computational equalities
are not exactly the same thing.  But the fact that there are so many
different but related points of view on similar and overlapping
concepts, and so many different but related uses and applications for
them, suggests to me that there is an important underlying
mathematical concept that should not lightly be discarded.  On the
other hand, the proof of the pudding is in the eating, and this whole
discussion would be much more concrete if we had some actual
references working out what type theory without judgmental equality
looks like, with proofs of whatever properties it may be claimed to
have, and perhaps even an implementation of it; so I don't mean to
discourage anyone from trying to develop such a thing.

-- 
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.

^ permalink raw reply	[flat|nested] 71+ messages in thread

* [HoTT] Re: Why do we need judgmental equality?
  2019-02-09 11:53 ` Felix Rech
  2019-02-09 14:04   ` Nicolai Kraus
@ 2019-02-11  6:51   ` Matt Oliveri
  1 sibling, 0 replies; 71+ messages in thread
From: Matt Oliveri @ 2019-02-11  6:51 UTC (permalink / raw)
  To: Homotopy Type Theory


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

On Saturday, February 9, 2019 at 6:53:15 AM UTC-5, Felix Rech wrote:
>
> Judgmental equality cannot be taken as assumptions. If one wants to use 
> judgmental equalities then one has to give concrete definitions that 
> satisfy those equalities and cannot hide the definition details. This makes 
> it impossible to change definitions later on without breaking constructions 
> that depend on them.
>

I worry that this will indeed be a modularity problem in practice. You 
generally can't specify behavior strictly at the interface between 
subsystems. Semantic purists would point out that such an interface 
wouldn't make sense anyway, unless the subsystem's type is an hset, and you 
use paths. In general, you should specify a bunch of coherences. Aside from 
being way harder though, we don't know how to do it in general, because of 
the infinite object problem.

With a 2-level theory, you could at least have second-class module 
signatures with strict equality.

In nontrivial definitions, judgmental equalities seem more arbitrary than 
> natural. If we define addition of natural numbers for example then we can 
> choose between x + 0 = x and 0 + x = x as judgmental equality but we cannot 
> have both. This makes it hard to find the right definitions and to predict 
> their behavior.
> Another motivation was of course that it would simplify the implementation 
> of proof checkers and parts of the metatheory.
>

This problem is solved by the special case of 2-level theories where strict 
equality is reflective (like extensional type theory (ETT)). What this does 
for you in practice is that you never have to see coercions between e.g. 
types (F (x + 0)) and (F (0 + x)), since they can be proven judgmentally 
equal by induction. (What I mean is that there's no record in terms of 
rewriting with nat equality. Not that all such reasoning can be done 
automatically. (It presumably is easy to automate both plus-zero rewrites 
though.))

Without reflective equality, strict equality doesn't seem to provide any 
benefit over paths in this case, because you need a coercion, and paths 
between nats are already unique.

-- 
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 #1.2: Type: text/html, Size: 2959 bytes --]

^ permalink raw reply	[flat|nested] 71+ messages in thread

* [HoTT] Re: Why do we need judgmental equality?
  2019-02-09 11:57   ` Felix Rech
  2019-02-09 12:39     ` Martín Hötzel Escardó
@ 2019-02-11  6:58     ` Matt Oliveri
  1 sibling, 0 replies; 71+ messages in thread
From: Matt Oliveri @ 2019-02-11  6:58 UTC (permalink / raw)
  To: Homotopy Type Theory


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

If the stronger type theory is not conservative, you generally can't draw 
mathematical conclusions on the basis of those computations, though.

On Saturday, February 9, 2019 at 6:57:51 AM UTC-5, Felix Rech wrote:
>
> On Friday, 8 February 2019 22:19:24 UTC+1, Martín Hötzel Escardó wrote:
>>
>> I do understand that they are used to compute, and so if you are 
>> interested in constructive mathematics (like I am) then they are useful.
>>
>
> I agree that the ability to compute canonical forms for terms is essential 
> but one does not need to integrate computation into the type system to do 
> that. At least, one can alway interprete terms of a type theory without an 
> equality judgment in a stronger type theory that has judgmental equalities 
> and do the computations there.
>

-- 
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 #1.2: Type: text/html, Size: 1587 bytes --]

^ permalink raw reply	[flat|nested] 71+ messages in thread

* Re: [HoTT] Why do we need judgmental equality?
  2019-02-09 12:30 ` [HoTT] " Thorsten Altenkirch
@ 2019-02-11  7:01   ` Matt Oliveri
  2019-02-11  8:04     ` Valery Isaev
  0 siblings, 1 reply; 71+ messages in thread
From: Matt Oliveri @ 2019-02-11  7:01 UTC (permalink / raw)
  To: Homotopy Type Theory


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

I think you're right. From discussions about autophagy, it seems like no 
one knows how to match judgmental equality using equality types, unless 
that equality type family is propositionally truncated in some way.

Consequently, my guess is that Valery's Q transformation actually yields 
something rather like a 2-level system.

On Saturday, February 9, 2019 at 7:30:07 AM UTC-5, Thorsten Altenkirch 
wrote:
>
> Hi,
>
>  
>
> what we need is a strict equality on all types. If we would state the laws 
> of type theory just using the equality type we would also need to add 
> coherence laws. Since I would include the laws for substitution (never 
> understood why substitution is different from application) this would 
> include the laws for infinity categories and this would make even basic 
> type theory certainly much more complicated if not unusable. Instead one 
> introduces a 2-level system with strict equality on one level and weak 
> equality on another. For historic and pragmatic reasons this is combined 
> with the computational aspects of type theory which is expressed as 
> judgemental equality. However, there are reasons to separate these 
> concerns, e.g. to work with higher dimensional constructions in type theory 
> such as semi-simplicial types it is helpful to work with hypothetical 
> strict equalities (see our paper (
> http://www.cs.nott.ac.uk/~psztxa/publ/csl16.pdf). 
>
>  
>
> I do think that the computational behaviour of type theory is important 
> too. However, this can be expressed by demandic a form of computational 
> adequacy, that is for every term there is a strictly equal normal form. It 
> is not necessary that strict equality in general is decidable (indeed 
> different applications of type theory may demand different decision 
> procedures).
>
>  
>
> Thorsten
>
>  
>
>  
>
> *From: *<homotopyt...@googlegroups.com <javascript:>> on behalf of Felix 
> Rech <s9fe...@gmail.com <javascript:>>
> *Date: *Wednesday, 30 January 2019 at 11:55
> *To: *Homotopy Type Theory <homotopyt...@googlegroups.com <javascript:>>
> *Subject: *[HoTT] Why do we need judgmental equality?
>
>  
>
> 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.
For more options, visit https://groups.google.com/d/optout.

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

^ permalink raw reply	[flat|nested] 71+ messages in thread

* Re: [HoTT] Why do we need judgmental equality?
  2019-02-11  7:01   ` Matt Oliveri
@ 2019-02-11  8:04     ` Valery Isaev
  2019-02-11  8:28       ` Matt Oliveri
  0 siblings, 1 reply; 71+ messages in thread
From: Valery Isaev @ 2019-02-11  8:04 UTC (permalink / raw)
  To: Matt Oliveri; +Cc: Homotopy Type Theory

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

Hi Matt,

I should point out that when I say "a type theory" I mean an ordinary
dependently typed language, without any strict equalities or 2-levelness.
Any such theory has only (dependent) types and terms and usual structural
rules.
Any "coherence problem" is solved by simply adding an infinite tower of
terms. For example, in MLTT, if f : A -> B -> C, you can define function
swap(f) = \x y -> f y x : B -> A -> C. Then swap \circ swap = id
definitionally. Of course, you cannot have such a definitional equality in
Q(MLTT), but instead you have a propositional equality p : Id(swap \circ
swap, id) and also an infinite tower of terms, which assure that p is
coherent. Any rule that holds definitionally in MLTT will be true in
Q(MLTT) propositionally.

Regards,
Valery Isaev


пн, 11 февр. 2019 г. в 10:01, Matt Oliveri <atmacen@gmail.com>:

> I think you're right. From discussions about autophagy, it seems like no
> one knows how to match judgmental equality using equality types, unless
> that equality type family is propositionally truncated in some way.
>
> Consequently, my guess is that Valery's Q transformation actually yields
> something rather like a 2-level system.
>
> On Saturday, February 9, 2019 at 7:30:07 AM UTC-5, Thorsten Altenkirch
> wrote:
>>
>> Hi,
>>
>>
>>
>> what we need is a strict equality on all types. If we would state the
>> laws of type theory just using the equality type we would also need to add
>> coherence laws. Since I would include the laws for substitution (never
>> understood why substitution is different from application) this would
>> include the laws for infinity categories and this would make even basic
>> type theory certainly much more complicated if not unusable. Instead one
>> introduces a 2-level system with strict equality on one level and weak
>> equality on another. For historic and pragmatic reasons this is combined
>> with the computational aspects of type theory which is expressed as
>> judgemental equality. However, there are reasons to separate these
>> concerns, e.g. to work with higher dimensional constructions in type theory
>> such as semi-simplicial types it is helpful to work with hypothetical
>> strict equalities (see our paper (
>> http://www.cs.nott.ac.uk/~psztxa/publ/csl16.pdf).
>>
>>
>>
>> I do think that the computational behaviour of type theory is important
>> too. However, this can be expressed by demandic a form of computational
>> adequacy, that is for every term there is a strictly equal normal form. It
>> is not necessary that strict equality in general is decidable (indeed
>> different applications of type theory may demand different decision
>> procedures).
>>
>>
>>
>> Thorsten
>>
>>
>>
>>
>>
>> *From: *<homotopyt...@googlegroups.com> on behalf of Felix Rech <
>> s9fe...@gmail.com>
>> *Date: *Wednesday, 30 January 2019 at 11:55
>> *To: *Homotopy Type Theory <homotopyt...@googlegroups.com>
>> *Subject: *[HoTT] Why do we need judgmental equality?
>>
>>
>>
>> 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.
> 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.

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

^ permalink raw reply	[flat|nested] 71+ messages in thread

* Re: [HoTT] Re: Why do we need judgmental equality?
  2019-02-09 14:44     ` Jon Sterling
  2019-02-09 20:34       ` Michael Shulman
@ 2019-02-11  8:23       ` Matt Oliveri
  2019-02-11 13:03         ` Jon Sterling
  1 sibling, 1 reply; 71+ messages in thread
From: Matt Oliveri @ 2019-02-11  8:23 UTC (permalink / raw)
  To: Homotopy Type Theory


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

On Saturday, February 9, 2019 at 9:44:39 AM UTC-5, Jonathan Sterling wrote:
>
> But this approach is not likely to yield *proof assistants* that are more 
> usable than existing systems which have replaced definitional equality with 
> propositional equality. 
>
> I am referring to Nuprl --


A discussion of the usability of propositional equality would not be 
complete without distinguishing equality that's reflective, or at least 
"subsumptive", from equality that's merely strict. Subsumptive equality is 
when the equality elimination rule rewrites in the type of a term without 
changing the term. There are no coercions. The way reflective equality is 
implemented in Nuprl is essentially a combination of subsumptive equality 
and extensionality principles. In ITT + UIP or Observational TT (OTT), 
there's a strict propositional equality, but you still have coercions.

I see the avoidance of coercions as the main practical benefit of Nuprl's 
approach.

One's approach to automation of equality checking is somewhat orthogonal, 
and I'm less opinionated about that. A number of dependent type systems 
exist based on an idea of Aaron Stump to use a combination of some 
algorithmic equality, and subsumptive (but non-extensional, non-reflective) 
equality. My impression is that Zombie is one such system.

usually Nuprl is characterized as using equality reflection, but this is 
> not totally accurate (though there is a sense in which it is true).


To clarify, it depends on what you take to be judgmental equality. If it's 
the equality that determines what's well-typed, then Nuprl has equality 
reflection. Of course no useful system will implement reflective equality 
as an algorithm, since it's infeasible. So any algorithmic equality will be 
some other equality judgment. But the "real" judgmental equality is 
precisely the equality type. (As you say later.)

When I say "definitional equality" for a formalism, what I mean is that if 
> I have a proof object D of a judgment J, if J is definitionally equal to 
> J', then D is also already a proof of J'. Definitional equality is the 
> silent equality. In most formalisms, definitional equality includes some 
> combination of alpha/beta/eta/xi, but in Nuprl is included ONLY alpha.


Interesting. So you're counting Nuprl's proof trees and, say, Agda's terms 
as proof objects?

But what about Nuprl's direct computation rules? These allow untyped beta 
reduction and expansion anywhere in a goal. This justifies automatic beta 
normalization by all tactics. I don't know if Nuprlrs take advantage of 
this, but I think they should.

Proof objects must NOT be confused with realizers, of course -- just like 
> we do not confuse Coq proofs with the OCaml code that they could be extract 
> to.
>

To clarify, the realizers in Nuprl are Nuprl's *terms*. They are what get 
normalized; they are what appear in goals. The thing in Coq corresponding 
most closely to Nuprl's proof trees are Coq's proof scripts, not terms. The 
passage from Nuprl's proofs to terms is called "witness extraction", and is 
superficially similar to Coq's program extraction, but its role is 
completely different. A distinction between proof objects and terms is 
practically necessary to avoid coercions, since you still need to tell the 
proof assistant how to use equality *somehow*. In other words, whereas 
Coq's proof scripts are an extra, Nuprl's proof engine is primitive. 
(Similarly, in Andromeda, the distinction between AML programs and terms is 
necessary.)

...the equality type (a judgment whose derivations are crucially taken only 
> up to alpha, rather than up to beta/eta/xi).
>

Although you may wish otherwise, Nuprl's judgments all respect 
computational equivalence, which includes beta conversion. (This is the 
justification of the direct computation rules.)

Nuprl is in essence what it looks like to remove all definitional 
> equalities and replace them with internal equalities. The main difference 
> between Nuprl and Thorsten's proposal is that Nuprl's underlying objects 
> are untyped -- but that is not an essential part of the idea.
>

This doesn't seem right, since Nuprl effectively has untyped beta 
conversion as definitional equality. So I would say it *is* essential that 
Nuprl is intrinsically untyped. Its untyped definitional equality is all 
about the underlying untyped computation system.

The reason I bring this up is that the question of whether such an idea can 
> be made usable, namely using a formalism with only alpha equivalence 
> regarded silently/definitionally, and all other equations mediated through 
> the equality type, can be essentially reduced to the question of whether 
> Nuprl is practical and usable, or whether it is possible to implement a 
> version of that idea which is practical and usable.
>

This is an interesting comparison. But because I consider Nuprl as having 
untyped definitional equality, and a powerful approach to avoiding 
coercions, I have to disagree strongly. By your argument, Thorsten's 
proposal would be at least as bad as Nuprl. (For practical usability.) But 
I think it would probably be much worse, because I think Nuprl is pretty 
good. Some of that is because of beta conversion. But avoiding coercions 
using subsumptive equality is also really powerful. Thorsten didn't say, 
but I'm guessing his proposal wouldn't use that.

(I would really like it if Nuprl could be accurately likened to some other 
proposal, since it'd probably get more people thinking about it. Oh well. 
The most similar systems to Nuprl, other than its successors, are 
Andromeda, with reflective equality, and the Stump lineage I mentioned, 
with subsumptive equality. PVS, Mizar, and F* might be similar too.)

The main purpose of this message is not to disagree with you, Jon. I'm 
mostly trying to sing the praises of Nuprl, because I feel that you've 
badly undersold it.

I don't know what the best way to deal with dependent types is. But I think 
avoiding type annotations and coercions while getting extensional equality 
is really good. I don't know about avoiding *all* type annotations; maybe 
that makes automation too hard. But I suspect the ideal proof assistant 
will be more like Nuprl than like Coq or Agda.

-- 
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 #1.2: Type: text/html, Size: 7914 bytes --]

^ permalink raw reply	[flat|nested] 71+ messages in thread

* Re: [HoTT] Why do we need judgmental equality?
  2019-02-11  8:04     ` Valery Isaev
@ 2019-02-11  8:28       ` Matt Oliveri
  2019-02-11  8:37         ` Matt Oliveri
  0 siblings, 1 reply; 71+ messages in thread
From: Matt Oliveri @ 2019-02-11  8:28 UTC (permalink / raw)
  To: Homotopy Type Theory


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

OK, thanks. I stand corrected. But in that case, I'm with Thorsten: 2-level 
seems easier.

On Monday, February 11, 2019 at 3:04:58 AM UTC-5, Валерий Исаев wrote:
>
> Hi Matt,
>
> I should point out that when I say "a type theory" I mean an ordinary 
> dependently typed language, without any strict equalities or 2-levelness. 
> Any such theory has only (dependent) types and terms and usual structural 
> rules.
> Any "coherence problem" is solved by simply adding an infinite tower of 
> terms. For example, in MLTT, if f : A -> B -> C, you can define function 
> swap(f) = \x y -> f y x : B -> A -> C. Then swap \circ swap = id 
> definitionally. Of course, you cannot have such a definitional equality in 
> Q(MLTT), but instead you have a propositional equality p : Id(swap \circ 
> swap, id) and also an infinite tower of terms, which assure that p is 
> coherent. Any rule that holds definitionally in MLTT will be true in 
> Q(MLTT) propositionally.
>
> Regards,
> Valery Isaev
>
>
> пн, 11 февр. 2019 г. в 10:01, Matt Oliveri <atm...@gmail.com <javascript:>
> >:
>
>> I think you're right. From discussions about autophagy, it seems like no 
>> one knows how to match judgmental equality using equality types, unless 
>> that equality type family is propositionally truncated in some way.
>>
>> Consequently, my guess is that Valery's Q transformation actually yields 
>> something rather like a 2-level system.
>>
>> On Saturday, February 9, 2019 at 7:30:07 AM UTC-5, Thorsten Altenkirch 
>> wrote:
>>>
>>> Hi,
>>>
>>>  
>>>
>>> what we need is a strict equality on all types. If we would state the 
>>> laws of type theory just using the equality type we would also need to add 
>>> coherence laws. Since I would include the laws for substitution (never 
>>> understood why substitution is different from application) this would 
>>> include the laws for infinity categories and this would make even basic 
>>> type theory certainly much more complicated if not unusable. Instead one 
>>> introduces a 2-level system with strict equality on one level and weak 
>>> equality on another. For historic and pragmatic reasons this is combined 
>>> with the computational aspects of type theory which is expressed as 
>>> judgemental equality. However, there are reasons to separate these 
>>> concerns, e.g. to work with higher dimensional constructions in type theory 
>>> such as semi-simplicial types it is helpful to work with hypothetical 
>>> strict equalities (see our paper (
>>> http://www.cs.nott.ac.uk/~psztxa/publ/csl16.pdf). 
>>>
>>>  
>>>
>>> I do think that the computational behaviour of type theory is important 
>>> too. However, this can be expressed by demandic a form of computational 
>>> adequacy, that is for every term there is a strictly equal normal form. It 
>>> is not necessary that strict equality in general is decidable (indeed 
>>> different applications of type theory may demand different decision 
>>> procedures).
>>>
>>>  
>>>
>>> Thorsten
>>>
>>

-- 
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 #1.2: Type: text/html, Size: 4944 bytes --]

^ permalink raw reply	[flat|nested] 71+ messages in thread

* Re: [HoTT] Why do we need judgmental equality?
  2019-02-11  8:28       ` Matt Oliveri
@ 2019-02-11  8:37         ` Matt Oliveri
  2019-02-11  9:32           ` Rafaël Bocquet
  0 siblings, 1 reply; 71+ messages in thread
From: Matt Oliveri @ 2019-02-11  8:37 UTC (permalink / raw)
  To: Homotopy Type Theory


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

Come to think of it, that's pretty cool though, that you can systematically 
produce all the higher coherences for a system of judgmental equations!

On Monday, February 11, 2019 at 3:28:53 AM UTC-5, Matt Oliveri wrote:
>
> OK, thanks. I stand corrected. But in that case, I'm with Thorsten: 
> 2-level seems easier.
>
> On Monday, February 11, 2019 at 3:04:58 AM UTC-5, Валерий Исаев wrote:
>>
>> Hi Matt,
>>
>> I should point out that when I say "a type theory" I mean an ordinary 
>> dependently typed language, without any strict equalities or 2-levelness. 
>> Any such theory has only (dependent) types and terms and usual structural 
>> rules.
>> Any "coherence problem" is solved by simply adding an infinite tower of 
>> terms. For example, in MLTT, if f : A -> B -> C, you can define function 
>> swap(f) = \x y -> f y x : B -> A -> C. Then swap \circ swap = id 
>> definitionally. Of course, you cannot have such a definitional equality in 
>> Q(MLTT), but instead you have a propositional equality p : Id(swap \circ 
>> swap, id) and also an infinite tower of terms, which assure that p is 
>> coherent. Any rule that holds definitionally in MLTT will be true in 
>> Q(MLTT) propositionally.
>>
>> Regards,
>> Valery Isaev
>>
>

-- 
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 #1.2: Type: text/html, Size: 2170 bytes --]

^ permalink raw reply	[flat|nested] 71+ messages in thread

* Re: [HoTT] Why do we need judgmental equality?
  2019-02-11  8:37         ` Matt Oliveri
@ 2019-02-11  9:32           ` Rafaël Bocquet
  0 siblings, 0 replies; 71+ messages in thread
From: Rafaël Bocquet @ 2019-02-11  9:32 UTC (permalink / raw)
  To: HomotopyTypeTheory

I have been thinking about the relationship between type theories with 
weak or strong computation rules, here is what I currently know about it.

Note that in the presence of UIP, type theories with weak and strong 
computation rules are equivalent. This is a consequence of the 
conservativity of extensional type theory over intensional type theory. 
(As Théo said, the proof does not rely on the presence of strong 
computation rules in ITT)

Without UIP, there are coherence theorems to be proven. As explained by 
Thorsten, we can replace a type theory T (presented by generators (type 
and term constructors) and relations (definitional equalities)) by a 
two-level type theory whose outer layer has strict identity types, and 
in which the definitional equalities of T become generators of the 
identity types of the outer layer. Here, "strict" means that we either 
include the equality reflection rule, or the UIP principle. By the same 
arguments as in Hofmann's conservativity proof, both choices are equivalent.

What is interesting is that for some choices of type-theoretic 
structures and definitional equalities, UIP can be derived in the 
two-level type theory, rather than taken as an axiom, in which case the 
strong type theory is a conservative extension of the weak theory. 
Proving that UIP is derivable is very similar to proving coherence 
statements of the form "all diagrams commute". (it is an acylicity 
condition)


If F : WTT ---> STT is an extension of a weak type theory WTT by new 
equations, and W2TT is a two-level type theory associated to WTT, the 
situation is as follows:

   WTT -------------------> STT
    |          F             |
   G|                       H|~
    v                        v
   W2TT ---> W2TT+UIP ---> W2TT+EXT
        K              L

(The objects of this diagram are the initial models of the theories)
G and L are always conservative, H is an isomorphism, and if UIP is 
derivable in W2TT, then K is conservative.


I think that I know how to prove that UIP is derivable when considering 
extensions corresponding to weak computation rules (propositional 
identity types, ...), although I have not written a detailed proof yet.
The core of the proof is a procedure that performs weak head 
normalization, up to homotopy and coherently, in the weak two-level type 
theory. Because the strong theory is strongly normalising, repeatedly 
applying that procedure terminates.

--
Rafaël Bocquet

-- 
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.

^ permalink raw reply	[flat|nested] 71+ messages in thread

* Re: [HoTT] Re: Why do we need judgmental equality?
  2019-02-09 20:34       ` Michael Shulman
@ 2019-02-11 12:17         ` Matt Oliveri
  2019-02-11 13:04           ` Michael Shulman
  0 siblings, 1 reply; 71+ messages in thread
From: Matt Oliveri @ 2019-02-11 12:17 UTC (permalink / raw)
  To: Homotopy Type Theory


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

On Saturday, February 9, 2019 at 3:34:22 PM UTC-5, Michael Shulman wrote:
>
> From an implementation point of view, I agree that in the long run we 
> should have proof assistants that don't hardcode a fixed set of 
> judgmental equalities.  But I don't think that means eliminating all 
> judgmental equalities; it just means making the logical framework more 
> flexible, such as Agda's ability to postulate new reductions or 
> Andromeda's framework with equality reflection.  In particular, the 
> new equalities that we postulate should still be *substitutive* (as 
> Jon says, allowing to perturb a judgment without altering the proof 
> object) rather than *transportive* (requiring the proof object to be 
> altered) -- I think Vladimir was the one who suggested words like 
> those.


I first heard those terms was on this list:
https://groups.google.com/forum/#!topic/homotopytypetheory/1bUtH8CLGQg

It seems from that discussion that they were associated with Vladimir 
Voevodsky's proposal for HTS. 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.

Judgmental, definitional, substitutive, and computational equalities 
> are not exactly the same thing.  But the fact that there are so many 
> different but related points of view on similar and overlapping 
> concepts, and so many different but related uses and applications for 
> them, suggests to me that there is an important underlying 
> mathematical concept that should not lightly be discarded.
>

This is too vague. I wouldn't know whether I'm discarding it or not. You 
seem to be downplaying the differences between these notions. Why? If you 
don't care about the difference, why don't you just deal with strict or 
exact equality, and leave the implementation details to someone else? 
Coherence issues don't penetrate to a lower level than strict equality. 
Judgmental, definitional, and substitutive equality are special cases of 
strict equality that differ in their implementation properties.

-- 
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 #1.2: Type: text/html, Size: 3541 bytes --]

^ permalink raw reply	[flat|nested] 71+ messages in thread

* Re: [HoTT] Re: Why do we need judgmental equality?
  2019-02-11  8:23       ` Matt Oliveri
@ 2019-02-11 13:03         ` Jon Sterling
  2019-02-11 13:22           ` Matt Oliveri
  0 siblings, 1 reply; 71+ messages in thread
From: Jon Sterling @ 2019-02-11 13:03 UTC (permalink / raw)
  To: 'Martin Escardo' via Homotopy Type Theory

Hi Matt, I don't have time to get sucked further into this conversation, but let me just say that what you are saying about "untyped definitional equality" and beta about nuprl is not accurate, or at least, it is not accurate if you take the broad definition of 'definitional equality' that I set in my message.

The lack of coercions in the realizers is true, but I did (apparently pointlessly) exhort readers to not confuse a realizer with a proof. There are coercions in the proof objects -- we must compare apples with apples. 

On Mon, Feb 11, 2019, at 3:23 AM, Matt Oliveri wrote:
> On Saturday, February 9, 2019 at 9:44:39 AM UTC-5, Jonathan Sterling 
> wrote:But this approach is not likely to yield *proof assistants* that 
> are more usable than existing systems which have replaced definitional 
> equality with propositional equality. 
> >  
> > I am referring to Nuprl --
> 
> A discussion of the usability of propositional equality would not be 
> complete without distinguishing equality that's reflective, or at least 
> "subsumptive", from equality that's merely strict. Subsumptive equality 
> is when the equality elimination rule rewrites in the type of a term 
> without changing the term. There are no coercions. The way reflective 
> equality is implemented in Nuprl is essentially a combination of 
> subsumptive equality and extensionality principles. In ITT + UIP or 
> Observational TT (OTT), there's a strict propositional equality, but 
> you still have coercions.
> 
> I see the avoidance of coercions as the main practical benefit of 
> Nuprl's approach.
> 
> One's approach to automation of equality checking is somewhat 
> orthogonal, and I'm less opinionated about that. A number of dependent 
> type systems exist based on an idea of Aaron Stump to use a combination 
> of some algorithmic equality, and subsumptive (but non-extensional, 
> non-reflective) equality. My impression is that Zombie is one such 
> system.
> 
> > usually Nuprl is characterized as using equality reflection, but this is not totally accurate (though there is a sense in which it is true).
> 
> To clarify, it depends on what you take to be judgmental equality. If 
> it's the equality that determines what's well-typed, then Nuprl has 
> equality reflection. Of course no useful system will implement 
> reflective equality as an algorithm, since it's infeasible. So any 
> algorithmic equality will be some other equality judgment. But the 
> "real" judgmental equality is precisely the equality type. (As you say 
> later.)
> 
> > When I say "definitional equality" for a formalism, what I mean is that if I have a proof object D of a judgment J, if J is definitionally equal to J', then D is also already a proof of J'. Definitional equality is the silent equality. In most formalisms, definitional equality includes some combination of alpha/beta/eta/xi, but in Nuprl is included ONLY alpha.
> 
> Interesting. So you're counting Nuprl's proof trees and, say, Agda's 
> terms as proof objects?
> 
> But what about Nuprl's direct computation rules? These allow untyped 
> beta reduction and expansion anywhere in a goal. This justifies 
> automatic beta normalization by all tactics. I don't know if Nuprlrs 
> take advantage of this, but I think they should.
> 
> > Proof objects must NOT be confused with realizers, of course -- just like we do not confuse Coq proofs with the OCaml code that they could be extract to.
> 
> To clarify, the realizers in Nuprl are Nuprl's *terms*. They are what 
> get normalized; they are what appear in goals. The thing in Coq 
> corresponding most closely to Nuprl's proof trees are Coq's proof 
> scripts, not terms. The passage from Nuprl's proofs to terms is called 
> "witness extraction", and is superficially similar to Coq's program 
> extraction, but its role is completely different. A distinction between 
> proof objects and terms is practically necessary to avoid coercions, 
> since you still need to tell the proof assistant how to use equality 
> *somehow*. In other words, whereas Coq's proof scripts are an extra, 
> Nuprl's proof engine is primitive. (Similarly, in Andromeda, the 
> distinction between AML programs and terms is necessary.)
> 
> > ...the equality type (a judgment whose derivations are crucially taken only up to alpha, rather than up to beta/eta/xi).
> 
> Although you may wish otherwise, Nuprl's judgments all respect 
> computational equivalence, which includes beta conversion. (This is the 
> justification of the direct computation rules.)
> 
> > Nuprl is in essence what it looks like to remove all definitional equalities and replace them with internal equalities. The main difference between Nuprl and Thorsten's proposal is that Nuprl's underlying objects are untyped -- but that is not an essential part of the idea.
> 
> This doesn't seem right, since Nuprl effectively has untyped beta 
> conversion as definitional equality. So I would say it *is* essential 
> that Nuprl is intrinsically untyped. Its untyped definitional equality 
> is all about the underlying untyped computation system.
> 
> > The reason I bring this up is that the question of whether such an idea can be made usable, namely using a formalism with only alpha equivalence regarded silently/definitionally, and all other equations mediated through the equality type, can be essentially reduced to the question of whether Nuprl is practical and usable, or whether it is possible to implement a version of that idea which is practical and usable.
> 
> This is an interesting comparison. But because I consider Nuprl as 
> having untyped definitional equality, and a powerful approach to 
> avoiding coercions, I have to disagree strongly. By your argument, 
> Thorsten's proposal would be at least as bad as Nuprl. (For practical 
> usability.) But I think it would probably be much worse, because I 
> think Nuprl is pretty good. Some of that is because of beta conversion. 
> But avoiding coercions using subsumptive equality is also really 
> powerful. Thorsten didn't say, but I'm guessing his proposal wouldn't 
> use that.
> 
> (I would really like it if Nuprl could be accurately likened to some 
> other proposal, since it'd probably get more people thinking about it. 
> Oh well. The most similar systems to Nuprl, other than its successors, 
> are Andromeda, with reflective equality, and the Stump lineage I 
> mentioned, with subsumptive equality. PVS, Mizar, and F* might be 
> similar too.)
> 
> The main purpose of this message is not to disagree with you, Jon. I'm 
> mostly trying to sing the praises of Nuprl, because I feel that you've 
> badly undersold it.
> 
> I don't know what the best way to deal with dependent types is. But I 
> think avoiding type annotations and coercions while getting extensional 
> equality is really good. I don't know about avoiding *all* type 
> annotations; maybe that makes automation too hard. But I suspect the 
> ideal proof assistant will be more like Nuprl than like Coq or Agda.
>  
> 
> 
>  -- 
>  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.

^ permalink raw reply	[flat|nested] 71+ messages in thread

* Re: [HoTT] Re: Why do we need judgmental equality?
  2019-02-11 12:17         ` Matt Oliveri
@ 2019-02-11 13:04           ` Michael Shulman
  2019-02-11 15:09             ` Matt Oliveri
  0 siblings, 1 reply; 71+ messages in thread
From: Michael Shulman @ 2019-02-11 13:04 UTC (permalink / raw)
  To: Matt Oliveri; +Cc: Homotopy Type Theory

On Mon, Feb 11, 2019 at 4:17 AM Matt Oliveri <atmacen@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.

^ permalink raw reply	[flat|nested] 71+ messages in thread

* Re: [HoTT] Re: Why do we need judgmental equality?
  2019-02-11 13:03         ` Jon Sterling
@ 2019-02-11 13:22           ` Matt Oliveri
  2019-02-11 13:37             ` Jon Sterling
  0 siblings, 1 reply; 71+ messages in thread
From: Matt Oliveri @ 2019-02-11 13:22 UTC (permalink / raw)
  To: Homotopy Type Theory


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

I'm not convinced that I've made a mistake about Nuprl. If had mistakenly 
taken realizers to be the proof objects, then *all* equality would be 
definitional. That's not what I'm saying. The untyped beta conversion is 
special because beta normalization can be automatically used as necessary 
by all tactics invoked in the proof object. That means all proof objects 
(following this approach) are robust to "perturbations" that are beta 
conversions. Like I said, I'm not sure Nuprl folks do that. If not, you are 
technically correct that definitional equality is alpha. But they can and 
should do that. So the design of the system fully supports definitional 
beta conversion. (And nothing more.)

Your exhortation was not pointless. I agreed with it, and attempted to 
explain the reason for the difference in more detail.

On Monday, February 11, 2019 at 8:03:26 AM UTC-5, Jonathan Sterling wrote:
>
> Hi Matt, I don't have time to get sucked further into this conversation, 
> but let me just say that what you are saying about "untyped definitional 
> equality" and beta about nuprl is not accurate, or at least, it is not 
> accurate if you take the broad definition of 'definitional equality' that I 
> set in my message. 
>
> The lack of coercions in the realizers is true, but I did (apparently 
> pointlessly) exhort readers to not confuse a realizer with a proof. There 
> are coercions in the proof objects -- we must compare apples with apples. 
>
> On Mon, Feb 11, 2019, at 3:23 AM, Matt Oliveri wrote: 
> > On Saturday, February 9, 2019 at 9:44:39 AM UTC-5, Jonathan Sterling 
> > wrote:But this approach is not likely to yield *proof assistants* that 
> > are more usable than existing systems which have replaced definitional 
> > equality with propositional equality. 
> > >   
> > > I am referring to Nuprl -- 
> > 
> > A discussion of the usability of propositional equality would not be 
> > complete without distinguishing equality that's reflective, or at least 
> > "subsumptive", from equality that's merely strict. Subsumptive equality 
> > is when the equality elimination rule rewrites in the type of a term 
> > without changing the term. There are no coercions. The way reflective 
> > equality is implemented in Nuprl is essentially a combination of 
> > subsumptive equality and extensionality principles. In ITT + UIP or 
> > Observational TT (OTT), there's a strict propositional equality, but 
> > you still have coercions. 
> > 
> > I see the avoidance of coercions as the main practical benefit of 
> > Nuprl's approach. 
> > 
> > One's approach to automation of equality checking is somewhat 
> > orthogonal, and I'm less opinionated about that. A number of dependent 
> > type systems exist based on an idea of Aaron Stump to use a combination 
> > of some algorithmic equality, and subsumptive (but non-extensional, 
> > non-reflective) equality. My impression is that Zombie is one such 
> > system. 
> > 
> > > usually Nuprl is characterized as using equality reflection, but this 
> is not totally accurate (though there is a sense in which it is true). 
> > 
> > To clarify, it depends on what you take to be judgmental equality. If 
> > it's the equality that determines what's well-typed, then Nuprl has 
> > equality reflection. Of course no useful system will implement 
> > reflective equality as an algorithm, since it's infeasible. So any 
> > algorithmic equality will be some other equality judgment. But the 
> > "real" judgmental equality is precisely the equality type. (As you say 
> > later.) 
> > 
> > > When I say "definitional equality" for a formalism, what I mean is 
> that if I have a proof object D of a judgment J, if J is definitionally 
> equal to J', then D is also already a proof of J'. Definitional equality is 
> the silent equality. In most formalisms, definitional equality includes 
> some combination of alpha/beta/eta/xi, but in Nuprl is included ONLY alpha. 
> > 
> > Interesting. So you're counting Nuprl's proof trees and, say, Agda's 
> > terms as proof objects? 
> > 
> > But what about Nuprl's direct computation rules? These allow untyped 
> > beta reduction and expansion anywhere in a goal. This justifies 
> > automatic beta normalization by all tactics. I don't know if Nuprlrs 
> > take advantage of this, but I think they should. 
> > 
> > > Proof objects must NOT be confused with realizers, of course -- just 
> like we do not confuse Coq proofs with the OCaml code that they could be 
> extract to. 
> > 
> > To clarify, the realizers in Nuprl are Nuprl's *terms*. They are what 
> > get normalized; they are what appear in goals. The thing in Coq 
> > corresponding most closely to Nuprl's proof trees are Coq's proof 
> > scripts, not terms. The passage from Nuprl's proofs to terms is called 
> > "witness extraction", and is superficially similar to Coq's program 
> > extraction, but its role is completely different. A distinction between 
> > proof objects and terms is practically necessary to avoid coercions, 
> > since you still need to tell the proof assistant how to use equality 
> > *somehow*. In other words, whereas Coq's proof scripts are an extra, 
> > Nuprl's proof engine is primitive. (Similarly, in Andromeda, the 
> > distinction between AML programs and terms is necessary.) 
> > 
> > > ...the equality type (a judgment whose derivations are crucially taken 
> only up to alpha, rather than up to beta/eta/xi). 
> > 
> > Although you may wish otherwise, Nuprl's judgments all respect 
> > computational equivalence, which includes beta conversion. (This is the 
> > justification of the direct computation rules.) 
> > 
> > > Nuprl is in essence what it looks like to remove all definitional 
> equalities and replace them with internal equalities. The main difference 
> between Nuprl and Thorsten's proposal is that Nuprl's underlying objects 
> are untyped -- but that is not an essential part of the idea. 
> > 
> > This doesn't seem right, since Nuprl effectively has untyped beta 
> > conversion as definitional equality. So I would say it *is* essential 
> > that Nuprl is intrinsically untyped. Its untyped definitional equality 
> > is all about the underlying untyped computation system. 
> > 
> > > The reason I bring this up is that the question of whether such an 
> idea can be made usable, namely using a formalism with only alpha 
> equivalence regarded silently/definitionally, and all other equations 
> mediated through the equality type, can be essentially reduced to the 
> question of whether Nuprl is practical and usable, or whether it is 
> possible to implement a version of that idea which is practical and usable. 
> > 
> > This is an interesting comparison. But because I consider Nuprl as 
> > having untyped definitional equality, and a powerful approach to 
> > avoiding coercions, I have to disagree strongly. By your argument, 
> > Thorsten's proposal would be at least as bad as Nuprl. (For practical 
> > usability.) But I think it would probably be much worse, because I 
> > think Nuprl is pretty good. Some of that is because of beta conversion. 
> > But avoiding coercions using subsumptive equality is also really 
> > powerful. Thorsten didn't say, but I'm guessing his proposal wouldn't 
> > use that. 
> > 
> > (I would really like it if Nuprl could be accurately likened to some 
> > other proposal, since it'd probably get more people thinking about it. 
> > Oh well. The most similar systems to Nuprl, other than its successors, 
> > are Andromeda, with reflective equality, and the Stump lineage I 
> > mentioned, with subsumptive equality. PVS, Mizar, and F* might be 
> > similar too.) 
> > 
> > The main purpose of this message is not to disagree with you, Jon. I'm 
> > mostly trying to sing the praises of Nuprl, because I feel that you've 
> > badly undersold it. 
> > 
> > I don't know what the best way to deal with dependent types is. But I 
> > think avoiding type annotations and coercions while getting extensional 
> > equality is really good. I don't know about avoiding *all* type 
> > annotations; maybe that makes automation too hard. But I suspect the 
> > ideal proof assistant will be more like Nuprl than like Coq or Agda.
>

-- 
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 #1.2: Type: text/html, Size: 9636 bytes --]

^ permalink raw reply	[flat|nested] 71+ messages in thread

* Re: [HoTT] Re: Why do we need judgmental equality?
  2019-02-11 13:22           ` Matt Oliveri
@ 2019-02-11 13:37             ` Jon Sterling
  0 siblings, 0 replies; 71+ messages in thread
From: Jon Sterling @ 2019-02-11 13:37 UTC (permalink / raw)
  To: 'Martin Escardo' via Homotopy Type Theory

Hi Matt, my final comment is just to clarify that even if you take the tactic trees as the proof objects (which is a position that I think is fine to argue), it is not acceptable to say that they are robust to "beta perturbations", because if your tactics run beta rules automatically, it is trivial for me to cook up an example where a beta-perturbation would make your tactic script fail to terminate (even if the theorem is true). This is because in Nuprl, you are often working with fixed points (a very cool feature!), and must be circumspect in the computation rules that you apply to them -- for instance, consider proving something about an infinite stream of binary digits. The "substitutive" or "perturbative equality" in Nuprl is indeed alpha, I can confirm, regardless of whether you are thinking of tactic scripts or finished proofs as the proof objects.

I just want to re-emphasize what Mike was saying about "ideas" being so fuzzy that they can be characterized using multiple, conflicting explanations -- definitional equality is one of these things, and is a scientific or philosophical concept rather than a technical concept (as Martin-Lof convincingly argued in the 1970s in his famous paper on definitional equality).  You may have your own way to understand what is happening in Nuprl, and that's ok --- but the way that I am propounding in this thread is an analogy that allows us to compare apples with apples, a very difficult thing to do in this context. If there is anything mathematical to be said about these things, we need a common technical basis, and it seems like the simplest way to do that is to analyze what function definitional equality plays in practice -- it is the thing which (1) doesn't require proof, and (2) doesn't add any coercions to the thing that counts as proof. That is the "universal property" of definitional equality.

I'm too busy to respond further (paper deadline!), so I would request that people wait a few days to contact me about it :)



On Mon, Feb 11, 2019, at 8:22 AM, Matt Oliveri wrote:
> I'm not convinced that I've made a mistake about Nuprl. If had 
> mistakenly taken realizers to be the proof objects, then *all* equality 
> would be definitional. That's not what I'm saying. The untyped beta 
> conversion is special because beta normalization can be automatically 
> used as necessary by all tactics invoked in the proof object. That 
> means all proof objects (following this approach) are robust to 
> "perturbations" that are beta conversions. Like I said, I'm not sure 
> Nuprl folks do that. If not, you are technically correct that 
> definitional equality is alpha. But they can and should do that. So the 
> design of the system fully supports definitional beta conversion. (And 
> nothing more.)
> 
> Your exhortation was not pointless. I agreed with it, and attempted to 
> explain the reason for the difference in more detail.
> 
> On Monday, February 11, 2019 at 8:03:26 AM UTC-5, Jonathan Sterling 
> wrote:Hi Matt, I don't have time to get sucked further into this 
> conversation, but let me just say that what you are saying about 
> "untyped definitional equality" and beta about nuprl is not accurate, 
> or at least, it is not accurate if you take the broad definition of 
> 'definitional equality' that I set in my message. 
> >  
> > The lack of coercions in the realizers is true, but I did (apparently pointlessly) exhort readers to not confuse a realizer with a proof. There are coercions in the proof objects -- we must compare apples with apples. 
> >  
> > On Mon, Feb 11, 2019, at 3:23 AM, Matt Oliveri wrote: 
> > > On Saturday, February 9, 2019 at 9:44:39 AM UTC-5, Jonathan Sterling 
> > > wrote:But this approach is not likely to yield *proof assistants* that 
> > > are more usable than existing systems which have replaced definitional 
> > > equality with propositional equality. 
> > > > 
> > > > I am referring to Nuprl -- 
> > > 
> > > A discussion of the usability of propositional equality would not be 
> > > complete without distinguishing equality that's reflective, or at least 
> > > "subsumptive", from equality that's merely strict. Subsumptive equality 
> > > is when the equality elimination rule rewrites in the type of a term 
> > > without changing the term. There are no coercions. The way reflective 
> > > equality is implemented in Nuprl is essentially a combination of 
> > > subsumptive equality and extensionality principles. In ITT + UIP or 
> > > Observational TT (OTT), there's a strict propositional equality, but 
> > > you still have coercions. 
> > > 
> > > I see the avoidance of coercions as the main practical benefit of 
> > > Nuprl's approach. 
> > > 
> > > One's approach to automation of equality checking is somewhat 
> > > orthogonal, and I'm less opinionated about that. A number of dependent 
> > > type systems exist based on an idea of Aaron Stump to use a combination 
> > > of some algorithmic equality, and subsumptive (but non-extensional, 
> > > non-reflective) equality. My impression is that Zombie is one such 
> > > system. 
> > > 
> > > > usually Nuprl is characterized as using equality reflection, but this is not totally accurate (though there is a sense in which it is true). 
> > > 
> > > To clarify, it depends on what you take to be judgmental equality. If 
> > > it's the equality that determines what's well-typed, then Nuprl has 
> > > equality reflection. Of course no useful system will implement 
> > > reflective equality as an algorithm, since it's infeasible. So any 
> > > algorithmic equality will be some other equality judgment. But the 
> > > "real" judgmental equality is precisely the equality type. (As you say 
> > > later.) 
> > > 
> > > > When I say "definitional equality" for a formalism, what I mean is that if I have a proof object D of a judgment J, if J is definitionally equal to J', then D is also already a proof of J'. Definitional equality is the silent equality. In most formalisms, definitional equality includes some combination of alpha/beta/eta/xi, but in Nuprl is included ONLY alpha. 
> > > 
> > > Interesting. So you're counting Nuprl's proof trees and, say, Agda's 
> > > terms as proof objects? 
> > > 
> > > But what about Nuprl's direct computation rules? These allow untyped 
> > > beta reduction and expansion anywhere in a goal. This justifies 
> > > automatic beta normalization by all tactics. I don't know if Nuprlrs 
> > > take advantage of this, but I think they should. 
> > > 
> > > > Proof objects must NOT be confused with realizers, of course -- just like we do not confuse Coq proofs with the OCaml code that they could be extract to. 
> > > 
> > > To clarify, the realizers in Nuprl are Nuprl's *terms*. They are what 
> > > get normalized; they are what appear in goals. The thing in Coq 
> > > corresponding most closely to Nuprl's proof trees are Coq's proof 
> > > scripts, not terms. The passage from Nuprl's proofs to terms is called 
> > > "witness extraction", and is superficially similar to Coq's program 
> > > extraction, but its role is completely different. A distinction between 
> > > proof objects and terms is practically necessary to avoid coercions, 
> > > since you still need to tell the proof assistant how to use equality 
> > > *somehow*. In other words, whereas Coq's proof scripts are an extra, 
> > > Nuprl's proof engine is primitive. (Similarly, in Andromeda, the 
> > > distinction between AML programs and terms is necessary.) 
> > > 
> > > > ...the equality type (a judgment whose derivations are crucially taken only up to alpha, rather than up to beta/eta/xi). 
> > > 
> > > Although you may wish otherwise, Nuprl's judgments all respect 
> > > computational equivalence, which includes beta conversion. (This is the 
> > > justification of the direct computation rules.) 
> > > 
> > > > Nuprl is in essence what it looks like to remove all definitional equalities and replace them with internal equalities. The main difference between Nuprl and Thorsten's proposal is that Nuprl's underlying objects are untyped -- but that is not an essential part of the idea. 
> > > 
> > > This doesn't seem right, since Nuprl effectively has untyped beta 
> > > conversion as definitional equality. So I would say it *is* essential 
> > > that Nuprl is intrinsically untyped. Its untyped definitional equality 
> > > is all about the underlying untyped computation system. 
> > > 
> > > > The reason I bring this up is that the question of whether such an idea can be made usable, namely using a formalism with only alpha equivalence regarded silently/definitionally, and all other equations mediated through the equality type, can be essentially reduced to the question of whether Nuprl is practical and usable, or whether it is possible to implement a version of that idea which is practical and usable. 
> > > 
> > > This is an interesting comparison. But because I consider Nuprl as 
> > > having untyped definitional equality, and a powerful approach to 
> > > avoiding coercions, I have to disagree strongly. By your argument, 
> > > Thorsten's proposal would be at least as bad as Nuprl. (For practical 
> > > usability.) But I think it would probably be much worse, because I 
> > > think Nuprl is pretty good. Some of that is because of beta conversion. 
> > > But avoiding coercions using subsumptive equality is also really 
> > > powerful. Thorsten didn't say, but I'm guessing his proposal wouldn't 
> > > use that. 
> > > 
> > > (I would really like it if Nuprl could be accurately likened to some 
> > > other proposal, since it'd probably get more people thinking about it. 
> > > Oh well. The most similar systems to Nuprl, other than its successors, 
> > > are Andromeda, with reflective equality, and the Stump lineage I 
> > > mentioned, with subsumptive equality. PVS, Mizar, and F* might be 
> > > similar too.) 
> > > 
> > > The main purpose of this message is not to disagree with you, Jon. I'm 
> > > mostly trying to sing the praises of Nuprl, because I feel that you've 
> > > badly undersold it. 
> > > 
> > > I don't know what the best way to deal with dependent types is. But I 
> > > think avoiding type annotations and coercions while getting extensional 
> > > equality is really good. I don't know about avoiding *all* type 
> > > annotations; maybe that makes automation too hard. But I suspect the 
> > > ideal proof assistant will be more like Nuprl than like Coq or Agda.
>  
> 
> 
>  -- 
>  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.

^ permalink raw reply	[flat|nested] 71+ messages in thread

* Re: [HoTT] Re: Why do we need judgmental equality?
  2019-02-11 13:04           ` Michael Shulman
@ 2019-02-11 15:09             ` Matt Oliveri
  2019-02-11 17:20               ` Michael Shulman
  0 siblings, 1 reply; 71+ messages in thread
From: Matt Oliveri @ 2019-02-11 15:09 UTC (permalink / raw)
  To: Homotopy Type Theory


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

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 
> <javascript:>> 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.

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

^ permalink raw reply	[flat|nested] 71+ messages in thread

* Re: [HoTT] Re: Why do we need judgmental equality?
  2019-02-11 15:09             ` Matt Oliveri
@ 2019-02-11 17:20               ` Michael Shulman
  2019-02-11 18:17                 ` Thorsten Altenkirch
                                   ` (2 more replies)
  0 siblings, 3 replies; 71+ messages in thread
From: Michael Shulman @ 2019-02-11 17:20 UTC (permalink / raw)
  To: Matt Oliveri; +Cc: Homotopy Type Theory

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.

^ permalink raw reply	[flat|nested] 71+ messages in thread

* Re: [HoTT] Re: Why do we need judgmental equality?
  2019-02-11 17:20               ` Michael Shulman
@ 2019-02-11 18:17                 ` Thorsten Altenkirch
  2019-02-11 18:45                   ` Alexander Kurz
  2019-02-12 11:03                   ` Matt Oliveri
  2019-02-11 19:27                 ` Matt Oliveri
  2019-02-11 20:11                 ` Matt Oliveri
  2 siblings, 2 replies; 71+ messages in thread
From: Thorsten Altenkirch @ 2019-02-11 18:17 UTC (permalink / raw)
  To: Michael Shulman, Matt Oliveri; +Cc: Homotopy Type Theory

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.

^ permalink raw reply	[flat|nested] 71+ messages in thread

* Re: [HoTT] Re: Why do we need judgmental equality?
  2019-02-11 18:17                 ` Thorsten Altenkirch
@ 2019-02-11 18:45                   ` Alexander Kurz
  2019-02-11 22:58                     ` Thorsten Altenkirch
  2019-02-12 11:03                   ` Matt Oliveri
  1 sibling, 1 reply; 71+ messages in thread
From: Alexander Kurz @ 2019-02-11 18:45 UTC (permalink / raw)
  To: Thorsten Altenkirch; +Cc: Michael Shulman, Matt Oliveri, Homotopy Type Theory

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.

^ permalink raw reply	[flat|nested] 71+ messages in thread

* Re: [HoTT] Re: Why do we need judgmental equality?
  2019-02-11 17:20               ` Michael Shulman
  2019-02-11 18:17                 ` Thorsten Altenkirch
@ 2019-02-11 19:27                 ` Matt Oliveri
  2019-02-11 21:49                   ` Michael Shulman
  2019-02-11 20:11                 ` Matt Oliveri
  2 siblings, 1 reply; 71+ messages in thread
From: Matt Oliveri @ 2019-02-11 19:27 UTC (permalink / raw)
  To: Homotopy Type Theory


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

Jon's definitional equality is based on proof objects. The Andromeda terms 
aren't proof objects, since you can't check just a term. So the fact that 
Andromeda terms don't have coercions for strict equality doesn't do 
anything for definitional equality. I would guess AML programs should be 
considered the relevant proof objects. I'd say definitional equality in 
Andromeda is pretty interesting, since algebraic effect handlers let you 
locally add new automation for equality. But it can't be as rich as strict 
equality (if you have e.g. induction on nats). And globally, it sounds like 
it's just alpha conversion.

On Monday, February 11, 2019 at 12:20:46 PM UTC-5, Michael Shulman 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 <atm...@gmail.com 
> <javascript:>> 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. 
>

-- 
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 #1.2: Type: text/html, Size: 4135 bytes --]

^ permalink raw reply	[flat|nested] 71+ messages in thread

* Re: [HoTT] Re: Why do we need judgmental equality?
  2019-02-11 17:20               ` Michael Shulman
  2019-02-11 18:17                 ` Thorsten Altenkirch
  2019-02-11 19:27                 ` Matt Oliveri
@ 2019-02-11 20:11                 ` Matt Oliveri
  2 siblings, 0 replies; 71+ messages in thread
From: Matt Oliveri @ 2019-02-11 20:11 UTC (permalink / raw)
  To: Homotopy Type Theory


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

You'll have to ask Jon about what "idea" Nuprl's intrinsic untypedness is 
"not an essential part of". I'd say the most important thing about Nuprl is 
dependent refinement typing. In particular, Nuprl is extrinsic dependent 
typing, since the intrinsic type system is trivial. That turns out to be 
very interesting too, but makes the approach less broadly applicable.

I have some outlandish views about Nuprl. I don't consider its PER 
semantics to be a model, in the usual sense of model theory. It's 
proof-theoretic semantics. It's a semantic justification of some proof 
principles. Kind of like a strong normalization proof for ITT. You can 
point out that it's technically a realizability model. But I'd say that's 
because the terms are realizers. *What are they realizing?* That would be a 
model. The model theory of Nuprlish systems is currently virtually 
nonexistent. Somebody ought to fix that. There's a set-theoretic semantics 
(actually two, and they are different... sort of) for an old version of 
Nuprl. That's it, AFAIK.

On Monday, February 11, 2019 at 12:20:46 PM UTC-5, Michael Shulman 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. 
>

-- 
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 #1.2: Type: text/html, Size: 3039 bytes --]

^ permalink raw reply	[flat|nested] 71+ messages in thread

* Re: [HoTT] Re: Why do we need judgmental equality?
  2019-02-11 19:27                 ` Matt Oliveri
@ 2019-02-11 21:49                   ` Michael Shulman
  2019-02-12  9:01                     ` Matt Oliveri
  0 siblings, 1 reply; 71+ messages in thread
From: Michael Shulman @ 2019-02-11 21:49 UTC (permalink / raw)
  To: Matt Oliveri; +Cc: Homotopy Type Theory

Well, I can't tell exactly what Jon meant by "I have a proof object D
of a judgment J, if J is definitionally equal to J', then D is also
already a proof of J'.".  If he meant that an entire typing judgment
"M:A" is only "definitionally equal" to a typing judgment "N:B" if
*the very same derivation tree* of M:A counts also as a derivation of
N:B, then in the ordinary presentations of *any* ordinary type theory
I don't think any two judgments that differ by anything more than
alpha-equivalence would be considered "definitionally equal".  Look
for instance at appendix A.2 of the HoTT book: coercion along
judgmental equality is a rule that alters a derivation tree.  What it
doesn't alter is the *term*, and since Jon also said "In most
formalisms, definitional equality includes some combination of
alpha/beta/eta/xi" I assumed that his "proof objects" in a MLTT-like
theory would refer to the terms rather than the derivation trees.

Regardless of what Jon meant, it seems to me that insofar as
"definitional equality" is distinguished from all these other kinds of
strict equality, it should refer to pairs of terms (i.e. bits of
syntax that denote something in a model) that are *equal by
definition*.  For instance, (\lambda x. x^2)(3) is equal by definition
to 3^2, because \lambda x. x^2 denotes by definition the function that
takes its argument and squares it.  I think this is roughly the same
as what I would mean by "equality of sense", although the latter is a
primarily philosophical concept and as such cannot be pinned down with
mathematical rigor.  AML programs do not denote something in a model,
and I can't think of any sense in which two of them could be "equal by
definition".  A judgmental, strict, exact, or substitutional equality
might include only definitional equalities, as in ordinary ITT, or it
might include other non-definitional ones, as in ETT with reflection
rule.  So I would say that Andromeda with its reflection rule does not
include a "definitional equality" as a distinguished notion of the
core language.  However, when using Andromeda as a logical framework
to implement some object language, one might assert a particular class
of substitutional equalities in the object language that are all
definitional.

On Mon, Feb 11, 2019 at 11:27 AM Matt Oliveri <atmacen@gmail.com> wrote:
>
> Jon's definitional equality is based on proof objects. The Andromeda terms aren't proof objects, since you can't check just a term. So the fact that Andromeda terms don't have coercions for strict equality doesn't do anything for definitional equality. I would guess AML programs should be considered the relevant proof objects. I'd say definitional equality in Andromeda is pretty interesting, since algebraic effect handlers let you locally add new automation for equality. But it can't be as rich as strict equality (if you have e.g. induction on nats). And globally, it sounds like it's just alpha conversion.
>
> On Monday, February 11, 2019 at 12:20:46 PM UTC-5, Michael Shulman 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 <atm...@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.
>
> --
> 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.

^ permalink raw reply	[flat|nested] 71+ messages in thread

* Re: [HoTT] Re: Why do we need judgmental equality?
  2019-02-11 18:45                   ` Alexander Kurz
@ 2019-02-11 22:58                     ` Thorsten Altenkirch
  2019-02-12  2:09                       ` Jacques Carette
  0 siblings, 1 reply; 71+ messages in thread
From: Thorsten Altenkirch @ 2019-02-11 22:58 UTC (permalink / raw)
  To: Alexander Kurz; +Cc: Michael Shulman, Matt Oliveri, Homotopy Type Theory

I think it is rather misleading to think that 0 and the empty set have something in common because in set theory they are represented by the same construction {}. This is rather an accident of representation, it is like saying that the number 49 and the letter 'a' have something in common because they are both represented by the same bit sequence.

Indeed, I think having access and being able to talk about the accidental representation of objects as you can do in set theory is detrimental because it stops abstraction and this is precisely one of the main advantages of type theory.

Thorsten

On 11/02/2019, 18:45, "homotopytypetheory@googlegroups.com on behalf of Alexander Kurz" <homotopytypetheory@googlegroups.com on behalf of axhkrz@gmail.com> wrote:

    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.
    




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.

^ permalink raw reply	[flat|nested] 71+ messages in thread

* Re: [HoTT] Re: Why do we need judgmental equality?
  2019-02-11 22:58                     ` Thorsten Altenkirch
@ 2019-02-12  2:09                       ` Jacques Carette
  0 siblings, 0 replies; 71+ messages in thread
From: Jacques Carette @ 2019-02-12  2:09 UTC (permalink / raw)
  To: Thorsten Altenkirch, Alexander Kurz
  Cc: Michael Shulman, Matt Oliveri, Homotopy Type Theory

Some of you might already have seen the interesting discussion "Set 
theories without junk theorems" at MO
https://mathoverflow.net/questions/90820/set-theories-without-junk-theorems
that is very much about these accidents of representation.
Jacques

On 2019-02-11 17:58 , Thorsten Altenkirch wrote:
> I think it is rather misleading to think that 0 and the empty set have something in common because in set theory they are represented by the same construction {}. This is rather an accident of representation, it is like saying that the number 49 and the letter 'a' have something in common because they are both represented by the same bit sequence.
>
> Indeed, I think having access and being able to talk about the accidental representation of objects as you can do in set theory is detrimental because it stops abstraction and this is precisely one of the main advantages of type theory.
>
> Thorsten
>
> On 11/02/2019, 18:45, "homotopytypetheory@googlegroups.com on behalf of Alexander Kurz" <homotopytypetheory@googlegroups.com on behalf of axhkrz@gmail.com> wrote:
>
>      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.
>      
>
>
>
>
> 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.

^ permalink raw reply	[flat|nested] 71+ messages in thread

* Re: [HoTT] Re: Why do we need judgmental equality?
  2019-02-11 21:49                   ` Michael Shulman
@ 2019-02-12  9:01                     ` Matt Oliveri
  2019-02-12 17:54                       ` Michael Shulman
  0 siblings, 1 reply; 71+ messages in thread
From: Matt Oliveri @ 2019-02-12  9:01 UTC (permalink / raw)
  To: Homotopy Type Theory


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

On Monday, February 11, 2019 at 4:50:19 PM UTC-5, Michael Shulman wrote:
>
> Well, I can't tell exactly what Jon meant by "I have a proof object D 
> of a judgment J, if J is definitionally equal to J', then D is also 
> already a proof of J'.".  If he meant that an entire typing judgment 
> "M:A" is only "definitionally equal" to a typing judgment "N:B" if 
> *the very same derivation tree* of M:A counts also as a derivation of 
> N:B, then in the ordinary presentations of *any* ordinary type theory 
> I don't think any two judgments that differ by anything more than 
> alpha-equivalence would be considered "definitionally equal".
>

Right. So I assumed he didn't mean that. I'm pretty sure that for ITT, the 
terms are the proof objects. But it's not clear what should count as proof 
objects otherwise. This is a weakness of the definition. I guessed at what 
the proof objects were for Nuprl, but it looks like Jon had something else 
in mind.

If the proof objects are taken to be whatever notion of formal proof the 
formalizer needs to produce, then definitional equality is an important 
consideration for proof engineering. That's what I was thinking about. 
Crucially, proof automation changes the notion of proof, in practice. But 
this makes things fuzzy.

AML programs do not denote something in a model, 
> and I can't think of any sense in which two of them could be "equal by 
> definition".


You seem confused. Definitional equality is not a relation on proof 
objects, it's a relation on expressions appearing in the judgments they 
prove. AML programs don't appear in judgments. (Well, not any semantically 
relevant judgments.)

For instance, (\lambda x. x^2)(3) is equal by definition 
> to 3^2, because \lambda x. x^2 denotes by definition the function that 
> takes its argument and squares it.


This sure seems completely different from what Jon was getting at. But 
anyway, what's the difference between "denoting by definition" and regular 
denoting?

An important aspect of Jon's definition of "definitional equality", which I 
think is right, is that it doesn't have to do with models. Definitional 
equality is an intentional issue. An issue tied to implementation. ITT pins 
definitional equality to judgmental equality, which *does* have to do with 
models, and I think that's *bad*. I suspect that the discomfort or lack of 
understanding many mathematicians supposedly have with definitional 
equality stems from the fact that it is, in fact, an implementation issue.

So I would say that Andromeda with its reflection rule does not 
> include a "definitional equality" as a distinguished notion of the 
> core language.


Agree.

However, when using Andromeda as a logical framework 
> to implement some object language, one might assert a particular class 
> of substitutional equalities in the object language that are all 
> definitional.
>

How would you tell when a class of equalities is definitional?

On Mon, Feb 11, 2019 at 11:27 AM Matt Oliveri <atm...@gmail.com 
> <javascript:>> wrote: 
> > 
> > Jon's definitional equality is based on proof objects. The Andromeda 
> terms aren't proof objects, since you can't check just a term. So the fact 
> that Andromeda terms don't have coercions for strict equality doesn't do 
> anything for definitional equality. I would guess AML programs should be 
> considered the relevant proof objects. I'd say definitional equality in 
> Andromeda is pretty interesting, since algebraic effect handlers let you 
> locally add new automation for equality. But it can't be as rich as strict 
> equality (if you have e.g. induction on nats). And globally, it sounds like 
> it's just alpha conversion. 
>

-- 
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 #1.2: Type: text/html, Size: 5443 bytes --]

^ permalink raw reply	[flat|nested] 71+ messages in thread

* Re: [HoTT] Re: Why do we need judgmental equality?
  2019-02-11 18:17                 ` Thorsten Altenkirch
  2019-02-11 18:45                   ` Alexander Kurz
@ 2019-02-12 11:03                   ` Matt Oliveri
  2019-02-12 15:36                     ` Thorsten Altenkirch
  1 sibling, 1 reply; 71+ messages in thread
From: Matt Oliveri @ 2019-02-12 11:03 UTC (permalink / raw)
  To: Homotopy Type Theory


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

Let's say that "objects" are untyped, and "elements" are typed, by 
definition. These are semantic entities. Nuprl's (closed) terms are untyped 
in that you are allowed to think of them as objects. You can also think of 
them as elements. This is not the same. I'd like to distance Nuprl, based 
on PERs, from set theory. In set theory, objects are given their final 
meaning by the universe, and sets are types only in the most boring 
possible sense that you gather up objects and call them elements. In Nuprl, 
terms obtain their computational meaning as objects, but their mathematical 
meaning as elements. Interpreted as PERs, Nuprl's types let you ask whether 
two objects implement the same element. Equality of elements is not 
equality of objects, and the way you think about objects and elements is 
different. A variable has a declared type, and it denotes an arbitrary 
element of that type. It is meaningless to think of it as an object (unless 
the declared type is a subtype of the type of objects).

You are right that you don't need to explain elements in terms of objects. 
That doesn't necessarily make it a bad idea.

Each PER indicates how its elements are implemented by objects. There's no 
requirement that an object will have a unique type. Each type can be 
thought of as an abstract view of certain objects.

Constructions in Nuprl are heavily based on types, as in any strong type 
system. You wouldn't bother with a strong type system if you weren't going 
to do that. You can construct elements using the usual sorts of rules. 
Because Nuprl also has objects, you also have the option of constructing 
objects and then proving they implement elements of one or more types. If 
you've never felt at all constrained by a strong type system, great; you 
don't have to do that. But for many people, the intrinsically untyped 
approach is sometimes helpful. An element is an element; it doesn't matter 
whether it's an element by construction, or a verified object. I see this 
as a tremendous benefit for strongly typed programming.

On Monday, February 11, 2019 at 1:17:25 PM UTC-5, Thorsten Altenkirch 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
>
>

-- 
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 #1.2: Type: text/html, Size: 3366 bytes --]

^ permalink raw reply	[flat|nested] 71+ messages in thread

* Re: [HoTT] Re: Why do we need judgmental equality?
  2019-02-12 11:03                   ` Matt Oliveri
@ 2019-02-12 15:36                     ` Thorsten Altenkirch
  2019-02-12 15:59                       ` Matt Oliveri
  0 siblings, 1 reply; 71+ messages in thread
From: Thorsten Altenkirch @ 2019-02-12 15:36 UTC (permalink / raw)
  To: Matt Oliveri, Homotopy Type Theory

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


You are right that you don't need to explain elements in terms of objects. That doesn't necessarily make it a bad idea.

Not necessarily but I think it is a bad idea. Why do I need to understand objects to understand elements? Why do I have to capture all possible constructions if I just want to talk about some specific ones?

This is something that irritates me about set theory: if I want to say for all natural numbers …, I am actually saying for all sets which turn out to be natural numbers… At least conceptually this is rubbish. Who thinks like this?

Yes and in computer science we think about types sorting untyped programs. But why? Why do I need to think about untyped programs to understand typed ones. Untyped programs are just weird. Do you understand the untyped lambda calculus? It’s syntax is simple but its meaning is a headfuck. It took Dana Scott a while to come up with a mathematical semantics.

I think we should put our mouth where our heart is. Typed objects are easier to understand, they make sense by themselves so lets refer to them. Yes we implement them based in intyped things, trees, strings, bit sequences but we don’t need low level concepts to understand high level concepts!! Yes we need them to implement them but this is another issue.

Thorsten
--
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: 4777 bytes --]

^ permalink raw reply	[flat|nested] 71+ messages in thread

* Re: [HoTT] Re: Why do we need judgmental equality?
  2019-02-12 15:36                     ` Thorsten Altenkirch
@ 2019-02-12 15:59                       ` Matt Oliveri
  0 siblings, 0 replies; 71+ messages in thread
From: Matt Oliveri @ 2019-02-12 15:59 UTC (permalink / raw)
  To: Homotopy Type Theory


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

On Tuesday, February 12, 2019 at 10:36:08 AM UTC-5, Thorsten Altenkirch 
wrote:
>
> Why do I need to understand objects to understand elements?
>

As a user of Nuprl, you don't. Objects give you a new way to reason, which 
you don't have to use. You would only need to understand the object-based 
semantics of types to fully understand the language.

Why do I have to capture all possible constructions if I just want to talk 
> about some specific ones?
>

I don't understand this.

This is something that irritates me about set theory: if I want to say for 
> all natural numbers …, I am actually saying for all sets which turn out to 
> be natural numbers… At least conceptually this is rubbish. Who thinks like 
> this?
>

This doesn't seem to have anything to do with Nuprl. In Nuprl, saying for 
all natural numbers is a Pi type with domain nat, as usual.

Yes and in computer science we think about types sorting untyped programs. 
> But why?
>

Some computer scientists like untyped programs.

Do you understand the untyped lambda calculus?
>

Yeah, I'd say so.

It took Dana Scott a while to come up with a mathematical semantics.
>

Because understanding this connection between computation and math turned 
out to be much harder than understanding computation on its own, 
operationally. Before denotational models, the untyped lambda calculus was 
already well-understood operationally. Scott deepened our understanding of 
it, and of general recursive types more generally. It's not all or nothing.

I think we should put our mouth where our heart is. Typed objects are 
> easier to understand, they make sense by themselves so lets refer to them. 
> Yes we implement them based in intyped things, trees, strings, bit 
> sequences but we don’t need low level concepts to understand high level 
> concepts!! Yes we need them to implement them but this is another issue.
>

I truly believe that it's useful for the type system to let users reason 
about the implementation of typed elements in terms of untyped or 
less-typed objects. This is refinement typing, and it's not just Nuprl vs 
the world.

-- 
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 #1.2: Type: text/html, Size: 4239 bytes --]

^ permalink raw reply	[flat|nested] 71+ messages in thread

* Re: [HoTT] Re: Why do we need judgmental equality?
  2019-02-12  9:01                     ` Matt Oliveri
@ 2019-02-12 17:54                       ` Michael Shulman
  2019-02-13  6:37                         ` Matt Oliveri
  0 siblings, 1 reply; 71+ messages in thread
From: Michael Shulman @ 2019-02-12 17:54 UTC (permalink / raw)
  To: Matt Oliveri; +Cc: Homotopy Type Theory

For sure definitional equality doesn't have to do with models.  Like
all the kinds of equality we are discussing, it is a syntactic notion.
Actually I would say it is a *philosophical* notion, and as such is
imprecisely specified; syntactic notions like judgmental equality can
do a better or worse job of capturing it in different theories (and in
some cases may not even be intended to capture it at all).

> what's the difference between "denoting by definition" and regular denoting?

x+(y+z) and (x+y)+z denote the same natural number for any natural
numbers x,y,z, because we can prove that they are equal.  But they
don't denote the same natural number *by definition*, because this
proof is not just unfolding the meanings of definitions; it involves
at least a little thought and a pair of inductions.

For a more radical example, "1+1=2" and "there do not exist positive
integers x,y,z,n with n>2 and x^n+y^n=z^n" denote the same
proposition, namely "true".  But that's certainly not the case by
definition!  Same reference; different senses.

-- 
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.

^ permalink raw reply	[flat|nested] 71+ messages in thread

* Re: [HoTT] Re: Why do we need judgmental equality?
  2019-02-12 17:54                       ` Michael Shulman
@ 2019-02-13  6:37                         ` Matt Oliveri
  2019-02-13 10:01                           ` Ansten Mørch Klev
  0 siblings, 1 reply; 71+ messages in thread
From: Matt Oliveri @ 2019-02-13  6:37 UTC (permalink / raw)
  To: Homotopy Type Theory


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

OK. So it sounds like definitional equality is another way of thinking 
about equality of sense, and is generally not the same as strict equality. 
That's a relief.

But the use of judgmental equality for capturing a system of paths that's 
fully coherent is actually about strict equality, in general; not 
necessarily judgmental or definitional equality.

So to bring things back to HoTT, what are people's opinions about the best 
use of these three equalities?

My opinion is that strict equality should be implemented as judgmental 
equality, which should be richer than definitional equality, by using a 
2-level system with reflective equality. This is the case in HTS and 
computational higher dimensional type theory. We would still probably want 
to consider different theories of strict equality, but there would be no 
obligation to implement them as equality algorithms. Definitional equality 
would be a quite separate issue, pertaining to proof automation.

On Tuesday, February 12, 2019 at 12:54:24 PM UTC-5, Michael Shulman wrote:
>
> For sure definitional equality doesn't have to do with models.  Like 
> all the kinds of equality we are discussing, it is a syntactic notion. 
> Actually I would say it is a *philosophical* notion, and as such is 
> imprecisely specified; syntactic notions like judgmental equality can 
> do a better or worse job of capturing it in different theories (and in 
> some cases may not even be intended to capture it at all). 
>
> > what's the difference between "denoting by definition" and regular 
> denoting? 
>
> x+(y+z) and (x+y)+z denote the same natural number for any natural 
> numbers x,y,z, because we can prove that they are equal.  But they 
> don't denote the same natural number *by definition*, because this 
> proof is not just unfolding the meanings of definitions; it involves 
> at least a little thought and a pair of inductions. 
>
> For a more radical example, "1+1=2" and "there do not exist positive 
> integers x,y,z,n with n>2 and x^n+y^n=z^n" denote the same 
> proposition, namely "true".  But that's certainly not the case by 
> definition!  Same reference; different senses. 
>

-- 
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 #1.2: Type: text/html, Size: 2907 bytes --]

^ permalink raw reply	[flat|nested] 71+ messages in thread

* Re: [HoTT] Re: Why do we need judgmental equality?
  2019-02-13  6:37                         ` Matt Oliveri
@ 2019-02-13 10:01                           ` Ansten Mørch Klev
  0 siblings, 0 replies; 71+ messages in thread
From: Ansten Mørch Klev @ 2019-02-13 10:01 UTC (permalink / raw)
  To: Matt Oliveri; +Cc: Homotopy Type Theory

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

I would object to the characterization of definitional identity as identity
of sense. Sense is often glossed as mode of givenness; or one might say
that the sense of an expression determines a route to its reference. Now
take terms such as 7+5 and 9+3. These are definitionally identical, but
they present the number twelve in different ways; qua senses each
determines a different route to ssssssssssss(0). Hence they are not the
same senses. Identity of sense is, to my mind, a stricter relation than
definitional identity.

Very often, also in this thread, the notions of judgemental identity and
definitional identity seem to be treated as one and the same thing. But by
judgemental identity we should mean a certain form of identity assertion
that is different from the assertion that an identity proposition/type is
true/inhabited; and by definitional identity we should mean one among
several relations on terms that may properly be called a relation of
identity.

Here is an argument for the need of a form of identity assertion other than
p : Id(A,a,b). The proposition Id(A,a,b) is formed by applying the function
Id to the type of individuals (set in Martin-Löf's terminology) A, and the
elements a,b : A. The notion of a function, however, presupposes a notion
of identity: f is a function only if, when applied to identical arguments
a, b, we get identical results f(a), f(b). On pain of circularity, the
notion of identity appealed to here cannot be propositional identity.
A notion of identity is also implicit in the notion of domain presupposed
by the notion of a function: f is a function from the domain A to the
domain B. To have the right to speak of A as a domain we need to know what
it is for elements of A to be identical, we need to know a criterion of
identity for A.

In type theory the alternative form of identity assertion, used for
instance in the explanation of what a function is, is the identity
judgement a = b : A. There is nothing in the argument just given that
forces the relation picked out by this form of identity assertion to be
definitional identity; but there may be other arguments why such an
interpretation is preferable.





On Wed, Feb 13, 2019 at 7:37 AM Matt Oliveri <atmacen@gmail.com> wrote:

> OK. So it sounds like definitional equality is another way of thinking
> about equality of sense, and is generally not the same as strict equality.
> That's a relief.
>
> But the use of judgmental equality for capturing a system of paths that's
> fully coherent is actually about strict equality, in general; not
> necessarily judgmental or definitional equality.
>
> So to bring things back to HoTT, what are people's opinions about the best
> use of these three equalities?
>
> My opinion is that strict equality should be implemented as judgmental
> equality, which should be richer than definitional equality, by using a
> 2-level system with reflective equality. This is the case in HTS and
> computational higher dimensional type theory. We would still probably want
> to consider different theories of strict equality, but there would be no
> obligation to implement them as equality algorithms. Definitional equality
> would be a quite separate issue, pertaining to proof automation.
>
> On Tuesday, February 12, 2019 at 12:54:24 PM UTC-5, Michael Shulman wrote:
>>
>> For sure definitional equality doesn't have to do with models.  Like
>> all the kinds of equality we are discussing, it is a syntactic notion.
>> Actually I would say it is a *philosophical* notion, and as such is
>> imprecisely specified; syntactic notions like judgmental equality can
>> do a better or worse job of capturing it in different theories (and in
>> some cases may not even be intended to capture it at all).
>>
>> > what's the difference between "denoting by definition" and regular
>> denoting?
>>
>> x+(y+z) and (x+y)+z denote the same natural number for any natural
>> numbers x,y,z, because we can prove that they are equal.  But they
>> don't denote the same natural number *by definition*, because this
>> proof is not just unfolding the meanings of definitions; it involves
>> at least a little thought and a pair of inductions.
>>
>> For a more radical example, "1+1=2" and "there do not exist positive
>> integers x,y,z,n with n>2 and x^n+y^n=z^n" denote the same
>> proposition, namely "true".  But that's certainly not the case by
>> definition!  Same reference; different senses.
>>
> --
> 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.

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

^ permalink raw reply	[flat|nested] 71+ messages in thread

* Re: [HoTT] Re: Why do we need judgmental equality?
  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
  1 sibling, 1 reply; 71+ messages in thread
From: Thorsten Altenkirch @ 2019-02-16 15:59 UTC (permalink / raw)
  To: Anders Mörtberg, Homotopy Type Theory

[-- 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 --]

^ permalink raw reply	[flat|nested] 71+ messages in thread

* Re: [HoTT] Re: Why do we need judgmental equality?
  2019-02-16 15:59     ` Thorsten Altenkirch
@ 2019-02-17  1:25       ` Michael Shulman
  2019-02-17  7:56         ` Thorsten Altenkirch
                           ` (2 more replies)
  0 siblings, 3 replies; 71+ messages in thread
From: Michael Shulman @ 2019-02-17  1:25 UTC (permalink / raw)
  To: Homotopy Type Theory

The supposed arbitrariness of some types having strict eta and others
not has been mentioned at least twice.  However, I don't find it
arbitrary at all: *negative* types have strict eta, while positive
types don't.  Since negative types are determined by maps *in*, all of
their elements, identifications, and so on are determined directly,
and strictly; whereas positive types are determined by maps *out*, and
in particular their higher groupoid structure must be freely generated
for some sense of "free", giving rise to lots of scope for flabbiness.
It's quite common in higher category theory for "semi-strictified
objects" to admit some strict limits and other "mapping in" universal
properties (e.g. the category of algebras and pseudomorphisms for a
2-monad has strict PIE-limits, the category of fibrant objects in a
model category has strict pullbacks of fibrations, etc.), but much
rarer for them to have strict colimits and other "mapping out"
universal properties.

In particular, the difference in whether Sigma-types have strict eta
or not simply lies in whether we are talking about positive
Sigma-types or negative Sigma-types, which are different things, even
though they turn out to be equivalent.  Type theorists and logicians
are familiar by now with the fact that positive and negative binary
products / conjunctions are different things, even though they happen
to be equivalent in "cartesian" type theory and logic, because they
can be disentangled in linear logic.  I don't know whether any kind of
"linear dependent type theory" can disentangle positive and negative
Sigma-types, but both syntactically and semantically it still makes
sense to me to consider them as different things that just happen to
be equivalent.  It also happens sometimes in category theory that a
limit and a colimit coincide (e.g. split idempotents, biproducts in an
additive category, etc.
https://ncatlab.org/nlab/show/absolute+colimit); but depending on
whether we consider them as a limit or a colimit, it's natural that we
might get different amounts of strictness.

On Sat, Feb 16, 2019 at 7:59 AM Thorsten Altenkirch
<Thorsten.Altenkirch@nottingham.ac.uk> wrote:
>
> 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.
> 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.

^ permalink raw reply	[flat|nested] 71+ messages in thread

* Re: [HoTT] Re: Why do we need judgmental equality?
  2019-02-17  1:25       ` Michael Shulman
@ 2019-02-17  7:56         ` Thorsten Altenkirch
  2019-02-17  9:14           ` Matt Oliveri
                             ` (2 more replies)
  2019-02-17  9:05         ` Matt Oliveri
  2019-02-17 13:29         ` Nicolai Kraus
  2 siblings, 3 replies; 71+ messages in thread
From: Thorsten Altenkirch @ 2019-02-17  7:56 UTC (permalink / raw)
  To: Michael Shulman, Homotopy Type Theory; +Cc: agda list

On 17/02/2019, 01:25, "homotopytypetheory@googlegroups.com on behalf of Michael Shulman" <homotopytypetheory@googlegroups.com on behalf of shulman@sandiego.edu> wrote:

    However, I don't find it
    arbitrary at all: *negative* types have strict eta, while positive
    types don't.

This is a very good point. However Streams are negative types but for example agda doesn't use eta conversion on them, I think for a good reason. Actually I am not completely sure whether this is undecidable.

E.g. the following equation cannot be proven using refl (it can be proven in cubical agda btw). The corresponding equation for Sigma types holds definitionally.

infix 5 _∷_

record Stream (A : Set) : Set where
  constructor _∷_
  coinductive
  field
    hd : A
    tl : Stream A

open Stream
etaStream : {A : Set}{s : Stream A} → hd s ∷ tl s ≡ s
etaStream = {!refl!}

CCed to the agda list. Maybe somebody can comment on the decidabilty status?




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.

^ permalink raw reply	[flat|nested] 71+ messages in thread

* Re: [HoTT] Re: Why do we need judgmental equality?
  2019-02-17  1:25       ` Michael Shulman
  2019-02-17  7:56         ` Thorsten Altenkirch
@ 2019-02-17  9:05         ` Matt Oliveri
  2019-02-17 13:29         ` Nicolai Kraus
  2 siblings, 0 replies; 71+ messages in thread
From: Matt Oliveri @ 2019-02-17  9:05 UTC (permalink / raw)
  To: Homotopy Type Theory


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

What about strict uniqueness for the empty type? In general, what about the 
"discrete" inductive types of computational HDTT, including HTS-style 
natural numbers? I understand that this is not something we expect all 
models to have, but they're useful when available, and they have strict 
extensionality.

On Saturday, February 16, 2019 at 8:25:43 PM UTC-5, Michael Shulman wrote:
>
> The supposed arbitrariness of some types having strict eta and others 
> not has been mentioned at least twice.  However, I don't find it 
> arbitrary at all: *negative* types have strict eta, while positive 
> types don't.  ...
>

-- 
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 #1.2: Type: text/html, Size: 1269 bytes --]

^ permalink raw reply	[flat|nested] 71+ messages in thread

* Re: [HoTT] Re: Why do we need judgmental equality?
  2019-02-17  7:56         ` Thorsten Altenkirch
@ 2019-02-17  9:14           ` Matt Oliveri
  2019-02-17  9:18           ` Michael Shulman
  2019-02-17 14:22           ` [Agda] " Andreas Abel
  2 siblings, 0 replies; 71+ messages in thread
From: Matt Oliveri @ 2019-02-17  9:14 UTC (permalink / raw)
  To: Homotopy Type Theory


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

(Since I've already made such a fuss about Nuprl anyway...)

Nuprl has a type of streams (of whatever) up to bisimilarity. That is, 
bisimilar streams are judgmentally equal. Bisimilarity of bit streams is 
already undecidable. This is essentially the same problem as extensional 
equality of functions (nat->bool). I think eta *reduction* of streams would 
be OK to throw in, but it won't get you strict extensionality.

On Sunday, February 17, 2019 at 2:56:40 AM UTC-5, Thorsten Altenkirch wrote:
>
> On 17/02/2019, 01:25, "homotopyt...@googlegroups.com <javascript:> on 
> behalf of Michael Shulman" <homotopyt...@googlegroups.com <javascript:> 
> on behalf of shu...@sandiego.edu <javascript:>> wrote: 
>
>     However, I don't find it 
>     arbitrary at all: *negative* types have strict eta, while positive 
>     types don't. 
>
> This is a very good point. However Streams are negative types but for 
> example agda doesn't use eta conversion on them, I think for a good reason. 
> Actually I am not completely sure whether this is undecidable. 
>
> E.g. the following equation cannot be proven using refl (it can be proven 
> in cubical agda btw). The corresponding equation for Sigma types holds 
> definitionally. 
>
> infix 5 _∷_ 
>
> record Stream (A : Set) : Set where 
>   constructor _∷_ 
>   coinductive 
>   field 
>     hd : A 
>     tl : Stream A 
>
> open Stream 
> etaStream : {A : Set}{s : Stream A} → hd s ∷ tl s ≡ s 
> etaStream = {!refl!} 
>
> CCed to the agda list. Maybe somebody can comment on the decidabilty 
> status? 
>
>

-- 
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 #1.2: Type: text/html, Size: 2913 bytes --]

^ permalink raw reply	[flat|nested] 71+ messages in thread

* Re: [HoTT] Re: Why do we need judgmental equality?
  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 12:08             ` Matt Oliveri
  2019-02-17 14:22           ` [Agda] " Andreas Abel
  2 siblings, 2 replies; 71+ messages in thread
From: Michael Shulman @ 2019-02-17  9:18 UTC (permalink / raw)
  To: Thorsten Altenkirch; +Cc: Homotopy Type Theory, agda list

Well, I'm not really convinced that coinductive types should be
treated as basic type formers, rather than simply constructed out of
inductive types and extensional functions.  For one thing, I have no
idea how to construct coinductive types as basic type formers in
homotopical models.  I think the issue that you raise, Thorsten, could
be regarded as another argument against treating them basically, or at
least against regarding them as really "negative" in the same way that
Pis and (negative) Sigmas are.

And as for adding random extra strict equalities pertaining certain
positive types that happen to hold in some particular model, Matt, I
would say similarly that the general perspective gives yet another
reason why you shouldn't do that.  (-:

But the real point is that the general perspective I was proposing
doesn't claim to be the *only* way to do things; obviously it isn't.
It's just a non-arbitrary "baseline" that is consistent and makes
sense and matches a common core of equalities used in many type
theories, so that when you deviate from it you're aware that you're
being deviant.  (-:

On Sat, Feb 16, 2019 at 11:56 PM Thorsten Altenkirch
<Thorsten.Altenkirch@nottingham.ac.uk> wrote:
>
> On 17/02/2019, 01:25, "homotopytypetheory@googlegroups.com on behalf of Michael Shulman" <homotopytypetheory@googlegroups.com on behalf of shulman@sandiego.edu> wrote:
>
>     However, I don't find it
>     arbitrary at all: *negative* types have strict eta, while positive
>     types don't.
>
> This is a very good point. However Streams are negative types but for example agda doesn't use eta conversion on them, I think for a good reason. Actually I am not completely sure whether this is undecidable.
>
> E.g. the following equation cannot be proven using refl (it can be proven in cubical agda btw). The corresponding equation for Sigma types holds definitionally.
>
> infix 5 _∷_
>
> record Stream (A : Set) : Set where
>   constructor _∷_
>   coinductive
>   field
>     hd : A
>     tl : Stream A
>
> open Stream
> etaStream : {A : Set}{s : Stream A} → hd s ∷ tl s ≡ s
> etaStream = {!refl!}
>
> CCed to the agda list. Maybe somebody can comment on the decidabilty status?
>
>
>
>
> 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.

^ permalink raw reply	[flat|nested] 71+ messages in thread

* Re: [HoTT] Re: Why do we need judgmental equality?
  2019-02-17  9:18           ` Michael Shulman
@ 2019-02-17 10:52             ` Thorsten Altenkirch
  2019-02-17 11:35               ` streicher
  2019-02-17 12:08             ` Matt Oliveri
  1 sibling, 1 reply; 71+ messages in thread
From: Thorsten Altenkirch @ 2019-02-17 10:52 UTC (permalink / raw)
  To: Michael Shulman; +Cc: Homotopy Type Theory, agda list

For me the idea of inductive vs coinductive or how I called this a while ago data vs codata is an important basic intuition which comes before formal model constructions. Types are defined by constructors or by destructors, eg coproducts are defined by constructors while functions are defined by destructors, namely application. That is a function is something you can apply to arguments obtaining a result. Lambda is a derived construction, I can construct a function if I have a method to compute the result. Similarily natural numbers and lists are given by constructors, while streams are defined by destructors, to give a stream means to be able to say what its head and its tail are. And that is perfectly right Sigma types can be either given by a constructor or by destructors so in this sense they are twitters. 

There are reductions which just means that certain type formers are universal in that we can define all other from them, e.g. function types together with some inductive types are sufficient to derive a certain class of codata types. That doesn't mean that the dichotomy between data and codata isn't an important basic intuition.

On 17/02/2019, 09:19, "Michael Shulman" <shulman@sandiego.edu> wrote:

    Well, I'm not really convinced that coinductive types should be
    treated as basic type formers, rather than simply constructed out of
    inductive types and extensional functions.  For one thing, I have no
    idea how to construct coinductive types as basic type formers in
    homotopical models.  I think the issue that you raise, Thorsten, could
    be regarded as another argument against treating them basically, or at
    least against regarding them as really "negative" in the same way that
    Pis and (negative) Sigmas are.
    
    And as for adding random extra strict equalities pertaining certain
    positive types that happen to hold in some particular model, Matt, I
    would say similarly that the general perspective gives yet another
    reason why you shouldn't do that.  (-:
    
    But the real point is that the general perspective I was proposing
    doesn't claim to be the *only* way to do things; obviously it isn't.
    It's just a non-arbitrary "baseline" that is consistent and makes
    sense and matches a common core of equalities used in many type
    theories, so that when you deviate from it you're aware that you're
    being deviant.  (-:
    
    On Sat, Feb 16, 2019 at 11:56 PM Thorsten Altenkirch
    <Thorsten.Altenkirch@nottingham.ac.uk> wrote:
    >
    > On 17/02/2019, 01:25, "homotopytypetheory@googlegroups.com on behalf of Michael Shulman" <homotopytypetheory@googlegroups.com on behalf of shulman@sandiego.edu> wrote:
    >
    >     However, I don't find it
    >     arbitrary at all: *negative* types have strict eta, while positive
    >     types don't.
    >
    > This is a very good point. However Streams are negative types but for example agda doesn't use eta conversion on them, I think for a good reason. Actually I am not completely sure whether this is undecidable.
    >
    > E.g. the following equation cannot be proven using refl (it can be proven in cubical agda btw). The corresponding equation for Sigma types holds definitionally.
    >
    > infix 5 _∷_
    >
    > record Stream (A : Set) : Set where
    >   constructor _∷_
    >   coinductive
    >   field
    >     hd : A
    >     tl : Stream A
    >
    > open Stream
    > etaStream : {A : Set}{s : Stream A} → hd s ∷ tl s ≡ s
    > etaStream = {!refl!}
    >
    > CCed to the agda list. Maybe somebody can comment on the decidabilty status?
    >
    >
    >
    >
    > 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.
    




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.

^ permalink raw reply	[flat|nested] 71+ messages in thread

* Re: [HoTT] Re: Why do we need judgmental equality?
  2019-02-17 10:52             ` Thorsten Altenkirch
@ 2019-02-17 11:35               ` streicher
  2019-02-17 11:44                 ` Thorsten Altenkirch
  0 siblings, 1 reply; 71+ messages in thread
From: streicher @ 2019-02-17 11:35 UTC (permalink / raw)
  To: Thorsten Altenkirch; +Cc: Michael Shulman, Homotopy Type Theory, agda list

> For me the idea of inductive vs coinductive or how I called this a while
> ago data vs codata is an important basic intuition which comes before
> formal model constructions. Types are defined by constructors or by
> destructors, eg coproducts are defined by constructors while functions are
> defined by destructors, namely application. That is a function is
> something you can apply to arguments obtaining a result. Lambda is a
> derived construction, I can construct a function if I have a method to
> compute the result. Similarily natural numbers and lists are given by
> constructors, while streams are defined by destructors, to give a stream
> means to be able to say what its head and its tail are. And that is
> perfectly right Sigma types can be either given by a constructor or by
> destructors so in this sense they are twitters.
>
> There are reductions which just means that certain type formers are
> universal in that we can define all other from them, e.g. function types
> together with some inductive types are sufficient to derive a certain
> class of codata types. That doesn't mean that the dichotomy between data
> and codata isn't an important basic intuition.
>
> On 17/02/2019, 09:19, "Michael Shulman" <shulman@sandiego.edu> wrote:
>
>     Well, I'm not really convinced that coinductive types should be
>     treated as basic type formers, rather than simply constructed out of
>     inductive types and extensional functions.  For one thing, I have no
>     idea how to construct coinductive types as basic type formers in
>     homotopical models.  I think the issue that you raise, Thorsten, could
>     be regarded as another argument against treating them basically, or at
>     least against regarding them as really "negative" in the same way that
>     Pis and (negative) Sigmas are.
>
>     And as for adding random extra strict equalities pertaining certain
>     positive types that happen to hold in some particular model, Matt, I
>     would say similarly that the general perspective gives yet another
>     reason why you shouldn't do that.  (-:
>

But function types are neither inductive nor conductive. Only N-> (-) ist
coinductive.
In presence of function types most coinductive types can be implemented.

Maybe coinductive is a style of programming but nothing really foundational.

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 HomotopyTypeTheory+unsubscribe@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

^ permalink raw reply	[flat|nested] 71+ messages in thread

* Re: [HoTT] Re: Why do we need judgmental equality?
  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
  0 siblings, 2 replies; 71+ messages in thread
From: Thorsten Altenkirch @ 2019-02-17 11:44 UTC (permalink / raw)
  To: streicher; +Cc: Michael Shulman, Homotopy Type Theory, agda list


    
    But function types are neither inductive nor conductive. Only N-> (-) ist
    coinductive.
    In presence of function types most coinductive types can be implemented.
    
You think of terminal coalgebras - that is not what I mean. To avoid this confusion I am using the term codata but most people in CS understand coinductive better. You can define a type by saying how elements can be constructed, this is data Alternatively you say what you can do with it, i.e. how elements can be destructed. The function type is not data, functions are not understood by the way they are constructed but what you can do with it. A function is something you can apply to an argument and you get a result. Codata types always introduce non-trivial equalities, because all you can do with a function is applying it to arguments two functions which provide the same output for all inputs are equal. Hence functional extensionality should hold.

    Maybe coinductive is a style of programming but nothing really foundational.

I think you miss something important here.




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.

^ permalink raw reply	[flat|nested] 71+ messages in thread

* Re: [HoTT] Re: Why do we need judgmental equality?
  2019-02-17  9:18           ` Michael Shulman
  2019-02-17 10:52             ` Thorsten Altenkirch
@ 2019-02-17 12:08             ` Matt Oliveri
  2019-02-17 12:13               ` Matt Oliveri
  2019-02-20  0:22               ` Michael Shulman
  1 sibling, 2 replies; 71+ messages in thread
From: Matt Oliveri @ 2019-02-17 12:08 UTC (permalink / raw)
  To: Homotopy Type Theory


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

What about infinitary (non-elementary) limits? Are there infinitary 
homotopy-limits? They are more common than discrete inductive types, right? 
So what if I considered a stream of A to be essentially an omega-fold 
product of A. Would that have a strict extensionality principle?

More generally, I would try and say that a coinductive type is some limit 
of an external diagram of elimination spines. This might address Thomas 
Streicher's objection, since the collection of elimination spines is 
countable externally.

On Sunday, February 17, 2019 at 4:19:01 AM UTC-5, Michael Shulman wrote:
>
> Well, I'm not really convinced that coinductive types should be 
> treated as basic type formers, rather than simply constructed out of 
> inductive types and extensional functions.  For one thing, I have no 
> idea how to construct coinductive types as basic type formers in 
> homotopical models.  I think the issue that you raise, Thorsten, could 
> be regarded as another argument against treating them basically, or at 
> least against regarding them as really "negative" in the same way that 
> Pis and (negative) Sigmas are. 
>
> And as for adding random extra strict equalities pertaining certain 
> positive types that happen to hold in some particular model, Matt, I 
> would say similarly that the general perspective gives yet another 
> reason why you shouldn't do that.  (-: 
>
> But the real point is that the general perspective I was proposing 
> doesn't claim to be the *only* way to do things; obviously it isn't. 
> It's just a non-arbitrary "baseline" that is consistent and makes 
> sense and matches a common core of equalities used in many type 
> theories, so that when you deviate from it you're aware that you're 
> being deviant.  (-: 
>
> On Sat, Feb 16, 2019 at 11:56 PM Thorsten Altenkirch 
> <Thorsten....@nottingham.ac.uk <javascript:>> wrote: 
> > 
> > On 17/02/2019, 01:25, "homotopyt...@googlegroups.com <javascript:> on 
> behalf of Michael Shulman" <homotopyt...@googlegroups.com <javascript:> 
> on behalf of shu...@sandiego.edu <javascript:>> wrote: 
> > 
> >     However, I don't find it 
> >     arbitrary at all: *negative* types have strict eta, while positive 
> >     types don't. 
> > 
> > This is a very good point. However Streams are negative types but for 
> example agda doesn't use eta conversion on them, I think for a good reason. 
> Actually I am not completely sure whether this is undecidable. 
> > 
> > E.g. the following equation cannot be proven using refl (it can be 
> proven in cubical agda btw). The corresponding equation for Sigma types 
> holds definitionally. 
> > 
> > infix 5 _∷_ 
> > 
> > record Stream (A : Set) : Set where 
> >   constructor _∷_ 
> >   coinductive 
> >   field 
> >     hd : A 
> >     tl : Stream A 
> > 
> > open Stream 
> > etaStream : {A : Set}{s : Stream A} → hd s ∷ tl s ≡ s 
> > etaStream = {!refl!} 
> > 
> > CCed to the agda list. Maybe somebody can comment on the decidabilty 
> status? 
>

-- 
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 #1.2: Type: text/html, Size: 4677 bytes --]

^ permalink raw reply	[flat|nested] 71+ messages in thread

* Re: [HoTT] Re: Why do we need judgmental equality?
  2019-02-17 12:08             ` Matt Oliveri
@ 2019-02-17 12:13               ` Matt Oliveri
  2019-02-20  0:22               ` Michael Shulman
  1 sibling, 0 replies; 71+ messages in thread
From: Matt Oliveri @ 2019-02-17 12:13 UTC (permalink / raw)
  To: Homotopy Type Theory


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

On Sunday, February 17, 2019 at 7:08:52 AM UTC-5, Matt Oliveri wrote:
>
> since the collection of elimination spines is countable externally.
>

Oh wait, I guess not.

-- 
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 #1.2: Type: text/html, Size: 822 bytes --]

^ permalink raw reply	[flat|nested] 71+ messages in thread

* Re: [HoTT] Re: Why do we need judgmental equality?
  2019-02-17  1:25       ` Michael Shulman
  2019-02-17  7:56         ` Thorsten Altenkirch
  2019-02-17  9:05         ` Matt Oliveri
@ 2019-02-17 13:29         ` Nicolai Kraus
  2 siblings, 0 replies; 71+ messages in thread
From: Nicolai Kraus @ 2019-02-17 13:29 UTC (permalink / raw)
  To: Michael Shulman; +Cc: Homotopy Type Theory

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

On Sun, Feb 17, 2019 at 1:25 AM Michael Shulman <shulman@sandiego.edu>
wrote:

> The supposed arbitrariness of some types having strict eta and others
> not has been mentioned at least twice.  However, I don't find it
> arbitrary at all [...] In particular, the difference in whether
> Sigma-types have strict eta
> or not simply lies in whether we are talking about positive
> Sigma-types or negative Sigma-types


Since I've mentioned eta for Sigma in this context: thanks for this
explanation, Mike!
-- Nicolai


>

-- 
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: 1440 bytes --]

^ permalink raw reply	[flat|nested] 71+ messages in thread

* Re: [Agda] [HoTT] Re: Why do we need judgmental equality?
  2019-02-17  7:56         ` Thorsten Altenkirch
  2019-02-17  9:14           ` Matt Oliveri
  2019-02-17  9:18           ` Michael Shulman
@ 2019-02-17 14:22           ` Andreas Abel
  2 siblings, 0 replies; 71+ messages in thread
From: Andreas Abel @ 2019-02-17 14:22 UTC (permalink / raw)
  To: Thorsten Altenkirch, Michael Shulman, Homotopy Type Theory; +Cc: agda list

 > CCed to the agda list. Maybe somebody can comment on the decidabilty 
status?

Ulrich Berger and Anton Setzer: Undecidability of Equality for Codata Types

     Talk given at CMCS'18 Thessaloniki, Greece, 15 April 2018

 
http://www.cs.swan.ac.uk/~csetzer/articles/CMCS2018/bergerSetzerProceedingsCMCS18.pdf


On 2019-02-17 08:56, Thorsten Altenkirch wrote:
> On 17/02/2019, 01:25, "homotopytypetheory@googlegroups.com on behalf of Michael Shulman" <homotopytypetheory@googlegroups.com on behalf of shulman@sandiego.edu> wrote:
> 
>      However, I don't find it
>      arbitrary at all: *negative* types have strict eta, while positive
>      types don't.
> 
> This is a very good point. However Streams are negative types but for example agda doesn't use eta conversion on them, I think for a good reason. Actually I am not completely sure whether this is undecidable.
> 
> E.g. the following equation cannot be proven using refl (it can be proven in cubical agda btw). The corresponding equation for Sigma types holds definitionally.
> 
> infix 5 _∷_
> 
> record Stream (A : Set) : Set where
>    constructor _∷_
>    coinductive
>    field
>      hd : A
>      tl : Stream A
> 
> open Stream
> etaStream : {A : Set}{s : Stream A} → hd s ∷ tl s ≡ s
> etaStream = {!refl!}
> 
> CCed to the agda list. Maybe somebody can comment on the decidabilty status?
> 
> 
> 
> 
> 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.
> 
> 
> 
> 
> _______________________________________________
> Agda mailing list
> Agda@lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
> 

-- 
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.

^ permalink raw reply	[flat|nested] 71+ messages in thread

* Re: [HoTT] Re: Why do we need judgmental equality?
  2019-02-17 11:44                 ` Thorsten Altenkirch
@ 2019-02-17 14:24                   ` Bas Spitters
  2019-02-17 19:36                   ` Thomas Streicher
  1 sibling, 0 replies; 71+ messages in thread
From: Bas Spitters @ 2019-02-17 14:24 UTC (permalink / raw)
  To: Thorsten Altenkirch
  Cc: streicher, Michael Shulman, Homotopy Type Theory, agda list

I think Thomas is referring to M-types which can be constructed in
HoTT, moreover, they have the right equality in guarded or cubical
type theory.
I've collected some references here. Please feel free to expand.
https://ncatlab.org/nlab/show/M-type

On Sun, Feb 17, 2019 at 12:44 PM Thorsten Altenkirch
<Thorsten.Altenkirch@nottingham.ac.uk> wrote:
>
>
>
>     But function types are neither inductive nor conductive. Only N-> (-) ist
>     coinductive.
>     In presence of function types most coinductive types can be implemented.
>
> You think of terminal coalgebras - that is not what I mean. To avoid this confusion I am using the term codata but most people in CS understand coinductive better. You can define a type by saying how elements can be constructed, this is data Alternatively you say what you can do with it, i.e. how elements can be destructed. The function type is not data, functions are not understood by the way they are constructed but what you can do with it. A function is something you can apply to an argument and you get a result. Codata types always introduce non-trivial equalities, because all you can do with a function is applying it to arguments two functions which provide the same output for all inputs are equal. Hence functional extensionality should hold.
>
>     Maybe coinductive is a style of programming but nothing really foundational.
>
> I think you miss something important here.
>
>
>
>
> 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.

^ permalink raw reply	[flat|nested] 71+ messages in thread

* Re: [HoTT] Re: Why do we need judgmental equality?
  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
  1 sibling, 1 reply; 71+ messages in thread
From: Thomas Streicher @ 2019-02-17 19:36 UTC (permalink / raw)
  To: Thorsten Altenkirch; +Cc: Michael Shulman, Homotopy Type Theory, agda list

admittedly, by coinductive I understand terminal coalgebra

in MLTT even function types are inductive though that's a bit of
cheating in my eyes

so I must say I don't understand what you mean by codata types
technically

I know positive and negative polarity in the sense of linear logic people
presumably, that'scloser to what you have in mind

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 HomotopyTypeTheory+unsubscribe@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

^ permalink raw reply	[flat|nested] 71+ messages in thread

* Re: [HoTT] Re: Why do we need judgmental equality?
  2019-02-17 19:36                   ` Thomas Streicher
@ 2019-02-17 21:41                     ` Thorsten Altenkirch
  0 siblings, 0 replies; 71+ messages in thread
From: Thorsten Altenkirch @ 2019-02-17 21:41 UTC (permalink / raw)
  To: Thomas Streicher; +Cc: Michael Shulman, Homotopy Type Theory, agda list

I tried to explain in common sense term what is a function? And my answer is that it is something you can apply to an element of the domain and you get an element of the codomain. You don’t know how you can inspect the function that is all you know. Hence the function type is explained by what you can do with it. That’s coastal. Compare this with natural numbers. A natural number is 0 or the successor of a natural number. You explain how to produce them. That’s data. What is a stream? A stream is something you can get the head and the tail of. So that is codata as well.

Sent from my iPhone

> On 17 Feb 2019, at 19:36, Thomas Streicher <streicher@mathematik.tu-darmstadt.de> wrote:
> 
> admittedly, by coinductive I understand terminal coalgebra
> 
> in MLTT even function types are inductive though that's a bit of
> cheating in my eyes
> 
> so I must say I don't understand what you mean by codata types
> technically
> 
> I know positive and negative polarity in the sense of linear logic people
> presumably, that'scloser to what you have in mind
> 
> thomas



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.

^ permalink raw reply	[flat|nested] 71+ messages in thread

* [HoTT] Re: Why do we need judgmental equality?
  2019-02-08 21:19 ` Martín Hötzel Escardó
                     ` (3 preceding siblings ...)
  2019-02-09 11:57   ` Felix Rech
@ 2019-02-18 17:37   ` Martín Hötzel Escardó
  2019-02-18 19:22     ` Licata, Dan
  4 siblings, 1 reply; 71+ messages in thread
From: Martín Hötzel Escardó @ 2019-02-18 17:37 UTC (permalink / raw)
  To: Homotopy Type Theory


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

On Friday, 8 February 2019 21:19:24 UTC, Martín Hötzel Escardó wrote:
>
>  why is it claimed that definitional equalities are essential to dependent 
> type theories?
>

I've tested what happens if we replace definitional/judgmental
equalities in MLTT by identity types, working in the fragment of Agda 
that only has Π and universes (built-in) and hence my Π has its usual 
judgemental rules, including the η rule (but this rule could be disabled).

In order to switch off definitional equalities for the identity type
and Σ types, I work with them given as hypothetical arguments to a module
(and no hence with no definitions):

  _≡_ : {X : 𝓤} → X → X → 𝓤        -- Identity type.

  refl : {X : 𝓤} (x : X) → x ≡ x

  J : {X : 𝓤} (x : X) (A : (y : X) → x ≡ y → 𝓤)
    → A x (refl x) → (y : X) (r : x ≡ y) → A y r

  J-comp : {X : 𝓤} (x : X) (A : (y : X) → x ≡ y → 𝓤)
            → (a : A x (refl x)) → J x A a x (refl x) ≡ a

  Σ : {X : 𝓤} → (X → 𝓤) → 𝓤

  _,_ : {X : 𝓤} {Y : X → 𝓤} (x : X) → Y x → Σ Y

  Σ-elim : {X : 𝓤} {Y : X → 𝓤} {A : Σ Y → 𝓤}
         → ((x : X) (y : Y x) → A (x , y))
         → (z : Σ Y) → A z

  Σ-comp : {X : 𝓤} {Y : X → 𝓤} {A : Σ Y → 𝓤}
         → (f : (x : X) (y : Y x) → A (x , y))
         → (x : X)
         → (y : Y x)
         → Σ-elim f (x , y) ≡ f x y

Everything I try to do with the identity type just works, including
the more advanced things of univalent mathematics - but obviously I
haven't tried everything that can be tried.

However, although I can define both projections pr₁ and pr₂ for Σ, and
prove the η-rule σ ≡ (pr₁ σ , pr₂ σ), I get

 p : pr₁ (x , y) ≡ x

but only

     pr₂ (x , y) ≡ transport Y (p ⁻¹) y

It doesn't seem to be possible to get pr₂ (x , y) ≡ y without further
assumptions. But maybe I overlooked something.

One idea, which I haven't tested, is to replace Σ-elim and Σ-comp by
the the single axiom

  Σ-single :
      {X : 𝓤} {Y : X → 𝓤} (A : Σ Y → 𝓤)
    → (f : (x : X) (y : Y x) → A (x , y))
    → is-contr (Σ λ (g : (z : Σ Y) → A z)
                       → (x : X) (y : Y x) → g (x , y) ≡ f x y)

I don't know whether this works. (I suspect the fact that "induction
principles ≃ contractibility of the given data with their computation
rules" is valid only in the presence of definitional equalities for
the induction principle, and that the contractibility version has a
better chance to work in the absence of definitional equalities.)

One can also wonder whether the presentation taking the projections
with their computation rules as primitive, and the η rule would
work. But again we can define Σ-elim but not Σ-comp for it.

In any case, without further identities, simply replacing definitional
equalities by identity types doesn't seem to work, although I may be 
missing something.

Martin



-- 
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 #1.2: Type: text/html, Size: 4621 bytes --]

^ permalink raw reply	[flat|nested] 71+ messages in thread

* Re: [HoTT] Re: Why do we need judgmental equality?
  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ó
  0 siblings, 1 reply; 71+ messages in thread
From: Licata, Dan @ 2019-02-18 19:22 UTC (permalink / raw)
  To: Martín Hötzel Escardó; +Cc: Homotopy Type Theory

Hi,

I’m confused — does it even type check to ask  pr₂ (x , y) ≡ y ?

I would expect 

x : A
y : B(x)
(x,y) : Σ A B
fst (x,y) : A
snd (x,y) : B(fst (x,y))

so if beta for fst is weak, then

pr₂ (x , y) ≡ transport Y (p ⁻¹) y

is the best you could hope for.  I.e., you have a path for the first beta, and a path over it for the second.  

-Dan

> On Feb 18, 2019, at 12:37 PM, Martín Hötzel Escardó <escardo.martin@gmail.com> wrote:
> 
> On Friday, 8 February 2019 21:19:24 UTC, Martín Hötzel Escardó wrote:
>  why is it claimed that definitional equalities are essential to dependent type theories?
> 
> I've tested what happens if we replace definitional/judgmental
> equalities in MLTT by identity types, working in the fragment of Agda 
> that only has Π and universes (built-in) and hence my Π has its usual 
> judgemental rules, including the η rule (but this rule could be disabled).
> 
> In order to switch off definitional equalities for the identity type
> and Σ types, I work with them given as hypothetical arguments to a module
> (and no hence with no definitions):
> 
>   _≡_ : {X : 𝓤} → X → X → 𝓤        -- Identity type.
> 
>   refl : {X : 𝓤} (x : X) → x ≡ x
> 
>   J : {X : 𝓤} (x : X) (A : (y : X) → x ≡ y → 𝓤)
>     → A x (refl x) → (y : X) (r : x ≡ y) → A y r
> 
>   J-comp : {X : 𝓤} (x : X) (A : (y : X) → x ≡ y → 𝓤)
>             → (a : A x (refl x)) → J x A a x (refl x) ≡ a
> 
>   Σ : {X : 𝓤} → (X → 𝓤) → 𝓤
> 
>   _,_ : {X : 𝓤} {Y : X → 𝓤} (x : X) → Y x → Σ Y
> 
>   Σ-elim : {X : 𝓤} {Y : X → 𝓤} {A : Σ Y → 𝓤}
>          → ((x : X) (y : Y x) → A (x , y))
>          → (z : Σ Y) → A z
> 
>   Σ-comp : {X : 𝓤} {Y : X → 𝓤} {A : Σ Y → 𝓤}
>          → (f : (x : X) (y : Y x) → A (x , y))
>          → (x : X)
>          → (y : Y x)
>          → Σ-elim f (x , y) ≡ f x y
> 
> Everything I try to do with the identity type just works, including
> the more advanced things of univalent mathematics - but obviously I
> haven't tried everything that can be tried.
> 
> However, although I can define both projections pr₁ and pr₂ for Σ, and
> prove the η-rule σ ≡ (pr₁ σ , pr₂ σ), I get
> 
>  p : pr₁ (x , y) ≡ x
> 
> but only
> 
>      pr₂ (x , y) ≡ transport Y (p ⁻¹) y
> 
> It doesn't seem to be possible to get pr₂ (x , y) ≡ y without further
> assumptions. But maybe I overlooked something.
> 
> One idea, which I haven't tested, is to replace Σ-elim and Σ-comp by
> the the single axiom
> 
>   Σ-single :
>       {X : 𝓤} {Y : X → 𝓤} (A : Σ Y → 𝓤)
>     → (f : (x : X) (y : Y x) → A (x , y))
>     → is-contr (Σ λ (g : (z : Σ Y) → A z)
>                        → (x : X) (y : Y x) → g (x , y) ≡ f x y)
> 
> I don't know whether this works. (I suspect the fact that "induction
> principles ≃ contractibility of the given data with their computation
> rules" is valid only in the presence of definitional equalities for
> the induction principle, and that the contractibility version has a
> better chance to work in the absence of definitional equalities.)
> 
> One can also wonder whether the presentation taking the projections
> with their computation rules as primitive, and the η rule would
> work. But again we can define Σ-elim but not Σ-comp for it.
> 
> In any case, without further identities, simply replacing definitional
> equalities by identity types doesn't seem to work, although I may be 
> missing something.
> 
> Martin
> 
> 
> 
> 
> -- 
> 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.

^ permalink raw reply	[flat|nested] 71+ messages in thread

* Re: [HoTT] Re: Why do we need judgmental equality?
  2019-02-18 19:22     ` Licata, Dan
@ 2019-02-18 20:23       ` Martín Hötzel Escardó
  0 siblings, 0 replies; 71+ messages in thread
From: Martín Hötzel Escardó @ 2019-02-18 20:23 UTC (permalink / raw)
  To: Homotopy Type Theory


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

Sorry, I was being silly. Martin

On Monday, 18 February 2019 19:22:23 UTC, dlicata wrote:
>
> Hi, 
>
> I’m confused — does it even type check to ask  pr₂ (x , y) ≡ y ? 
>
> I would expect 
>
> x : A 
> y : B(x) 
> (x,y) : Σ A B 
> fst (x,y) : A 
> snd (x,y) : B(fst (x,y)) 
>
> so if beta for fst is weak, then 
>
> pr₂ (x , y) ≡ transport Y (p ⁻¹) y 
>
> is the best you could hope for.  I.e., you have a path for the first beta, 
> and a path over it for the second.   
>
> -Dan 
>
> > On Feb 18, 2019, at 12:37 PM, Martín Hötzel Escardó <
> escardo...@gmail.com <javascript:>> wrote: 
> > 
> > On Friday, 8 February 2019 21:19:24 UTC, Martín Hötzel Escardó wrote: 
> >  why is it claimed that definitional equalities are essential to 
> dependent type theories? 
> > 
> > I've tested what happens if we replace definitional/judgmental 
> > equalities in MLTT by identity types, working in the fragment of Agda 
> > that only has Π and universes (built-in) and hence my Π has its usual 
> > judgemental rules, including the η rule (but this rule could be 
> disabled). 
> > 
> > In order to switch off definitional equalities for the identity type 
> > and Σ types, I work with them given as hypothetical arguments to a 
> module 
> > (and no hence with no definitions): 
> > 
> >   _≡_ : {X : 𝓤} → X → X → 𝓤        -- Identity type. 
> > 
> >   refl : {X : 𝓤} (x : X) → x ≡ x 
> > 
> >   J : {X : 𝓤} (x : X) (A : (y : X) → x ≡ y → 𝓤) 
> >     → A x (refl x) → (y : X) (r : x ≡ y) → A y r 
> > 
> >   J-comp : {X : 𝓤} (x : X) (A : (y : X) → x ≡ y → 𝓤) 
> >             → (a : A x (refl x)) → J x A a x (refl x) ≡ a 
> > 
> >   Σ : {X : 𝓤} → (X → 𝓤) → 𝓤 
> > 
> >   _,_ : {X : 𝓤} {Y : X → 𝓤} (x : X) → Y x → Σ Y 
> > 
> >   Σ-elim : {X : 𝓤} {Y : X → 𝓤} {A : Σ Y → 𝓤} 
> >          → ((x : X) (y : Y x) → A (x , y)) 
> >          → (z : Σ Y) → A z 
> > 
> >   Σ-comp : {X : 𝓤} {Y : X → 𝓤} {A : Σ Y → 𝓤} 
> >          → (f : (x : X) (y : Y x) → A (x , y)) 
> >          → (x : X) 
> >          → (y : Y x) 
> >          → Σ-elim f (x , y) ≡ f x y 
> > 
> > Everything I try to do with the identity type just works, including 
> > the more advanced things of univalent mathematics - but obviously I 
> > haven't tried everything that can be tried. 
> > 
> > However, although I can define both projections pr₁ and pr₂ for Σ, and 
> > prove the η-rule σ ≡ (pr₁ σ , pr₂ σ), I get 
> > 
> >  p : pr₁ (x , y) ≡ x 
> > 
> > but only 
> > 
> >      pr₂ (x , y) ≡ transport Y (p ⁻¹) y 
> > 
> > It doesn't seem to be possible to get pr₂ (x , y) ≡ y without further 
> > assumptions. But maybe I overlooked something. 
> > 
> > One idea, which I haven't tested, is to replace Σ-elim and Σ-comp by 
> > the the single axiom 
> > 
> >   Σ-single : 
> >       {X : 𝓤} {Y : X → 𝓤} (A : Σ Y → 𝓤) 
> >     → (f : (x : X) (y : Y x) → A (x , y)) 
> >     → is-contr (Σ λ (g : (z : Σ Y) → A z) 
> >                        → (x : X) (y : Y x) → g (x , y) ≡ f x y) 
> > 
> > I don't know whether this works. (I suspect the fact that "induction 
> > principles ≃ contractibility of the given data with their computation 
> > rules" is valid only in the presence of definitional equalities for 
> > the induction principle, and that the contractibility version has a 
> > better chance to work in the absence of definitional equalities.) 
> > 
> > One can also wonder whether the presentation taking the projections 
> > with their computation rules as primitive, and the η rule would 
> > work. But again we can define Σ-elim but not Σ-comp for it. 
> > 
> > In any case, without further identities, simply replacing definitional 
> > equalities by identity types doesn't seem to work, although I may be 
> > missing something. 
> > 
> > Martin 
> > 
> > 
> > 
> > 
> > -- 
> > 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 <javascript:>. 
>
> > 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.

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

^ permalink raw reply	[flat|nested] 71+ messages in thread

* Re: [HoTT] Re: Why do we need judgmental equality?
  2019-02-17 12:08             ` Matt Oliveri
  2019-02-17 12:13               ` Matt Oliveri
@ 2019-02-20  0:22               ` Michael Shulman
  1 sibling, 0 replies; 71+ messages in thread
From: Michael Shulman @ 2019-02-20  0:22 UTC (permalink / raw)
  To: Matt Oliveri; +Cc: Homotopy Type Theory

On Sun, Feb 17, 2019 at 4:08 AM Matt Oliveri <atmacen@gmail.com> wrote:
> What about infinitary (non-elementary) limits? Are there infinitary homotopy-limits? They are more common than discrete inductive types, right? So what if I considered a stream of A to be essentially an omega-fold product of A. Would that have a strict extensionality principle?

Yes, that might work.  I think that the last time I thought about
coinductive types in homotopy models I was trying to give them some
kind of dependent coinduction principle.  But if we take seriously the
positive/negative perspective that I advanced before, we would expect
coinductive types to have simply a destructor, a non-dependent
corecursor, a beta-rule for destructing the corecursor, and an
eta-principle saying something like that the endomorphism defined from
the destructor and the corecursor is the identity.  And that would
probably be modeled by the omega-fold product of a type with itself.

More generally, if F is a functor that preserves fibrations, fibrant
objects, and sequential limits (like F(X) = A x X for streams), then
the infinite limit

... -> F(F(F(1))) -> F(F(1)) -> F(1) -> 1

might be a model for the corresponding coinductive type with such an
eta-principle.

So maybe there's nothing wrong with coinductive types as such, and the
point is just that computational considerations like decidability
don't always match up with the principled category-theoretic
explanations.  (-:

> On Sunday, February 17, 2019 at 4:19:01 AM UTC-5, Michael Shulman wrote:
>>
>> Well, I'm not really convinced that coinductive types should be
>> treated as basic type formers, rather than simply constructed out of
>> inductive types and extensional functions.  For one thing, I have no
>> idea how to construct coinductive types as basic type formers in
>> homotopical models.  I think the issue that you raise, Thorsten, could
>> be regarded as another argument against treating them basically, or at
>> least against regarding them as really "negative" in the same way that
>> Pis and (negative) Sigmas are.
>>
>> And as for adding random extra strict equalities pertaining certain
>> positive types that happen to hold in some particular model, Matt, I
>> would say similarly that the general perspective gives yet another
>> reason why you shouldn't do that.  (-:
>>
>> But the real point is that the general perspective I was proposing
>> doesn't claim to be the *only* way to do things; obviously it isn't.
>> It's just a non-arbitrary "baseline" that is consistent and makes
>> sense and matches a common core of equalities used in many type
>> theories, so that when you deviate from it you're aware that you're
>> being deviant.  (-:
>>
>> On Sat, Feb 16, 2019 at 11:56 PM Thorsten Altenkirch
>> <Thorsten....@nottingham.ac.uk> wrote:
>> >
>> > On 17/02/2019, 01:25, "homotopyt...@googlegroups.com on behalf of Michael Shulman" <homotopyt...@googlegroups.com on behalf of shu...@sandiego.edu> wrote:
>> >
>> >     However, I don't find it
>> >     arbitrary at all: *negative* types have strict eta, while positive
>> >     types don't.
>> >
>> > This is a very good point. However Streams are negative types but for example agda doesn't use eta conversion on them, I think for a good reason. Actually I am not completely sure whether this is undecidable.
>> >
>> > E.g. the following equation cannot be proven using refl (it can be proven in cubical agda btw). The corresponding equation for Sigma types holds definitionally.
>> >
>> > infix 5 _∷_
>> >
>> > record Stream (A : Set) : Set where
>> >   constructor _∷_
>> >   coinductive
>> >   field
>> >     hd : A
>> >     tl : Stream A
>> >
>> > open Stream
>> > etaStream : {A : Set}{s : Stream A} → hd s ∷ tl s ≡ s
>> > etaStream = {!refl!}
>> >
>> > CCed to the agda list. Maybe somebody can comment on the decidabilty status?
>
> --
> 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.

^ permalink raw reply	[flat|nested] 71+ messages in thread

end of thread, other threads:[~2019-02-20  0:22 UTC | newest]

Thread overview: 71+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2019-01-30 11:54 [HoTT] Why do we need judgmental equality? 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
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

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).