prove that the category of types and functions is symmetric monoidal

[WhatisRT]

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.

[FabrizioRomanoGenovese]

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)

[marcosh]

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 category Idris
• 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?

[FabrizioRomanoGenovese]

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.

[marcosh]

we are going to use TypesAsCategoryExtensional, btw, so we have extensionality