fancy inductive types and mathematics

Stream: maths

[Kevin Buzzard]

When I was working on the perfectoid project I exchanged some comments with @Sebastian Ullrich and I said something like "I'm not sure we use any inductive types in our repo" and he replied "you use nat!" and my first thought was "I'm not sure we do...". We do use nat and int a few times, but the data below seems to indicate that mostly we are making lots of new structures and classes, and proving relations between these classes.

link to gist

span ℤ should be a thing :-) I guess this is why I was never excited by all these inductive-recursive questions -- I don't think we see those kinds of things in maths.