# Identity versus equality

46 views

### Ansten Mørch Klev

May 5, 2020, 4:48:13 AM5/5/20
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é

May 6, 2020, 12:02:31 PM5/6/20
to Ansten Mørch Klev, HomotopyT...@googlegroups.com
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
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

May 6, 2020, 3:01:52 PM5/6/20
to "Joyal, André", HomotopyT...@googlegroups.com
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

### Michael Shulman

May 6, 2020, 3:18:51 PM5/6/20
to Steve Awodey, Joyal, André, HomotopyT...@googlegroups.com
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

May 6, 2020, 3:31:15 PM5/6/20
to Michael Shulman, "Joyal, André", HomotopyT...@googlegroups.com
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é

May 6, 2020, 4:31:01 PM5/6/20
to Steve Awodey, Michael Shulman, HomotopyT...@googlegroups.com
Dear Steve and Mike,

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

May 6, 2020, 6:52:28 PM5/6/20
to Steve Awodey, Michael Shulman, "Joyal, André", homotopyt...@googlegroups.com
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

May 6, 2020, 6:54:32 PM5/6/20
to Michael Shulman, Steve Awodey, Joyal, André, homotopyt...@googlegroups.com
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é

May 6, 2020, 7:29:17 PM5/6/20
to Thorsten Altenkirch, Michael Shulman, Steve Awodey, homotopyt...@googlegroups.com
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

May 7, 2020, 2:11:17 AM5/7/20
to Joyal, André, Thorsten Altenkirch, Michael Shulman, Steve Awodey, homotopyt...@googlegroups.com
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

### Thorsten Altenkirch

May 7, 2020, 2:58:55 AM5/7/20
to Joyal, André, Michael Shulman, Steve Awodey, homotopyt...@googlegroups.com
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

May 7, 2020, 5:05:27 AM5/7/20
to Thorsten Altenkirch, Joyal, André, Michael Shulman, Steve Awodey, homotopyt...@googlegroups.com
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

### Thomas Streicher

May 7, 2020, 6:09:35 AM5/7/20
to Thorsten Altenkirch, Joyal, André, Michael Shulman, Steve Awodey, homotopyt...@googlegroups.com
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é

May 7, 2020, 12:13:19 PM5/7/20
to Thomas Streicher, Thorsten Altenkirch, Michael Shulman, Steve Awodey, homotopyt...@googlegroups.com

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

May 7, 2020, 5:41:28 PM5/7/20
to Joyal, André, Thomas Streicher, Thorsten Altenkirch, Michael Shulman, Steve Awodey, homotopyt...@googlegroups.com
>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

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

### Joyal, André

May 7, 2020, 7:43:59 PM5/7/20
to David Roberts, Thomas Streicher, Thorsten Altenkirch, Michael Shulman, Steve Awodey, homotopyt...@googlegroups.com
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

May 7, 2020, 7:57:06 PM5/7/20
to Joyal, André, Thomas Streicher, Thorsten Altenkirch, Michael Shulman, Steve Awodey, homotopyt...@googlegroups.com
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,

### Thomas Streicher

May 8, 2020, 2:40:44 AM5/8/20
to David Roberts, Joyal, André, Thorsten Altenkirch, Michael Shulman, Steve Awodey, homotopyt...@googlegroups.com
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é

May 8, 2020, 5:06:51 PM5/8/20
to Thomas Streicher, David Roberts, Thorsten Altenkirch, Michael Shulman, Steve Awodey, homotopyt...@googlegroups.com
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

May 8, 2020, 7:44:12 PM5/8/20
to "Joyal, André", Thomas Streicher, David Roberts, Thorsten Altenkirch, Michael Shulman, Steve Awodey, homotopyt...@googlegroups.com
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é

May 8, 2020, 10:46:17 PM5/8/20
to Steve Awodey, Thomas Streicher, David Roberts, Thorsten Altenkirch, Michael Shulman, Steve Awodey, homotopyt...@googlegroups.com
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

May 8, 2020, 10:50:16 PM5/8/20
to Homotopy Type Theory, "Joyal, André"
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

May 8, 2020, 11:10:24 PM5/8/20
to 'Martin Escardo' via Homotopy Type Theory
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
>

### Thomas Streicher

May 9, 2020, 4:28:33 AM5/9/20
to Joyal, André, David Roberts, Thorsten Altenkirch, Michael Shulman, Steve Awodey, homotopyt...@googlegroups.com
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é

May 9, 2020, 11:53:55 AM5/9/20
to Thomas Streicher, David Roberts, Thorsten Altenkirch, Michael Shulman, Steve Awodey, homotopyt...@googlegroups.com
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

May 9, 2020, 2:43:18 PM5/9/20
to Joyal, André, David Roberts, Thorsten Altenkirch, Michael Shulman, Steve Awodey, homotopyt...@googlegroups.com
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é

May 9, 2020, 4:18:11 PM5/9/20
to Thomas Streicher, David Roberts, Thorsten Altenkirch, Michael Shulman, Steve Awodey, homotopyt...@googlegroups.com
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

May 9, 2020, 5:28:06 PM5/9/20
to 'Martin Escardo' via Homotopy Type Theory
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
>

### Joyal, André

May 9, 2020, 10:19:11 PM5/9/20
to Jon Sterling, 'Martin Escardo' via Homotopy Type Theory
Dear Jon,

You wrote:

<<The coherence problems involved in formulating everyday notions like simplicial types (what an amazing world we live in to be able to call this everyday!) can be resolved by extending Homotopy Type Theory with a "sub-homotopical" layer, a second equality type that is meant to capture the strict mathematical equality instead of paths.>>

That is interesting.
Is the "strict" equality like the equality relation between the maps of a Quillen model structure?
I am curious to see the description of such a formal system.

Is it related to Vladimir's theory with 3 levels of equality (which I never understood)?

Best,
André

________________________________________
From: homotopyt...@googlegroups.com [homotopyt...@googlegroups.com] on behalf of Jon Sterling [j...@jonmsterling.com]
Sent: Saturday, May 09, 2020 5:27 PM
To: 'Martin Escardo' via Homotopy Type Theory

Dear André,

Best,
Jon

To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/b1d32ac0-e364-4405-9e48-e0e1e0b37732%40www.fastmail.com.

### Jon Sterling

May 9, 2020, 11:04:11 PM5/9/20
to "Joyal, André", 'Martin Escardo' via Homotopy Type Theory
Dear André,

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

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

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

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

Best,
Jon

### Thomas Streicher

May 10, 2020, 5:10:00 AM5/10/20
to Jon Sterling, "Joyal, André", 'Martin Escardo' via Homotopy Type Theory
Dear Andr'e and Jon,

I mostly agree with what Jon said. I also think that intensional type
theory within an extensional type theory (it is 2 levels and not 3) is
an attractive system for cubical type theory.
In the simplicial case this is a bit more problematic since the
filling conditions for Kan complexes involve classical existential
quantification and as shown by Thierry et.al. this is important!

That the extensional level is just formulated using J and K is a
possibility. It has to be seen in practice how far it goes.

Let me finish with a remark on how constructive traditional topos
theory is. I don't mean the logic represented by a topos but which
logical principles one uses when doing topos theory.
Since one wants to develop toposes relative to fairly general base
toposes people introduced fibered/indexed reasoning. But the reasoning
about fibrations is per se fairly classical and also involves choice
for classes typically. So this reasoning is performed on a meta level
and not within the logic of the base topos. For the situations when
this is partly possible Benabou invented the notion of "definability".

This is sometimes swept under the carpet because of some "antilogical"
tendencies which were influential at the time of the genesis of topos
theory (beautifully described in a little essay by Reyes I recnely
found on his home page). I am aware that I am on dangerous grounds now
since Andr'e has really experienced and shaped these days (when I
started high school).
But it coincides with my impression of what is the practice of the
working topos theorist...

I think the real antagonism is or was that those days (and I am afraid
still nowadays) traditional logicians are mainly adherents of a one
world view. This has changed recently where even among set theorists
there is a "multiverse" and a "universe" fraction and the former is
getting larger compared to the past. This is funny in a sense since
one of the reasons for a multiverse veiw was independnce results is
set theory...

Anyway both traditional topos theory and higher dimensional category
theory was and is developed within a unrestricted metatheory which
could be formalized in ZFC + every set is an element of some Grothendieck universe.

It is not impossible that certain aspects and fragments can be
developed in weaker systems but there is no guarantee that this will
always work.

Thomas

### Thorsten Altenkirch

May 10, 2020, 7:46:19 AM5/10/20
to Jon Sterling, 'Martin Escardo' via Homotopy Type Theory
Hi Jon,

I just had an exchange with Andre regarding this which I forgot to cc to the list.

Defining simplicial types isn't entirely straightforward (as you know I suppose), because Delta is not directed. We can do semi-simplicial types as a Reedy limit, i.e. an infinite Sigma type (actually you can do it as a coinductive definition). You need some extra principles, e.g. that strict Nat is fibrant or maybe better that certain coinductive types exist.

However, presheaves over Delta cannot be written as a Reedy limit. Now there are a number of ways to address this. We can work with semi-simplicial sets and add Hornfillers by stating equivalences (there is no coherence problem because these are propositional). To regain identities we can add the assumption that the higher category is univalent (i.e. for every object the type of objects paired with an equivalence is contractible) which entails the existence of degeneracies.

The question of how to define simplicial types remains however. I find that looking at the lower levels of simplicial presheaves it is actually strange that binary composition is handled via horn-fillers whlle identity, i.e. nullary composition, is built into the structure. Maybe we should treat identity in the same way as composition, which means that we introduce a family modelling degeneracies.

What I mean is that if we write down the first levels of a semisimplicial type we have

X0 : U
X1 : X0 -> X0 -> U
X2 : (x0,x1,x2 : X0) -> X0 x0 x1 -> X0 x1 x2 -> X0 x0 x2 -> U

But we can add degeneracies by adding families which say that some object is a degeneracy:

I0 : (x0 : X0) -> X1 x0 x0 -> U
I1_0 : (x0 x1 : X0)(f : X1 x0 x1)(i : X1 x0 x0) -> I0 x0 i -> X2 x0 x1 x1 i f f -> U
I1_1 : (x0 x1 : X0)(f : X1 x0 x1)(i : X1 x1 x1) -> I0 x1 i -> X2 x0 x0 x1 f i f -> U

That is while X2 can be viewed as a proof-relevant predicate that a triangle commutes, I0 is a predicate that an arrow is an identity and I1_0 , I1_1 are predicates that triangles are degenerate.

Adding horn-fillers type-theoretically corresponds to saying that certain types are contractible:

(x0,x1,x2 : X0)(f : X1 x0 x1)(g : X1 x1 x2) -> is-contractible ((h : X1 x0 x2) \times X2 x0 x1 x2 f g h)

where is-contractible(A) = (a : A) \times ((x : A) -> a = x)

Similarly we can add degeneracies

(x0 : X0) -> is-contractible (X1 x0 x0)
(x0 x1 : X0)(f : X1 x0 x1)(i : X1 x0 x0)(j : I0 x0 i) -> is-contractible ((x : X2 x0 x1 x1 i f f) \times I1_0 x0 x1 f i j x)
(x0 x1 : X0)(f : X1 x0 x1)(i : X1 x1 x1)(j : I0 x0 i) -> is-contractible ((x : X2 x0 x0 x1 f i f) \times I1_0 x1 x1 f i j x)

This is related to Kraus' & Sattler's directed replacement:
https://arxiv.org/abs/1704.04543

Andre mentioned that degeneracies play an important role in the classical theory of simplicial sets, e.g. to show that geometric realisation preserves finite limits. However, the situation is quote different here because we work with types not sets. Hence you would expect that the topologies are also higher-dimensional objects. Has anybody looked at this?

Thorsten
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/b1d32ac0-e364-4405-9e48-e0e1e0b37732%40www.fastmail.com.

### Thorsten Altenkirch

May 10, 2020, 8:00:05 AM5/10/20
to Thomas Streicher, Jon Sterling, "Joyal, André", 'Martin Escardo' via Homotopy Type Theory
Dear Thomas,

I mostly agree with what Jon said. I also think that intensional type
theory within an extensional type theory (it is 2 levels and not 3) is
an attractive system for cubical type theory.

That seems to be putting the cart before the horse. HoTT is the theory I want to work in, the strict layer is only there to do some internalized metatheory.

In the simplicial case this is a bit more problematic since the
filling conditions for Kan complexes involve classical existential
quantification and as shown by Thierry et.al. this is important!

I think we have two discussions here: one is about simplicial sets which is about the reduction of HoTT to set level structures and the other is about (semi-)simplicial types which is about modelling higher structures within HoTT.

The classical assumptions in the filling conditions for Kan complexes can be avoided as was shown by Gambino and Sattler:
https://arxiv.org/abs/1510.00669
who develop a theory of uniform fibrations that captures both cubical and simplicial sets. This means we can model Pi-types using uniform simplicial sets. However, it is not clear how to interpret a univalent universe in uniform simplicial sets. It is possible to do this in uniform cubical sets due to the fact that the interval is a tiny object.

That the extensional level is just formulated using J and K is a
possibility. It has to be seen in practice how far it goes.

You need K on the strict level, because that is exactly the point that you don’t need to care about coherences anymore. Btw, I think calling it "extensional level" is a misnomer because actually the fibrant layer is more extensional than the strict one because it is univalent.

So for example if you define semi-simplicial types in a 2-level type theory it is essential that you have K.

Cheers,
Thorsten

### Ulrik Buchholtz

May 10, 2020, 8:53:22 AM5/10/20
to Homotopy Type Theory
Dear André,

On Saturday, May 9, 2020 at 10:18:11 PM UTC+2, joyal wrote:
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;

Let me remind everyone that we don't have a proof that it's impossible to define simplicial types in book HoTT! As long as we haven't settled this question either way, the predicament we're in (and I agree it's a predicament) is more an indictment of type theorists than of type theory. (And I include myself as a type theorist here.)

Anyway, from your phrasing of (1), it looks like you're after a directed type theory. Several groups are working on type theories where your (1) is valid syntax, but you have to write Space (or Anima or ...) to indicate the covariant universe of homotopy types and maps, rather than the full universe.

(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;

Again, let me remind everyone, that groups are precisely one of the few structures we know how to handle (along with grouplike E_n-types, and connective/general spectra): To equip a type G with a group structure is to give a pointed connected type BG and an equivalence of G with the loop type of BG. The type of objects of Gr is the universe of pointed, connected types.

When you replace groups by monoids, it gets more embarrassing.

Earlier (on May 7) you wrote:
At some level, all mathematics is based on some kind of set theory.
Is it not obvious?
We cannot escape Cantor's paradise!

That is exactly the question, isn't it?

What HoTT/UF offers us is another axis of foundational variation, besides the old classical/constructive, impredicative/predicative, infinitist/finitist, namely: everything is based on sets/general homotopy types are not reducible to sets.

I don't know of catchy names for these positions, but I think that working with HoTT has a tendency of making the latter position more plausible: Why should there for any type be a set that surjects onto it?

A question: Recall that if we assume the axiom of choice (AC) for sets, then there is a surjection from a set onto Set, namely the map that takes a cardinal (or ordinal) to the set of ordinals below it.
Is there (with AC for sets) also a surjection from a set to the type of 1-types? To the full universe?

The 2-level type theories can be viewed as another way of making a type theory that is faithful to the idea that everything is based on sets. I like to think of the outer layer as an exoskeleton for type theory, giving it a bit of extra strength while we don't know how to use its own powers fully, or whether indeed it is strong enough to effect constructions like that of simplicial types. Every type (which for me is a fibrant type, since that's the mathematically meaningful ones) has a corresponding exotype (indeed an exoset), but there are more exotypes, such as the exonatural numbers, which are sometimes useful.

Best wishes,
Ulrik

### Michael Shulman

May 10, 2020, 10:01:17 AM5/10/20
to Ulrik Buchholtz, Homotopy Type Theory
On Sun, May 10, 2020 at 5:53 AM Ulrik Buchholtz
<ulrikbu...@gmail.com> wrote:
> What HoTT/UF offers us is another axis of foundational variation, besides the old classical/constructive, impredicative/predicative, infinitist/finitist, namely: everything is based on sets/general homotopy types are not reducible to sets.

Exactly!

> A question: Recall that if we assume the axiom of choice (AC) for sets, then there is a surjection from a set onto Set, namely the map that takes a cardinal (or ordinal) to the set of ordinals below it.
> Is there (with AC for sets) also a surjection from a set to the type of 1-types? To the full universe?

As far as I know, it is an open question whether AC for sets implies
these stronger principles (although I'd be surprised if it were true).
Those principles are true, of course, in the model of simplicial sets
based on ZFC, and there are models in which they fail, but I don't
know of a model in which they fail but AC for sets holds. Although I
don't think I've really tried to look for one either; has anyone?

There is however the theorem stated at
https://ncatlab.org/nlab/show/n-types+cover#relation_to_other_axioms,
that AC for sets together with the axiom "every type is surjected onto
by a set" is equivalent to the "oo-AC" that "every surjection onto a
set has a section".

> The 2-level type theories can be viewed as another way of making a type theory that is faithful to the idea that everything is based on sets.

While I kind of see how one could say this, I think it's misleading
especially in light of the above dichotomy, becuase 2LTT doesn't imply
any of the *internal* "types are based on sets" axioms for the fibrant
layer. As you know, 2LTT without additional axioms is conservative
over HoTT, while even with stronger axioms it can still be modeled in
many or all higher toposes.

> I like to think of the outer layer as an exoskeleton for type theory, giving it a bit of extra strength while we don't know how to use its own powers fully, or whether indeed it is strong enough to effect constructions like that of simplicial types. Every type (which for me is a fibrant type, since that's the mathematically meaningful ones) has a corresponding exotype (indeed an exoset), but there are more exotypes, such as the exonatural numbers, which are sometimes useful.

I think "exo-" is a great prefix for the outer layer!

### Michael Shulman

May 10, 2020, 10:02:06 AM5/10/20
to Thorsten Altenkirch, Jon Sterling, 'Martin Escardo' via Homotopy Type Theory
On Sun, May 10, 2020 at 4:46 AM Thorsten Altenkirch
<Thorsten....@nottingham.ac.uk> wrote:
> Defining simplicial types isn't entirely straightforward (as you know I suppose), because Delta is not directed. We can do semi-simplicial types as a Reedy limit, i.e. an infinite Sigma type

We can certainly *talk* about simplicial types in 2LTT as exofunctors
from the exocategory Delta to the exocategory Type. I assume the
point you're making is that we don't have a (fibrant) *type of*
simplicial types, whereas we do have a fibrant type of semisimplicial
types (under appropriate axioms)?

> You need some extra principles, e.g. that strict Nat is fibrant or maybe better that certain coinductive types exist.

Personally, I think the best axiom to use here is that exo-Nat is
*cofibrant*, i.e. Pi-types with domain exo-Nat preserve fibrancy. We
don't know how to model "exo-Nat is fibrant" in all higher toposes,
but it's easy to interpret "exo-Nat is cofibrant" in such models,
since Pi-types with domain exo-Nat are just externally-infinite
products.

### Nicolai Kraus

May 10, 2020, 10:20:37 AM5/10/20
to Michael Shulman, Thorsten Altenkirch, Jon Sterling, 'Martin Escardo' via Homotopy Type Theory
On 10/05/2020 15:01, Michael Shulman wrote:
> On Sun, May 10, 2020 at 4:46 AM Thorsten Altenkirch
> <Thorsten....@nottingham.ac.uk> wrote:
>> Defining simplicial types isn't entirely straightforward (as you know I suppose), because Delta is not directed. We can do semi-simplicial types as a Reedy limit, i.e. an infinite Sigma type
> We can certainly *talk* about simplicial types in 2LTT as exofunctors
> from the exocategory Delta to the exocategory Type. I assume the
> point you're making is that we don't have a (fibrant) *type of*
> simplicial types, whereas we do have a fibrant type of semisimplicial
> types (under appropriate axioms)?

Judging from the rest of his message, I believe that Thorsten was
talking about the direct replacement construction in Christian's and my
abstract arXiv:1704.04543. With the assumption "exo-Nat is cofibrant",
this gives us a fibrant type that one could call "simplicial types" (and
Thorsten does). But of course it's an encoding. If we decide to use such
encodings, I fear we may lose the main advantage that the "axiomatic"
representations in HoTT have, namely avoiding encodings. (I mean the
"main advantage" of HoTT compared to traditional approaches, e.g. taking
bisimplicial sets.)

>> You need some extra principles, e.g. that strict Nat is fibrant or maybe better that certain coinductive types exist.
> Personally, I think the best axiom to use here is that exo-Nat is
> *cofibrant*, i.e. Pi-types with domain exo-Nat preserve fibrancy. We
> don't know how to model "exo-Nat is fibrant" in all higher toposes,
> but it's easy to interpret "exo-Nat is cofibrant" in such models,
> since Pi-types with domain exo-Nat are just externally-infinite
> products.

I completely agree with your preference for this axiom :-)
But Thorsten does has a point if we consider the "engineering level"
that was discussed earlier in this thread. Allowing coinductive types
with exo-Nat as an index makes it possible to use your paper (Higher
Stucture Identity Principle, arXiv:2004.06572) and get a construction of
semi-simplicial types which is more convenient to use in a proof assistant.

-- Nicolai

### Nicolai Kraus

May 10, 2020, 10:27:30 AM5/10/20
to Michael Shulman, Ulrik Buchholtz, Homotopy Type Theory
On Sun, May 10, 2020 at 3:01 PM Michael Shulman <shu...@sandiego.edu> wrote:
On Sun, May 10, 2020 at 5:53 AM Ulrik Buchholtz
<ulrikbu...@gmail.com> wrote:
> The 2-level type theories can be viewed as another way of making a type theory that is faithful to the idea that everything is based on sets.

While I kind of see how one could say this, I think it's misleading
especially in light of the above dichotomy, becuase 2LTT doesn't imply
any of the *internal* "types are based on sets" axioms for the fibrant
layer.  As you know, 2LTT without additional axioms is conservative
over HoTT, while even with stronger axioms it can still be modeled in
many or all higher toposes.

I agree with Mike - sorry Ulrik :-)
For me, "everything is based on sets" would mean that every fibrant type can be written as the realization of a (semi-) simplicial type, or something like this.

### Michael Shulman

May 10, 2020, 10:35:08 AM5/10/20
to Nicolai Kraus, Thorsten Altenkirch, Jon Sterling, 'Martin Escardo' via Homotopy Type Theory
Many or all coinductive types can be constructed, at least up to
equivalence, using Pi-types and (some kind of) Nat. Is there any
chance that "exo-Nat is cofibrant" could be used to justify the
existence/fibrancy of the coinductive types you want?

### Nicolai Kraus

May 10, 2020, 10:52:22 AM5/10/20
to Michael Shulman, Thorsten Altenkirch, Jon Sterling, 'Martin Escardo' via Homotopy Type Theory
I would guess that "exo-Nat is cofibrant" justifies the coinductive type in question, but not its judgmental computation rules. And the judgmental computation rules are probably the very reason why one would want this coinductive type. But this is just a guess.
-- Nicolai

### Michael Shulman

May 10, 2020, 11:16:17 AM5/10/20
to Nicolai Kraus, Thorsten Altenkirch, Jon Sterling, 'Martin Escardo' via Homotopy Type Theory
I forget -- does "exo-Nat is cofibrant" imply that exo-limits of
towers of fibrations are fibrant? That's another useful axiom that
holds in models and might make it easier to construct coinductive
types with judgmental computation rules.
> --
> 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/CA%2BAZBBr0Zh-uLfEZCXUapK5KHFDxkzxyvLW22zyjmrB8KmWtYQ%40mail.gmail.com.

### Nicolai Kraus

May 10, 2020, 11:23:18 AM5/10/20
to Michael Shulman, Thorsten Altenkirch, Jon Sterling, 'Martin Escardo' via Homotopy Type Theory
Yes, I think that is one main motivation for this axiom (that you've
suggested in this form :-) and I also believe that it was Vladimir's
main motivation for his axiom "exo-Nat is fibrant". I think the two
axioms really serve the same purpose, but the "cofibrant" version is
much more harmless.

### Ulrik Buchholtz

May 10, 2020, 11:35:17 AM5/10/20
to Homotopy Type Theory
On Sunday, May 10, 2020 at 4:27:30 PM UTC+2, Nicolai Kraus wrote:
I agree with Mike - sorry Ulrik :-)
For me, "everything is based on sets" would mean that every fibrant type can be written as the realization of a (semi-) simplicial type, or something like this.

No need to apologize: I know I was being slightly provocative by juxtaposing a question about sets cover (SC) and a comment on 2-level type theory in this context, in order to provoke some discussion :-)

Wouldn't you agree, however, that even though basic 2LTT is conservative over HoTT, from a certain point of view, 2LTT privileges the “ground floor” exosets? In your very nice paper, https://arxiv.org/abs/1705.03307, you decorate the inner (fibrant, endo-) types as special, and leave the exotypes undecorated, privileging the latter. While from a user's perspective, however, it's the (inner) types that are standard/mathematical, and the exotypes that are special.

And regardless of the decorations, the mere fact that we bring in the exoset level makes the theory harder to justify from the philosophical position that general homotopy types are not reducible to sets. One can in fact see the conservativity result as foundational reduction (in the sense of https://math.stanford.edu/~feferman/papers/reductive.pdf section 5) from a system justified by the principle that everything is based on sets to a system justified by a framework where that isn't the case.

Another connection is that it seems it should be easier to find an axiom, which might imply SC, that would allow us to construct the type of semi-simplicial types, rather than such an axiom that doesn't imply SC. But I don't know any such axiom statable in book HoTT either way.

BTW, you probably meant “simplicial set” above. And yes, that kind of axiom would be the strongest expression of “everything is based sets”, and it currently needs 2LTT to even be stated.

Cheers,
Ulrik

### Nicolai Kraus

May 10, 2020, 12:13:26 PM5/10/20
to Michael Shulman, Thorsten Altenkirch, Jon Sterling, 'Martin Escardo' via Homotopy Type Theory
I have to correct what I said an hour ago (thanks, Mike). We don't know whether "exo-Nat is cofibrant" implies that exo-limits of towers are fibrant. (And probably it doesn't.)
In other words, we don't know the connection between axioms (A2) and (A3) in arXiv:1705.03307.
-- Nicolai

### Michael Shulman

May 10, 2020, 12:29:08 PM5/10/20
Okay. But the implication works in the other way, doesn't it? A
product indexed by exo-Nat is the exo-limit of a tower of finite
products. So maybe the tower axiom is the best one.
> To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CA%2BAZBBrJF92OezfqYyh9vy-JQNesC8%2BpacAPPrq-xDZN5Y6qNQ%40mail.gmail.com.

### Michael Shulman

May 10, 2020, 12:31:01 PM5/10/20
to Ulrik Buchholtz, Homotopy Type Theory
I realize this may be controversial too, but I think there's at least
one sense in which sets are "more fundamental", namely that ordinary
syntax consists of sets, because it is a (non-higher) inductive type.
I think this is kind of the "reason" for the conservativity theorem.

I don't think this fact detracts from the importance and independence
of the homotopical point of view, any more than the fact that (say)
finite sets have decidable equality detracts from the importance of
constructivism. It's just the fact that simpler things are simpler.
> --
> 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/7b9eb7c9-040a-46e8-b470-28958f8d7713%40googlegroups.com.

### Nicolai Kraus

May 10, 2020, 12:51:30 PM5/10/20
to Joyal, André, Thomas Streicher, David Roberts, Thorsten Altenkirch, Michael Shulman, Steve Awodey, homotopyt...@googlegroups.com
Dear André and everyone,

I feel it's worth pointing out that there are two strategies to express
"everyday mathematics" in HoTT. In CS-speak, they would probably be
called "shallow embedding" and "deep embedding". Shallow embedding is
the "HoTT style", deep embedding is the "pre-HoTT type theory style".
Shallow means that one uses that the host language shares structure with
the object one wants to define, while deep means one doesn't. To explain
what I mean, let's look at the type theoretic definition of a group (a
1-group, not a higher group).

Definition using deep embedding: A group is a tuple
(X,h,e,o,i,assoc,...), where
X : Type     -- carrier
h : is-0-truncated(X)     -- carrier is set
e : X   -- unit
o : X * X -> X     -- composition
i : X -> X     -- inverses
assoc : (h o g) o f = h o (g o f)
... [and so on]

Definition using shallow embedding: A group is a pointed connected 1-type.

Fortunately, these definitions are equivalent (via the Eilenberg-McLan
spaces construction). But they behave differently when we want to work
with them or change them. It's easy to change the second definition to
define infinity groups instead of 1-groups (see e.g. arXiv:1802.04315 ,
arXiv:1805.02069, and Ulrik's comment). But it's unclear whether there
is a nice way for the first definition. The second definition has better
computational properties than the first.

When you say this:

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

You are referring to shallow embedding. In everyday mathematics, you
don't say (1) either. You probably say (1) with "Type" replaced by "Set"
or by "simplicial set". Both of these can be expressed straightforwardly
in type theory using only (h-)sets (i.e. embedding deeply).

We strive to use shallow embedding as often as possible for the reasons
in the above example. But let's assume that we *can* say (1) in HoTT,
using "Type", because we find some encoding that we're reasonably happy
with; there's a question which I've asked myself before:

Will we not destroy the advantages of deep (over shallow) embedding if
we fall back to encodings (and thus destroy the main selling point of
HoTT)? For me, the justification of still using deep embedding is that
statements using encodings (e.g. "the universe is a higher category)
might still imply statements which don't use encodings and are
interesting. However, if we want to develop a theory of certain higher
structures for it's own sake, then it's not so clear to me whether it's
really better to use the HoTT-style deep embedding.

Kind regards,
Nicolai

### Joyal, André

May 10, 2020, 2:04:30 PM5/10/20
to Ulrik Buchholtz, Homotopy Type Theory
Dear Ulrik,

You wrote:

<<The 2-level type theories can be viewed as another way of making a type theory that is faithful to the idea that everything is based on sets. I like to think of the outer layer as an exoskeleton for type theory, giving it a bit of extra strength while we don't know how to use its own powers fully, or whether indeed it is strong enough to effect constructions like that of simplicial types. Every type (which for me is a fibrant type, since that's the mathematically meaningful ones) has a corresponding exotype (indeed an exoset), but there are more exotypes, such as the exonatural numbers, which are sometimes useful.>>

I like the idea of calling exo-skeleton the outer layer of a type theory.
Category theorists like to distinguish between the internal and the external properties of a category.
Logician are distinguishing a formal theory from its meta-theory.
A theory and its meta-theory may interact as in Gödel's incompleteness theorem.
There are two layers interacting in ML type theory.
Is it possible to interpret the outer layer internally, as in Gödel's incompleteness theorem?

You wrote:

<<Again, let me remind everyone, that groups are precisely one of the few structures we know how to handle (along with grouplike E_n-types, and connective/general spectra): To equip a type G with a group structure is to give a pointed connected type BG and an equivalence of G with the loop type of BG. The type of objects of Gr is the universe of pointed, connected types.>>

I like the idea of studying groups via the equivalence between groups and pointed connected spaces.
It is one of the great miracle of homotopy theory (discovered by Kan).
It is quite amazing if you think about it: (non-abelian) groups were introduced for the purpose
of studying symmetries, mostly in Galois theory. The fundamental group of a space was introduced
by Poincaré to study covering spaces in connection with the Klein-Poincaré
uniformisation theorem for Riemann surfaces. The loop space of a pointed space
is a kind of beef-up version of the fundamental group; the fact that it contains
all the homotopy invariant informations about that space is a great marvel.
Topologists are interested in nilpotent groups (ex. the work of Hilton) and
the connection with Lie algebras (the Whitehead bracket).
By a theorem of Quillen, connected differential graded Lie algebras are rational models of simply connected spaces.
Also, in Goodwillie's calculus, the derivative of the identity functor is the Lie algebra operad.

I am afraid the equivalence between groups and pointed connected spaces
will be meaningless (tautological) if the former is defined to be the latter.

Best,
André

From: homotopyt...@googlegroups.com [homotopyt...@googlegroups.com] on behalf of Ulrik Buchholtz [ulrikbu...@gmail.com]
Sent: Sunday, May 10, 2020 8:53 AM
To: Homotopy Type Theory

Subject: Re: [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.

### Nicolai Kraus

May 10, 2020, 2:18:36 PM5/10/20
to Michael Shulman, homotopyt...@googlegroups.com
Yes, this is nice. We should add it to the next revision of the paper (arXiv:1705.03307).

### Nicolai Kraus

May 10, 2020, 2:56:20 PM5/10/20
to Ulrik Buchholtz, Homotopy Type Theory
On Sun, May 10, 2020 at 4:35 PM Ulrik Buchholtz <ulrikbu...@gmail.com> wrote:
No need to apologize: I know I was being slightly provocative by juxtaposing a question about sets cover (SC) and a comment on 2-level type theory in this context, in order to provoke some discussion :-)

It worked :-)

Wouldn't you agree, however, that even though basic 2LTT is conservative over HoTT, from a certain point of view, 2LTT privileges the “ground floor” exosets? In your very nice paper, https://arxiv.org/abs/1705.03307, you decorate the inner (fibrant, endo-) types as special, and leave the exotypes undecorated, privileging the latter. While from a user's perspective, however, it's the (inner) types that are standard/mathematical, and the exotypes that are special.

I think I see where you are coming from. But for me, decorating the inner types as special was simply a pragmatic choice, not a philosophical one. Since most/all statements in the paper are "proper" 2LTT, there are more exo- / outer types involved than endo- / inner ones. But as a user, one is interested in the fibrant types (and maybe even assumes that they coincide with the inner theory), and only adds some small exo-sprinkles like "exo-Nat is cofibrant"; then, it makes sense to decorate the exo-types instead, as e.g. in https://arxiv.org/abs/2004.06572
And maybe it would be less confusing if we did the same in the paper that you linked to. I'm not sure.

And regardless of the decorations, the mere fact that we bring in the exoset level makes the theory harder to justify from the philosophical position that general homotopy types are not reducible to sets. One can in fact see the conservativity result as foundational reduction (in the sense of https://math.stanford.edu/~feferman/papers/reductive.pdf section 5) from a system justified by the principle that everything is based on sets to a system justified by a framework where that isn't the case.

That's interesting, thanks for the link!

Another connection is that it seems it should be easier to find an axiom, which might imply SC, that would allow us to construct the type of semi-simplicial types, rather than such an axiom that doesn't imply SC. But I don't know any such axiom statable in book HoTT either way.

Good question.

BTW, you probably meant “simplicial set” above. And yes, that kind of axiom would be the strongest expression of “everything is based sets”, and it currently needs 2LTT to even be stated.

You're right, I meant "set". (Otherwise it'd be silly, a type X is the realization of the [fibrant replacement of] the constant presheaf X.)

Nicolai

Cheers,
Ulrik

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

### Michael Shulman

May 10, 2020, 2:58:04 PM5/10/20
to Nicolai Kraus, Joyal, André, Thomas Streicher, David Roberts, Thorsten Altenkirch, Steve Awodey, homotopyt...@googlegroups.com
On Sun, May 10, 2020 at 9:51 AM Nicolai Kraus <nicola...@gmail.com> wrote:
> It's easy to change the second definition to
> define infinity groups instead of 1-groups (see e.g. arXiv:1802.04315 ,
> arXiv:1805.02069, and Ulrik's comment). But it's unclear whether there
> is a nice way for the first definition.

On the other hand, it's easy to change the first definition to define
monoids/semigroups/rings/fields/lattices/universal-algebras/etc., and
impossible to do the same for the second. I think the fact that
groups are part of the general theory of algebraic structures on sets
is more important to incorporate in a definition. The equivalence
between groups and connected pointed 1-types is better viewed as a
theorem than a definition.

And hence, the "definition" of oo-groups as connected pointed types is
more of a hack than a true definition. In an ideal world, that would
be a theorem too. (And the corresponding theorem in classical
mathematics has important content: there are important oo-groupoids
that are obtained by delooping oo-groups nontrivially.)

### Thorsten Altenkirch

May 10, 2020, 3:15:16 PM5/10/20
to Michael Shulman, nicolai.kraus, Jon Sterling, 'Martin Escardo' via Homotopy Type Theory, nicolai.kraus
I thought so but now Nicolai says it is not?

From a type-theoretic point of view it seems more natural to say that indexed M-types are fibrant even if the index is not. Saying that natural numbers are cofibrant assigns a special role to one particular inductive type.

Thorsten

### Nicolai Kraus

May 10, 2020, 3:18:23 PM5/10/20
to Joyal, André, Thomas Streicher, David Roberts, Thorsten Altenkirch, Michael Shulman, Steve Awodey, homotopyt...@googlegroups.com
In the last paragraph of my message below, the words "deep" and "shallow" have to be swapped.

### Thorsten Altenkirch

May 10, 2020, 3:20:42 PM5/10/20
to Michael Shulman, Jon Sterling, 'Martin Escardo' via Homotopy Type Theory

﻿On 10/05/2020, 15:06, "Michael Shulman" <shu...@sandiego.edu> wrote:

On Sun, May 10, 2020 at 4:46 AM Thorsten Altenkirch
<Thorsten....@nottingham.ac.uk> wrote:
> Defining simplicial types isn't entirely straightforward (as you know I suppose), because Delta is not directed. We can do semi-simplicial types as a Reedy limit, i.e. an infinite Sigma type

We can certainly *talk* about simplicial types in 2LTT as exofunctors
from the exocategory Delta to the exocategory Type. I assume the
point you're making is that we don't have a (fibrant) *type of*
simplicial types, whereas we do have a fibrant type of semisimplicial
types (under appropriate axioms)?

Yes, by talking about I meant within HoTT. I mean we want to understand them as structures not just as some set-level encoding.

Also I find the Kan-condition more natural in HoTT because we just need to state an equivalence. On the level of set-level Mathematics we either hide the witness or we need to introduce uniformity conditions.

I also don't think it is an issue that Delta is not direct because Delta is based on the hack to build identities into the framework but obtain composition via the Kan condition. Hence I think we should represent identities in the same way as composition.

> You need some extra principles, e.g. that strict Nat is fibrant or maybe better that certain coinductive types exist.

Personally, I think the best axiom to use here is that exo-Nat is
*cofibrant*, i.e. Pi-types with domain exo-Nat preserve fibrancy. We
don't know how to model "exo-Nat is fibrant" in all higher toposes,
but it's easy to interpret "exo-Nat is cofibrant" in such models,
since Pi-types with domain exo-Nat are just externally-infinite
products.