Stratify cells in wildcat #1550
Conversation
| (** Why can't coq resolve this? *) | ||
| refine (compose_cate_fun f h | ||
| $@ (_ $@R h) | ||
| $@ (compose_cate_fun g h)^$). | ||
| exact al. |
There was a problem hiding this comment.
Not sure why coq got dumber here.
|
What sort of "getting out of hand" do you anticipate? This seems to me to be a discrete change that's over with when finished, not the start of a lot of further changes that would add additional underscores. I guess one way to reduce the underscores would be to go the oo-route and just assume that everything is an oo-graph. I forget whether we decided there are any examples where the whole oo-graph structure is hard to define? If we don't go that far, we could still collapse at least the definitions of n-graphs into something inductive or recursive. |
|
In the future, we might want to write down a definition of 2/pseudo-functor. Already looking at the Is1Functor instances we can see that having so many unbundled typeclasses around leads to many underscores. It will be even worse if we ever start to write down such definitions. This is what I mean by getting out of hand. But I guess this is something expected when working with higher categories, the amount of data grows very quickly and you really have to do something clever to handle it. I believe the oo-graph route is the way forward eventually, but there are a few things that need to be worked out there first. I agree that this will reduce the number of underscores we have. The only example I can think of where it might be hard to write down the oo-graph structure is the "category" whose n-cells are n-transfors (perhaps invertible at some point). I'm not sure this is a blocker for adopting oo-graphs however. Doing something inductive or recursive may be possible, but it got too tricky for me when I tried this a few months back. I also didn't see the point if we are going to go for oo-graphs anyway. Anyway, the reason I wanted to do this was so I could push through with the 3x3 lemma for pushouts which has been sitting on my todo problem list for too long. 0:-) |
|
Yes, looking back at #1302 I remember now that there were cases where it was at least tricky to correctly define all the higher cells, like pType. But also that we should be able to cop out in any case by defining the dimensions we care about at the bottom and using ordinary paths above that. It might be worth experimenting with just introducing oo-graphs to replace graphs/2graphs/3graphs, but keeping all the other structures the way they are. |
I have gone ahead and split the cells data for wildcats as discussed in #1545. We now have the typeclasses
Is2GraphandIs3Graph.This also prompted me to go through the wildcat library and do a little cleanup. This included naming things properly etc. Unfortunately, there are example where coq isn't smart enough to guess things anymore. (Especially when mixing
->*and$->). The solution is to probably try to stick to wildcat notation as much as possible.This was much trickier than anticipated to carry out however. The completely unbundled approach to algebraic hierarchies is not very rigid with respect to changes lower down, and the number of underscores in the code has increased a bit. I can quickly see that this will get out of hand fast, so perhaps we need to bundle some things up in a clever way at some point.