Tag Archives: Tim Gowers
Two types of universe for two types of mathematician
Thank you Johan for pointing out to me that the mathlib stats page had got really good! But one thing that made me laugh is that somehow on their stats for commits I see I have done just enough to … Continue reading
The invisible map
Is a subgroup of a group a group? Is 3 a topology on 2? Is a natural number a real number? Decisions like this have consequences. Continue reading
Posted in Type theory, undergrad maths
Tagged Andrej Bauer, function, Tim Gowers, Type theory
7 Comments
Xena 