Curious if anyone in type theory land knows where ‘enumerations’ (ie. finite sets) of labels were first talked about with respect to Martin-Löf Type Theory - see Chapter 6 of “Programming in Martin-Löf’s Type Theory”. cse.chalmers.se/research/group
Conversation
I've seen them before in “ΠΣ: Dependent Types without the Sugar” - but the paper didn't seem to reference where it the idea came from: cs.nott.ac.uk/~psztxa/publ/p
1
1
I'm curious about possibly using these enumerations to implement a 'core' representation of disjoint unions, and this is more to satisfy my curiosity. I'd also like to be able to point others to the source too!
Replying to
Found an earlier version, using a less enum-like (and more number-like) syntax! github.com/michaelt/marti On page 35 Martin-Löf introduces finite sets and shows that ℕ₀ is equivalent to ⊥. And on page 37 he talks about how ℕ₂ is equivalent to the booleans.
1
2
Thanks to for reminding me (on Freenode's ##dependent) about github.com/michaelt/marti. It's a great resource!
4