Wildcat improvements #1766
Wildcat improvements #1766
Conversation
| Definition equiv_postcompose_cat_equiv {A : Type} `{HasEquivs A} `{!HasMorExt A} | ||
| {x y z : A} (f : y $<~> z) | ||
| : (x $-> y) <~> (x $-> z) | ||
| := emap (opyon x) f. |
There was a problem hiding this comment.
This used to be in another file with a long proof, but now it has a one-line proof.
| Definition equiv_precompose_cat_equiv {A : Type} `{HasEquivs A} `{!HasMorExt A} | ||
| {x y z : A} (f : x $<~> y) | ||
| : (y $-> z) <~> (x $-> z) | ||
| := @equiv_postcompose_cat_equiv A^op _ _ _ _ _ _ z y x f. |
There was a problem hiding this comment.
And this was proved with a separate long proof, even though it is just the dual result.
| exact ((cat_eissect f x)^$ $@ fmap (equiv_fun_0gpd f^-1$) h $@ cat_eissect f y). | ||
| Defined. | ||
|
|
||
| (** This is one example of many things that could be ported from Basics/Equivalences.v. *) |
There was a problem hiding this comment.
Thinking out loud here: It would be nice if we could derive all path. equiv (and maybe even group) lemmas from common wildcat ones.
There was a problem hiding this comment.
Yes, I think a lot of what we currently prove about Type is a special case of WildCat results, but there's a challenge about avoiding circularity, since the WildCat library uses some concepts about types. In any case, I'm seeing more and more ways that the WildCat library can have a real impact on other results, and also internal simplifications as more fundamental things get added.
There was a problem hiding this comment.
I think the circularity issues are a non-issue. We can always prove what we need in wildcat in the library. In fact, we could fully cut the dependency on Types as a result. and have Types depend on Wildcat. We shouldn't need much of Types to prove results about wildcats. On the other hand, we would gain a lot using wildcat in Types.
|
Looks great! I haven't had a chance to step through the proofs myself, but reading it all seems fine. Let's give this a few days before we merge in case I find anything. If you however wish to press on, I have no issue merging it now. |
|
Is it ok if we merge this tomorrow rather than in a few days? And if it's going to be tomorrow, I'll add one more commit. |
|
@jdchristensen That's fine. If I have any further comments we can continue after the merge no problem. |
|
Ok, I just added one new commit. I'll wait until tomorrow before merging. |
A bunch of additions to the WildCat library, as well as various simplifications to existing proofs. Many of these are for WIP that I hope to PR soon.