Define adjunction with nicer type (cf., #68)

uwplse / pumpkin-pi

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

MIT License

49 stars 9 forks source link

Define adjunction with nicer type (cf., #68) #74

Open nateyazdani opened 4 years ago

nateyazdani commented 4 years ago

As mentioned in the PR for auto-instantiated adjunction proofs (#68), the constant for each adjunction proof should be assigned a nicer type for the user. Currently, the type inferred by Coq refers to the fg_id' lemma, rather than the nice wrapper ${ornament}_retraction for an ornament ${ornament}.

This task is not technically challenging but involves a lot of annoying plumbing in OCaml to assemble the desired type.

tlringer commented 3 years ago

Nate has moved on to other things, so help improving this is always welcome.