maxsnew / cubical-categorical-logic

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

Profunctor function defs merged in #17

Closed stschaef closed 1 year ago

stschaef commented 1 year ago

Added definitions going between definitions of profunctor representability

I didn't mean to add Profunctor.Equivalence into this commit, but this shouldn't cause any issues because its not used anywhere. Actual push of those equivalences soon to come