All Questions
3
questions
0
votes
1
answer
130
views
increasing the universe level of a type in Lean by force
Given some term
A : Sort u
in Lean, is there a way to artificially increase the universe level and promote A to a term
...
- 722
7
votes
1
answer
378
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
240
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