Eliminators are undoubtedly the most difficult aspect of type theory. In this article we will try to make more clear how they work, but most importantly why we need them. This article will present some analogies between eliminators and constructs of programming languages (such Python, Rust, Scala, …) which can help who knows some basic of computer programming understanding eliminators.

Web version: https://dpdmancul.gitlab.io/blog/2023/01/eliminators