Is implication(function) more fundamental than lets say conjunction(product) in type theory?

Question

According to the answer at (How to define function type in AGDA) the function type is kind of a fundamental thing in Agda and needed for bootstrapping, hence end user can not define it like what they do for conjunction(product) type and has to be predefined at the language level. Does this mean that implication(function) type is more fundamental than types like product(conjunction) since function is used in defining those types?

Answer 1

For Agda, I think, as stated in the other question, that the fact that function types (or rather Π-types) are built-in while pairs (or even Σ-types) aren't so much is a reasonable argument that they are more fundamental in Agda. That said, even there it's not completely clear cut. For example, Σ-types/pairs are introduced in Agda via inductive data type declarations which are largely unrelated to Π-types. On the other hand, you could Church-encode pairs in terms of Π-types but to actually push this all the way through you'd need universes (which Agda does have) so it's not Π-types alone that do it.

I find comparing "how fundamental" things are very ambiguous and usually not useful. Something being "more fundamental" means it's "closer" to some foundations (fundament). In the context of a specific foundational system, e.g. Agda, that can be reasonably clear, but in general things that are fundamental in one foundation may be derived in another. More generically, "fundamental" has connotations that can easily pull in opposite directions. On the one hand, if I can derive $X$ from $Y$ but not vice versa, it would seem $Y$ is "more fundamental" in some sense. On the other hand, "fundamental" has connotations of simplicity, minimality, and a kind of unavoidability. If given all of $X$, $Y$, and $Z$ I can derive $W$, but given just $W$ I could derive each of $X$, $Y$, and $Z$, is $W$ more fundamental or less fundamental than $X$? Maybe $W$ is just a complex composite of $X$, $Y$, and $Z$. Because $X$ is derivable from $W$, that means $X$ is a more omnipresent concept; $X$ can exist even if $W$ does not but not vice versa.

At any rate, let's move to some more technical goodness that talks about how pairs and functions relate without trying to rank them. Unsurprisingly, category theory provides a good vantage point for gaining insight on these types of questions, though it is important to compare what the category theory suggests to what the type theorists actually do because these don't always line up. It can be quite interesting on both sides to see what is needed to make them line up.

Arguably the simplest example is cartesian closed categories. A cartesian category is one that has finite products, this means (the existence of terminal objects and) $\text{Hom}(A,B)\times\text{Hom}(A,C)\cong\text{Hom}(A,B\times C)$ (natural in $A$, $B$, and $C$). This is a characterization of binary products. A cartesian closed category additionally has $\text{Hom}(A\times B,C)\cong\text{Hom}(A,C^B)$ characterizing exponents in terms of products. This is to say a (parameterized) adjunction $-\times B\dashv (-)^B$. Hagino's Categorical Programming Language (CPL) described in his thesis allows declaring the function type constructor just this way (see sections 3.3.2 and 3.3.3). The type theoretic view of this is the simply typed lambda calculus (STLC) with products. But the STLC is usually not presented with products, or at the very least they are optional. So how are function types described in STLC without products? Usually by the following two rules (or some variation on them):$$\cfrac{\Gamma, x\!:\!A\vdash M:B}{\Gamma\vdash(\lambda x\!:\!A.M) : A\to B}\to\!\!I\qquad\cfrac{\Gamma\vdash M : A\to B\qquad \Gamma\vdash N:A}{\Gamma\vdash (M\,N) : B}\to\!\!E$$ This characterizes function types without any reference to product types. This is typical in modern type theory; type constructions are characterized without referencing other type constructions so that you can build type theories a la carte. In tihs sense, product types and function types are somewhat orthogonal.

Why does the categorical approach need products? Roughly speaking, an arrow $t\in\text{Hom}(A,B)$ corresponds to a term $x\!:\!A\vdash t:B$. So the issue is simply that we need some way of talking about arrows with more than one input. Products are one way, but an alternative, more direct approach would be to use (cartesian) multicategories. However, a more common approach is to split the adjunction characterizing function types in terms of product types into two adjunctions. Instead of having $-\times B\dashv (-)^B$ as described earlier, we can split this into $\Sigma_B\dashv p^*\dashv \Pi_B$ where $p : [\Gamma,B]\to [\Gamma]$ and $p^* : \mathcal{E}_\Gamma\to\mathcal{E}_{\Gamma,B}$. Here $\mathcal{E}_\Gamma$ can be thought of as a category of terms in context $\Gamma$. The machinery to do this is indexed or mostly equivalently fibered categories. $p^*$ is called a weakening functor and it corresponds to adding an unused variable (of type $B$) to the context. Now we can consider indexed-/fibered-categories where only one or the other (or neither or both) of those adjunctions hold. A simpler but less general approach to this is to use polycategories as Hasegawa does in Decomposing typed lambda calculus into a couple of categorical programming languages. A polycategory, $\mathcal{C}[x:B]$, is a category, $\mathcal{C}$, that has a terminal object and to which an arrow $x : 1 \to B$ is freely added. We of course have an inclusion of $\mathcal{C}$ into $\mathcal{C}[x:B]$, and this inclusion takes the place of $p^*$. When this perspective is related back to type theory, we end up splitting the lambda calculus into the kappa calculus and the zeta calculus. The kappa calculus captures a first-order notion of multi-parameter functions. The zeta calculus captures the higher-order aspect of the lambda calculus, but the result is quite strange and awkward. Either way, these approaches place product types and function types on somewhat even ground.