As a shapeless enthusiast I agree with you that the Peano examples (which seem to be the go-to for any dependent types demo; not just for Scala... they must think it's helpful!) is terrible for people who don't already get dependent typing and logic programming. Which are the people you're supposed to be reaching with a demo.

I have a talk to intro typelevel proofs in Scala (with shapeless as the example target), that uses the kind of geometric proofs we all did in high school as an analogy. I think that's more of an accessible metaphor, but it also seems like precisely what Odersky is trying to eliminate in Dotty - the use of inductive implicit derivation to form "proofs" of invariants that are also implementations. Admittedly, it's an approach that seems rather difficult for a lot of engineers to grasp, which means it's of questionable utility. But it always seemed really elegant to me - type systems are about proving invariants, and Scala's just gives you powerful ways to prove things by unifying that concept into implicits.