idris-ct
idris-ct copied to clipboard
prove that the category of types and functions is symmetric monoidal
It might be better to have cartesian monoidal categories instead. That way, we get a general machinery and just have to show the existence of finite products or binary products and a terminal object.
This actually makes sense. It may be easier to prove that type product is indeed a categorical product, then one could implement the proof that product gives always a monoidal structure (which we already know is true)
yes, that makes a lot of sense.
so the steps here could be:
- define categorical product
- define terminal object
- prove that
(,)
is a categorical product in the categoryIdris
- prove that
Idris
has a terminal object - prove that any category with finite products can be seen as a monoidal category
does this seem right?
Yes. The thing that may be a pain here is defining terminality. If $T$ is terminal, then you want to prove that f,g:X->T implies f = g for each X, f,g. I don't even think this is true without assuming extensionality, actually.
we are going to use TypesAsCategoryExtensional
, btw, so we have extensionality