molikto’s weblog
2021-01-18
Notes on dependent type theory
Q: Is
universe lifting a la McBride
good enough?
one problem is small category, locally small category, and large category cannot be expressed properly
or can we get universe polymorphism AND cumulativity? Arend seems do this…
Q: how does Arend do
packed/unpacked structures
? it seems good.
searching Lean archive, found
some
discussion about difference between Arend and Lean
reread the paper
Towards a practical programming language based on dependent type theory
for how to do more complex meta variables
Q
: it seems Lean’s typeclass will bind a symbol to a single type class?
so it has have different theory for additive group and multiplicative groups
?