Kevin Buzzard (Jul 21 2019 at 23:52):
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.
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.
Last updated: May 09 2021 at 10:11 UTC