sync

_apl.md

@@ -59,6 +59,12 @@ character (set).
 
 We write $\BB = \{\f,\t\}$ where $\f$ represents false and $\t$ represents true.
 
+$(A\times B)\to C\cong A\to (B\to C)$ by $f(a,b) = c \leftrightarrow f,(a)b = c$ or $f,(a)b = f(a,b)$.
+
+$A\to (B\to C) \cong (A\times B)\to C$ by $g(a)b = c \leftrightarrow g`(a,b) = c$ or $g`(a,b) = g(a)b$.
+
+$\pi(a,b) = (a,b)$, $\pi_0(a,b) = a$, $\pi_1(a,b) = b$.
+
 ## Type
 
 If $X$, $X_i$ are types

vs.md

@@ -23,6 +23,8 @@ isomorphism between them.
 
 A vector space over the real numbers $\RR$ is a set having a scalar multiplication
 and a commutative vector addition satisfying a distributive law.
+A vector space homomorphism is a _linear transformation_. Two vector spaces are
+equivalent if and only if they have the same _dimension_.
 
 The set of all functions from a set $I$ to the real numbers, $\RR^I = \{x\colon I\to\RR\}$
 is a vector space over $\RR$.