RE: [HoTT] Identity versus equality

["Joyal, André" <"joyal..."@uqam.ca>]

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
Subject: Re: [HoTT] Identity versus equality

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


On Sat, May 9, 2020, at 4:18 PM, Joyal, André wrote:
> 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,
>
> > 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
>
> --
> 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/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 HomotopyT...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/b1d32ac0-e364-4405-9e48-e0e1e0b37732%40www.fastmail.com.