Dependent Function Spaces

If we allow B to be a family in the type $A \rightarrow B$, we get a new type, denoted by fun(A;x.B), or $x:A \rightarrow B$, which generalizes the type $A \rightarrow B$. The rules are:

$$\frac{{\sf E}, y:A \vdash b[y/x] \in B[y/x]} {{\sf E} \vdash (x\mapsto b) \in fun(A;x.B)} newy$$

$$\frac{{\sf E} \vdash f \in fun(A;x.B) {\sf E} \vdash a \in A} {{\sf E} \vdash f(a) \in B[a/x]}$$

Example   Back to our example Dates. We see that $m: {\sf Month} \rightarrow {\sf Day}[m]$ is just $fun({\sf Month};m.{\sf Day})$, where Day is a family of twelve types. And $\lambda (x.maxday[x])$ is a term in it.