Re: [HoTT] Identity versus equality

[Steve Awodey <steve...@gmail.com>]

Dear André,

I would prefer to say that t current systems of type theory have failed to *compute* pi_4(S^3), so as not to diminish the value of Guillaume’s beautiful proof, which has even been formally checked in different proof assistants. 
You of course know the difference between proving something in type theory and computing the value of a term, but some readers may not. 

Best wishes,

Steve 

Ps: In my opinion, for what it’s worth, making a system that will compute the value of Brunerie’s constant is an engineering problem, not a mathematical one. Which is not to say it would not be an important advance!

> On May 8, 2020, at 17:06, Joyal, André <joyal...@uqam.ca> wrote:
> 
> Dear Thomas,
> 
> You 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.