Reducing products in HoTT to church/scott encodings

Question

So I am currently going though the HoTT book with some people. I made the claim that most inductive types we will see can be reduced to types containing only dependent function types and universes by taking the type of the recuror as inspiration for the equivalent type. I started to sketch how I thought this would work and after some stumbling I came to what I thought was an answer.

$$\cdot \times \cdot \equiv \prod_{A, B, C : \mathcal{U}} (A \to B \to C) \to C$$ $$ (\cdot, \cdot) \equiv \lambda a : A. \lambda b : B. \lambda C : \mathcal{U}. \lambda g : A \to B \to C. g(a)(b)$$ $$ ind_{A \times B} \equiv \lambda C. \lambda g. \lambda p. g(pr_1(p))(pr_2(p)) $$

This gives the correct defining equations (defining equations for $pr_1$ and $pr_2$ omitted) but this would mean that $ind_{A \times B}$ would have the wrong type.

$$\text{ind}_{A \times B} : \prod_{C : A \times B \to \mathcal{U}} (\prod_{a:A} \prod_{b:B} C((a, b))) \to \prod_{p : A \times B} C((pr_1(p), pr_2(p)))$$

And there doesn't seem to be a simple fix to this. I also thought about the following definition.

$$ ind_{A \times B} \equiv \lambda C. \lambda g. \lambda p. p(C(p))(g) $$

But this just doesn't typecheck.

Another idea I had is to use $uniq_{A \times B}$ to convert $C((pr_1(p), pr_2(p)))$ to $C(p)$ but it's not clear how to make that work. First off I'd have to show how to reduce identity types dependent function types which is proving even harder in my scribblings than products. Additionally $uniq_{A \times B}$ doesn't seem to be definable without the proper form of induction so even if I allowed myself identity types as presented in the book I'd be no closer to having a definition of $uniq_{A \times B}$

So it seems like we can define the recursor here but not the inductor. We can define something that's pretty close to looking like the inductor but doesn't quite make it. The recursion lets us perform logic taking this type to be the meaning of logical conjunction but it doesn't let us prove things about products which seems lacking.

Can we make the sort of reduction I claimed can be made? That is, can we define a type using only dependent function types and universes that has a pairing function and inductor with the same defining equations and types as products? It's my growing suspicion that I made a false claim. It seems like we're able to get so frustratingly close but just not quite make it. If we can't define it what kind of argument explains why we can't? Do products as presented in the HoTT book increase the strength of the system?

Answer 1

The standard reference I often give is Induction is not derivable in second order dependent type theory by Herman Geuvers, which says that there is no type

$$N : \mathrm{Type}$$

with functions $$Z:N\qquad S:N\rightarrow N $$

such that

$$\mathrm{ind}:\Pi P:N\rightarrow \mathrm{Type}.P\ Z\rightarrow (\Pi m:N.P\ m\rightarrow P\ (S\ m))\rightarrow \Pi n:N. P\ n $$

is provable. This suggests that indeed, such an encoding cannot work for pairs as you describe.

The system this is proven for is a subset of the Calculus of Constructions, which contains powerful product types and a universe. I suspect this result can be extended to the system you are interested in, depending on what you have.

Sadly, I don't know the complete answer to your question. I suspect that adding certain parametricity principles "internally" is exactly what is required to make these encodings work with the full induction principle. Neel Krishnaswami, whose knowledge is a strict superset of my own, wrote a paper along these lines with Derek Dreyer:

Internalizing Relational Parametricity in the Extensional Calculus of Constructions

Also of interest is the following paper by Bernardy, Jansson and Patterson (Bernardy has thought deeply about these topics):

Parametricity and Dependent Types

Obviously parametricity has a strong relationship with HoTT in general, but I don't know what the details are. I think Steve Awodey has considered these questions, since the encoding trick is useful in contexts where we don't really know what the eliminators should look like.

Answer 2

To get your idea working you need something extra, as was pointed out in @cody's answer. Sam Speight worked under the supervision of Steve Awodey to see what can be achieved in HoTT using an impredicative universe, see Impredicative Encodings of Inductive Types in HoTT blog post.