At the moment I'm about to get my head around homotopy type theory as a new perspective into mathematics. Insofar, I'm trying to mess around with it, prove some simple things and see where it gets; but I'm stuck, again.
The questions
My problem can be boiled down to a simple example. Consider a relatively simple inductive type family
$$\mathsf{T} : \mathbf{2}\to \mathbf{2}\to \mathcal{U}$$
defined by two constructors
- $A_1 : \mathsf{T}(0_{\mathbf{2}},0_{\mathbf{2}})$
- $A_2 : \Pi_{b : \mathbf{2}} \mathsf{T}(1_{\mathbf{2}},b)$
where I'm using the notation from the HoTT Book, i.e. $\mathbf{2}$ is a boolean, $\mathcal{U}$ is some universe, etc.
Now,
- is there a function $f : \Pi_{b:\mathbf{2}} \mathsf{T}(0_{\mathbf{2}},b)\to b = 0_{\mathbf{2}}$?
- How is it defined?
- How is this definition justified (e.g. how would it be defined using the induction principle of $\mathsf{T}$, or such)?
Ideas
From a meta perspective, one might argue: any term $t$ with type $\mathsf{T}(0_{\mathbf{2}},b)$ must be $A_1$, i.e. $t \equiv A_1$. But then, $b \equiv 0_{\mathbf{2}}$, since $A_1 : \mathsf{T}(0_{\mathbf{2}},0_{\mathbf{2}})$.
So, how defining this more formally. My first thought was, use induction over $\mathsf{T}$ (resp. pattern matching), but this won't work, since its not defined for every $t : \mathsf{T}$. Clearly
$$f(b, A_1) :\equiv \textsf{refl}_{0_{\mathbf{2}}}$$
But what about $f(b, A_2)$?
Is there a way to use this idea within the theory?
Disclaimer
While this question might have an answer and explanation in a broader context then homotopy type theory, in the end I probably need some answer especially in HoTT, mainly because I'm not fluent in (intensional) type theory nor do I have sufficient skill to translate general ideas around pattern matching, type theory, etc. into HoTT (yet). But I'm thankful for any advice/hint. : )
Best Answer
This seemingly simple question is actually fairly deep, and leads quite directly to the "encode-decode method" used in HoTT to give synthetic proofs of classical theorems of algebraic topology. The key is to generalize the type of $f$. As you note, "$f(b,A_2)$" doesn't even make sense because $A_2$ doesn't have the correct type to be the second argument of $f$; but we need something analogous to "$f(b,A_2)$" in order to define $f$ by induction on $\mathsf{T}$.
Thus, instead of $f:\Pi_{b:\mathbf{2}} \mathsf{T}(0_{\mathbf{2}},b) \to (b=0_{\mathbf{2}})$, we will define $g:\Pi_{a:\mathbf{2}} \Pi_{b:\mathbf{2}} \mathsf{T}(a,b) \to P(a,b)$, where $P:\mathbf{2}\to \mathbf{2}\to \mathcal{U}$ is some type family such that $P(0_{\mathbf{2}},b) \equiv (b=0_{\mathbf{2}})$. Since the type of $g$ is more general, we will be able to use the induction principle for it; then we can define $f(b,t) = g(0_{\mathbf{2}},b,t)$.
How do we obtain $P$? By a recursion principle. In this case, that means case analysis on the first argument $a:\mathbf{2}$ of $P$. Our desired equality $P(0_{\mathbf{2}},b) \equiv (b=0_{\mathbf{2}})$ is the first case, and since we don't care about the other case we take it to be trivial to inhabit:
$$\begin{align*} P(0_{\mathbf{2}},b) &:\equiv (b=0_{\mathbf{2}})\\ P(1_{\mathbf{2}},b) &:\equiv \mathbf{1} \end{align*}$$
Now we can define $g$ by the induction principle of $\mathsf{T}$, with two cases corresponding to the two constructors of $\mathsf{T}$:
$$\begin{align*} g(0_{\mathbf{2}},0_{\mathbf{2}},A_1) &:\equiv \mathsf{refl}_{0_{\mathbf{2}}}\\ g(1_{\mathbf{2}},b,A_2) &:\equiv \star \end{align*}$$
Note that $g(a,b,t) : P(a,b)$ in both cases. Now, as noted above, we can define your $f:\Pi_{b:\mathbf{2}} \mathsf{T}(0_{\mathbf{2}},b) \to (b=0_{\mathbf{2}})$ by $f(b,t) = g(0_{\mathbf{2}},b,t)$.
This sort of trick, of defining a desired function by generalizing the domain and finding the codomain as a particular value of a recursively defined type family, is a fundamental way of characterizing inductively defined type families over inductive types, including particularly the identity type (in which case in HoTT it often goes by the name of the "encode-decode method"). It's introduced in sections 2.12 and 2.13 of the HoTT book for characterizing the identity types of coproducts and the natural numbers (in fact you need it even to prove that $0_{\mathbf{2}}\neq 1_{\mathbf{2}}$!), and then again in chapters 6 and 8 to study higher inductive types and compute homotopy groups of spheres.