# 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] (current) 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 == |