molikto’s weblog

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?