unwanted equality proofs described as main problem

[nicolaikraus]

In the preface of the book, there is a discussion about identity proofs in an h-set which are not judgmentally equal to reflexivity:

"In some cases, the proliferation of such superfluous identity terms makes it very difficult or impossible to formulate what should be a straightforward concept, such as the definition of a (semi-)simplicial type."

While it is true that these equality proofs add a lot of unwanted difficulties (I myself have asked Dan whether he knew a clever trick to do something about it in Agda), they are not at all the reason why it is "very difficult or impossible" to define semi-simplicial types. Am I the only one who finds the quoted sentence somewhat misleading?

[guillaumebrunerie]

What is the reason then?

[mikeshulman]

There are other reasons why this is a difficult problem, but I was under the impression that Vladimir and Hugo had clever and mostly successful approaches to it which founded on exactly the problem of such garbage paths in Nat, motivating Vladimir to suggest his type theory with two equalities.

Perhaps "what should be a straightforward concept" is too glib, however, given how much work it took the two of them to get even to that point. (-:

On Fri, Apr 5, 2013 at 12:11 AM, nicolaikraus notifications@github.comwrote:

In the preface of the book, there is a discussion about identity proofs in an h-set which are not judgmentally equal to reflexivity:

"In some cases, the proliferation of such superfluous identity terms makes it very difficult or impossible to formulate what should be a straightforward concept, such as the definition of a (semi-)simplicial type."

While it is true that these equality proofs add a lot of unwanted difficulties (I myself have asked Dan whether he knew a clever trick to do something about it in Agda), they are not at all the reason why it is "very difficult or impossible" to define semi-simplicial types. Am I the only one who finds the quoted sentence somewhat misleading?

— Reply to this email directly or view it on GitHubhttps://github.com/HoTT/book/issues/69 .

[awodey]

the "straighforward concept" is just that of a functor Delta --> type the problem is exactly all the garbage paths -- if they weren't there, it would be easy. with them in there, one has to do something else tricky. the attempts at that have been given so far have still choked on the proliferation of coherence conditions arizing from the garbage.

On Apr 5, 2013, at 12:17 AM, Mike Shulman notifications@github.com wrote:

There are other reasons why this is a difficult problem, but I was under the impression that Vladimir and Hugo had clever and mostly successful approaches to it which founded on exactly the problem of such garbage paths in Nat, motivating Vladimir to suggest his type theory with two equalities.

Perhaps "what should be a straightforward concept" is too glib, however, given how much work it took the two of them to get even to that point. (-:

On Fri, Apr 5, 2013 at 12:11 AM, nicolaikraus notifications@github.comwrote:

In the preface of the book, there is a discussion about identity proofs in an h-set which are not judgmentally equal to reflexivity:

"In some cases, the proliferation of such superfluous identity terms makes it very difficult or impossible to formulate what should be a straightforward concept, such as the definition of a (semi-)simplicial type."

While it is true that these equality proofs add a lot of unwanted difficulties (I myself have asked Dan whether he knew a clever trick to do something about it in Agda), they are not at all the reason why it is "very difficult or impossible" to define semi-simplicial types. Am I the only one who finds the quoted sentence somewhat misleading?

— Reply to this email directly or view it on GitHubhttps://github.com/HoTT/book/issues/69 .

— Reply to this email directly or view it on GitHub.

[mikeshulman]

Wait... the problem with a functor Delta -> Type is not the garbage paths in Nat, it's making precise what you mean by coherence conditions for a functor-up-to-homotopy at all levels, which I think is a much more serious problem than garbage paths. It's only after you decide to deal with that first problem by going Reedy fibrant that the garbage paths in Nat start to be the problem.

On Fri, Apr 5, 2013 at 12:26 AM, Steve Awodey notifications@github.comwrote:

the "straighforward concept" is just that of a functor Delta --> type the problem is exactly all the garbage paths -- if they weren't there, it would be easy. with them in there, one has to do something else tricky. the attempts at that have been given so far have still choked on the proliferation of coherence conditions arizing from the garbage.

On Apr 5, 2013, at 12:17 AM, Mike Shulman notifications@github.com wrote:

There are other reasons why this is a difficult problem, but I was under the impression that Vladimir and Hugo had clever and mostly successful approaches to it which founded on exactly the problem of such garbage paths in Nat, motivating Vladimir to suggest his type theory with two equalities.

Perhaps "what should be a straightforward concept" is too glib, however, given how much work it took the two of them to get even to that point. (-:

On Fri, Apr 5, 2013 at 12:11 AM, nicolaikraus notifications@github.comwrote:

In the preface of the book, there is a discussion about identity proofs in an h-set which are not judgmentally equal to reflexivity:

"In some cases, the proliferation of such superfluous identity terms makes it very difficult or impossible to formulate what should be a straightforward concept, such as the definition of a (semi-)simplicial type."

While it is true that these equality proofs add a lot of unwanted difficulties (I myself have asked Dan whether he knew a clever trick to do something about it in Agda), they are not at all the reason why it is "very difficult or impossible" to define semi-simplicial types. Am I the only one who finds the quoted sentence somewhat misleading?

— Reply to this email directly or view it on GitHub< https://github.com/HoTT/book/issues/69> .

— Reply to this email directly or view it on GitHub.

— Reply to this email directly or view it on GitHubhttps://github.com/HoTT/book/issues/69#issuecomment-15938462 .

[awodey]

fair enough.

On Apr 5, 2013, at 12:28 AM, Mike Shulman notifications@github.com wrote:

Wait... the problem with a functor Delta -> Type is not the garbage paths in Nat, it's making precise what you mean by coherence conditions for a functor-up-to-homotopy at all levels, which I think is a much more serious problem than garbage paths. It's only after you decide to deal with that first problem by going Reedy fibrant that the garbage paths in Nat start to be the problem.

On Fri, Apr 5, 2013 at 12:26 AM, Steve Awodey notifications@github.comwrote:

the "straighforward concept" is just that of a functor Delta --> type the problem is exactly all the garbage paths -- if they weren't there, it would be easy. with them in there, one has to do something else tricky. the attempts at that have been given so far have still choked on the proliferation of coherence conditions arizing from the garbage.

On Apr 5, 2013, at 12:17 AM, Mike Shulman notifications@github.com wrote:

There are other reasons why this is a difficult problem, but I was under the impression that Vladimir and Hugo had clever and mostly successful approaches to it which founded on exactly the problem of such garbage paths in Nat, motivating Vladimir to suggest his type theory with two equalities.

Perhaps "what should be a straightforward concept" is too glib, however, given how much work it took the two of them to get even to that point. (-:

On Fri, Apr 5, 2013 at 12:11 AM, nicolaikraus notifications@github.comwrote:

In the preface of the book, there is a discussion about identity proofs in an h-set which are not judgmentally equal to reflexivity:

"In some cases, the proliferation of such superfluous identity terms makes it very difficult or impossible to formulate what should be a straightforward concept, such as the definition of a (semi-)simplicial type."

While it is true that these equality proofs add a lot of unwanted difficulties (I myself have asked Dan whether he knew a clever trick to do something about it in Agda), they are not at all the reason why it is "very difficult or impossible" to define semi-simplicial types. Am I the only one who finds the quoted sentence somewhat misleading?

— Reply to this email directly or view it on GitHub< https://github.com/HoTT/book/issues/69> .

— Reply to this email directly or view it on GitHub.

— Reply to this email directly or view it on GitHubhttps://github.com/HoTT/book/issues/69#issuecomment-15938462 .

— Reply to this email directly or view it on GitHub.

[txa]

Yes, this was my impression too – especially after seeing Richard Garners presentation.

When we try to define semi-simplicial sets you end up having the proof of functoriality of the previous level showing up in the functor part of the next level and so on. This is also the conclusion Hugo seems to have arrived at.

What do you mean "by going Reedy fibrant" ?

[mikeshulman]

Reedy fibrant means having the n-simplices dependent over their boundaries.

On Fri, Apr 5, 2013 at 12:37 AM, Thorsten Altenkirch < notifications@github.com> wrote:

Yes, this was my impression too – especially after seeing Richard Garners presentation.

When we try to define semi-simplicial sets you end up having the proof of functoriality of the previous level showing up in the functor part of the next level and so on. This is also the conclusion Hugo seems to have arrived at.

What do you mean "by going Reedy fibrant" ?

T.

From: Mike Shulman <notifications@github.com<mailto: notifications@github.com>> Reply-To: HoTT/book reply@reply.github.com<mailto:reply@reply.github.com>

Date: Thursday, 4 April 2013 23:28 To: HoTT/book book@noreply.github.com<mailto:book@noreply.github.com> Subject: Re: [book] unwanted equality proofs described as main problem (#69)

Wait... the problem with a functor Delta -> Type is not the garbage paths in Nat, it's making precise what you mean by coherence conditions for a functor-up-to-homotopy at all levels, which I think is a much more serious problem than garbage paths. It's only after you decide to deal with that first problem by going Reedy fibrant that the garbage paths in Nat start to be the problem.

On Fri, Apr 5, 2013 at 12:26 AM, Steve Awodey <notifications@github.com mailto:notifications@github.com>wrote:

the "straighforward concept" is just that of a functor Delta --> type the problem is exactly all the garbage paths -- if they weren't there, it would be easy. with them in there, one has to do something else tricky. the attempts at that have been given so far have still choked on the proliferation of coherence conditions arizing from the garbage.

On Apr 5, 2013, at 12:17 AM, Mike Shulman <notifications@github.com mailto:notifications@github.com> wrote:

There are other reasons why this is a difficult problem, but I was under the impression that Vladimir and Hugo had clever and mostly successful approaches to it which founded on exactly the problem of such garbage paths in Nat, motivating Vladimir to suggest his type theory with two equalities.

Perhaps "what should be a straightforward concept" is too glib, however, given how much work it took the two of them to get even to that point. (-:

On Fri, Apr 5, 2013 at 12:11 AM, nicolaikraus < notifications@github.commailto:notifications@github.com>wrote:

In the preface of the book, there is a discussion about identity proofs in an h-set which are not judgmentally equal to reflexivity:

"In some cases, the proliferation of such superfluous identity terms makes it very difficult or impossible to formulate what should be a straightforward concept, such as the definition of a (semi-)simplicial type."

While it is true that these equality proofs add a lot of unwanted difficulties (I myself have asked Dan whether he knew a clever trick to do something about it in Agda), they are not at all the reason why it is "very difficult or impossible" to define semi-simplicial types. Am I the only one who finds the quoted sentence somewhat misleading?

— Reply to this email directly or view it on GitHub< https://github.com/HoTT/book/issues/69> .

— Reply to this email directly or view it on GitHub.

— Reply to this email directly or view it on GitHub< https://github.com/HoTT/book/issues/69#issuecomment-15938462> .

— Reply to this email directly or view it on GitHub< https://github.com/HoTT/book/issues/69#issuecomment-15938507>.

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 send it back to me, and immediately delete it. Please do not use, copy or disclose the information contained in this message or in any attachment. Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham.

This message has been checked for viruses but the contents of an attachment

may still contain software viruses which could damage your computer system:

you are advised to perform your own checks. Email communications with the

University of Nottingham may be monitored as permitted by UK legislation.

— Reply to this email directly or view it on GitHubhttps://github.com/HoTT/book/issues/69#issuecomment-15938655 .

[peterlefanulumsdaine]

Even in the Reedy fibrant approach, I would say the problem is not so much garbage paths in Nat, as that one can't add definitional equalities to an inductive hypothesis. (The equalities involved are not just in Nat, iirc.)

-p.

Sent from my iPhone

On Apr 5, 2013, at 12:28 AM, Mike Shulman notifications@github.com wrote:

Wait... the problem with a functor Delta -> Type is not the garbage paths in Nat, it's making precise what you mean by coherence conditions for a functor-up-to-homotopy at all levels, which I think is a much more serious problem than garbage paths. It's only after you decide to deal with that first problem by going Reedy fibrant that the garbage paths in Nat start to be the problem.

On Fri, Apr 5, 2013 at 12:26 AM, Steve Awodey notifications@github.comwrote:

the "straighforward concept" is just that of a functor Delta --> type the problem is exactly all the garbage paths -- if they weren't there, it would be easy. with them in there, one has to do something else tricky. the attempts at that have been given so far have still choked on the proliferation of coherence conditions arizing from the garbage.

On Apr 5, 2013, at 12:17 AM, Mike Shulman notifications@github.com wrote:

There are other reasons why this is a difficult problem, but I was under the impression that Vladimir and Hugo had clever and mostly successful approaches to it which founded on exactly the problem of such garbage paths in Nat, motivating Vladimir to suggest his type theory with two equalities.

Perhaps "what should be a straightforward concept" is too glib, however, given how much work it took the two of them to get even to that point. (-:

On Fri, Apr 5, 2013 at 12:11 AM, nicolaikraus notifications@github.comwrote:

In the preface of the book, there is a discussion about identity proofs in an h-set which are not judgmentally equal to reflexivity:

"In some cases, the proliferation of such superfluous identity terms makes it very difficult or impossible to formulate what should be a straightforward concept, such as the definition of a (semi-)simplicial type."

While it is true that these equality proofs add a lot of unwanted difficulties (I myself have asked Dan whether he knew a clever trick to do something about it in Agda), they are not at all the reason why it is "very difficult or impossible" to define semi-simplicial types. Am I the only one who finds the quoted sentence somewhat misleading?

— Reply to this email directly or view it on GitHub< https://github.com/HoTT/book/issues/69> .

— Reply to this email directly or view it on GitHub.

— Reply to this email directly or view it on GitHubhttps://github.com/HoTT/book/issues/69#issuecomment-15938462 .

— Reply to this email directly or view it on GitHub.

[mikeshulman]

Oh, really? Okay. Well, in any case, I think Nicolai has a point and this sentence should be rewritten.

On Fri, Apr 5, 2013 at 8:49 AM, Peter LeFanu Lumsdaine < notifications@github.com> wrote:

Even in the Reedy fibrant approach, I would say the problem is not so much garbage paths in Nat, as that one can't add definitional equalities to an inductive hypothesis. (The equalities involved are not just in Nat, iirc.)

-p.

Sent from my iPhone

On Apr 5, 2013, at 12:28 AM, Mike Shulman notifications@github.com wrote:

Wait... the problem with a functor Delta -> Type is not the garbage paths in Nat, it's making precise what you mean by coherence conditions for a functor-up-to-homotopy at all levels, which I think is a much more serious problem than garbage paths. It's only after you decide to deal with that first problem by going Reedy fibrant that the garbage paths in Nat start to be the problem.

On Fri, Apr 5, 2013 at 12:26 AM, Steve Awodey notifications@github.comwrote:

the "straighforward concept" is just that of a functor Delta --> type the problem is exactly all the garbage paths -- if they weren't there, it would be easy. with them in there, one has to do something else tricky. the attempts at that have been given so far have still choked on the proliferation of coherence conditions arizing from the garbage.

On Apr 5, 2013, at 12:17 AM, Mike Shulman notifications@github.com wrote:

There are other reasons why this is a difficult problem, but I was under the impression that Vladimir and Hugo had clever and mostly successful approaches to it which founded on exactly the problem of such garbage paths in Nat, motivating Vladimir to suggest his type theory with two equalities.

Perhaps "what should be a straightforward concept" is too glib, however, given how much work it took the two of them to get even to that point. (-:

On Fri, Apr 5, 2013 at 12:11 AM, nicolaikraus < notifications@github.com>wrote:

In the preface of the book, there is a discussion about identity proofs in an h-set which are not judgmentally equal to reflexivity:

"In some cases, the proliferation of such superfluous identity terms makes it very difficult or impossible to formulate what should be a straightforward concept, such as the definition of a (semi-)simplicial type."

While it is true that these equality proofs add a lot of unwanted difficulties (I myself have asked Dan whether he knew a clever trick to do something about it in Agda), they are not at all the reason why it is "very difficult or impossible" to define semi-simplicial types. Am I the only one who finds the quoted sentence somewhat misleading?

— Reply to this email directly or view it on GitHub< https://github.com/HoTT/book/issues/69> .

— Reply to this email directly or view it on GitHub.

— Reply to this email directly or view it on GitHub< https://github.com/HoTT/book/issues/69#issuecomment-15938462> .

— Reply to this email directly or view it on GitHub.

— Reply to this email directly or view it on GitHubhttps://github.com/HoTT/book/issues/69#issuecomment-15953776 .

[awodey]

I think the sentence is actually OK as it is - and one doesn't want to get into too much detail at that point the fact is that if there were no garbage paths, things would be more straightforward. the sentence is about the "superfluous paths" in hsets, not about the defintion of a sType, which is only being mentioned as an example of the sort of thing that gets complicate by such extra paths.

On Apr 5, 2013, at 9:00 AM, Mike Shulman notifications@github.com wrote:

Oh, really? Okay. Well, in any case, I think Nicolai has a point and this sentence should be rewritten.

On Fri, Apr 5, 2013 at 8:49 AM, Peter LeFanu Lumsdaine < notifications@github.com> wrote:

Even in the Reedy fibrant approach, I would say the problem is not so much garbage paths in Nat, as that one can't add definitional equalities to an inductive hypothesis. (The equalities involved are not just in Nat, iirc.)

-p.

Sent from my iPhone

On Apr 5, 2013, at 12:28 AM, Mike Shulman notifications@github.com wrote:

Wait... the problem with a functor Delta -> Type is not the garbage paths in Nat, it's making precise what you mean by coherence conditions for a functor-up-to-homotopy at all levels, which I think is a much more serious problem than garbage paths. It's only after you decide to deal with that first problem by going Reedy fibrant that the garbage paths in Nat start to be the problem.

On Fri, Apr 5, 2013 at 12:26 AM, Steve Awodey notifications@github.comwrote:

the "straighforward concept" is just that of a functor Delta --> type the problem is exactly all the garbage paths -- if they weren't there, it would be easy. with them in there, one has to do something else tricky. the attempts at that have been given so far have still choked on the proliferation of coherence conditions arizing from the garbage.

On Apr 5, 2013, at 12:17 AM, Mike Shulman notifications@github.com wrote:

There are other reasons why this is a difficult problem, but I was under the impression that Vladimir and Hugo had clever and mostly successful approaches to it which founded on exactly the problem of such garbage paths in Nat, motivating Vladimir to suggest his type theory with two equalities.

Perhaps "what should be a straightforward concept" is too glib, however, given how much work it took the two of them to get even to that point. (-:

On Fri, Apr 5, 2013 at 12:11 AM, nicolaikraus < notifications@github.com>wrote:

In the preface of the book, there is a discussion about identity proofs in an h-set which are not judgmentally equal to reflexivity:

"In some cases, the proliferation of such superfluous identity terms makes it very difficult or impossible to formulate what should be a straightforward concept, such as the definition of a (semi-)simplicial type."

While it is true that these equality proofs add a lot of unwanted difficulties (I myself have asked Dan whether he knew a clever trick to do something about it in Agda), they are not at all the reason why it is "very difficult or impossible" to define semi-simplicial types. Am I the only one who finds the quoted sentence somewhat misleading?

— Reply to this email directly or view it on GitHub< https://github.com/HoTT/book/issues/69> .

— Reply to this email directly or view it on GitHub.

— Reply to this email directly or view it on GitHub< https://github.com/HoTT/book/issues/69#issuecomment-15938462> .

— Reply to this email directly or view it on GitHub.

— Reply to this email directly or view it on GitHubhttps://github.com/HoTT/book/issues/69#issuecomment-15953776 .

— Reply to this email directly or view it on GitHub.

[mikeshulman]

But the sentence implies that the garbage paths are the only thing preventing a "straightforward" defintiion of sType from working, which I think is misleading. The garbage paths make it more complicated, but it would already be complicated without them.

On Fri, Apr 5, 2013 at 9:05 AM, Steve Awodey notifications@github.comwrote:

I think the sentence is actually OK as it is - and one doesn't want to get into too much detail at that point the fact is that if there were no garbage paths, things would be more straightforward. the sentence is about the "superfluous paths" in hsets, not about the defintion of a sType, which is only being mentioned as an example of the sort of thing that gets complicate by such extra paths.

On Apr 5, 2013, at 9:00 AM, Mike Shulman notifications@github.com wrote:

Oh, really? Okay. Well, in any case, I think Nicolai has a point and this sentence should be rewritten.

On Fri, Apr 5, 2013 at 8:49 AM, Peter LeFanu Lumsdaine < notifications@github.com> wrote:

Even in the Reedy fibrant approach, I would say the problem is not so much garbage paths in Nat, as that one can't add definitional equalities to an inductive hypothesis. (The equalities involved are not just in Nat, iirc.)

-p.

Sent from my iPhone

On Apr 5, 2013, at 12:28 AM, Mike Shulman notifications@github.com wrote:

Wait... the problem with a functor Delta -> Type is not the garbage paths in Nat, it's making precise what you mean by coherence conditions for a functor-up-to-homotopy at all levels, which I think is a much more serious problem than garbage paths. It's only after you decide to deal with that first problem by going Reedy fibrant that the garbage paths in Nat start to be the problem.

On Fri, Apr 5, 2013 at 12:26 AM, Steve Awodey < notifications@github.com>wrote:

the "straighforward concept" is just that of a functor Delta --> type the problem is exactly all the garbage paths -- if they weren't there, it would be easy. with them in there, one has to do something else tricky. the attempts at that have been given so far have still choked on the proliferation of coherence conditions arizing from the garbage.

On Apr 5, 2013, at 12:17 AM, Mike Shulman < notifications@github.com> wrote:

There are other reasons why this is a difficult problem, but I was under the impression that Vladimir and Hugo had clever and mostly successful approaches to it which founded on exactly the problem of such garbage paths in Nat, motivating Vladimir to suggest his type theory with two equalities.

Perhaps "what should be a straightforward concept" is too glib, however, given how much work it took the two of them to get even to that point. (-:

On Fri, Apr 5, 2013 at 12:11 AM, nicolaikraus < notifications@github.com>wrote:

In the preface of the book, there is a discussion about identity proofs in an h-set which are not judgmentally equal to reflexivity:

"In some cases, the proliferation of such superfluous identity terms makes it very difficult or impossible to formulate what should be a straightforward concept, such as the definition of a (semi-)simplicial type."

While it is true that these equality proofs add a lot of unwanted difficulties (I myself have asked Dan whether he knew a clever trick to do something about it in Agda), they are not at all the reason why it is "very difficult or impossible" to define semi-simplicial types. Am I the only one who finds the quoted sentence somewhat misleading?

— Reply to this email directly or view it on GitHub< https://github.com/HoTT/book/issues/69> .

— Reply to this email directly or view it on GitHub.

— Reply to this email directly or view it on GitHub< https://github.com/HoTT/book/issues/69#issuecomment-15938462> .

— Reply to this email directly or view it on GitHub.

— Reply to this email directly or view it on GitHub< https://github.com/HoTT/book/issues/69#issuecomment-15953776> .

— Reply to this email directly or view it on GitHub.

— Reply to this email directly or view it on GitHubhttps://github.com/HoTT/book/issues/69#issuecomment-15954424 .

[txa]

Do we know how to define simplicial types in a hypothetical extensional Type Theory without UIP?

My impression is that we don't but I'd be pleased to be prove wrong.

[mikeshulman]

What does "extensional type theory without UIP" mean ?

On Fri, Apr 5, 2013 at 9:33 AM, Thorsten Altenkirch < notifications@github.com> wrote:

Do we know how to define simplicial types in a hypothetical extensional Type Theory without UIP?

My impression is that we don't but I'd be pleased to be prove wrong.

T.

From: Mike Shulman <notifications@github.com<mailto: notifications@github.com>> Reply-To: HoTT/book reply@reply.github.com<mailto:reply@reply.github.com>

Date: Friday, 5 April 2013 08:11 To: HoTT/book book@noreply.github.com<mailto:book@noreply.github.com> Cc: Thorsten Altenkirch txa@Cs.Nott.AC.UK<mailto:txa@Cs.Nott.AC.UK> Subject: Re: [book] unwanted equality proofs described as main problem (#69)

But the sentence implies that the garbage paths are the only thing preventing a "straightforward" defintiion of sType from working, which I think is misleading. The garbage paths make it more complicated, but it would already be complicated without them.

On Fri, Apr 5, 2013 at 9:05 AM, Steve Awodey <notifications@github.com mailto:notifications@github.com>wrote:

I think the sentence is actually OK as it is - and one doesn't want to get into too much detail at that point the fact is that if there were no garbage paths, things would be more straightforward. the sentence is about the "superfluous paths" in hsets, not about the defintion of a sType, which is only being mentioned as an example of the sort of thing that gets complicate by such extra paths.

On Apr 5, 2013, at 9:00 AM, Mike Shulman <notifications@github.com mailto:notifications@github.com> wrote:

Oh, really? Okay. Well, in any case, I think Nicolai has a point and this sentence should be rewritten.

On Fri, Apr 5, 2013 at 8:49 AM, Peter LeFanu Lumsdaine < notifications@github.commailto:notifications@github.com> wrote:

Even in the Reedy fibrant approach, I would say the problem is not so much garbage paths in Nat, as that one can't add definitional equalities to an inductive hypothesis. (The equalities involved are not just in Nat, iirc.)

-p.

Sent from my iPhone

On Apr 5, 2013, at 12:28 AM, Mike Shulman <notifications@github.com mailto:notifications@github.com> wrote:

Wait... the problem with a functor Delta -> Type is not the garbage paths in Nat, it's making precise what you mean by coherence conditions for a functor-up-to-homotopy at all levels, which I think is a much more serious problem than garbage paths. It's only after you decide to deal with that first problem by going Reedy fibrant that the garbage paths in Nat start to be the problem.

On Fri, Apr 5, 2013 at 12:26 AM, Steve Awodey < notifications@github.commailto:notifications@github.com>wrote:

the "straighforward concept" is just that of a functor Delta --> type the problem is exactly all the garbage paths -- if they weren't there, it would be easy. with them in there, one has to do something else tricky. the attempts at that have been given so far have still choked on the proliferation of coherence conditions arizing from the garbage.

On Apr 5, 2013, at 12:17 AM, Mike Shulman < notifications@github.commailto:notifications@github.com> wrote:

There are other reasons why this is a difficult problem, but I was under the impression that Vladimir and Hugo had clever and mostly successful approaches to it which founded on exactly the problem of such garbage paths in Nat, motivating Vladimir to suggest his type theory with two equalities.

Perhaps "what should be a straightforward concept" is too glib, however, given how much work it took the two of them to get even to that point. (-:

On Fri, Apr 5, 2013 at 12:11 AM, nicolaikraus < notifications@github.commailto:notifications@github.com>wrote:

In the preface of the book, there is a discussion about identity proofs in an h-set which are not judgmentally equal to reflexivity:

"In some cases, the proliferation of such superfluous identity terms makes it very difficult or impossible to formulate what should be a straightforward concept, such as the definition of a (semi-)simplicial type."

While it is true that these equality proofs add a lot of unwanted difficulties (I myself have asked Dan whether he knew a clever trick to do something about it in Agda), they are not at all the reason why it is "very difficult or impossible" to define semi-simplicial types. Am I the only one who finds the quoted sentence somewhat misleading?

— Reply to this email directly or view it on GitHub< https://github.com/HoTT/book/issues/69> .

— Reply to this email directly or view it on GitHub.

— Reply to this email directly or view it on GitHub< https://github.com/HoTT/book/issues/69#issuecomment-15938462> .

— Reply to this email directly or view it on GitHub.

— Reply to this email directly or view it on GitHub< https://github.com/HoTT/book/issues/69#issuecomment-15953776> .

— Reply to this email directly or view it on GitHub.

— Reply to this email directly or view it on GitHub< https://github.com/HoTT/book/issues/69#issuecomment-15954424> .

— Reply to this email directly or view it on GitHub< https://github.com/HoTT/book/issues/69#issuecomment-15954636>.

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 send it back to me, and immediately delete it. Please do not use, copy or disclose the information contained in this message or in any attachment. Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham.

This message has been checked for viruses but the contents of an attachment

may still contain software viruses which could damage your computer system:

you are advised to perform your own checks. Email communications with the

University of Nottingham may be monitored as permitted by UK legislation.

—

Reply to this email directly or view it on GitHubhttps://github.com/HoTT/book/issues/69#issuecomment-15955667 .

[awodey]

how about this:

"The proliferation of such superfluous identity terms can make it difficult to formulate what may seem like a straightforward concept, like that of being a singleton set, and can enormously complicate already difficult problems, such as the definition of a (semi-)simplicial type."

On Apr 5, 2013, at 9:11 AM, Mike Shulman notifications@github.com wrote:

But the sentence implies that the garbage paths are the only thing preventing a "straightforward" defintiion of sType from working, which I think is misleading. The garbage paths make it more complicated, but it would already be complicated without them.

On Fri, Apr 5, 2013 at 9:05 AM, Steve Awodey notifications@github.comwrote:

I think the sentence is actually OK as it is - and one doesn't want to get into too much detail at that point the fact is that if there were no garbage paths, things would be more straightforward. the sentence is about the "superfluous paths" in hsets, not about the defintion of a sType, which is only being mentioned as an example of the sort of thing that gets complicate by such extra paths.

On Apr 5, 2013, at 9:00 AM, Mike Shulman notifications@github.com wrote:

Oh, really? Okay. Well, in any case, I think Nicolai has a point and this sentence should be rewritten.

On Fri, Apr 5, 2013 at 8:49 AM, Peter LeFanu Lumsdaine < notifications@github.com> wrote:

Even in the Reedy fibrant approach, I would say the problem is not so much garbage paths in Nat, as that one can't add definitional equalities to an inductive hypothesis. (The equalities involved are not just in Nat, iirc.)

-p.

Sent from my iPhone

On Apr 5, 2013, at 12:28 AM, Mike Shulman notifications@github.com wrote:

Wait... the problem with a functor Delta -> Type is not the garbage paths in Nat, it's making precise what you mean by coherence conditions for a functor-up-to-homotopy at all levels, which I think is a much more serious problem than garbage paths. It's only after you decide to deal with that first problem by going Reedy fibrant that the garbage paths in Nat start to be the problem.

On Fri, Apr 5, 2013 at 12:26 AM, Steve Awodey < notifications@github.com>wrote:

the "straighforward concept" is just that of a functor Delta --> type the problem is exactly all the garbage paths -- if they weren't there, it would be easy. with them in there, one has to do something else tricky. the attempts at that have been given so far have still choked on the proliferation of coherence conditions arizing from the garbage.

On Apr 5, 2013, at 12:17 AM, Mike Shulman < notifications@github.com> wrote:

There are other reasons why this is a difficult problem, but I was under the impression that Vladimir and Hugo had clever and mostly successful approaches to it which founded on exactly the problem of such garbage paths in Nat, motivating Vladimir to suggest his type theory with two equalities.

Perhaps "what should be a straightforward concept" is too glib, however, given how much work it took the two of them to get even to that point. (-:

On Fri, Apr 5, 2013 at 12:11 AM, nicolaikraus < notifications@github.com>wrote:

In the preface of the book, there is a discussion about identity proofs in an h-set which are not judgmentally equal to reflexivity:

"In some cases, the proliferation of such superfluous identity terms makes it very difficult or impossible to formulate what should be a straightforward concept, such as the definition of a (semi-)simplicial type."

While it is true that these equality proofs add a lot of unwanted difficulties (I myself have asked Dan whether he knew a clever trick to do something about it in Agda), they are not at all the reason why it is "very difficult or impossible" to define semi-simplicial types. Am I the only one who finds the quoted sentence somewhat misleading?

— Reply to this email directly or view it on GitHub< https://github.com/HoTT/book/issues/69> .

— Reply to this email directly or view it on GitHub.

— Reply to this email directly or view it on GitHub< https://github.com/HoTT/book/issues/69#issuecomment-15938462> .

— Reply to this email directly or view it on GitHub.

— Reply to this email directly or view it on GitHub< https://github.com/HoTT/book/issues/69#issuecomment-15953776> .

— Reply to this email directly or view it on GitHub.

— Reply to this email directly or view it on GitHubhttps://github.com/HoTT/book/issues/69#issuecomment-15954424 .

— Reply to this email directly or view it on GitHub.

[txa]

Equality reflection holds for equalities in \Prop.

I did say "hypothetical", didn't I?

[mikeshulman]

@Thorsten: That's not at all obvious to me as a meaning of "extensional".

On Fri, Apr 5, 2013 at 9:46 AM, Thorsten Altenkirch < notifications@github.com> wrote:

Equality reflection holds for equalities in \Prop.

I did say "hypothetical", didn't I?

T.

From: Mike Shulman <notifications@github.com<mailto: notifications@github.com>> Reply-To: HoTT/book reply@reply.github.com<mailto:reply@reply.github.com>

Date: Friday, 5 April 2013 08:34 To: HoTT/book book@noreply.github.com<mailto:book@noreply.github.com> Cc: Thorsten Altenkirch txa@Cs.Nott.AC.UK<mailto:txa@Cs.Nott.AC.UK> Subject: Re: [book] unwanted equality proofs described as main problem (#69)

What does "extensional type theory without UIP" mean ?

On Fri, Apr 5, 2013 at 9:33 AM, Thorsten Altenkirch < notifications@github.commailto:notifications@github.com> wrote:

Do we know how to define simplicial types in a hypothetical extensional Type Theory without UIP?

My impression is that we don't but I'd be pleased to be prove wrong.

T.

From: Mike Shulman <notifications@github.com<mailto: notifications@github.com><mailto: notifications@github.commailto:notifications@github.com>> Reply-To: HoTT/book <reply@reply.github.com<mailto: reply@reply.github.com>mailto:reply@reply.github.com>

Date: Friday, 5 April 2013 08:11 To: HoTT/book <book@noreply.github.com<mailto:book@noreply.github.com mailto:book@noreply.github.com> Cc: Thorsten Altenkirch <txa@Cs.Nott.AC.UK<mailto:txa@Cs.Nott.AC.UK mailto:txa@Cs.Nott.AC.UK> Subject: Re: [book] unwanted equality proofs described as main problem (#69)

But the sentence implies that the garbage paths are the only thing preventing a "straightforward" defintiion of sType from working, which I think is misleading. The garbage paths make it more complicated, but it would already be complicated without them.

On Fri, Apr 5, 2013 at 9:05 AM, Steve Awodey <notifications@github.com mailto:notifications@github.com mailto:notifications@github.com>wrote:

I think the sentence is actually OK as it is - and one doesn't want to get into too much detail at that point the fact is that if there were no garbage paths, things would be more straightforward. the sentence is about the "superfluous paths" in hsets, not about the defintion of a sType, which is only being mentioned as an example of the sort of thing that gets complicate by such extra paths.

On Apr 5, 2013, at 9:00 AM, Mike Shulman <notifications@github.com mailto:notifications@github.com mailto:notifications@github.com> wrote:

Oh, really? Okay. Well, in any case, I think Nicolai has a point and this sentence should be rewritten.

On Fri, Apr 5, 2013 at 8:49 AM, Peter LeFanu Lumsdaine < notifications@github.commailto:notifications@github.com<mailto: notifications@github.com>> wrote:

Even in the Reedy fibrant approach, I would say the problem is not so much garbage paths in Nat, as that one can't add definitional equalities to an inductive hypothesis. (The equalities involved are not just in Nat, iirc.)

-p.

Sent from my iPhone

On Apr 5, 2013, at 12:28 AM, Mike Shulman < notifications@github.commailto:notifications@github.com mailto:notifications@github.com> wrote:

Wait... the problem with a functor Delta -> Type is not the garbage paths in Nat, it's making precise what you mean by coherence conditions for a functor-up-to-homotopy at all levels, which I think is a much more serious problem than garbage paths. It's only after you decide to deal with that first problem by going Reedy fibrant that the garbage paths in Nat start to be the problem.

On Fri, Apr 5, 2013 at 12:26 AM, Steve Awodey < notifications@github.commailto:notifications@github.com<mailto: notifications@github.com>>wrote:

the "straighforward concept" is just that of a functor Delta --> type the problem is exactly all the garbage paths -- if they weren't there, it would be easy. with them in there, one has to do something else tricky. the attempts at that have been given so far have still choked on the proliferation of coherence conditions arizing from the garbage.

On Apr 5, 2013, at 12:17 AM, Mike Shulman < notifications@github.commailto:notifications@github.com<mailto: notifications@github.com>> wrote:

There are other reasons why this is a difficult problem, but I was under the impression that Vladimir and Hugo had clever and mostly successful approaches to it which founded on exactly the problem of such garbage paths in Nat, motivating Vladimir to suggest his type theory with two equalities.

Perhaps "what should be a straightforward concept" is too glib, however, given how much work it took the two of them to get even to that point. (-:

On Fri, Apr 5, 2013 at 12:11 AM, nicolaikraus < notifications@github.commailto:notifications@github.com<mailto: notifications@github.com>>wrote:

In the preface of the book, there is a discussion about identity proofs in an h-set which are not judgmentally equal to reflexivity:

"In some cases, the proliferation of such superfluous identity terms makes it very difficult or impossible to formulate what should be a straightforward concept, such as the definition of a (semi-)simplicial type."

While it is true that these equality proofs add a lot of unwanted difficulties (I myself have asked Dan whether he knew a clever trick to do something about it in Agda), they are not at all the reason why it is "very difficult or impossible" to define semi-simplicial types. Am I the only one who finds the quoted sentence somewhat misleading?

— Reply to this email directly or view it on GitHub< https://github.com/HoTT/book/issues/69> .

— Reply to this email directly or view it on GitHub.

— Reply to this email directly or view it on GitHub< https://github.com/HoTT/book/issues/69#issuecomment-15938462> .

— Reply to this email directly or view it on GitHub.

— Reply to this email directly or view it on GitHub< https://github.com/HoTT/book/issues/69#issuecomment-15953776> .

— Reply to this email directly or view it on GitHub.

— Reply to this email directly or view it on GitHub< https://github.com/HoTT/book/issues/69#issuecomment-15954424> .

— Reply to this email directly or view it on GitHub< https://github.com/HoTT/book/issues/69#issuecomment-15954636>.

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 send it back to me, and immediately delete it. Please do not use, copy or disclose the information contained in this message or in any attachment. Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham.

This message has been checked for viruses but the contents of an attachment

may still contain software viruses which could damage your computer system:

you are advised to perform your own checks. Email communications with the

University of Nottingham may be monitored as permitted by UK legislation.

—

Reply to this email directly or view it on GitHub< https://github.com/HoTT/book/issues/69#issuecomment-15955667> .

— Reply to this email directly or view it on GitHub< https://github.com/HoTT/book/issues/69#issuecomment-15955742>.

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 send it back to me, and immediately delete it. Please do not use, copy or disclose the information contained in this message or in any attachment. Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham.

This message has been checked for viruses but the contents of an attachment

may still contain software viruses which could damage your computer system:

you are advised to perform your own checks. Email communications with the

University of Nottingham may be monitored as permitted by UK legislation.

—

Reply to this email directly or view it on GitHubhttps://github.com/HoTT/book/issues/69#issuecomment-15956381 .

[mikeshulman]

Can we find a better example for the first than being a singleton set? Since the obvious PAT definition of being a singleton actually does work as a definition of contractibility?

On Fri, Apr 5, 2013 at 9:39 AM, Steve Awodey notifications@github.comwrote:

how about this:

"The proliferation of such superfluous identity terms can make it difficult to formulate what may seem like a straightforward concept, like that of being a singleton set, and can enormously complicate already difficult problems, such as the definition of a (semi-)simplicial type."

On Apr 5, 2013, at 9:11 AM, Mike Shulman notifications@github.com wrote:

But the sentence implies that the garbage paths are the only thing preventing a "straightforward" defintiion of sType from working, which I think is misleading. The garbage paths make it more complicated, but it would already be complicated without them.

On Fri, Apr 5, 2013 at 9:05 AM, Steve Awodey notifications@github.comwrote:

I think the sentence is actually OK as it is - and one doesn't want to get into too much detail at that point the fact is that if there were no garbage paths, things would be more straightforward. the sentence is about the "superfluous paths" in hsets, not about the defintion of a sType, which is only being mentioned as an example of the sort of thing that gets complicate by such extra paths.

On Apr 5, 2013, at 9:00 AM, Mike Shulman notifications@github.com wrote:

Oh, really? Okay. Well, in any case, I think Nicolai has a point and this sentence should be rewritten.

On Fri, Apr 5, 2013 at 8:49 AM, Peter LeFanu Lumsdaine < notifications@github.com> wrote:

Even in the Reedy fibrant approach, I would say the problem is not so much garbage paths in Nat, as that one can't add definitional equalities to an inductive hypothesis. (The equalities involved are not just in Nat, iirc.)

-p.

Sent from my iPhone

On Apr 5, 2013, at 12:28 AM, Mike Shulman < notifications@github.com> wrote:

Wait... the problem with a functor Delta -> Type is not the garbage paths in Nat, it's making precise what you mean by coherence conditions for a functor-up-to-homotopy at all levels, which I think is a much more serious problem than garbage paths. It's only after you decide to deal with that first problem by going Reedy fibrant that the garbage paths in Nat start to be the problem.

On Fri, Apr 5, 2013 at 12:26 AM, Steve Awodey < notifications@github.com>wrote:

the "straighforward concept" is just that of a functor Delta --> type the problem is exactly all the garbage paths -- if they weren't there, it would be easy. with them in there, one has to do something else tricky. the attempts at that have been given so far have still choked on the proliferation of coherence conditions arizing from the garbage.

On Apr 5, 2013, at 12:17 AM, Mike Shulman < notifications@github.com> wrote:

There are other reasons why this is a difficult problem, but I was under the impression that Vladimir and Hugo had clever and mostly successful approaches to it which founded on exactly the problem of such garbage paths in Nat, motivating Vladimir to suggest his type theory with two equalities.

Perhaps "what should be a straightforward concept" is too glib, however, given how much work it took the two of them to get even to that point. (-:

On Fri, Apr 5, 2013 at 12:11 AM, nicolaikraus < notifications@github.com>wrote:

In the preface of the book, there is a discussion about identity proofs in an h-set which are not judgmentally equal to reflexivity:

"In some cases, the proliferation of such superfluous identity terms makes it very difficult or impossible to formulate what should be a straightforward concept, such as the definition of a (semi-)simplicial type."

While it is true that these equality proofs add a lot of unwanted difficulties (I myself have asked Dan whether he knew a clever trick to do something about it in Agda), they are not at all the reason why it is "very difficult or impossible" to define semi-simplicial types. Am I the only one who finds the quoted sentence somewhat misleading?

— Reply to this email directly or view it on GitHub< https://github.com/HoTT/book/issues/69> .

— Reply to this email directly or view it on GitHub.

— Reply to this email directly or view it on GitHub< https://github.com/HoTT/book/issues/69#issuecomment-15938462> .

— Reply to this email directly or view it on GitHub.

— Reply to this email directly or view it on GitHub< https://github.com/HoTT/book/issues/69#issuecomment-15953776> .

— Reply to this email directly or view it on GitHub.

— Reply to this email directly or view it on GitHub< https://github.com/HoTT/book/issues/69#issuecomment-15954424> .

— Reply to this email directly or view it on GitHub.

— Reply to this email directly or view it on GitHubhttps://github.com/HoTT/book/issues/69#issuecomment-15956019 .

[peterlefanulumsdaine]

On Fri, Apr 5, 2013 at 9:46 AM, Thorsten Altenkirch < notifications@github.com> wrote:

Equality reflection holds for equalities in \Prop.

I did say "hypothetical", didn't I?

Assuming equality reflection for equalities in h-props — or even for equalities just in contractible types — one can derive full equality refelection, and hence UIP:

given any a1, a2 : A, and p : a1 = a2, consider the type { a : A & a1 = a }, and its elements (a1, 1) and (a2, p). The type is contractible, so these pairs are definitionally equal. So their pr1’s are definitionally equal; so a1, a2 are definitionally equal.

–p.

[txa]

Indeed, the word extensional is overloaded.

In the context of Type Theory by "Extensional Type Theory" we usually mean the variant of type theory with the equality reflection rule and UIP.

People often complain about the bureaucracy of having to keep track of equality proofs in intensional type theory. However, as soon as we have relevant equalities there is no way to avoid this because the choice of equality may change your result (we may get 0 instead of 1).

A compromise would be a Type Theory where all propositional equalities can be ignored (I.e. we have equality reflection for those) but not for non-propositional equalities. This is also related to the system described in Harper's and Licata's POPL paper.

Hence my question: if people think that the problem with formulating simplicial types has to do with the bureaucracy of intensional type theory then it should be possible to solve the problem in such a system.

My impression from Richard's analysis (and our own attempts) was that this wasn't the case but that the solution of the problem involves the generation of weak higher order functor laws. Which may be possible but hard.

[txa]

Thank you Peter.

This makes it clear that equality reflection forces UIP.

[andrejbauer]

Could we convince Throsten not to send these horrible replies with everything quoted and that stupid legalese from his university? (You could use github.com directly, rather than email.)

[txa]

Have you had too much beer?

[txa]

Ok, we could fix this by introducing judgmental Prop (and Set) and then saying that any judgemental Prop gives us equality reflection. Nat would be a judgemental Set and hence its equality a judgemental Prop.

Can we define semisimplicial sets in such a system?

[mikeshulman]

Maybe we could keep the discussion on github relevant to the book, and discuss hypothetical new type theories elsewhere? On Apr 5, 2013 5:50 PM, "Thorsten Altenkirch" notifications@github.com wrote:

Ok, we could fix this by introducing judgmental Prop (and Set) and then saying that any judgemental Prop gives us equality reflection. Nat would be a judgemental Set and hence its equality a judgemental Prop.

Can we define semisimplicial sets in such a system?

T.

From: Peter LeFanu Lumsdaine <notifications@github.com<mailto: notifications@github.com>> Reply-To: HoTT/book reply@reply.github.com<mailto:reply@reply.github.com>

To: HoTT/book book@noreply.github.com<mailto:book@noreply.github.com> Cc: Thorsten Altenkirch txa@Cs.Nott.AC.UK<mailto:txa@Cs.Nott.AC.UK> Subject: Re: [book] unwanted equality proofs described as main problem (#69)

On Fri, Apr 5, 2013 at 9:46 AM, Thorsten Altenkirch < notifications@github.commailto:notifications@github.com> wrote:

Equality reflection holds for equalities in \Prop.

I did say "hypothetical", didn't I?

Assuming equality reflection for equalities in h-props — or even for equalities just in contractible types — one can derive full equality refelection, and hence UIP:

given any a1, a2 : A, and p : a1 = a2, consider the type { a : A & a1 = a }, and its elements (a1, 1) and (a2, p). The type is contractible, so these pairs are definitionally equal. So their pr1’s are definitionally equal; so a1, a2 are definitionally equal.

–p.

— Reply to this email directly or view it on GitHub< https://github.com/HoTT/book/issues/69#issuecomment-15957094>.

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 send it back to me, and immediately delete it. Please do not use, copy or disclose the information contained in this message or in any attachment. Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham.

This message has been checked for viruses but the contents of an attachment

may still contain software viruses which could damage your computer system:

you are advised to perform your own checks. Email communications with the

University of Nottingham may be monitored as permitted by UK legislation.

— Reply to this email directly or view it on GitHubhttps://github.com/HoTT/book/issues/69#issuecomment-15982730 .

[txa]

Sure, any followup should be discussed on univalent-foundations@googlegroups.com univalent-foundations@googlegroups.com

[mikeshulman]

I don't think the original issue here is solved. Steve suggested

"The proliferation of such superfluous identity terms can make it difficult to formulate what may seem like a straightforward concept, like that of being a singleton set, and can enormously complicate already difficult problems, such as the definition of a (semi-)simplicial type."

and I asked if we could find a better example than "being a singleton". Anyone have any other suggestions?

[awodey]

by "being a singleton set" I had in mind contractibility. Of course, the genial solution is in fact not difficult, because it's just being a singleton. So how about this wording: "The proliferation of such superfluous identity terms can make it a subtle matter to formulate what may seem like a straightforward concept, like that of being a point, and can enormously complicate already difficult problems, such as the definition of a (semi-)simplicial type."

[peterlefanulumsdaine]

Actually, reading this paragraph again, I don’t think it’s accurate at all. None of these difficulties are caused by the proliferation of identity terms in h-sets. The only subtlety I see in the definition of contractibility is why it’s not just defining connectedness — but for types already known to be h-sets, these are equivalent anyway. The serious difficulties in defining (semi-)simplicial types all come from identity proofs in those (arbitrary) types, not in e.g. Nat or any other h-sets: we can easily define semi-simplicial and even simplicial h-sets.

The absence of reflection adds a little bit of extra bureaucracy in working with h-sets, but no serious subtleties — and surely Martin Hofmann’s work showing the conservativity of intensional-TT-with-UIP-and-funext over extensional TT gives a pretty good formal justification of this fact?

[awodey]

there are two different things being said here: 1) even in hsets, and even in "hpoints", there are unexpected paths. Not unexpected by YOU or a homotopy-theorists, but certainly unexpected by a logician, number-theorist, etc. One needs to be aware of this even in doing simple things. 2) in cases involving more elaborate structure like sSets, these extra paths IN COMBINATION WITH OTHERS can complicate things considerably. The point of trying to get definitional equations for Nat is not to have to worry about the trivial paths when trying to deal with the nontrivial ones.

[peterlefanulumsdaine]

1) even in hsets, and even in "hpoints", there are unexpected paths. Not unexpected by YOU or a homotopy-theorists, but certainly unexpected by a logician, number-theorist, etc.

OK, I see what you’re saying here. Perhaps the result type of [apD] gives a clearer example: one might well think that [x = y] should always imply [f x = f y], and be surprised that this isn’t right in the dependent case?

2) in cases involving more elaborate structure like sSets, these extra paths IN COMBINATION WITH OTHERS can complicate things considerably.

I’m simply still not convinced this is the case. For instance, in Vladimir and Hugo’s approaches to semi-simplicial types, I’d understood that their key point was not the strict equality on Nat itself, but rather the ability to induct over Nat into strict equality on other types (of arbitrary h-level) — in particular, the ability to strengthen one’s inductive hypothesis to include definitional equalities. Perhaps Hugo or Vladimir can clarify whether they feel this is accurate?

[peterlefanulumsdaine]

PS re point (2) — while as I said I’m still not persuaded of that point, it’s clear from this discussion that it’s at least somewhat subjective, so I promise not to argue any further if others still prefer to include it :-)

[awodey]

someone else should decide and close this issue.

On Apr 7, 2013, at 12:10 PM, Peter LeFanu Lumsdaine notifications@github.com wrote:

PS re point (2) — while as I said I’m still not persuaded of that point, it’s clear from this discussion that it’s at least somewhat subjective, so I promise not to argue any further if others still prefer to include it :-)

— Reply to this email directly or view it on GitHub.

[txa]

"The proliferation of such superfluous identity terms can make it a subtle matter to formulate what may seem like a straightforward concept, like that of being a point, and can enormously complicate already difficult problems, such as the definition of a (semi-)simplicial type."

I would suggest that we delete this sentence.

Initially it was intended to explain why it is hard to formally define (semi-)simplicial types. The discussion so far seems to indicate that there is no evidence that this is the case.

It seems now that we want to retain a sentence which expresses that explicit transport terms are bad and make our lives more difficult. Indeed, I know that Dan and Guillaume were complaining a lot about this. However, in this case these were usually not proof-irrelvant identities and their problems were mostly caused by the lack of definitional equalities when working with path constructors.

It seems to me that the idea that the presence of "superflouous identitiy terms" in Type Theory is a big problem is a myth which we should not proliferate.

T.

From: Steve Awodey notifications@github.com<mailto:notifications@github.com> Reply-To: HoTT/book reply@reply.github.com<mailto:reply@reply.github.com> Date: Sunday, 7 April 2013 09:02 To: HoTT/book book@noreply.github.com<mailto:book@noreply.github.com> Cc: Thorsten Altenkirch txa@Cs.Nott.AC.UK<mailto:txa@Cs.Nott.AC.UK> Subject: Re: [book] unwanted equality proofs described as main problem (#69)

by "being a singleton set" I had in mind contractibility. Of course, the genial solution is in fact not difficult, because it's just being a singleton. So how about this wording: "The proliferation of such superfluous identity terms can make it a subtle matter to formulate what may seem like a straightforward concept, like that of being a point, and can enormously complicate already difficult problems, such as the definition of a (semi-)simplicial type."

— Reply to this email directly or view it on GitHubhttps://github.com/HoTT/book/issues/69#issuecomment-16015586.

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 send it back to me, and immediately delete it. Please do not use, copy or disclose the information contained in this message or in any attachment. Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham.

This message has been checked for viruses but the contents of an attachment

may still contain software viruses which could damage your computer system:

you are advised to perform your own checks. Email communications with the

University of Nottingham may be monitored as permitted by UK legislation.

[txa]

On the other hand we should actually mention that defining (semi)-simplicial types is an open problem. This seems rather be related to the general issue of coherence laws when trying to generalize a concept from HSets to general types.

So I suggest to replace the whole paragraph starting with

Another basic issue is the difficulty of working with types, like the natural numbers, which are essentially sets (i.e., discrete spaces), containing only trivial paths.

by a discussion how difficult it is to generalize concepts from sets to types citing (semi-)simplicial types as one example.

From: Thorsten Altenkirch psztxa@exmail.nottingham.ac.uk<mailto:psztxa@exmail.nottingham.ac.uk> Date: Sunday, 7 April 2013 12:22 To: HoTT/book reply@reply.github.com<mailto:reply@reply.github.com> Subject: Re: [book] unwanted equality proofs described as main problem (#69)

"The proliferation of such superfluous identity terms can make it a subtle matter to formulate what may seem like a straightforward concept, like that of being a point, and can enormously complicate already difficult problems, such as the definition of a (semi-)simplicial type."

I would suggest that we delete this sentence.

Initially it was intended to explain why it is hard to formally define (semi-)simplicial types. The discussion so far seems to indicate that there is no evidence that this is the case.

It seems now that we want to retain a sentence which expresses that explicit transport terms are bad and make our lives more difficult. Indeed, I know that Dan and Guillaume were complaining a lot about this. However, in this case these were usually not proof-irrelvant identities and their problems were mostly caused by the lack of definitional equalities when working with path constructors.

It seems to me that the idea that the presence of "superflouous identitiy terms" in Type Theory is a big problem is a myth which we should not proliferate.

T.

From: Steve Awodey notifications@github.com<mailto:notifications@github.com> Reply-To: HoTT/book reply@reply.github.com<mailto:reply@reply.github.com> Date: Sunday, 7 April 2013 09:02 To: HoTT/book book@noreply.github.com<mailto:book@noreply.github.com> Cc: Thorsten Altenkirch txa@Cs.Nott.AC.UK<mailto:txa@Cs.Nott.AC.UK> Subject: Re: [book] unwanted equality proofs described as main problem (#69)

by "being a singleton set" I had in mind contractibility. Of course, the genial solution is in fact not difficult, because it's just being a singleton. So how about this wording: "The proliferation of such superfluous identity terms can make it a subtle matter to formulate what may seem like a straightforward concept, like that of being a point, and can enormously complicate already difficult problems, such as the definition of a (semi-)simplicial type."

— Reply to this email directly or view it on GitHubhttps://github.com/HoTT/book/issues/69#issuecomment-16015586.

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 send it back to me, and immediately delete it. Please do not use, copy or disclose the information contained in this message or in any attachment. Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham.

This message has been checked for viruses but the contents of an attachment

may still contain software viruses which could damage your computer system:

you are advised to perform your own checks. Email communications with the

University of Nottingham may be monitored as permitted by UK legislation.

[awodey]

the original context was to explain there may be many extra paths around, even in cases where they don't really do anything, like in a point or the Id of a set. the semi-simplicial types were just an example of the sort of complication that can result.

Here is the passage, from the Open Problems section of the intro:

" Another basic issue is the difficulty of working with types, like the natural numbers, which are essentially sets (i.e., discrete spaces), containing only trivial paths. At present, homotopy type theory can really only characterize spaces up to homotopy equivalence, which means that these discrete spaces'' may only be \emph{homotopy equivalent} to discrete spaces. Type-theoretically, this means there are many paths that are equal to reflexivity, but not \emph{judgmentally} equal to it (see \cref{sec:types-vs-sets} for the meaning ofjudgmentally''). While this homotopy-invariance has advantages, these ``meaningless'' identity terms do introduce needless complications into arguments and constructions, so it would be convenient to have a systematic way of eliminating or collapsing them. In some cases, the proliferation of such superfluous identity terms makes it very difficult or impossible to formulate what should be a straightforward concept, such as the definition of a (semi-)simplicial type. "

I think something like this point still needs to be made.

[txa]

I just don't think the point (that there is an issue with propositional equalities) is valid.

In informal type theory we could just agree that we simply omit transports along a propositional equality.

However, in formal type theory this would lead to potentially non-terminating terms in inconsistent contexts. To resolve this we should remember on what assumptions the equality we have just used depends and only reduce if they are values. But this is exactly what is happening and hence these identity terms are not meaningless.

Btw, I don't think it is a big problem to have non-terminating reductions in inconsistent contexts anyway. But if you don't want them then this is what you have to do.

From: Steve Awodey notifications@github.com<mailto:notifications@github.com> Reply-To: HoTT/book reply@reply.github.com<mailto:reply@reply.github.com> Date: Sunday, 7 April 2013 14:20 To: HoTT/book book@noreply.github.com<mailto:book@noreply.github.com> Cc: Thorsten Altenkirch txa@Cs.Nott.AC.UK<mailto:txa@Cs.Nott.AC.UK> Subject: Re: [book] unwanted equality proofs described as main problem (#69)

the original context was to explain there may be many extra paths around, even in cases where they don't really do anything, like in a point or the Id of a set. the semi-simplicial types were just an example of the sort of complication that can result.

Here is the passage, from the Open Problems section of the intro:

" Another basic issue is the difficulty of working with types, like the natural numbers, which are essentially sets (i.e., discrete spaces), containing only trivial paths. At present, homotopy type theory can really only characterize spaces up to homotopy equivalence, which means that these discrete spaces'' may only be \emph{homotopy equivalent} to discrete spaces. Type-theoretically, this means there are many paths that are equal to reflexivity, but not \emph{judgmentally} equal to it (see \cref{sec:types-vs-sets} for the meaning ofjudgmentally''). While this homotopy-invariance has advantages, these ``meaningless'' identity terms do introduce needless complications into arguments and constructions, so it would be convenient to have a systematic way of eliminating or collapsing them. In some cases, the proliferation of such superfluous identity terms makes it very difficult or impossible to formulate what should be a straightforward concept, such as the definition of a (semi-)simplicial type. "

I think something like this point still needs to be made.

— Reply to this email directly or view it on GitHubhttps://github.com/HoTT/book/issues/69#issuecomment-16021581.

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 send it back to me, and immediately delete it. Please do not use, copy or disclose the information contained in this message or in any attachment. Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham.

This message has been checked for viruses but the contents of an attachment

may still contain software viruses which could damage your computer system:

you are advised to perform your own checks. Email communications with the

University of Nottingham may be monitored as permitted by UK legislation.

[txa]

Let me correct myself: we can only agree to omit propositional equalities where the fact that they are propositional doesn't depend on assumptions. Otherwise we get UIP as Peter has shown.

From: Thorsten Altenkirch psztxa@exmail.nottingham.ac.uk<mailto:psztxa@exmail.nottingham.ac.uk> Date: Sunday, 7 April 2013 15:30 To: HoTT/book reply@reply.github.com<mailto:reply@reply.github.com> Subject: Re: [book] unwanted equality proofs described as main problem (#69)

I just don't think the point (that there is an issue with propositional equalities) is valid.

In informal type theory we could just agree that we simply omit transports along a propositional equality.

However, in formal type theory this would lead to potentially non-terminating terms in inconsistent contexts. To resolve this we should remember on what assumptions the equality we have just used depends and only reduce if they are values. But this is exactly what is happening and hence these identity terms are not meaningless.

Btw, I don't think it is a big problem to have non-terminating reductions in inconsistent contexts anyway. But if you don't want them then this is what you have to do.

From: Steve Awodey notifications@github.com<mailto:notifications@github.com> Reply-To: HoTT/book reply@reply.github.com<mailto:reply@reply.github.com> Date: Sunday, 7 April 2013 14:20 To: HoTT/book book@noreply.github.com<mailto:book@noreply.github.com> Cc: Thorsten Altenkirch txa@Cs.Nott.AC.UK<mailto:txa@Cs.Nott.AC.UK> Subject: Re: [book] unwanted equality proofs described as main problem (#69)

the original context was to explain there may be many extra paths around, even in cases where they don't really do anything, like in a point or the Id of a set. the semi-simplicial types were just an example of the sort of complication that can result.

Here is the passage, from the Open Problems section of the intro:

" Another basic issue is the difficulty of working with types, like the natural numbers, which are essentially sets (i.e., discrete spaces), containing only trivial paths. At present, homotopy type theory can really only characterize spaces up to homotopy equivalence, which means that these discrete spaces'' may only be \emph{homotopy equivalent} to discrete spaces. Type-theoretically, this means there are many paths that are equal to reflexivity, but not \emph{judgmentally} equal to it (see \cref{sec:types-vs-sets} for the meaning ofjudgmentally''). While this homotopy-invariance has advantages, these ``meaningless'' identity terms do introduce needless complications into arguments and constructions, so it would be convenient to have a systematic way of eliminating or collapsing them. In some cases, the proliferation of such superfluous identity terms makes it very difficult or impossible to formulate what should be a straightforward concept, such as the definition of a (semi-)simplicial type. "

I think something like this point still needs to be made.

— Reply to this email directly or view it on GitHubhttps://github.com/HoTT/book/issues/69#issuecomment-16021581.

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 send it back to me, and immediately delete it. Please do not use, copy or disclose the information contained in this message or in any attachment. Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham.

This message has been checked for viruses but the contents of an attachment

may still contain software viruses which could damage your computer system:

you are advised to perform your own checks. Email communications with the

University of Nottingham may be monitored as permitted by UK legislation.

[cangiuli]

I'm not sure where this conversation stands, so I'm conservatively tagging the issue for feature-freeze.

[mikeshulman]

I think discussions about the wording of the introduction are for the debugging phase (changed).

[andrejbauer]

What is the status of this issue?

[txa]

In the introduction the view is maintained that the proliferation of "unnecessary identities" is the main obstacle to defining semisimplicial types. So far nobody has been able to give a convincing justification of this assertion. To me at seems that the need of higher coherence equations is the main obstacle.

[mikeshulman]

Since there is dissent, why not just remove the offending sentence

In some cases, the proliferation of such superfluous identity terms makes it very difficult or impossible to formulate what should be a straightforward concept, such as the definition of a (semi-)simplicial type.

? The previous sentence already makes the point that we want to make; we don't really need an example.

[awodey]

Ok.

Sent from my iPhone

On Apr 26, 2013, at 9:50 PM, Mike Shulman notifications@github.com wrote:

Since there is dissent, why not just remove the offending sentence

In some cases, the proliferation of such superfluous identity terms makes it very difficult or impossible to formulate what should be a straightforward concept, such as the definition of a (semi-)simplicial type.

? The previous sentence already makes the point that we want to make; we don't really need an example.

— Reply to this email directly or view it on GitHub.