uwplse/pumpkin-pi

Generate a proof of adjunction

tlringer opened this issue 5 years ago · 4 comments

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 5 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 5 years ago

Resolved by #68.