2-cat of pointed types

[Alizter]

We show the (2,1)-category structure for pointed types. In order to do this easily, we introduce a new tactic called pelim which allows easy path induction on the pointed equation of various pointed structures. This is particularly useful in removing funext from various pType coherences.

Various places seemed to break from these changes, but could easily be fixed by replacing pointed notations with wildcat notations. This perhaps hints at a larger refactoring that should be done.

My motivation for showing these coherences is the need for 1-functoriality of pre/postcomposition for some unrelated work. Therefore it made sense to quickly generalize to the full 2-category while I was at it.

[jdchristensen]

Nice! I'll take a close look tomorrow. A couple of questions for now. First, how does pelim compare with pointed_reduce and pointed_reduce_pmap? Can we unify them? Second, I'm surprised that just adding the (2,1)-category structure made various pointed notations like <~>* need to be replaced with wildcat notations. Do you have any idea why this happens? One issue with wildcat notations is that you don't always know which wildcat Coq is choosing to interpret your notation with...

[Alizter]

Nice! I'll take a close look tomorrow. A couple of questions for now. First, how does pelim compare with pointed_reduce and pointed_reduce_pmap? Can we unify them?

I originally tried to modify pointed_reduce to avoid using path_induction and instead use pelim, however it changed too much and pelim is a little slower due to the reduction I needed to do in the tactic.

Also it is not entirely trivial the order in which to do pelim on the hypotheses. If you look at the functoriality of the assocciators in the 2-category definition, you will see that the pelim order for similar proofs vary subtly in their order. I don't think it will be entirely trivial to get tactics to choose this order.

I think having the manual control is a little better. I would however like to improve the performance of pelim before we start using it more widely since it does more unfolding than it probably needs. The main idea comes from recognising that point equations typically have an application on the LHS and when you do a generalize dependent of the pointed structure applied to its basepoint you get a hypothesis that almost always fits paths_ind_r.

Thinking about it, using right-handed path induction consistently should lead to a far superior pointed_elim, therefore it might be worth investigating swapping the regular path induction for the right handed side at some point.

Second, I'm surprised that just adding the (2,1)-category structure made various pointed notations like <~>* need to be replaced with wildcat notations. Do you have any idea why this happens?

I was also surprised, but I think this is because extra groupoid instances throw off Coq's unification. This is apparent in the fact that a few proofs had to be changed from srapply to snrapply followed by exact. I'm not entirely sure this is the full picture however.

One issue with wildcat notations is that you don't always know which wildcat Coq is choosing to interpret your notation with...

Yes that might be true. I think the better option would be to redefine ->* as a specific form of $->, but I haven't checked if this is fully sensible just yet. (Especially if it changes universe numbers).

[Alizter]

I've just pushed another commit simplifying a few other proofs, but we can undo those if we don't feel they are necessary.

[jdchristensen]

Ok, I'm reviewing now, so hold off on pushing anything else for a bit.

[jdchristensen]

LGTM! Feel free to merge once the minor things I "pointed" out are fixed.

[jdchristensen]

The new pelim works very well! I see that it plays a slightly different role than pointed_reduce. pointed_reduce is more ambitious, trying to replace a pointed function with a strictly pointed function, while pelim is designed to handle things once the functions aren't needed any more, and only pointedness conditions remain. This is why the order of the arguments to pelim is important.

[Alizter]

@jdchristensen I can say that I didn't design pelim on purpose, it was a happy accident. I was simply trying to remove some funext from the precomposition lemmas and noticed that this pattern I was doing kept working so I turned it into a tactic. I'm glad it worked out in the end, and I hope it can be more widely useful. Especially in the cases where pointed_reduce leaves a poorly reduced goal.

[jdchristensen]

and I hope it can be more widely useful.

I may use it today after this is merged!

[Alizter]

@jdchristensen All comments addressed. I'll merge once the CI is green.

[Alizter]

@jdchristensen I've made the clearing a try. It doesn't affect anything but it might be useful for the reasons you've stated, although I haven't encountered such a situation yet.

[jdchristensen]

I think it's ok if you merge now that one build has succeeded.

[jdchristensen]

Did you do a squash merge by accident? Just a reminder that that's not our usual procedure.

[Alizter]

@jdchristensen That was on purpose sorry. I forgot that we preferred not to do this. I've gone ahead and forbid them from the repository settings so now only merge is available.