Understanding eliminators
Skip to main
You are using an outdated browser. Please upgrade your browser to improve your experience.
Published January 16, 2023
| Version v1
Publication
Open
Understanding eliminators
Authors/Creators
Peressoni, Davide
Description
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 articles 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. Agda will be used to implement all eliminators, since it is a language (and proof assistant) built on top of Martin-Löf’s type theory. Don’t worry if you don’t know how to develop: the only prerequisite is to know how to define a math function by cases, which all of us studied at school.
Files
eliminators.pdf
Files<br>(122.1 kB)
Name<br>Size
Download all
eliminators.pdf
md5:9d35a9998a7f2d6eb3c73c66555efc8a
122.1 kB
Preview
Download
Additional details
Identifiers
URL
https://dpdmancul.gitlab.io/blog/2023/01/eliminators/
Dates
Available
2023-01-16
Views
Downloads
Show more details
All versions<br>This version
Views
Total views
Downloads
Total downloads
Data volume
Total data volume
0 Bytes<br>0 Bytes
More info on how stats are collected....
Versions
External resources
Indexed in
OpenAIRE
Communities
Keywords and subjects
Keywords
type theory
math
agda
MeSH
Programming Languages
Details
DOI
DOI Badge
DOI
10.5281/zenodo.20600315
Markdown
[](https://doi.org/10.5281/zenodo.20600315)
reStructuredText
.. image:: https://zenodo.org/badge/DOI/10.5281/zenodo.20600315.svg<br>:target: https://doi.org/10.5281/zenodo.20600315
HTML
Image URL
https://zenodo.org/badge/DOI/10.5281/zenodo.20600315.svg
Target URL
https://doi.org/10.5281/zenodo.20600315
Resource type<br>Publication
Publisher<br>Davide Peressoni
Languages
English
Rights
License
Creative Commons Attribution Share Alike 4.0 International
Permits almost any use subject to providing credit and license notice. Frequently used for media assets and educational materials. The most common license for Open Access scientific publications. Not recommended for software.
Read more
Citation
Export
Technical metadata
Created
June 8, 2026
Modified
June 8, 2026
Jump up
This site uses cookies. Find out more on how we use cookies
Accept all cookies<br>Accept only essential cookies