Identity versus equality

[Ansten Mørch Klev]

The discussion yesterday provides a good occasion for me to pose a question I have long wanted to put to this list: is there a convention generally agreed upon in the HoTT-community for when (if ever) to use 'identity' instead of 'equality'?

Here are some relevant data.

A Germanic equivalent for 'identity' is 'sameness'.

A Germanic equivalent for 'equality' is 'likeness'.

For Aristotle equality means sameness of quantity. This is how one must understand 'equal' in Euclid's Elements, where a triangle may have all sides equal (clearly, they cannot be identical). The axiom in the Elements that has given rise to the term 'Euclidean relation' and which is appealed to in Elements I.1 is phrased in terms of 'equal' rather than 'identical'. 

In Diophantus's Arithmetica, on the other hand, the two terms of an equation are said to be equal, not identical, and this would become the standard terminology in algebra. For instance, the sign '=' was introduced by Robert Recorde as a sign of equality, not as a sign of identity. The explanation for this apparent discrepancy with the Aristotelian/Euclidean terminology might be that when dealing with numbers, equality just is identity, since for two numbers to be identical as to magnitude just is for them to be the same number. Aristotle says as much in Metaphysics M.7. 

Hilbert and Bernays might be one of the few logic books in the modern era to distinguish equality from identity (volume I, chapter 5). 'Equality' is there used for any equivalence relation and glossed as the obtaining of "irgendeine Art von Übereinstimmung". Identity, by contrast, is "Übereinstimmung in jeder Hinsicht", as expressed by indiscernibility within the given language. 

Frege, by contrast, explicitly identifies (sic!) equality with identity, and glosses the latter as sameness or coincidence, in the first footnote to his paper on sense and reference.  Kleene and Church do the same in their famous textbooks: if one looks under 'identity' in the index to any of those books one is referred to 'equality'.  

Clearly the two cannot be assumed to mean the same by analysts who speak of two functions being identically equal!

[Joyal, André]

Dear all,

A few more thoughts.

We all agree that terminology and notation are important.

I love the story of the equality sign = introduced by Robert Recorde (1512-1558).

"because no two things can be more equal than a pair of parallel lines".

It took more than a century before been universally adopted.

René Descartes (1596-1650) used a different symbol  in his work (something like \alpha).

We may ask why Recorde's notation won over Descartes's notation?

Of course, we may never know.

I dare to say that Recorde's notation was *better*.

Among other things, the equality sign = is symmetric:

the expression a=b and b=a are mirror image of each other.

Recorde's motive for introducing the notation was more about

convenience and aesthetic than about philosophy and history.

The notation was gradually adopted because it is simple and useful.

It was not because Recorde was a powerful academic,

since he eventually died in prison.

There is something to learn from the history of the equality sign.

I guess that it can also applied to terminology.

A new notation or terminology has a good chance to be adopted universally

if it is simple and useful, but it may take time.

André

---

From: homotopyt...@googlegroups.com [homotopyt...@googlegroups.com] on behalf of Ansten Mørch Klev [anste...@gmail.com]
Sent: Tuesday, May 05, 2020 4:47 AM
To: HomotopyT...@googlegroups.com
Subject: [HoTT] Identity versus 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 HomotopyTypeThe...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAJHZuqYLY-_DB9uh-0FW0jr2KSoQ%2BpwRGD0PPjq%2BxyQvaJFN2A%40mail.gmail.com.

[Steve Awodey]

Dear Andre’ (and all),

The sign a = b is pretty well established in mathematics as meaning “a equals b”, 

which does indeed clash with our choice in the book to use it for the identity type, 

and to call the elements of this type “identifications”.  

Thorsten has rightly pointed out this clash.

Although I am personally not eager to make any changes in our current terminology and/or notation, 

I’m certainly glad to consider the possibiiy 

(we did agree to return to this question at some point, so maybe this is it : - ).

We need both symbols and words for two notions:

- judgemental equality, currently a\equiv b, 

- propositional equality, currently a = b, short for Id(a,b).

There seems to be a proposal to revise this to something like:

- judgemental equality: written a = b and pronounced “a equals b”,

- propositional equality, written maybe a \cong b, and pronunced ”a iso b”,

(the elements of this type are called “isos").

Another (partial) option would be:

- judgemental equality: written a = b and pronounced “a equals b”,

- propositional equality, written Id(a,b) and shortened somehow a ? b, 

and pronunced ”a idenitfied with b” 

(the elements of this type are called “identifications").

Do either of these seem preferable?

Are there other proposals?

And how should one decide?

Regards,

Steve

To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/8C57894C7413F04A98DDF5629FEC90B1652F515E%40Pli.gst.uqam.ca.

[Michael Shulman]

As I've said before, I strongly disagree that the standard
interpretation of "a=b" as meaning "a equals b" clashes in any way
with its use to denote the identity type. Almost without exception,
whenever a mathematican working informally says "equals", that *must*
be formalized as referring to the identity type. Ask any
mathematician on the street whether x+y=y+x for all natural numbers x
and y, and they will say yes. But this is false if = means judgmental
equality. Judgmental equality is a technical object of type theory
that the "generic mathematician" is not aware of at all, so it cannot
co-opt the standard notation "=" or word "equals" if we want "informal
type theory" to be at all comprehensible to such readers.

> To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/05375057-883F-4487-8919-2579F5771AFC%40cmu.edu.

[Steve Awodey]

I totally agree with you, Mike.

But I think Thorsten was pointing out (he will correct me if I’m wrong)
that a = b meaning “equals” is maybe not the same as “identity”?

and I do think that the terminology “identification” is good for the elements of this type, which traditionally was called the “identity type".

maybe the answer is to say that mathematics simply doesn’t deal with the “metaphysical" notion of “identity”, as distinct from equality.
we just use both words interchangeably for the single notion expressd by a = b, which is short for Id(a,b).

> To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAOvivQwTR4qK094%2Bkmgj%3D2547UxGgmbjW9k5MgLe%2Bne9xPef3w%40mail.gmail.com.

[Joyal, André]

Dear Steve and Mike,

Thank you for your reply.
I guess we essentially agree.
The idea that the equality relation a=b depends on a choice of identification of a with b is fundamental.
In a sense, it has been around since a long time, but not formally recognized
except in ML type theory and possibly in category theory.

I am dreaming of a formal system in which the identity type Id(a,b)
is so natural, that it disappear by not been problematic.
How could we teach homotopy type theory to engineers?

André

________________________________________
From: Steve Awodey [awo...@cmu.edu]
Sent: Wednesday, May 06, 2020 3:31 PM
To: Michael Shulman
Cc: Joyal, André; HomotopyT...@googlegroups.com
Subject: Re: [HoTT] Identity versus equality

[Thorsten Altenkirch]

I always thought that equality and identity are synonyms. Sometimes we talk about equations and sometimes we call them identities. So yes, I agree completely.

Thorsten

To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/35D53A79-56C0-42F7-A58F-6052CE26FA87%40cmu.edu.

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.

[Thorsten Altenkirch]

I agree but let me try to make this more precise. We cannot talk about judgemental equality within Mathematics it is not a proposition. Judgemental equality is important when we talk about Mathematics, it is a property of a mathematical text. The same applies to typing: we cannot talk about typing because it is not a proposition it is a part of the structure of our argument.

This becomes clear in the example: we talk about numbers but x+y is an expression, hence talking about judgemental equality only makes sense when we talk about Mathematics. To say that x+y is not judgemental equal to y+x doesn't make any sense within our argument it is a sentence about it.

When I say that 0+x is definitionally equal to x I don't prove anything but I just point out a fact that follows from the definition of +. That is I draw attention to it.

Hence clearly there is no reason to use any other word that equality to mean that two objects are equal which means that the equality type is inhabited which is signified by using =. There is the issue that we may have a more that one way in which two objects can be equal which creates the need to talk about elements of an equality type. I don't like the word "identifications" because it seems to suggest that the two objects are not properly equal but just "identified" artificially.

Thorsten

To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAOvivQwTR4qK094%2Bkmgj%3D2547UxGgmbjW9k5MgLe%2Bne9xPef3w%40mail.gmail.com.

[Joyal, André]

Dear Thorsten,

I have naive question for experts.

I believe that judgemental equality is on the syntactic side of type theory,
while propositional equality is on the semantical side.
The homotopical interpretation of type theory is mainly
concerned with propositional equality.
What is the semantic of judgemental equality?
(independantly of the semantic of propositional equality).
Could we reverse the role of the two equalities?
Could we regard judgemental equality as the true meaning
of type theory, while regarding propositional equality
as a purely formal game?

André

________________________________________
From: Thorsten Altenkirch [Thorsten....@nottingham.ac.uk]
Sent: Wednesday, May 06, 2020 6:54 PM
To: Michael Shulman; Steve Awodey
Cc: Joyal, André; homotopyt...@googlegroups.com

Subject: Re: [HoTT] Identity versus equality

I agree but let me try to make this more precise. We cannot talk about judgemental equality within Mathematics it is not a proposition. Judgemental equality is important when we talk about Mathematics, it is a property of a mathematical text. The same applies to typing: we cannot talk about typing because it is not a proposition it is a part of the structure of our argument.

[Egbert Rijke]

Dear all,

Perhaps I would say that judgmental equality is even more on the semantic side than the identity type. We can reason about the identity type within type theory, but we can only reason about judgmental equality when we're considering semantics for type theory. For example, when you study dependent type theory as an essentially algebraic theory, and want to know what equalities hold in the algebras for that theory, then you're studying judgmental equality. It has been said a few times that we cannot talk about judgmental equality in mathematics, but I disagree. When we do semantics of type theory we *have to* talk about judgmental equality, and of course there is nothing that stops us from doing so.

With kind regards,

Egbert

To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/8C57894C7413F04A98DDF5629FEC90B1652F526C%40Pli.gst.uqam.ca.

[Thorsten Altenkirch]

Dear Andre,

It seems that Egbert already gave the perfect answer. When we about Type Theory we don't only talk about syntax but about the relation of syntax and semantics. And then judgemental equality is modelled by propositional equality in the metatheory. Not a reversal but a level shift.

I wouldn't say that propositional equality is a purely formal game, indeed we explain the nature of equality by modelling it. In a set theoretic setting it is enough to say that equality is a congruence, i.e. an equivalence relation that is preserved by all functions. But this is not sufficient to explain structural equality which is not propositional. As you know best (because you have invented many of the important notions) a better explanation of equality is that is an omega groupoid and that all functions are modelled as functors on these groupoids.

Cheers,
Thorsten

[Ansten Mørch Klev]

Dear all,

Thank you for your answers and for the stimulating discussion so far. I agree that identity, to the extent that it is distinguished from equality, is more of a philosopher's concept. One could perhaps say that in mathematical logic there is an overlap of two terminological traditions: a philosophical one, in which "identity" and "equality" are distinguished, and a mathematical one, where they are not. 

Regarding judgemental equality/identity: if by this one understands definitional identity, then a case can be made that it is found also outside type theory. Namely, instead of saying that a and b are definitionally identical, we can also say that they are identical by definition. And this phrase, "identical by definition", could well be used by a "generic mathematician", could it not?

There is also the common practice of using a special identity sign when writing definitions. One might say that the notion of definitional identity captures the semantics of this special sign. 

With kind regards,

Ansten Klev

To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/67E9DCCA-F9CA-45B7-9AC8-E5A7E94FE9A9%40nottingham.ac.uk.

[Thomas Streicher]

In my eyes the reason for the confusion (or rather different views)
arises from the different situation we have in syntax and in semantics.

In syntax the "real thing" is propositional equality and judgemental
equality is just an auxiliary notion. In mathematics it's the well
known difference between equality requiring proof (e.g. by induction) and
checking equality by mere symbolic computation. The latter is just a
technical device and not something conceptually basic.

The situation is very different in models (be they simplicial, cubical
or whatever). There judgemental equality gets interpreted as equality
of morphism and propositional equality gets interpreted as being homotopic.
Since the outer level of 2-level type theory is extensional there is
no judgemental equality (as in extensional TT).

This latter view is the view of people working in higher dimensional
category theory as e.g. you, Andr'e when you are not posting on the
list but write your beautiful texts on quasicats, Lurie or Cisinski
(and quite a few others). In these works people are not afraid of
refering to equality of objects, e.g. when defining the infinite
dimensional analogue of Grothendieck fibrations. And this for very
good reasons since there are important parts of category theory where
equality of objects does play a role (typically Grothendieck fibrations).

Fibered cats also often don't allow one to speak about equality of
objects in the base but it is there. This is very clearly expressed so
in the last paragraph of B'enabou's JSL article of fibered cats from 1985.
I think this applies equally well to infinity cats mutatis mutandis.

This phenomenon is not new. Consider good old topos theory. There are
things expressible in the internal logic of a topos and there are
things which can't be expressed in it as e.g. well pointedness or
every epi splits. The first holds vacuously when (misleadingly)
expressed in the internal language of a topos and the second amounts
to so called internal AC (which amounts to epis being preserved by
arbitrary exponentiation). This doesn't mean at all that internal language is
a bad thing. It just means that that it has its limitations...

Analogously, so in infinity category theory. Let us assume for a
moment that HoTT were the internal language of infinity toposes (which
I consider as problematic). There are many things which can be
expressed in the internal language but not everything as e.g. being a
Grothendieck fibration or being a mono...

I mean these are facts which one has to accept. One might find them
deplorable or a good thing but one has to accept them...

One of the reasons why I do respect Voevodsky a lot is that although
he developed HoTT (or better the "univalent view") he also suggested
2-level type theory when he saw its limitations.

I hope you apologize but I can't supress the following analogy coming
to my mind. After revolution in Russia and the civil war when economy
lay down the Bolsheviks reintroduced a bit of market economy under the
name NEP (at least that's the acronym in German) to help up the economy.
(To finish the story NEP was abandoned by Stalin which lead to well known
catastrophies like the forced collectivization...)

Sorry for that but one has to be careful when changing things and
think twice before throwing away old things...some of them might be
still useful and even indispensible!

Thomas

[Joyal, André]

Thank you all for your comments.

Thomas wrote:

<<The situation is very different in models (be they simplicial, cubical
or whatever). There judgemental equality gets interpreted as equality
of morphism and propositional equality gets interpreted as being homotopic.
Since the outer level of 2-level type theory is extensional there is
no judgemental equality (as in extensional TT).>>

I agree, there is some some kind of (weak) Quillen model structure associated to every model of type theory.
All of higher category theory seems to be based on good old set theory.
For example, a quasi-category is a simplicial set.
The category of sets could be replaced by a topos, but a topos is a category
and every category has a set of objects and a set of arrows.
At some level, all mathematics is based on some kind of set theory.
Is it not obvious?
We cannot escape Kantor's paradise!
Of course, we could possibly work exclusively with countable sets.
The set of natural numbers is the socle on which all mathematics is constructed.
Still, I would not want to refer constantly to recursion when I do mathematics.
There is a hierarchy of mathematical languages, and Peano's arithmetic is at the ground level.
Modern mathematics is mostly concerned with higher levels of abstraction.
Its usefulness is without questions, athough its foundation can be problematic.
Type theory is the only theory I know which includes two levels in its formalism.
Judgemental equality is at the lower level. It is not inferior, it is more fundamental.

Best,
André

________________________________________
From: Thomas Streicher [stre...@mathematik.tu-darmstadt.de]
Sent: Thursday, May 07, 2020 6:09 AM
To: Thorsten Altenkirch
Cc: Joyal, André; Michael Shulman; Steve Awodey; homotopyt...@googlegroups.com

Subject: Re: [HoTT] Identity versus equality

In my eyes the reason for the confusion (or rather different views)

[David Roberts]

>every category has a set of objects and a set of arrows.

I'm sorry, but where does it say that? The whole point of ETCS was to avoid an ambient set theory, no? Not to mention the original 'General theory of natural equivalences' avoided defining categories using sets.

Humbly,

David

David Roberts
Webpage: https://ncatlab.org/nlab/show/David+Roberts
Blog: https://thehighergeometer.wordpress.com

--
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 HomotopyTypeThe...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/8C57894C7413F04A98DDF5629FEC90B1652F5334%40Pli.gst.uqam.ca.

[Joyal, André]

Dear David,

This is getting controversial!

As you know, there are many notions of category.

Let me say that an ordinary category with a "set" of objects

and a "set" of arrows lives on the ground floor.

There is then a notion of category internal to a category;

let me say that such categories live on the first floor.

By induction, there a notion of category for every floor.

Of course, one can introduce an abstract notion of category

without specifying the level. For example, one

could consider a type theory classifying the notion of (\infty,1)-category.

But the type theory must be described by specifying a formal system.

The "predicates" in the formal system form a set, actually a countable set.

The syntactic category of any formal system lives on the ground floor.

Hence the generic category lives on the first floor.

I would love to remove set theory (in a naive sense) 

from the foundation of mathematics if that were possible.

Is that really desirable?

Maybe we should accept the situation

and use it to improve mathematics.

Best,

André

---

From: David Roberts [drobert...@gmail.com]
Sent: Thursday, May 07, 2020 5:41 PM
To: Joyal, André
Cc: Thomas Streicher; Thorsten Altenkirch; Michael Shulman; Steve Awodey; homotopyt...@googlegroups.com

[David Roberts]

Dear André,

I merely meant that the definition of category only requires first-order logic as in (Eilenberg–Mac Lane 1945), or at best a low-level dependent type theory (https://ncatlab.org/nlab/show/type-theoretic+definition+of+category). See also: https://ncatlab.org/nlab/show/fully+formal+ETCS#the_theory_etcs

Regards,

David

David Roberts
Webpage: https://ncatlab.org/nlab/show/David+Roberts
Blog: https://thehighergeometer.wordpress.com

[Thomas Streicher]

Dear Robert,

in what I said I didn't mean set theory literally. I was rather referring
to all kinds of categorical logic where equality is interpreted as
(fiberwise) diagonal like (traditional) topos theory in particular.
These kinds of gadgets all have the advantage that "Set" is not ruled
out as a model.

Since the diagonal is hardly ever fibrant HoTT rules out Set as a model.

But this is not my main problem. My main problem is that there is at least
one area of category theory where one has to speak about equality of
objects and these are Grothendieck fibrations. And these are intrinsic
for doing topos theory over general base toposes.
(That I really like them is, admittedly, also an important reason for me
not being ready to give them up! And for reasons of personal and
cultural "antagonisms" they are not very popular among the majority of
category theorists... Thus, there are many people who would not be too
sad about working in a framework not allowing to speak about them.)
But I want to emphasize that real masters of infinite dimensional
categories do not have the faintest problem speaking about equality
when speaking about infinite dimensional versions of Grothendieck
fibrations!)

Though (traditional) topos theory can be developed over fairly general
toposes and this, at least philosophically, is an important aspect one
cannot deny that most toposes of interest heavily rely on Set, be they
of the Grothendieck kind or be they of the realizability kind!

Thomas

PS Above I put Set into inverted commas because the logician in me
finds it amusing to speak about "the" category of sets which is
nothing but an illusion... Even the nowadays not so little number of
adherents of the "multiverse" view of set theory would share this view!
But even the "universe" view is nothing but an ideology because since
Cohen set theory is mainly a business of constructing different models
via forcing.
Thus, since Set is (sort of) an illusion it is important to do toposes
over arbitrary bases for which purpose one needs Grothendieck fibrations
which do not make sense without equality of objects.

PPS Some people might get the impression I am a "crypto set
theorist". Nothing could be more wrong. I am anti-ideological and
pluralist and I like "deviating" ideas. But I am interested in
calibrating what one needs for which goals. What I am allergic at is
ideological positions which want to forbid someone doing certain
things because they do not fit to some ideological positions...
And one has to accept that not all combinations are possible. Thus
pluralist is better to inegrist!

[Joyal, André]

Dear Thomas,

You are right, the equality of objects in a Grothendieck fibration is judgemental.

Propositional equality of type theory has been studied a lot during the last decades.
I feel quite confortable with it, with the homotopy interpretation and the univalence principle, etc.
I confess that I am much less at ease with judgmental equality and the syntax of type theory.
Until now, type theory has failed to prove that pi_4(S^3)=C_2.
Is it the symptom of a fundamental problem?
Is it because the reduction algoritms are not optimal?
Or because computers are not powerful enough?
What is the abstract theory of terms reduction in type theory?
I apologise for my ignorance.

Best,
André

________________________________________t
From: Thomas Streicher [stre...@mathematik.tu-darmstadt.de]
Sent: Friday, May 08, 2020 2:40 AM
To: David Roberts
Cc: Joyal, André; Thorsten Altenkirch; Michael Shulman; Steve Awodey; homotopyt...@googlegroups.com

Subject: Re: [HoTT] Identity versus equality

Dear Robert,

[Steve Awodey]

Dear André,

I would prefer to say that t current systems of type theory have failed to *compute* pi_4(S^3), so as not to diminish the value of Guillaume’s beautiful proof, which has even been formally checked in different proof assistants.
You of course know the difference between proving something in type theory and computing the value of a term, but some readers may not.

Best wishes,

Steve

Ps: In my opinion, for what it’s worth, making a system that will compute the value of Brunerie’s constant is an engineering problem, not a mathematical one. Which is not to say it would not be an important advance!

> On May 8, 2020, at 17:06, Joyal, André <joyal...@uqam.ca> wrote:
>
> Dear 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 HomotopyTypeThe...@googlegroups.com.

> To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/8C57894C7413F04A98DDF5629FEC90B1652F54CC%40Pli.gst.uqam.ca.

[Joyal, André]

Dear Steve,

Thank you for stressing the distinction between computing and proving.
I was thinking about the computation of a natural number by reduction of terms.
I must be confused.

But in type theory, is it not true that every proof is a computation?

Best,
André

________________________________________
From: Steve Awodey [steve...@gmail.com]
Sent: Friday, May 08, 2020 7:44 PM
To: Joyal, André
Cc: Thomas Streicher; David Roberts; Thorsten Altenkirch; Michael Shulman; Steve Awodey; homotopyt...@googlegroups.com

[Steve Awodey]

To elaborate a bit further in response to some private inquiries:

Brunerie’s proof that pi_4(S^3) = Z_2 , which is an entirely formal proof within homotopy type theory, has two main parts:

(1) it is shown that there is a natural number n such that pi_4(S^3) = Z_n ,
(2) it is shown that n = 2.

Since the proof of (1) is constructive, it produces an actual term t : Nat .
In a system of type theory with the canonicity property
(like intensional MLTT w/o HITs or UA, or some of the more recent cubical type theories),
there is an algorithm which, from any such term t : Nat, will *compute* a numeral t* such that t* == t (definitionally).
This numeral t* denotes a natural number directly.

Applying the algorithm to (the term representing) “Brunerie’s number” n in (1),
we should be able to use it to *compute* that n = 2, avoiding the need for the (quite intricate) proof in part (2).
This is the part that (up to now) has not been possible to do *in practice*, as Andre’ Joyal was pointing out.
Thus we still require the proof in (2) to know that n = 2.

The system of “Book HoTT” allows to formally prove many things that cannot be computed in that system,
because terms coming from HITs or involving UA need not compute.
An advantage of cubical systems is that all terms compute — in principle.
But more practical work seems to be required in order to take advantage of this feature in practice.

Regards,

Steve

[Jon Sterling]

Dear André,

To answer your question about what is the abstract theory of term reduction in type theory, one very beautiful option is rewriting theory, the study of abstract rewriting systems; this is perhaps the most venerable and mathematically deep tool to study term reduction, but it does not readily support many of the kinds of "reductions" that occur in dependent type theory, especially the more exotic cubical type theories.

For this and other reasons, some of us (including Steve and myself and many others) have been lately studying computation in these type theories using more abstract tools like Artin gluing --- the disadvantage of this approach is the gluing has little to say about the efficiency or algorithmic aspects of computation in type theory, but it is enough to prove that existence proofs do carry algorithms to compute numerals.

Simultaneously, we are working on improving the algorithmic / practical aspects of cubical type theory so that in the future we may be able to actually execute the algorithm that corresponds to Brunerie's proof. My collaborators and I are currently experimentally programming a new reduction algorithm for cubical type theory that I designed this fall; I do not know whether it will help significantly, but we will see.

Best,
Jon

> https://groups.google.com/d/msgid/HomotopyTypeTheory/8C57894C7413F04A98DDF5629FEC90B1652F5565%40Pli.gst.uqam.ca.
>

[Thomas Streicher]

Dear Andr'e,

in most models of HoTT judgemental equality is equality of morphisms
and propositional equality is being homotopic.
But that is very different from its appearance in formal systems
where judgemental equality is much more restricted and just serves the
purpose of computation. There are artificial versions of type theory
with excessively few computation rules (only mere lambda calculus).

I fully understand why you find judgemental equality puzzling: it is
of very subjective nature. Mathematicians are typically interested in
equalities which are not decided by a rewrite system.
Judgemental equality has a very subjective nature because it
identifies a computational fragment of mathematics and there are many
different such. In Book HoTT one is as computational as traditional
intensional TT is and then adds univalence which lacks any
computational meaning. This is at least frivolous from the perspective
of a traditionalist type theorist... But it is ok and was implemented
in the NuPrl system.

Now for people who use type theory as a way of doing homotopy theory
synthetically the computational aspect is absolutely irrelevant a
priori. When one does ordinary math (including homotopy) computability
is a gimmick and no one would insist on everything being computable.

So if one has shown that the homotopy group of some pointed space is
Z_n for some n and one wants to know what n is then in Book HoTT you
have to guess n and then show that n equal your guess. In cubical type
theory in principle the n can be computed but it may take a very long
time (or the normalization proof is faulty :-)).

The main problem is that programs extracted from proofs are typically
not very efficient (well in rare cases they are but you have to be lucky).

Anyway, my brief answer to the question you raise is:
(1) conceptually judgemental equality is absolutely redundant
and hopelessly subjective
(2) systems with a bare minimum of judgemental equality are not
suitable for the various proof checkers in use since then every
computation has to be done by hand.

Thomas

[Joyal, André]

Thank you Thomas, Jon and Steve for answering my question.

You are very generous to an old man.
Let me pretend that I still have enough time to study the computational aspects of type theory.

By the way, if type theory is not very effective in practice, why do we insist that it should always compute?
The dream of a formal system in which every proof leads to an actual computation may be far off.
Not that we should abandon it, new discoveries are always possible.
Is there a version of type theory for proving and verifying, less for computing?
The notations of type theory are very useful in homotopy theory.
But the absence of simplicial types is a serious obstacle to applications.

Best,
André

________________________________________
From: Thomas Streicher [stre...@mathematik.tu-darmstadt.de]
Sent: Saturday, May 09, 2020 4:28 AM
To: Joyal, André
Cc: David Roberts; Thorsten Altenkirch; Michael Shulman; Steve Awodey; homotopyt...@googlegroups.com

Subject: Re: [HoTT] Identity versus equality

Dear Andr'e,

[Thomas Streicher]

Dear Andr'e,

> By the way, if type theory is not very effective in practice, why do we insist that it should always compute?
> The dream of a formal system in which every proof leads to an actual computation may be far off.
> Not that we should abandon it, new discoveries are always possible.
> Is there a version of type theory for proving and verifying, less
> for computing?

In my opinion the currenrly implemented type theories are essentially
for proving and not for computing.
But if you haven't mechanized PART of equational reasoning it would be
much much more painful than it still is.
But that is "only" a pragmatic issue.

> The notations of type theory are very useful in homotopy theory.
> But the absence of simplicial types is a serious obstacle to applications.

In cubical type theory they sort of live well with cubes not being
fibrant... They have them as pretypes. But maybe I misunderstand...

Thomas

[Joyal, André]

Dear Thomas,

You wrote

<<In my opinion the currenrly implemented type theories are essentially
for proving and not for computing.
But if you haven't mechanized PART of equational reasoning it would be
much much more painful than it still is.
But that is "only" a pragmatic issue.>>

Type theory has very nice features. I wish they could be preserved and developped further.
But I find it frustrating that I cant do my everyday mathematics with it.
For example, I cannot say

(1) Let X:\Delta^{op}---->Type be a simplicial type;
(2) Let G be a type equipped with a group structure;
(3) Let BG be the classifying space of a group G;
(4) Let Gr be the category of groups;
(5) Let SType be the category of simplical types.
(6) Let Map(X,Y) be the simplicial types of maps X--->Y
between two simplicial types X and Y.

It is crucial to have (1)
For example, a group could be defined to
be a simplicial object satisfying the Segal conditions.
The classifying space of a group is the colimit of this simplicial object.
The category of groups can be defined to be
a simplicial objects satisfiying the Rezk conditions (a complete Segal space).

Is there some aspects of type theory that we may give up as a price
for solving these problems ?

Best,
André

________________________________________
From: Thomas Streicher [stre...@mathematik.tu-darmstadt.de]

Sent: Saturday, May 09, 2020 2:43 PM

To: Joyal, André
Cc: David Roberts; Thorsten Altenkirch; Michael Shulman; Steve Awodey; homotopyt...@googlegroups.com
Subject: Re: [HoTT] Identity versus equality

Dear Andr'e,

[Jon Sterling]

Dear André,

The coherence problems involved in formulating everyday notions like simplicial types (what an amazing world we live in to be able to call this everyday!) can be resolved by extending Homotopy Type Theory with a "sub-homotopical" layer, a second equality type that is meant to capture the strict mathematical equality instead of paths. This is sometimes called Two Level Type Theory. In this case, it is possible to define simplicial types, using the strict equality to sidestep the problem of defining homotopy coherent structures in HoTT.

There are a number of ways to achieve this, and they have different tradeoffs depending on what your goals are. The space of possible realizations of this idea corresponds to what Thomas has referred to as the "subjectivity" of judgmental equality.

Best,
Jon

> --
> 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 HomotopyTypeThe...@googlegroups.com.
> To view this discussion on the web visit

> https://groups.google.com/d/msgid/HomotopyTypeTheory/8C57894C7413F04A98DDF5629FEC90B1652F563A%40Pli.gst.uqam.ca.
>