First-class lifts? First-class composition of lifts?

uwplse / pumpkin-pi

An extension to PUMPKIN PATCH with support for proof repair across type equivalences.

MIT License

49 stars 9 forks source link

First-class lifts? First-class composition of lifts? #83

Open Ptival opened 4 years ago

Ptival commented 4 years ago

I often find myself having some sort of sequence of lifts I need to do on different values.

Modules make it so that I can stash all of those things in a module, and lift the module. But it might be worth considering, depending on how feasible it is, to be able to define a given lift between two-types as something first class? (this might already be doable with the Find ornament command?)

If so, is it also feasible to define the composition of two lifts as a first-class object?

tlringer commented 3 years ago

Sorry to get to this so late. Deadlines!

Can you give me an idea of the syntax you want for this? Maybe a small mockup of an example case that I could get working?