search

HoTT / Coq-HoTT

A Coq library for Homotopy Type Theory
http://homotopytypetheory.org/
Other
1.25k stars 193 forks source link

Remove ssreflect #186

Closed andrejbauer closed 9 years ago

andrejbauer commented 11 years ago

It seems to me that the ssrefelect stuff is not working, and nobody is really going to fix it. Also, I would not want ssreflect to be used in the HoTT library. Should we just get rid of ssreflect?

spitters commented 11 years ago

Cyril was planning to have a look at it.

Also, we are looking at using canonical structures together with HoTT, it seems that we can learn from ssr here.

On Tue, Aug 20, 2013 at 11:33 PM, Andrej Bauer notifications@github.comwrote:

It seems to me that the ssrefelect stuff is not working, and nobody is really going to fix it. Also, I would not want ssreflect to be used in the HoTT library. Should we just get rid of ssreflect?

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

andrejbauer commented 11 years ago

Ok, let's leave it in for a while then.

Who is "we" in we are looking at using canonical structures"?

Perhaps we should talk a bit about the philosophy of the HoTT library, especially given recent suggestions to use fancier tools, to bundle things differently, etc.

In my view the HoTT library serves two purposes:

  1. It formalizes some homotopy type theory.
  2. It teaches people how to formalize homotopy type theory.

In particular, I do not consider HoTT library to be a playground for experimenting with fancy methods of formalization, because that goes against the second point. You cannot expect a beginner to be able to get a handle on the library, if the first thing the library does is introduce some super-advanced techniques that only experts understand. A corollary of this is that the library should be structured in such a way that super-advanced techniques get introduced gradually. The user has to be able to tell where to start reading something comprehensible.

Of course, we have to strike a good balance between usability and simplicity. We use type classes to increase usability, but that sets the bar higher for a new user. Will usability really be enhanced that much further if we throw in canonical structures as well?

spitters commented 11 years ago

"we" = a student and I. I hope to be able to work more on this. Canonical structures and ssr are fairly standard in Coq. We should try to understand how to use them with HoTT/ how these techniques extend to HoTT. If we remove the dependency, the work will be lost.

I promise not the litter the entire library with Canonical Structures before I understand what I am doing. (I guess the same holds for people like Cyril and Assia).

On Wed, Aug 21, 2013 at 11:17 AM, Andrej Bauer notifications@github.comwrote:

Ok, let's leave it in for a while then.

Who is "we" in we are looking at using canonical structures"?

Perhaps we should talk a bit about the philosophy of the HoTT library, especially given recent suggestions to use fancier tools, to bundle things differently, etc.

In my view the HoTT library serves two purposes:

  1. It formalizes some homotopy type theory.
  2. It teaches people how to formalize homotopy type theory.

In particular, I do not consider HoTT library to be a playground for experimenting with fancy methods of formalization, because that goes against the second point. You cannot expect a beginner to be able to get a handle on the library, if the first thing the library does is introduce some super-advanced techniques that only experts understand. A corollary of this is that the library should be structured in such a way that super-advanced techniques get introduced gradually. The user has to be able to tell where to start reading something comprehensible.

Of course, we have to strike a good balance between usability and simplicity. We use type classes to increase usability, but that sets the bar higher for a new user. Will usability really be enhanced that much further if we throw in canonical structures as well?

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

andrejbauer commented 11 years ago

It may be best to make a branch. You could take over the ssreflect branch, which is kind of dead right now.

mikeshulman commented 11 years ago

And/or a fork.

spitters commented 11 years ago

We already have some Canonical Structures in hott, and can continue to try to use them.

We should think more about other ssr niceties. @Barbichu and I think that moving the other srr stuff in a branch would be a good solution for now.

On Wed, Aug 21, 2013 at 11:42 AM, Andrej Bauer notifications@github.comwrote:

It may be best to make a branch. You could take over the ssreflect branch, which is kind of dead right now.

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

andrejbauer commented 11 years ago

Indeed, there are are two of those in HProp and HSet. We should get rid of them until we discuss #194, or at the very least not add any new ones.

andrejbauer commented 10 years ago

I am going to go ahead and get rid of ssreflect. I'll put it in a branch in case anyone wants to look at it later.

JasonGross commented 10 years ago

This is done, now, right?

andrejbauer commented 10 years ago

Yes, it was closed by #292, where I forgot to reference this issue.