Left Inclusion is Not Equal to Right Inclusion I am reading through a type theory book and gave myself the following problem:  Let $A$ be a type.  Then we have the coproduct type $A+A$.  I want to show that left inclusion $l(a)$ is not equal to right inclusion $r(a)$ for all $a:A$.  In other words, I must find a function
$$
\prod_{x:A}(l(x)=r(x))\rightarrow 0
$$
where $0$ is the empty type.  
I have tried doing this using the induction principal for the equality type.  So, fix $a:A$.  I want to start with a function
$$
C:\prod_{x:A+A}(l(a)=x)\rightarrow \mathcal{U}
$$
and an element
$$
c:C\left(l(a),\operatorname{refl}_{l(a)}\right).
$$
I am having difficulty finding an appropriate $C$.
 A: The proposition you wish to prove is false: the two inclusions for $0 + 0$ are equal. So there can be no term of following type:
$$\left( \prod_{a : A} \mathsf{inl}(a) =_{A + A} \mathsf{inr}(a) \right) \to 0$$
However, there is a term of following type:
$$\prod_{a : A} (\mathsf{inl}(a) =_{A + A} \mathsf{inr}(a) \to 0)$$
Indeed, let $a$ be a variable of type $A$. By induction on coproducts, there is a dependent type $x : A + A \vdash C (x) \; \mathsf{type}$ defined by $C (\mathsf{inl}(a)) \equiv 1$ and $C (\mathsf{inr}(a)) \equiv 0$. By induction on equality, we get a dependent term $x : A + A, p : \mathsf{inl}(a) =_{A + A} x \vdash c (x, p) : C (x)$, defined by $c(\mathsf{inl}(a), \mathsf{refl}) \equiv {*}$, where $*$ is the canonical term of type $1$. Thus, $\lambda p . c (\mathsf{inr}(a), p)$ is a term of type $\mathsf{inl}(a) =_{1 + 1} \mathsf{inr}(a) \to 0$. Generalising over $a$ yields the required term. 
On the other hand, suppose we have any term of type $A$, say $a_0$. Then we can obtain
$$\left( \prod_{a : A} \mathsf{inl}(a) =_{A + A} \mathsf{inr}(a) \right) \to 0$$
by evaluating the input at $a_0$ and substituting it into the above proof.
