Re: [HoTT] Identity versus equality

[Thorsten Altenkirch <Thorsten....@nottingham.ac.uk>]

Hi Jon,

I just had an exchange with Andre regarding this which I forgot to cc to the list.

Defining simplicial types isn't entirely straightforward (as you know I suppose), because Delta is not directed. We can do semi-simplicial types as a Reedy limit, i.e. an infinite Sigma type (actually you can do it as a coinductive definition). You need some extra principles, e.g. that strict Nat is fibrant or maybe better that certain coinductive types exist. 

However, presheaves over Delta cannot be written as a Reedy limit. Now there are a number of ways to address this. We can work with semi-simplicial sets and add Hornfillers by stating equivalences (there is no coherence problem because these are propositional). To regain identities we can add the assumption that the higher category is univalent (i.e. for every object the type of objects paired with an equivalence is contractible) which entails the existence of degeneracies. 

The question of how to define simplicial types remains however. I find that looking at the lower levels of simplicial presheaves it is actually strange that binary composition is handled via horn-fillers whlle identity, i.e. nullary composition, is built into the structure. Maybe we should treat identity in the same way as composition, which means that we introduce a family modelling degeneracies. 

What I mean is that if we write down the first levels of a semisimplicial type we have

X0 : U
X1 : X0 -> X0 -> U
X2 : (x0,x1,x2 : X0) -> X0 x0 x1 -> X0 x1 x2 -> X0 x0 x2 -> U

But we can add degeneracies by adding families which say that some object is a degeneracy:

I0 : (x0 : X0) -> X1 x0 x0 -> U
I1_0 : (x0 x1 : X0)(f : X1 x0 x1)(i : X1 x0 x0) -> I0 x0 i -> X2 x0 x1 x1 i f f -> U
I1_1 : (x0 x1 : X0)(f : X1 x0 x1)(i : X1 x1 x1) -> I0 x1 i -> X2 x0 x0 x1 f i f -> U

That is while X2 can be viewed as a proof-relevant predicate that a triangle commutes, I0 is a predicate that an arrow is an identity and I1_0 , I1_1 are predicates that triangles are degenerate.

Adding horn-fillers type-theoretically corresponds to saying that certain types are contractible:

(x0,x1,x2 : X0)(f : X1 x0 x1)(g : X1 x1 x2) -> is-contractible ((h : X1 x0 x2) \times X2 x0 x1 x2 f g h)

where is-contractible(A) = (a : A) \times ((x : A) -> a = x)

Similarly we can add degeneracies

(x0 : X0) -> is-contractible (X1 x0 x0)
(x0 x1 : X0)(f : X1 x0 x1)(i : X1 x0 x0)(j : I0 x0 i) -> is-contractible ((x :  X2 x0 x1 x1 i f f) \times I1_0 x0 x1 f i j x)
(x0 x1 : X0)(f : X1 x0 x1)(i : X1 x1 x1)(j : I0 x0 i) -> is-contractible ((x :  X2 x0 x0 x1 f i f) \times I1_0 x1 x1 f i j x)

This is related to Kraus' & Sattler's directed replacement:
https://arxiv.org/abs/1704.04543

Andre mentioned that degeneracies play an important role in the classical theory of simplicial sets, e.g. to show that geometric realisation preserves finite limits. However, the situation is quote different here because we work with types not sets. Hence you would expect that the topologies are also higher-dimensional objects. Has anybody looked at this?

Thorsten

On 09/05/2020, 22:28, "homotopyt...@googlegroups.com on behalf of Jon Sterling" <homotopyt...@googlegroups.com on behalf of j...@jonmsterling.com> wrote:

    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.




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.