Rewrite

[spitters]

I am curious whether we can get this to work:

Require Import HProp. Goal forall {A B:Type}, IsHProp A -> A <~>B -> IsHProp B. intros ?? H e. rewrite <- e.

Error: Library Coq.Setoids.Setoid has to be required first.

It looks like hoq does not see the vo files in coq-HoTT/ (So why are they there at all?) So we need to copy them to the directory coq/ and recompile. This seems to require a little tweaking of the make file.

@andrejbauer @JasonGross before I embark on this, is this the way to proceed? Do you happen to know which part of the makefile to change?

[JasonGross]

@spitters, coq-HoTT is a copy of the upstream Coq git repository, and we have no control over its contents, except by picking a commit hash that we're tying ourselves to. You should manually copy the relevant .v files to coq/theories, git add them, tweak them as necessary, and add them to the STD_VFILES list in Makefile_targets.mk.

[mikeshulman]

I think we ought to keep anything and everything setoidy out of the HoTT library.

[JasonGross]

Why? Anytime we don't want to bring in univalence, using setoidy stuff will help us make use of equivalences. (In fact, we could set it up so that, on concrete types, having an equivalence is as easy as having an equality, in terms of rewriting, even without univalence.) It might also allow us to get rewrite or setoid_rewrite to insert terms that unfold to transport rather than paths_rect or match statements.

[spitters]

Precisely, this should be a way to get better proof terms.

On Thu, Sep 11, 2014 at 7:41 PM, Jason Gross notifications@github.com wrote:

Why? Anytime we don't want to bring in univalence, using setoidy stuff will help us make use of equivalences. (In fact, we could set it up so that, on concrete types, having an equivalence is as easy as having an equality, in terms of rewriting, even without univalence.) It might also allow us to get rewrite or setoid_rewrite to insert terms that unfold to transport rather than paths_rect or match statements.

— Reply to this email directly or view it on GitHub https://github.com/HoTT/HoTT/issues/488#issuecomment-55300427.

[andrejbauer]

@mikeshulman: Jason and Bas aren't proposing that we use setoids for formalization of mathematics, just that we can use the technology to have rewrite work also for equivalences. Right?

For instance, if we tell Coq that <~> is an equivalence relation on types, and that various type constructors preserve equivalence, then we will be able to rewrite along <~>.

[mattam82]

Yes, Setoid is just a historical name. What you want is generalized rewriting, i.e., rewriting with arbitrary relations in contexts that preserve them. With univalence, everything is equivalence-preserving, so you could rewrite with any equivalence pretty much everywhere, where for now you have to explicitely go through equality I suppose. I suppose the fact that this rewrite also goes under binders could help as well.

[mattam82]

And even without univalence, many definitions are provably equivalence preserving as well, indeed.

[andrejbauer]

And in fact, all definitions are equivalence preserving.

[mikeshulman]

Ok, I see; I guess this is worth investigating.

[spitters]

In fact, this can be one step towards a computational interpretation of univalence, we can see to what extend we can push through all the uses of equiv.

On Fri, Sep 12, 2014 at 5:31 PM, Matthieu Sozeau notifications@github.com wrote:

And even without univalence, many definitions are equivalence preserving as well, indeed.

— Reply to this email directly or view it on GitHub https://github.com/HoTT/HoTT/issues/488#issuecomment-55419431.

[andrejbauer]

Right. If we manage to push it through everything then how close are we to a computational interpretation of univalence?

[JasonGross]

We're not going to push it through everything. For example, @paths Type nat is only equivalence-invariant if we have univalence. However, if we push it through everything we currently have, using univalence when needed, I think all that's left will be to extend it to arbitrary W-types, and to prove that we've actually got everything. And to show that our algorithm terminates, because typeclass resolution doesn't have to terminate.

[spitters]

Here's something that allows rewriting with <~>. it's probably not complete, but I'd like to check whether there is an interest in this. I've been quite aggressive removing things from the coq std lib.

https://github.com/spitters/HoTT/tree/setoidrewrite

[mikeshulman]

Looks interesting to me! I'd like to see more examples.

[spitters]

There are some here. Any requests for the kinds of example you'd like to see? https://github.com/spitters/HoTT/blob/setoidrewrite/setoidtest.v

[mikeshulman]

Is there anywhere in the current library where this would be useful?

[JasonGross]

All of the places where we have long chains of manually composing equivalences/paths, where it's annoying to figure out the arguments manually, might be shorter using (setoid_)rewrite

[mikeshulman]

That's the sort of example I'd like to see.