All Questions
2
questions
7
votes
1
answer
386
views
Cardinality of Type in a given universe
I'm trying to determine the cardinality of Type u in Lean 3. So far I've been able to prove two inequalities:
...
- 173
11
votes
1
answer
241
views
Explicit vs implicit universes in lean
I've seen in mathlib several cases where the universes are explicit, that is Type u instead of Type*. Is there any advantage in ...
- 213