Differences

This shows you the differences between two versions of the page.

Link to this comparison view

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 ==
Link to graph
Log In
Improvements of the human condition