search

maxsnew / cubical-categorical-logic

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

Free Cartesian Category #60

Closed maxsnew closed 5 months ago

maxsnew commented 9 months ago

Implement the free cartesian category and its eliminator. WIP on https://github.com/maxsnew/multi-poly-cats/pull/57

hejohns commented 5 months ago

implemented by #94, see https://github.com/maxsnew/cubical-categorical-logic/pull/57#issuecomment-2192896788