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

Day Convolution Monoidal Structure #71

Open maxsnew opened 7 months ago

maxsnew commented 7 months ago

Given a monoidal structure on a base category C, define the Day convolution monoidal structure on Psh C

bond15 commented 7 months ago

I was starting to look at this following the 1lab definition. I can take a stab at this.