[[!redirects Sandbox > history]] [[!redirects Sandbox]] < [[nlab:Sandbox]] \section{Multivalued partial functions, or correspondences} Correspondence types are more important than actual function types. $$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type}}{\Gamma \vdash \mathrm{Corr}(A, B) \; \mathrm{type}}$$ $$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type}}{\Gamma, f:\mathrm{Corr}(A, B), x:A, y:B \vdash R(f, a, b) \; \mathrm{type}}$$ maybe it's like partial functions but without the requirement that the type family $P(x)$ be a proposition. Correspondences are [[type families]] $x\colon A, y \colon B \vdash R(x, y) \; \mathrm{type}$. From every correspondence, one could derive the [[multivalued partial function]] $$x:A, p:\sum_{y:B} R(x, y) \vdash f(x, p):B$$ and for every type family $x:A \vdash P(x)$ and every multivalued partial function $x:A, p:P(x), \vdash f(x, p):B$, one could define the correspondence $x:A, y:B \vdash R(x, y) \; \mathrm{type}$ as $$R(x, y) \coloneqq \sum_{p:P(x)} f(x, p) =_B y$$ category: redirected to nlab