Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | Next revision Both sides next revision | ||
|
babbys_first_hott [2015/02/06 13:57] nikolaj |
babbys_first_hott [2015/02/06 13:58] 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 ^ | ||
