search

uwplse / pumpkin-pi

An extension to PUMPKIN PATCH with support for proof repair across type equivalences.
MIT License
49 stars 9 forks source link

From adjunction and coherence, show user-friendly equivalence #62

Closed tlringer closed 3 years ago

tlringer commented 5 years ago

See #57, #39

tlringer commented 5 years ago

Jason Gross has shown an example of this in #39

tlringer commented 4 years ago

We'll need unpacked versions of ltv/vtl or the corresponding functions too, as seen in #39. I think the way I did this in #39 was not great, so Nate if you get to this before me, let's talk a bit about the functions we choose here.

tlringer commented 4 years ago

I got started on this in a branch, so if you start on this, let me know and we can sync on how far I've gotten.

nateyazdani commented 4 years ago

Recording current state of this for future reference, expanding on Talia's previous comment...

Per that commented commit, we want to start off with an instantiated example for our favorite ornament, list to vector. The unfolded_equiv branch is a good place to track this work, although unpacked_equiv is perhaps a better descriptor, in retrospect.

  1. Tweak the unpacked (_i.e., index-exposed) ornamental equivalence to use the adjointified packed ornamental equivalence. Concretely, this just means to use the adjointified retraction consistently, in order to prove retraction for the unpacked ornamental equivalence, which we will probably want to adjointify in turn.

  2. Credit Jason Gross for the example right away, so we don't forget.

  3. Commit and merge in this example instance.

  4. Minimize and regularize these example proofs, to serve as the template for automation.

  5. Commit and merge in this modification.

  6. Implement automation for the unpacked ornamental equivalence of any other (supported) ornament. Hopefully, this will proceed formulaically, due to the prior regularization.

  7. Commit and merge in the general automation.

  8. Move onto issues #39 and #34. N.B. that the comments on #39 provide useful context for the current template of the example (pending the changes described in this comment); however, that issue's scope is technically the application of the unpacked ornamental equivalence in order to derive a user-indexing of an ornamentally lifted function (given an appropriate indexing lemma), whereas this issue's scope is more precisely the unpacked ornamental equivalence, itself.

tlringer commented 3 years ago

Not worth it anymore with more general equivalence support, including for unpacking sigma types