Stop and think

[andrejbauer]

The library seems to be growing, which is fine, but I tihnk it is a good idea to stop every once in a while and do two things:

1. Clean up (we have 32 outstanding issues).
2. Look at how the library is organized and make sure we're going in the right direction.

Regarding the first point, I would like to encourage a period during which we resolve existing issues and try to decrease their number.

Regarding the second point, we have had lately a number of technical improvements (regarding autoconf, new powerful tactics, etc.). My position is that the library must be simple to understand and use by a Coq non-expert and that the installation procedure should require minimal requirements from the user. Both of these follow from the fact that our intended audience is a bunch of mathematicians who are not used to compiling stuff. Also, we want the mathematicians to start doing research and to contribute to the library (therefore, the default installation method is to clone from git). What do others think?

[awodey]

Sent from my iPhone

On Aug 25, 2013, at 4:50 PM, Andrej Bauer notifications@github.com wrote:

The library seems to be growing, which is fine, but I tihnk it is a good idea to stop every once in a while and do two things:

Clean up (we have 32 outstanding issues). Look at how the library is organized and make sure we're going in the right direction. Regarding the first point, I would like to encourage a period during which we resolve existing issues and try to decrease their number.

Regarding the second point, we have had lately a number of technical improvements (regarding autoconf, new powerful tactics, etc.). My position is that the library must be simple to understand and use by a Coq non-expert and that the installation procedure should require minimal requirements from the user. Both of these follow from the fact that our intended audience is a bunch of mathematicians who are not used to compiling stuff. Also, we want the mathematicians to start doing research and to contribute to the library (therefore, the default installation method is to clone from git). What do others think?

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

[JasonGross]

My position is that the library must be simple to understand and use by a Coq non-expert

What's your opinion of having powerful black-box-like tactics that make some structures significantly easier to use by automating grunge-work (such as issig, f_ap, path_forall_hammer, etc.), but documenting them clearly as powerful tactics which are straightforward to use but somewhat tricky to understand?

and that the installation procedure should require minimal requirements from the user.

I am working on bundling Coq so that the user only has to clone one git repository, rather than two. I am currently trying to figure out a problem where I get

jgross@cagnode17:~/HoTT$ /afs/csail.mit.edu/u/j/jgross/HoTT/coq-HoTT/bin/coqtop -indices-matter -boot -nois -coqlib ./coq -R ./coq/theories Coq -compile coq/theories/Init/Tactics
File "/afs/csail.mit.edu/u/j/jgross/HoTT/coq/theories/Init/NCoq_Init_Tactics.ml", line 1, characters 0-17:
Error: Unbound module Nativevalues
Warning:
Removed file /afs/csail.mit.edu/u/j/jgross/HoTT/coq/theories/Init/Tactics.vo
Anomaly: Library compilation failure. Please report.

[andrejbauer]

Well, powerful tactics are ok as long as:

1. We explain very clearly how they are used.
2. We keep the library proper simple, i.e., it should minimze the use of powerful tactics and fancy Coq features.

Regarding 2, it would be silly not to use any Coq technology, but it is better to minimize the technology because it is very off-putting to a beginner. One possibility is to start simple and gradually increase the use of technology.

I still think we should not mix two technologies, so I would banish canonical structures until we have a very, very good reason to use them. This library is not a playground for experimenting with new methods of math formalization because it has a target audience that will be completely lost by such experiments. Unless of course you think our target audience is someone else. (Are there any lurkers out there who can contribute to the discussion?)

[spitters]

I am trying to recreate Coq's Prop and Set. It seems that the current way works. I'll spend more time documenting it.

On Sun, Aug 25, 2013 at 11:14 PM, Andrej Bauer notifications@github.comwrote:

Well, powerful tactics are ok as long as:

1. We explain very clearly how they are used.
2. We keep the library proper simple, i.e., it should minimze the use of powerful tactics and fancy Coq features.

Regarding 2, it would be silly not to use any Coq technology, but it is better to minimize the technology because it is very off-putting to a beginner. One possibility is to start simple and gradually increase the use of technology.

I still think we should not mix two technologies, so I would banish canonical structures until we have a very, very good reason to use them. This library is not a playground for experimenting with new methods of math formalization because it has a target audience that will be completely lost by such experiments. Unless of course you think our target audience is someone else. (Are there any lurkers out there who can contribute to the discussion?)

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

[awodey]

Sent from my iPhone

On Aug 25, 2013, at 5:25 PM, Bas Spitters notifications@github.com wrote:

I am trying to recreate Coq's Prop and Set.

Why? We got rid of them for a reason.

It seems that the current way works. I'll spend more time documenting it.

On Sun, Aug 25, 2013 at 11:14 PM, Andrej Bauer notifications@github.comwrote:

Well, powerful tactics are ok as long as:

1. We explain very clearly how they are used.
2. We keep the library proper simple, i.e., it should minimze the use of powerful tactics and fancy Coq features.

Regarding 2, it would be silly not to use any Coq technology, but it is better to minimize the technology because it is very off-putting to a beginner. One possibility is to start simple and gradually increase the use of technology.

I still think we should not mix two technologies, so I would banish canonical structures until we have a very, very good reason to use them. This library is not a playground for experimenting with new methods of math formalization because it has a target audience that will be completely lost by such experiments. Unless of course you think our target audience is someone else. (Are there any lurkers out there who can contribute to the discussion?)

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

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

[spitters]

Here is a simple case:

It is much nicer to write P:A -> hProp instead of P: A-> Type, (forall a, IsProp (P a)).

The latter unbundled approach becomes quite verbose in longer examples.

On Sun, Aug 25, 2013 at 11:33 PM, Steve Awodey notifications@github.comwrote:

Sent from my iPhone

On Aug 25, 2013, at 5:25 PM, Bas Spitters notifications@github.com wrote:

I am trying to recreate Coq's Prop and Set.

Why? We got rid of them for a reason.

It seems that the current way works. I'll spend more time documenting it.

On Sun, Aug 25, 2013 at 11:14 PM, Andrej Bauer notifications@github.comwrote:

Well, powerful tactics are ok as long as:

1. We explain very clearly how they are used.
2. We keep the library proper simple, i.e., it should minimze the use of powerful tactics and fancy Coq features.

Regarding 2, it would be silly not to use any Coq technology, but it is better to minimize the technology because it is very off-putting to a beginner. One possibility is to start simple and gradually increase the use of technology.

I still think we should not mix two technologies, so I would banish canonical structures until we have a very, very good reason to use them. This library is not a playground for experimenting with new methods of math formalization because it has a target audience that will be completely lost by such experiments. Unless of course you think our target audience is someone else. (Are there any lurkers out there who can contribute to the discussion?)

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

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

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

[andrejbauer]

I agree it's nice to be able to write it, but not at the expense of using any kind of magic. You could define hProp to be a record, and then write A -> hProp, what's wrong with that? Again, plase refrain from using advanced Coq techniques until we discuss this issue. (You can always fork away to your heart's content, but leave the library alone.)

[spitters]

This can be done at the expense of writing much longer proofs. Basically, you would done by hand what the canonical structures do for you. Enrico and Assia have a nice paper. http://hal.inria.fr/hal-00816703/en

As I said, I'll document more and then we can discuss.

On Mon, Aug 26, 2013 at 12:13 AM, Andrej Bauer notifications@github.comwrote:

I agree it's nice to be able to write it, but not at the expense of using any kind of magic. You could define hProp to be a record, and then write A -> hProp, what's wrong with that? Again, plase refrain from using advanced Coq techniques until we discuss this issue. (You can always fork away to your heart's content, but leave the library alone.)

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

[awodey]

But the discussion should come before pulling such changes into the library. Isn't there a mechanism in place for discussing pull requests before pulling them?

Sent from my iPhone

On Aug 25, 2013, at 6:40 PM, Bas Spitters notifications@github.com wrote:

This can be done at the expense of writing much longer proofs. Basically, you would done by hand what the canonical structures do for you. Enrico and Assia have a nice paper. http://hal.inria.fr/hal-00816703/en

As I said, I'll document more and then we can discuss.

On Mon, Aug 26, 2013 at 12:13 AM, Andrej Bauer notifications@github.comwrote:

I agree it's nice to be able to write it, but not at the expense of using any kind of magic. You could define hProp to be a record, and then write A -> hProp, what's wrong with that? Again, plase refrain from using advanced Coq techniques until we discuss this issue. (You can always fork away to your heart's content, but leave the library alone.)

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

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

[mikeshulman]

I agree with Andrej and Steve. The place for experimentation is in branches and forks. I haven't been actually reading the recent pull requests due to a lack of time, but I suspect from skimming the comments that some of them ought to be reverted.

I am generally against "Adamization", i.e. writing "hammer" tactics which try many things in case one of them works. I want mathematicians reading the code and learning from it to be able to understand what is going on and be able to reproduce it in their own code. I am not against fancy tactics per se. For instance, I am in favor of the issig tactics and any improvements we can make to them, because it is easy to explain what they do, if not exactly how they manage to do it, and a user with a basic understanding of the library could reproduce what they do in any particular case -- all they do is save the user work without making the proof script any less comprehensible. Each powerful tactic should do one thing and one thing well, and it should be clearly documented and understandable what exactly it does.

On Sun, Aug 25, 2013 at 4:03 PM, Steve Awodey notifications@github.comwrote:

But the discussion should come before pulling such changes into the library. Isn't there a mechanism in place for discussing pull requests before pulling them?

Sent from my iPhone

On Aug 25, 2013, at 6:40 PM, Bas Spitters notifications@github.com wrote:

This can be done at the expense of writing much longer proofs. Basically, you would done by hand what the canonical structures do for you. Enrico and Assia have a nice paper. http://hal.inria.fr/hal-00816703/en

As I said, I'll document more and then we can discuss.

On Mon, Aug 26, 2013 at 12:13 AM, Andrej Bauer notifications@github.comwrote:

I agree it's nice to be able to write it, but not at the expense of using any kind of magic. You could define hProp to be a record, and then write A -> hProp, what's wrong with that? Again, plase refrain from using advanced Coq techniques until we discuss this issue. (You can always fork away to your heart's content, but leave the library alone.)

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

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

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

[JasonGross]

@awodey:

I am trying to recreate Coq's Prop and Set.

Why? We got rid of them for a reason.

What was that reason? I thought the reason to not use Prop was because it was a kind-of strange almost-hProp, in that it is consistent with proof-irrelevance, but does not require it, and does not make use of it. I, personally, would be very much in favor of Coq getting keywords meaning hProp and hSet, which, for example, allow a more powerful pattern matching syntax which assumes K (such as described in http://coq.inria.fr/files/adt-2fev10-corbineau.pdf) when dealing with types for which K provably holds.

@mikeshulman:

I am generally against "Adamization", i.e. writing "hammer" tactics which try many things in case one of them works. In that case, my commit adding the path_induction_hammer tactic should possibly be reverted. It tries everything I could think of to eliminate any paths appearing in the context or goals. However, I think that the path_forall_hammer tactic is closer to the issig tactic; it has a set strategy for simplifying transports involving path_forall which can be done fairly simply on the blackboard or by hand.

@awodey:

Isn't there a mechanism in place for discussing pull requests before pulling them?

I think in this case (or in at least one of these), I merged the relevant pull request after no one else commented on the content for two days, which happened to be a few minutes before Andrej commented with objections. Apologies for merging it too soon. Perhaps in the future I should wait longer before merging pull requests that look good to me?

@spitters: Do you have an example of a proof that becomes more annoying when you make hProp and hSet records rather than canonical structures? (I suppose it means that you have to wrap all of your types in BuildhSet or BuildhProp, and in this instance, the canonical structures are acting as coercions? I'm not sure whether or not it's actually working like that?...)

[peterlefanulumsdaine]

[Sub-topic: recovering Prop and Set.]

We did get rid of Coq’s Prop and Set for a good reason: from the POV of semantics (especially higher-categorical), their special treatment among universes seemed somewhat ad hoc and unnecessary.

However, the “unnecessary” part is in part because we can essentially recover all the important features of them (and more), as the defined objects hProp, hSet. So I’m all in favour of recovering them in this way, whether as records or canonical structures. From the little I’ve worked with canonical structures, I can well believe that introducing these as c.s.’s (if set up well) could be substantially more convenient to work with than record types. However, see below!

[Main topic: Stop and think!]

I agree with Andrej’s concerns over introducing “advanced technology” into the core library. In the particular case of canonical structures, I’m not sure whether I’m for or against. It can certainly make things much more convenient, and if that convenience can be achieved without a cost in transparency or usability for newcomers, then I’m in favour of including them — and I’m looking forward to trying out Bas’s exploration of them here, to see how working with it feels.

However, I’d be happier if that exploration were in a fork, not the main library — again, for the sake of keeping the main library a bit more stable, and a bit more consensus-driven.

So: would it make sense to ask that pull requests to the main library not merged until there’s been a bit more discussion on them (with the exception of bug fixes)?

Leaving merging until there’s been some discussion (at least, say, several people agreeing “yes, I’ve looked at this properly and I don’t object”) should help ensure that everyone stays reasonably happy with the library as it grows. The cost of this is that it would mean (especially when, as recently, many of the group are away from the project for a while) pull requests might take a while to get merged. However, if most development happens in forks, then hopefully slow acceptance of pull requests wouldn’t disrupt anyone’s workflow? Thoughts?

–p.

On Sun, Aug 25, 2013 at 7:46 PM, Jason Gross notifications@github.comwrote:

I am trying to recreate Coq's Prop and Set.

Why? We got rid of them for a reason.

What was that reason? I thought the reason to not use Prop was because it was a kind-of strange almost-hProp, in that it is consistent with proof-irrelevance, but does not require it, and does not make use of it. I, personally, would be very much in favor of Coq getting keywords meaning hProp and hSet, which, for example, allow a more powerful pattern matching syntax which assumes K (such as described in http://coq.inria.fr/files/adt-2fev10-corbineau.pdf) when dealing with types for which K provably holds.

I am generally against "Adamization", i.e. writing "hammer" tactics which try many things in case one of them works. In that case, my commit adding the path_induction_hammer tactic should possibly be reverted. It tries everything I could think of to eliminate any paths appearing in the context or goals. However, I think that the path_forall_hammer tactic is closer to the issig tactic; it has a set strategy for simplifying transports involving path_forall which can be done fairly simply on the blackboard or by hand.

Isn't there a mechanism in place for discussing pull requests before pulling them?

I think in this case (or in at least one of these), I merged the relevant pull request after no one else commented on the content for two days, which happened to be a few minutes before Andrej commented with objections. Apologies for merging it too soon. Perhaps in the future I should wait longer before merging pull requests that look good to me?

@spitters https://github.com/spitters: Do you have an example of a proof that becomes more annoying when you make hProp and hSet records rather than canonical structures? (I suppose it means that you have to wrap all of your types in BuildhSet or BuildhProp, and in this instance, the canonical structures are acting as coercions? I'm not sure whether or not it's actually working like that?...)

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

[mikeshulman]

IIRC Coq's Prop also has properties which hProp doesn't (at least not obviously), like being closed under impredicative quantification.

FWIW, my experience last year was that canonical structures were much harder to understand than typeclasses. This was probably partly due to prior experience with Haskell, but Haskell typeclasses were also easy to understand when I first learned them, and the ways in which they were most difficult are made easier in Coq by dependent types. Canonical structures felt much more like black magic and require all sorts of unintuitive tricks to do what you want.

In the past, I thought the general rule was that pull requests could be merged by anyone except the person who made them, so that there were at least two eyes on every change. If we want to change this to "at least three eyes" then we could require one additional "looks okay" comment before someone merges it.

[spitters]

On Mon, Aug 26, 2013 at 1:46 AM, Jason Gross notifications@github.comwrote:

What was that reason? I thought the reason to not use Prop was because it was a kind-of strange almost-hProp, in that it is consistent with proof-irrelevance, but does not require it, and does not make use of it. I, personally, would be very much in favor of Coq getting keywords meaning hProp and hSet, which, for example, allow a more powerful pattern matching syntax which assumes K (such as described in http://coq.inria.fr/files/adt-2fev10-corbineau.pdf) when dealing with types for which K provably holds.

There is currently a similar discussion going on on the agda mailing-list "another possible without-K problem". It is possible to build these things into the type checker using syntactic checks. Maybe this should be done at some point. For now we can use type classes, c.s.

I am generally against "Adamization", i.e. writing "hammer" tactics which try many things in case one of them works. In that case, my commit adding the path_induction_hammer tactic should possibly be reverted. It tries everything I could think of to eliminate any paths appearing in the context or goals. However, I think that the path_forall_hammer tactic is closer to the issig tactic; it has a set strategy for simplifying transports involving path_forall which can be done fairly simply on the blackboard or by hand.

Isn't there a mechanism in place for discussing pull requests before pulling them?

I pulled Jason's patch precisely for this reason. We discussed it. It seemed reasonable and noone objected.

@spitters https://github.com/spitters: Do you have an example of a proof that becomes more annoying when you make hProp and hSet records rather than canonical structures?

I need hProp as a record in the proof of epi_surj https://github.com/HoTT/HoTT/blob/master/theories/hit/epi.v All I did was trying to make the proof somewhat readable. I'll go through the code and write more documentation.

[spitters]

@mikeshulman: The paper by Assia and Enrico on CS is nice. Moreover, for now, I am only making very limited use of it.

On Mon, Aug 26, 2013 at 6:32 AM, Mike Shulman notifications@github.comwrote:

IIRC Coq's Prop also has properties which hProp doesn't (at least not obviously), like being closed under impredicative quantification.

FWIW, my experience last year was that canonical structures were much harder to understand than typeclasses. This was probably partly due to prior experience with Haskell, but Haskell typeclasses were also easy to understand when I first learned them, and the ways in which they were most difficult are made easier in Coq by dependent types. Canonical structures felt much more like black magic and require all sorts of unintuitive tricks to do what you want.

In the past, I thought the general rule was that pull requests could be merged by anyone except the person who made them, so that there were at least two eyes on every change. If we want to change this to "at least three eyes" then we could require one additional "looks okay" comment before someone merges it.

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

[spitters]

@andrejbauer: Another target audience would be Coq power users/developers who want to understand how Coq should develop (I am also thinking of @mattam82 and other Coq devs here). Is HoTT really the future of type theory, or is it just a playground for people who want to write slick proofs in algebraic topology?

I, for one, would like to understand whether it is possible to develop an algebraic hierarchy and how to use SIP in practice. We know we need either type classes or CS (and probably both) for the former.

On Sun, Aug 25, 2013 at 11:14 PM, Andrej Bauer notifications@github.comwrote:

Well, powerful tactics are ok as long as:

1. We explain very clearly how they are used.
2. We keep the library proper simple, i.e., it should minimze the use of powerful tactics and fancy Coq features.

Regarding 2, it would be silly not to use any Coq technology, but it is better to minimize the technology because it is very off-putting to a beginner. One possibility is to start simple and gradually increase the use of technology.

I still think we should not mix two technologies, so I would banish canonical structures until we have a very, very good reason to use them. This library is not a playground for experimenting with new methods of math formalization because it has a target audience that will be completely lost by such experiments. Unless of course you think our target audience is someone else. (Are there any lurkers out there who can contribute to the discussion?)

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

[awodey]

On Aug 26, 2013, at 6:32 AM, Mike Shulman notifications@github.com wrote:

IIRC Coq's Prop also has properties which hProp doesn't (at least not obviously), like being closed under impredicative quantification.

FWIW, my experience last year was that canonical structures were much harder to understand than typeclasses. This was probably partly due to prior experience with Haskell, but Haskell typeclasses were also easy to understand when I first learned them, and the ways in which they were most difficult are made easier in Coq by dependent types. Canonical structures felt much more like black magic and require all sorts of unintuitive tricks to do what you want.

In the past, I thought the general rule was that pull requests could be merged by anyone except the person who made them, so that there were at least two eyes on every change. If we want to change this to "at least three eyes" then we could require one additional "looks okay" comment before someone merges it.

I think 3 eyes (er, 6 eyes?) would make sense now that there are more people contributing -- especially since there's some uncertainty at the moment about where the library is heading.

[andrejbauer]

The reason that Prop is banned is that with it, through large elimination, we can immediately prove that our paths agrees with Coq's proof irrelevant equality = (which maps into Prop), which thereby trivializes the entire HoTT.

[guillaumebrunerie]

Equality is not proof irrelevant in Coq (unless you assume it). The problem is that Coq’s equality lands in Prop which is:

• impredicative
• small

I don’t think we know much about interaction between impredicativity and HoTT, but the fact that Prop is small is definitely a problem. For instance take G a big group (in a large universe), construct K(G,1), and consider its loop space. You will get something small (in Prop) and equivalent to G, contradiction. You can construct K(G,1) using HITs, but I think you can also doing using just univalence, by considering the type of G-torsors, or something like that.

Guillaume

On 2013/8/26 Andrej Bauer notifications@github.com wrote:

The reason that Prop is banned is that with it, through large elimination, we can immediately prove that our paths agrees with Coq's proof irrelevant equality = (which maps into Prop), which thereby trivializes the entire HoTT.

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

[peterlefanulumsdaine]

Weren’t these particular issues with Prop solved by the “-indices-matter” flag, though, which should ensure that un-squashed equality is not in Prop, and that if you squash it into Prop by hand, you can’t eliminate back into the un-squashed version? Or am I misremembering something?

–p.

On Mon, Aug 26, 2013 at 11:01 AM, Guillaume Brunerie < notifications@github.com> wrote:

Equality is not proof irrelevant in Coq (unless you assume it). The problem is that Coq’s equality lands in Prop which is:

• impredicative
• small

I don’t think we know much about interaction between impredicativity and HoTT, but the fact that Prop is small is definitely a problem. For instance take G a big group (in a large universe), construct K(G,1), and consider its loop space. You will get something small (in Prop) and equivalent to G, contradiction. You can construct K(G,1) using HITs, but I think you can also doing using just univalence, by considering the type of G-torsors, or something like that.

Guillaume

On 2013/8/26 Andrej Bauer notifications@github.com wrote:

The reason that Prop is banned is that with it, through large elimination, we can immediately prove that our paths agrees with Coq's proof irrelevant equality = (which maps into Prop), which thereby trivializes the entire HoTT.

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

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

[awodey]

I guess what's unclear is what exactly Bas intends when he says he wants to "recreate Coq's Prop and Set".

On Aug 26, 2013, at 11:31 AM, Peter LeFanu Lumsdaine notifications@github.com wrote:

Weren’t these particular issues with Prop solved by the “-indices-matter” flag, though, which should ensure that un-squashed equality is not in Prop, and that if you squash it into Prop by hand, you can’t eliminate back into the un-squashed version? Or am I misremembering something?

–p.

On Mon, Aug 26, 2013 at 11:01 AM, Guillaume Brunerie < notifications@github.com> wrote:

Equality is not proof irrelevant in Coq (unless you assume it). The problem is that Coq’s equality lands in Prop which is:

• impredicative
• small

I don’t think we know much about interaction between impredicativity and HoTT, but the fact that Prop is small is definitely a problem. For instance take G a big group (in a large universe), construct K(G,1), and consider its loop space. You will get something small (in Prop) and equivalent to G, contradiction. You can construct K(G,1) using HITs, but I think you can also doing using just univalence, by considering the type of G-torsors, or something like that.

Guillaume

On 2013/8/26 Andrej Bauer notifications@github.com wrote:

The reason that Prop is banned is that with it, through large elimination, we can immediately prove that our paths agrees with Coq's proof irrelevant equality = (which maps into Prop), which thereby trivializes the entire HoTT.

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

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

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

[spitters]

I seem to have opened a can of worms. I meant what Peter said: we can essentially recover all the important features of them (and more), as the defined objects hProp, hSet. So I’m all in favour of recovering them in this way, whether as records or canonical structures. From the little I’ve worked with canonical structures, I can well believe that introducing these as c.s.’s (if set up well) could be substantially more convenient to work with than record types. However, see below!

On Mon, Aug 26, 2013 at 5:38 PM, Steve Awodey notifications@github.comwrote:

I guess what's unclear is what exactly Bas intends when he says he wants to "recreate Coq's Prop and Set".

On Aug 26, 2013, at 11:31 AM, Peter LeFanu Lumsdaine < notifications@github.com> wrote:

Weren’t these particular issues with Prop solved by the “-indices-matter” flag, though, which should ensure that un-squashed equality is not in Prop, and that if you squash it into Prop by hand, you can’t eliminate back into the un-squashed version? Or am I misremembering something?

–p.

On Mon, Aug 26, 2013 at 11:01 AM, Guillaume Brunerie < notifications@github.com> wrote:

Equality is not proof irrelevant in Coq (unless you assume it). The problem is that Coq’s equality lands in Prop which is:

• impredicative
• small

I don’t think we know much about interaction between impredicativity and HoTT, but the fact that Prop is small is definitely a problem. For instance take G a big group (in a large universe), construct K(G,1), and consider its loop space. You will get something small (in Prop) and equivalent to G, contradiction. You can construct K(G,1) using HITs, but I think you can also doing using just univalence, by considering the type of G-torsors, or something like that.

Guillaume

On 2013/8/26 Andrej Bauer notifications@github.com wrote:

The reason that Prop is banned is that with it, through large elimination, we can immediately prove that our paths agrees with Coq's proof irrelevant equality = (which maps into Prop), which thereby trivializes the entire HoTT.

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

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

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

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

[awodey]

On Aug 26, 2013, at 2:07 PM, Bas Spitters notifications@github.com wrote:

I seem to have opened a can of worms. I meant what Peter said: we can essentially recover all the important features of them (and more), as the defined objects hProp, hSet.

that's a relief! it sounded as though you wanted to put back in something we were glad to have gotten rid of!

So I’m all in favour of recovering them in this way, whether as records or canonical structures. From the little I’ve worked with canonical structures, I can well believe that introducing these as c.s.’s (if set up well) could be substantially more convenient to work with than record types. However, see below!

On Mon, Aug 26, 2013 at 5:38 PM, Steve Awodey notifications@github.comwrote:

I guess what's unclear is what exactly Bas intends when he says he wants to "recreate Coq's Prop and Set".

On Aug 26, 2013, at 11:31 AM, Peter LeFanu Lumsdaine < notifications@github.com> wrote:

Weren’t these particular issues with Prop solved by the “-indices-matter” flag, though, which should ensure that un-squashed equality is not in Prop, and that if you squash it into Prop by hand, you can’t eliminate back into the un-squashed version? Or am I misremembering something?

–p.

On Mon, Aug 26, 2013 at 11:01 AM, Guillaume Brunerie < notifications@github.com> wrote:

Equality is not proof irrelevant in Coq (unless you assume it). The problem is that Coq’s equality lands in Prop which is:

• impredicative
• small

I don’t think we know much about interaction between impredicativity and HoTT, but the fact that Prop is small is definitely a problem. For instance take G a big group (in a large universe), construct K(G,1), and consider its loop space. You will get something small (in Prop) and equivalent to G, contradiction. You can construct K(G,1) using HITs, but I think you can also doing using just univalence, by considering the type of G-torsors, or something like that.

Guillaume

On 2013/8/26 Andrej Bauer notifications@github.com wrote:

The reason that Prop is banned is that with it, through large elimination, we can immediately prove that our paths agrees with Coq's proof irrelevant equality = (which maps into Prop), which thereby trivializes the entire HoTT.

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

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

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

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

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