Univalent type theory
1 view
Skip to first unread message
Martin Escardo
Mar 12, 2016, 6:05:31 PM3/12/16
to HomotopyT...@googlegroups.com
Does anybody object to the terminology of the title?
I want to avoid several things: priorities, applications, foundations.
Homotopy Type Theory suggests applications of type theory to Homotopy
(where I personally see things the other way round, with Homotopy giving
input to type theory).
Univalent Foundations sounds like we are talking about logic (I like
logic, but my interest in univalent type theory is mathematical, rather
than logical - at least at the moment.).
Of course, people (including myself) are free to continue to use
Homotopy Type Theory and Univalent Foundations as possible
terminologies. And these terminologies are there to stay with us.
It just seems to me that this third (additional) terminology, suggests a
more neutral mathematical point of view, in particular compatible with
HoTT and UF (whatever they are).
In my usage, "univalent type theory" is not a particular formal system.
It is not even a formal system, although I will always be happy for it
to have underlying formal systems we can refer to when we need to (and
in which we can write computer proofs when we want to, if we want to -
which I often do).
Finally, I didn't invent this terminology. I've just found myself
uttering it. Perhaps I heard it from somebody else.
M.
I want to avoid several things: priorities, applications, foundations.
Homotopy Type Theory suggests applications of type theory to Homotopy
(where I personally see things the other way round, with Homotopy giving
input to type theory).
Univalent Foundations sounds like we are talking about logic (I like
logic, but my interest in univalent type theory is mathematical, rather
than logical - at least at the moment.).
Of course, people (including myself) are free to continue to use
Homotopy Type Theory and Univalent Foundations as possible
terminologies. And these terminologies are there to stay with us.
It just seems to me that this third (additional) terminology, suggests a
more neutral mathematical point of view, in particular compatible with
HoTT and UF (whatever they are).
In my usage, "univalent type theory" is not a particular formal system.
It is not even a formal system, although I will always be happy for it
to have underlying formal systems we can refer to when we need to (and
in which we can write computer proofs when we want to, if we want to -
which I often do).
Finally, I didn't invent this terminology. I've just found myself
uttering it. Perhaps I heard it from somebody else.
M.
Joyal, André
Mar 13, 2016, 8:14:52 AM3/13/16
to Martin Escardo, HomotopyT...@googlegroups.com
Dear Martin,
I like the idea of "Univalent Type Theory".
Thank you very much.
André
________________________________________
From: HomotopyT...@googlegroups.com [HomotopyT...@googlegroups.com] on behalf of Martin Escardo [m.es...@cs.bham.ac.uk]
Sent: Saturday, March 12, 2016 6:05 PM
To: HomotopyT...@googlegroups.com
Subject: [HoTT] Univalent type theory
M.
--
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.
For more options, visit https://groups.google.com/d/optout.
Martin Escardo
May 3, 2016, 6:35:15 PM5/3/16
to Joyal, André, HomotopyT...@googlegroups.com
Here is another attempt to justify the terminology "univalent type theory":
"Univalent type theory" is what the two subjects "univalent foundations"
and "homotopy type theory" have in common.
The former proposes a new understanding of mathematics in general, based
on (a suitable) univalent type theory (with input from homotopy theory).
This is univalent foundations.
The latter proposes a new ("synthetic") approach to homotopy theory,
again based on (a suitable) univalent type theory. This is homotopy type
theory.
The HoTT Book addresses both, but fails to make the distinction
explicit, or even recognize that there is a distinction.
The core underlying the two is interesting on its own right, and
deserves its own name. And "univalent type theory" is a natural one.
Of course, it has to be made explicit that this doesn't refer to any
particular (formal or informal) type theory. But it does refer to the
type-theoretic view of the mathematical world (in both cases).
Martin
--
Martin Escardo
http://www.cs.bham.ac.uk/~mhe
"Univalent type theory" is what the two subjects "univalent foundations"
and "homotopy type theory" have in common.
The former proposes a new understanding of mathematics in general, based
on (a suitable) univalent type theory (with input from homotopy theory).
This is univalent foundations.
The latter proposes a new ("synthetic") approach to homotopy theory,
again based on (a suitable) univalent type theory. This is homotopy type
theory.
The HoTT Book addresses both, but fails to make the distinction
explicit, or even recognize that there is a distinction.
The core underlying the two is interesting on its own right, and
deserves its own name. And "univalent type theory" is a natural one.
Of course, it has to be made explicit that this doesn't refer to any
particular (formal or informal) type theory. But it does refer to the
type-theoretic view of the mathematical world (in both cases).
Martin
Martin Escardo
http://www.cs.bham.ac.uk/~mhe
Michael Shulman
May 3, 2016, 7:25:10 PM5/3/16
to Martin Escardo, Joyal, André, HomotopyT...@googlegroups.com
The way I use the term, "homotopy type theory" is much more than just
synthetic homotopy theory. It refers to the entire subject of the
interaction between homotopical ideas and type-theoretic ideas,
including applications of type theory to homotopy theory and also
applications of homotopy theory to type theory: both "homotopy (type
theory)" and "(homotopy type) theory" and everything in between.
synthetic homotopy theory. It refers to the entire subject of the
interaction between homotopical ideas and type-theoretic ideas,
including applications of type theory to homotopy theory and also
applications of homotopy theory to type theory: both "homotopy (type
theory)" and "(homotopy type) theory" and everything in between.
Vladimir Voevodsky
May 4, 2016, 6:13:57 AM5/4/16
to Martin Escardo, "Joyal, André", HomotopyT...@googlegroups.com
Hello,
I have given it some thought and I think that it is a little imprecise.
It is reasonable to call the study of type theories that satisfy the univalence axiom (e.g. MLTT + UA or Coquand’s cubical type theory) or even type theories that satisfy the univalence as a meta-principle the "univalent type theory".
It is, however, more reasonable to call the study of more general type theories inspired by the homotopy theory such as HTS and its versions or the Angiuli-Harper-Wilson type theory that has exact equality and therefore is not univalent “homotopy type theory”.
Univalent foundations are not inherently attached to type theory as their meta-language. We can talk about UF/UniMath or UF/HoTT or UF/(the abbreviation for Coquand’s cubical type theory here). UF however is more of a philosophical construct based on the idea that mathematics studies structures on collections that can be seen through the eye of set theory as infinity groupoids or other objects representing homotopy types. UF then subdivides those collections into collections of various h-levels 0,1,2,…, infinity and introduces other structure in this world of collections that connects them to mathematical concepts such as number systems or Cantor sets.
UF in this sense remains unarticulated.
Vladimir.
I have given it some thought and I think that it is a little imprecise.
It is reasonable to call the study of type theories that satisfy the univalence axiom (e.g. MLTT + UA or Coquand’s cubical type theory) or even type theories that satisfy the univalence as a meta-principle the "univalent type theory".
It is, however, more reasonable to call the study of more general type theories inspired by the homotopy theory such as HTS and its versions or the Angiuli-Harper-Wilson type theory that has exact equality and therefore is not univalent “homotopy type theory”.
Univalent foundations are not inherently attached to type theory as their meta-language. We can talk about UF/UniMath or UF/HoTT or UF/(the abbreviation for Coquand’s cubical type theory here). UF however is more of a philosophical construct based on the idea that mathematics studies structures on collections that can be seen through the eye of set theory as infinity groupoids or other objects representing homotopy types. UF then subdivides those collections into collections of various h-levels 0,1,2,…, infinity and introduces other structure in this world of collections that connects them to mathematical concepts such as number systems or Cantor sets.
UF in this sense remains unarticulated.
Vladimir.
Martin Escardo
May 4, 2016, 6:19:21 PM5/4/16
to Vladimir Voevodsky, Joyal, André, HomotopyT...@googlegroups.com
Thanks, Vladimir, for explicitly stating your view.
On 04/05/16 11:13, Vladimir Voevodsky wrote:
> It is reasonabe-le to call the study of type theories that satisfy the
> It is, however, more reasonable to call the study of more general
> type theories inspired by the homotopy theory such as HTS and its
> versions or the Angiuli-Harper-Wilson type theory that has exact
> equality and therefore is not univalent “homotopy type theory”.
I don't think I understand this sentence.
> Univalent foundations are not inherently attached to type theory as
> their meta-language.
OK. (But to understand this, I would like to have a hint of what a
non-type-theoretical rendering of UF could be.)
> We can talk about UF/UniMath or UF/HoTT or
> UF/(the abbreviation for Coquand’s cubical type theory here). UF
> however is more of a philosophical construct
I like this point of view, and it is my point of view too.
> based on the idea that mathematics studies structures on collections
> that can be seen through the eye of set theory as infinity groupoids
> or other objects representing homotopy types.
Exactly.
> UF then subdivides those collections into collections of various
> h-levels 0,1,2,…, infinity and introduces other structure in this
> world of collections that connects them to mathematical concepts
> such as number systems or Cantor sets.
Again I concur.
> UF in this sense remains unarticulated.
Good. And I concur here too.
Also univalent type theory remains unarticulated, and we are familiar
with a number of renderings of it, such as the Coq libraries, the Agda
libraries, cubicaltt, and more.
It is good that you have explicitly mentioned philosophy above.
Before most people in this list were born, including myself, Brouwer
postulated axioms for intuitionistic mathematics that made sets/types
to be spaces.
This was not called "topological type theory", though. And I am happy
it wasn't.
What *did* happen was that (1) topological understanding informed
intuitionistic mathematics, and (2) intuitionistic mathematics
provided a way to perform synthetic topology.
But hopefully, despite the incredibly precise match, nobody confuses
intuitionistic mathematics with synthetic topology.
It seems to me that the terminology "homotopy type theory" creates
precisely this kind of confusion. For instance, last week, in Prague,
a homotopy theorist, before any conversation even started, plainly
said to me "My work has nothing to benefit from Homotopy Type Theory",
even though my advertised talk (on univalence) didn't even mention
homotopy.
Martin
On 04/05/16 11:13, Vladimir Voevodsky wrote:
> It is reasonabe-le to call the study of type theories that satisfy the
> univalence axiom (e.g. MLTT + UA or Coquand’s cubical type theory)
> or even type theories that satisfy the univalence as a
> meta-principle the "univalent type theory".
Good.
> or even type theories that satisfy the univalence as a
> meta-principle the "univalent type theory".
> It is, however, more reasonable to call the study of more general
> type theories inspired by the homotopy theory such as HTS and its
> versions or the Angiuli-Harper-Wilson type theory that has exact
> equality and therefore is not univalent “homotopy type theory”.
> Univalent foundations are not inherently attached to type theory as
> their meta-language.
non-type-theoretical rendering of UF could be.)
> We can talk about UF/UniMath or UF/HoTT or
> UF/(the abbreviation for Coquand’s cubical type theory here). UF
> however is more of a philosophical construct
> based on the idea that mathematics studies structures on collections
> that can be seen through the eye of set theory as infinity groupoids
> or other objects representing homotopy types.
> UF then subdivides those collections into collections of various
> h-levels 0,1,2,…, infinity and introduces other structure in this
> world of collections that connects them to mathematical concepts
> such as number systems or Cantor sets.
> UF in this sense remains unarticulated.
Also univalent type theory remains unarticulated, and we are familiar
with a number of renderings of it, such as the Coq libraries, the Agda
libraries, cubicaltt, and more.
It is good that you have explicitly mentioned philosophy above.
Before most people in this list were born, including myself, Brouwer
postulated axioms for intuitionistic mathematics that made sets/types
to be spaces.
This was not called "topological type theory", though. And I am happy
it wasn't.
What *did* happen was that (1) topological understanding informed
intuitionistic mathematics, and (2) intuitionistic mathematics
provided a way to perform synthetic topology.
But hopefully, despite the incredibly precise match, nobody confuses
intuitionistic mathematics with synthetic topology.
It seems to me that the terminology "homotopy type theory" creates
precisely this kind of confusion. For instance, last week, in Prague,
a homotopy theorist, before any conversation even started, plainly
said to me "My work has nothing to benefit from Homotopy Type Theory",
even though my advertised talk (on univalence) didn't even mention
homotopy.
Martin
Vladimir Voevodsky
May 5, 2016, 5:01:53 AM5/5/16
to Martin Escardo, "Joyal, André", HomotopyT...@googlegroups.com
The universe of all types in HTS is not univalent and if you add the univalence axiom for this universe to the theory then the theory will become inconsistent. Only the universe of fibrant types in the HTS can be made univalent by the addition of the univalence axiom.
Vladimir.
Michael Shulman
May 6, 2016, 5:02:38 PM5/6/16
to Vladimir Voevodsky, Martin Escardo, Joyal, André, HomotopyT...@googlegroups.com
Vladimir, are you saying that you would *not* call HTS a "univalent
type theory", even though the fibrant types therein do satisfy
univalence?
type theory", even though the fibrant types therein do satisfy
univalence?
0 new messages