New answers tagged lambda-calculus
1
In a plain type theory with just dependent functions and a universe, you can define:
$$
\textbf 0 \equiv (A: \textrm{Type}) \rightarrow (B: \textrm{Type}) \rightarrow A \rightarrow B
$$
Then you get a map:
$$
\textrm{0m} : (X: \textrm{Type}) \rightarrow \textbf 0 \rightarrow X
$$
$$
\textrm{0m}\,\, X\,\, z\, \equiv z\,\, \textbf 0\,\, X\,\, z
$$
Note: This ...
Top 50 recent answers are included