Elimination of products
Closed this issue · 1 comments
In paragraph Foundations / Type theory / product types, it is stated that the elimination of products is currying: a function f : prod A B -> C is defined by a function g : A -> B -> C.
This is strange from a practical viewpoint: currying is just a syntactic trick, it eliminates nothing, functions f and g are the same.
This is also strange from the viewpoint of the theory of categories, which defines products as objects equipped with projection morphisms. These projections seem the natural elimination of products, functions that go out from them.
This is finally strange from the viewpoint of type theory, which previous paragraph is titled "dependent function types (pi-types)". Pi-type already means product type: a product type is a type of dependent functions, its elimination is simply the application of functions (equivalent to the projection morphisms above).
Currying shows if we define the binary product as an inductive type:
Inductive prod (A B : Type) : Type :=
pair : A -> B -> prod A B
This hides the 2-element index type and makes Coq produce currying in prod_rect. But is this a reason to claim that currying is the elimination of products? It does not even compile for infinite products, as currying would need an infinity of arguments. Here is another Coq definition of binary products as pi-types,
Definition prod_func (A B : Type) : Type
:= forall b : bool, if b then A else B.
EDIT
On the other hand, without function extensionality, the product morphisms of prod_func are not necessarily unique. So prod_func is not the categorical product. And neither is prod, for the same reason.
Well, there's no sense in which a function and its uncurried version are literally the same. Certainly they carry the same information, but we express that by saying that currying is an isomorphism (or, in HoTT, an equivalence).
It's true that binary products in type theory have two presentations: a positive one and a negative one. The two are explained and compared at https://ncatlab.org/nlab/show/product+type#definition. The HoTT Book chose the positive presentation, I think because all the other type constructors except for function types are positive, but many implementations of type theory use the negative one (in particular, the judgmental eta rule for products, aka "surjective pairing", is more natural from the negative point of view).
Semantically, the negative product is defined by being the categorical product, while the positive product is defined as a "representing tensor product in a cartesian multicategory". However, it is provable that each has the universal property of the other, so in that sense it doesn't really matter. There may be reasons to prefer one choice over the other, but the choice made by the book is a perfectly correct one. E.g. it's true that positive products only make sense in the binary/finite case, but they also fit into a more general scheme of inductive types which negative products don't. (Your prod_func, by the way, appears in exercise 1.6.)