1
$\begingroup$

In 1.12 of the HoTT book it is mentioned that it is a simple exercise to show that indiscernability of identicals follows from path induction. I am getting the sense that it is a special case but I am struggling to explicitly write down what is necessary to see this. I’m open to someone just giving me the answer, but in fact — if someone had the patience — I would prefer a hint.

$\endgroup$
5
  • 2
    $\begingroup$ Is “HoTT” a textbook? $\endgroup$ Commented May 7, 2022 at 23:36
  • 2
    $\begingroup$ @TymaGaidash Yes, that's the standard abbreviation for it (and it's clear from the tag). $\endgroup$ Commented May 7, 2022 at 23:43
  • 1
    $\begingroup$ It’s the standard text for the topic that is tagged: Homotopy Type Theory. $\endgroup$
    – ToucanIan
    Commented May 7, 2022 at 23:44
  • 1
    $\begingroup$ "HoTT" (i.e. "homotopy type theory") is usually used to refer to the whole subject. The book in question is generally referred to as "the homotopy type theory book" or "the HoTT Book". $\endgroup$ Commented May 11, 2022 at 0:59
  • 1
    $\begingroup$ Thanks for the clarifications $\endgroup$ Commented May 11, 2022 at 0:59

1 Answer 1

0
$\begingroup$

I have a proposed solution to the excercise.

Let $D: A \to \mathcal{U}$ and define $C(x,y,p) :\equiv D(x) \to D(y)$. Clearly we can define a $c: \Pi_{x:A} C(x,x,refl_x) \equiv \Pi_{x:A} D(x) \to D(x)$, namely $c: \equiv \lambda x. id_{D(x)}$. So, by path induction there is a function $f: \Pi_{x,y:A} \Pi_{p:x =_A y} C(x,y,p) \equiv \Pi_{x,y:A} \Pi_{p:x =_A y} D(x) \to D(y)$ such that $f(x,x,refl_x) :\equiv c(x) \equiv id_{D(x)}$. This is exactly the statement of indiscernability of identiticals given earlier in the section.

Note: Stringing the judgemental equalities together may be a little sloppy. I was just trying to be explicit on when I was using path induction and how the result is judgementally equal to the statement of indiscernability of identicals.

$\endgroup$

You must log in to answer this question.

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