New answers tagged

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