51 views

Skip to first unread message

May 5, 2020, 4:48:13 AM5/5/20

to HomotopyT...@googlegroups.com

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!

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é

--

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.

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.

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

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

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.

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.

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.

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

May 6, 2020, 4:31:01 PM5/6/20

to Steve Awodey, Michael Shulman, HomotopyT...@googlegroups.com

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

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.

Thorsten

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.

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.

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

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.

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

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

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

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

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

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

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

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

May 7, 2020, 12:13:19 PM5/7/20

to Thomas Streicher, Thorsten Altenkirch, Michael Shulman, Steve Awodey, homotopyt...@googlegroups.com

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)

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

David Roberts

Webpage: https://ncatlab.org/nlab/show/David+Roberts

Blog: https://thehighergeometer.wordpress.com

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.

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é

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,

David

David Roberts

Webpage: https://ncatlab.org/nlab/show/David+Roberts

Blog: https://thehighergeometer.wordpress.com

Webpage: https://ncatlab.org/nlab/show/David+Roberts

Blog: https://thehighergeometer.wordpress.com

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!

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!

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,

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,

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

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

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

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

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

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

>

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

>

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

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

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,

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

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

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.

fibrant... They have them as pretypes. But maybe I misunderstand...

Thomas

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,

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

>

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

>

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.

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

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

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

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

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.

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

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

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!

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.

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

Cheers,

Thorsten

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.

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

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

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

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.

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.

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

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.

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

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

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.

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

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.

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?

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?

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

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.

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

May 10, 2020, 11:23:18 AM5/10/20