3 ms·

I hope they implement this in Agda as well.

• guerrilla 6y ago
  Actually I wonder if its not already possible to implement it since it has had levels of universes for quite a while. Is that, with dependent types, not powerful enough?
  • gnulinux 6y ago
    I remember asking this question on agda subreddit a while ago (maybe 3 years ago? I don't know) and they told me it's not possible. However, they implemented Cubical type theory and a few other stuff (universe levels? Has it been implemented last couple years?) so maybe it's possible now.m I love doing algebra proofs with agda as a hobby but I'm by no means, even remotely, experienced in everything agda capable of.