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
Replying to
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!
1
1
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