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

Profunctor Equivalence Isos #19

Closed GenericMonkey closed 1 year ago

GenericMonkey commented 1 year ago

Merging in the Isos between the definitions, as well as some clean up in Profunctor General.

There are 6 equivalences specified (between each pair of definitions).

GenericMonkey commented 1 year ago

This completes the rest of the work for Issue #7