add tactics for box,cap

[ecavallo]

No description provided.

[cangiuli]

Can this tactic just print "Why are you trying to input a box???" (I agree there should probably be a tactic, but have a hard time imagining people using it.)

[ecavallo]

I think it has come up at least once, though i forget where. cap might be useful in paths.s2...

[favonia]

Can this tactic just print "Why are you trying to input a box???" (I agree there should probably be a tactic, but have a hard time imagining people using it.)

We can have --expert mode. (OTOH --favonia will print out more trolling messages.) RedPRL/algaett#23

[clayrat]

One possible use-case is for #457. The idea there is that you prove a certain lemma by introducing a relation P : susp A -> susp A -> type on props A (where P(N,N)=(), P(N,S)=A, P(S,N)=A, P(S,S)=() and meridians map to univalences) and then showing it's reflexive, implies identity and so on. So for showing reflexivity, you need to construct (x : susp A) -> P x x, which is easy for poles, but in the case of a meridian you get a pretty big box made out of univalences in the type. I might be doing something wrong, but it seems that you need to provide a term for that box directly?

[favonia]

I realized there is an annoying technical issue: box is empirically different from comp because you cannot reorder its faces arbitrarily. The core language never allows permutation, but I want to hide this aspect if possible.