# Tag Info

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 ...