# Tagged Questions

**0**

votes

**1**answer

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

**2**answers

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 ...