Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision Next revision Both sides next revision | ||
|
babbys_first_hott [2015/02/06 13:57] nikolaj |
babbys_first_hott [2015/08/02 20:46] nikolaj |
||
|---|---|---|---|
| Line 29: | Line 29: | ||
| $P\times Q \equiv {\large{\sum}}_{x:P} Q$ | $P\times Q \equiv {\large{\sum}}_{x:P} Q$ | ||
| - | If we tag the terms of a type $P$ resp. $Q$ with the value of Bool, we can identify disjunction $\lor$ as $P+Q\equiv{\large{\sum}}_{x:{\bf 2}}\dots$ where where the dots represent a suitable $if$-construction. Negation $\neg P$ is read as $P$ leading to absurum, i.e. $P\to{\bf 0}$. And lastly | + | If we tag the terms of a type $P$ resp. $Q$ with the value of Bool, we can identify disjunction $\lor$ as $P+Q\equiv{\large{\sum}}_{x:{\bf 2}}\dots$ where the dots represent a suitable $if$-construction. Negation $\neg P$ is read as $P$ leading to absurum, i.e. $P\to{\bf 0}$. And lastly |
| | **syntax** ^ computation ^ logic ^ geometry ^ | | **syntax** ^ computation ^ logic ^ geometry ^ | ||
| Line 98: | Line 98: | ||
| {{ thed.jpg?X400}} | {{ thed.jpg?X400}} | ||
| - | We can inductively define the circle $\mathbb S$ as type by postulating | + | We can inductively define the circle $\mathbb S$ as type by postulating |
| $base:\mathbb S$ | $base:\mathbb S$ | ||
| - | |||
| and | and | ||
| - | |||
| $loop:base=_{\mathbb S}base$. | $loop:base=_{\mathbb S}base$. | ||
| - | |||
| Now | Now | ||
| - | |||
| $\dots,loop^{-2},loop^{-1},refl_{base},loop,loop^2,loop^3,\dots$ | $\dots,loop^{-2},loop^{-1},refl_{base},loop,loop^2,loop^3,\dots$ | ||
| - | |||
| are all terms of $base=_{\mathbb S}base$. | are all terms of $base=_{\mathbb S}base$. | ||
| This type can be shown to be equivalent (in the formal sense discussed below) to the integers. Indeed, recall that the first homotopy group of the circle is isomorphic to $\mathbb Z$. | This type can be shown to be equivalent (in the formal sense discussed below) to the integers. Indeed, recall that the first homotopy group of the circle is isomorphic to $\mathbb Z$. | ||
| Line 128: | Line 122: | ||
| $isSet(A):={\large{\prod}}_{x:A}{\large{\prod}}_{y:A}\,isProp(x=y)$ | $isSet(A):={\large{\prod}}_{x:A}{\large{\prod}}_{y:A}\,isProp(x=y)$ | ||
| - | The above says that $x$ connects to $y$ via at most one invertible path and hence this characterizes as set as a discrete category. Since sense, characterized like here as types with lack of other structure, are generally different from sets characterized in a theory like ZFC. | + | The above says that $x$ connects to $y$ via at most one invertible path and hence this characterizes as set as a discrete category. Since sets, characterized like here as types with lack of other structure, are generally different from sets characterized in a theory like ZFC. |
| == Homotopy theory == | == Homotopy theory == | ||
