selectively bind arguments in a multi-lambda?

[ecavallo]

Not sure if this is a good idea. Sometimes I'm defining a cube and for whatever reason it's more convenient if I flip it along some diagonal first. I could define a flip : (dim -> dim -> A) -> (dim -> dim -> A), but then when I write flip ? I won't have any boundary information in the hole. So maybe it would be useful to be able to write something like this:

def cool : {
  (A : univ)
  (p : dim -> dim -> A)
  -> sub {dim -> dim -> A} #t {\i j => p j i}
} = {
  \A p * j => p j
}

where * means "skip over binding this variable". It should be possible for a tactic like that to propagate boundary info, right?

[jonsterling]

I think this is a sick idea. Maybe with a different notation.

[favonia]

To be clear, \ * => id, \x * => x and \x * * => x are all identity functions, right?