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

update to cubical HEAD #39

Closed maxsnew closed 1 year ago

maxsnew commented 1 year ago

I fixed most things except:

  1. Anything outside the Cubical subdirectory is considered obsolete. I changed the Makefile to only check things in Cubical.
  2. Profunctor.General I only implemented one function which I called FunctorComprehension in line with the discussion at https://github.com/maxsnew/multi-poly-cats/issues/36 . Profunctor.Equiv is not fixed at all.