This is quite interesting, thank you! How can I see that the disjunctions are not definable through implications within the intuitionistic logic? In the classical propositional logic, they are: $A \vee B = (B\to A)\to A$.

@PeterLeFanuLumsdaine The question is, why cannot we have a consistent implementation of the product type? I am ready to define everything monomorphically if needed. With the sum type, there is no problem as long as we specialize choice to a fixed result type. We will then have to write separate definitions of choice for different types. I am going to update the post to include OCaml code for this. But nothing works at all with the product type. My two questions still stand.

@QiaochuYuan Indeed I am trying to avoid introducing the product type by fiat. Perhaps we do not need to have full categorical semantics with products, in order to be able to write down the $\lambda$-calculus typing rules and perform computations... Also there are some papers explaining that you can define exponentials without necessarily having products.