Re: [HoTT] Identity versus equality

["Jon Sterling" <j...@jonmsterling.com>]

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



On Fri, May 8, 2020, at 10:46 PM, Joyal, André wrote:
> 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
> Subject: Re: [HoTT] Identity versus equality
> 
> Dear André,
> 
> I would prefer to say that t current systems of type theory have failed 
> to *compute* pi_4(S^3), so as not to diminish the value of Guillaume’s 
> beautiful proof, which has even been formally checked in different 
> proof assistants.
> You of course know the difference between proving something in type 
> theory and computing the value of a term, but some readers may not.
> 
> Best wishes,
> 
> Steve
> 
> Ps: In my opinion, for what it’s worth, making a system that will 
> compute the value of Brunerie’s constant is an engineering problem, not 
> a mathematical one. Which is not to say it would not be an important 
> advance!
> 
> > On May 8, 2020, at 17:06, Joyal, André <joyal...@uqam.ca> wrote:
> >
> > Dear Thomas,
> >
> > You 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,
> >
> > 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!
> >
> > --
> > 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 HomotopyT...@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 HomotopyT...@googlegroups.com.
> To view this discussion on the web visit 
> https://groups.google.com/d/msgid/HomotopyTypeTheory/8C57894C7413F04A98DDF5629FEC90B1652F5565%40Pli.gst.uqam.ca.
>