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

Generate a proof of adjunction #57

Closed tlringer closed 4 years ago

tlringer commented 5 years ago

See #39

tlringer commented 5 years ago

Useful: https://github.com/CoqHott/univalent_parametricity/blob/master/theories/HoTT.v

tlringer commented 5 years ago

This should quantify over all section/retraction proofs

tlringer commented 4 years ago

We can use this: https://github.com/jashug/IWTypes/blob/master/Adjointification.v

We should obviously credit Jasper everywhere we do

nateyazdani commented 4 years ago

Resolved by #68.