Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | |||
|
babbys_first_hott [2016/07/18 01:14] nikolaj |
babbys_first_hott [2017/03/13 00:13] nikolaj |
||
|---|---|---|---|
| Line 45: | Line 45: | ||
| $Semigroup\equiv{\large{\sum}}_{A:\mathrm{Type}}{\large{\sum}}_{m:A\to A\to A}{\large{\prod}}_{x:A}{\large{\prod}}_{y:A}{\large{\prod}}_{z:A}\ m(x,m(y,z))=_A m(m(x,y),z)$ | $Semigroup\equiv{\large{\sum}}_{A:\mathrm{Type}}{\large{\sum}}_{m:A\to A\to A}{\large{\prod}}_{x:A}{\large{\prod}}_{y:A}{\large{\prod}}_{z:A}\ m(x,m(y,z))=_A m(m(x,y),z)$ | ||
| - | A term of $SemiGroupStr$ is a pair $\langle A,\langle m,p\rangle\rangle$, where the first entry is a type $A$ and the second entry is pair, where the first entry is a function $m:A\to A\to A$ and the second entry is a proof $p$ that this this $m$ fulfills the usual axiom. We do constructive mathematics here, so $p$ is a function which takes any $x$ to a function which takes any $y$ to a ... to a function which takes any $m(m(x,y),z)$ to a term which demonstrates the required equality. | + | A term of $SemiGroupStr$ is a pair $\langle A,\langle m,p\rangle\rangle$, where the first entry is a type $A$ and the second entry is pair, where the first entry is a function $m:A\to A\to A$ and the second entry is a proof $p$ that this $m$ fulfills the usual axiom. We do constructive mathematics here, so $p$ is a function which takes any $x$ to a function which takes any $y$ to a ... to a function which takes any $m(m(x,y),z)$ to a term which demonstrates the required equality. |
| == Example 2 == | == Example 2 == | ||
