0
votes
1answer
219 views

prod and sig in COQ

Hello, Apparently in COQ the type prod (with one constructor pair) corresponds to cartesian product and the type sig (with one constructor exist) to dependent sum but how is described the fact that ...
1
vote
2answers
850 views

What is a semigroup or, what do I do with that associativity proof?

Mathematically, I know what a semigroup is: It is a set S along with an associative binary operation $* : S \times S \rightarrow S$. So far, so good. From a computational perspective, one can ...