# Indiscernability of identicals (HoTT)

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.

• Is “HoTT” a textbook? Commented May 7, 2022 at 23:36
• @TymaGaidash Yes, that's the standard abbreviation for it (and it's clear from the tag). Commented May 7, 2022 at 23:43
• It’s the standard text for the topic that is tagged: Homotopy Type Theory. Commented May 7, 2022 at 23:44
• "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". Commented May 11, 2022 at 0:59
• Thanks for the clarifications Commented May 11, 2022 at 0:59

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.