search

maxsnew / cubical-categorical-logic

Extensions to the cubical stdlib category theory for categorical logic/type theory
MIT License
25 stars 5 forks source link

Environment Comonad #21

Closed maxsnew closed 1 year ago

maxsnew commented 1 year ago

Need this for Eric's project. Implement the holes in https://github.com/maxsnew/multi-poly-cats/blob/main/Cubical/Categories/Comonad/Instances/Environment.agda .

maxsnew commented 1 year ago

completed in https://github.com/maxsnew/multi-poly-cats/commit/05a58210080752a1765aaf0e2451cb27ba2eaed7