To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/8C57894C7413F04A98DDF5629FEC90B1652F515E%40Pli.gst.uqam.ca.
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
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.
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.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/8C57894C7413F04A98DDF5629FEC90B1652F526C%40Pli.gst.uqam.ca.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/67E9DCCA-F9CA-45B7-9AC8-E5A7E94FE9A9%40nottingham.ac.uk.
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)
--
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.
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,
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
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,
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,