Internal monoids

[anuyts]

No description provided.

[anuyts]

My plan was to define monads as internal monoids in the monoidal category of endofunctors but I think I'm going to refrain from doing so as it looks like proving monoidality of the category of endofunctors is going to be more involved than I anticipated.
So my contributions here are:

• I (trivially) defined the category of endofunctors on a given category.
• I defined internal monoids in a strict monoidal category, morphisms of internal monoids, and indeed the category of internal monoids. However, one hole is open (to prove that the Homs of this category are sets); I suspect this may be easy to prove for someone who has more experience with the cubical library but I have no idea how to do it.

[ecavallo]

Looks good to me. I filled in the hole; there is some reflection machinery to help prove facts about records using lemmas for sigma-types.

[anuyts]

Good to know! I did contribute a few hand-proven record-to-Σ-isomorphisms by now.