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

Recursor for free cartesian categories #75

Closed maxsnew closed 5 months ago

maxsnew commented 7 months ago

This should be implemented using the eliminator, we just need to show that if C and D are cartesian categories then weaken C D is a displayed cartesian category.

hejohns commented 5 months ago

Should be closed by #94, once merged

rec: https://github.com/maxsnew/cubical-categorical-logic/blob/9f3919dd02b8c3b53650e99cbcaaed48b38fe583/Cubical/Categories/Constructions/Free/CartesianCategory/Base.agda#L221

weaken terminal: https://github.com/maxsnew/cubical-categorical-logic/blob/9f3919dd02b8c3b53650e99cbcaaed48b38fe583/Cubical/Categories/Displayed/Constructions/Weaken/Properties.agda#L36

weaken products: https://github.com/maxsnew/cubical-categorical-logic/blob/9f3919dd02b8c3b53650e99cbcaaed48b38fe583/Cubical/Categories/Displayed/Constructions/Weaken/Properties.agda#L42

We don't package up weakened terminal + weaken products for weakening cartesian categories.