2
$\begingroup$

I am working through HoTT and it was suggested (on page 43) that the reader prove the following proposition, if not(A or B) then (not A) and (not B) by exhibiting an element of the type $(A+B \to 0) \to (A\to 0) \times (B \to 0)$. Introduce the variable (or hypothesis) $g: A+B \to 0$. We need to form an expression $f(g) :\equiv \box : (A \to 0) \times (B \to 0)$. (I do not know the command for the box used in HoTT which is the expression we are trying to fill.) No with a function $g:A+B \to 0$ we implicitly have $g_0 : A \to B$ and $g_1 : B \to 0$ such that $g(inl(a)) \equiv g_0(a)$ and $g(inr(b)) \equiv g_1(b)$. So, we clearly can define $f(g) :\equiv (g_0,g_1)$.

How do I define $f$ explicitly? It feels wrong saying $f :\equiv \lambda g. (g_0,g_1)$. I assume I should use the recursor as was suggested in the converse direction which the preceeding paragraph works through.

$\endgroup$
0

1 Answer 1

2
$\begingroup$

Note that, if $g$ is of type $A+B\to 0$, then $\lambda a.g(\mathrm{inl}(a))$ is of type $A\to 0$ and $\lambda b.g(\mathrm{inr}(b))$ is of type $B\to 0$. (These are what you refer to as $g_0$ and $g_1$ in your post.) So the term $$\lambda g.(\lambda a.g(\mathrm{inl}(a)),\lambda b.g(\mathrm{inr}(b)))$$ is of type $(A+B\to 0)\to\left[(A\to 0)\times(B\to 0)\right]$.

$\endgroup$
5
  • $\begingroup$ Obviously! Thank you!!! $\endgroup$
    – ToucanIan
    Commented May 7, 2022 at 1:14
  • 1
    $\begingroup$ @ToucanIan my pleasure, happy it helped! :) $\endgroup$ Commented May 7, 2022 at 1:14
  • 1
    $\begingroup$ @ToucanIan if you are satisfied with the answer you can "accept" it by ticking the checkmark next to it, which will mark the question as answered and get it off the unanswered queue :) $\endgroup$ Commented May 7, 2022 at 1:15
  • $\begingroup$ Sorry. When I got that answer I went back to working and forgot! Thanks again. $\endgroup$
    – ToucanIan
    Commented May 7, 2022 at 7:04
  • $\begingroup$ @ToucanIan no problem, again am happy it helped! :) $\endgroup$ Commented May 7, 2022 at 9:56

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .