This is an automated archive made by the Lemmit Bot.

The original was posted on /r/programminglanguages by /u/kalyani-tt on 2023-10-23 21:48:59.

I’ve written up a blogpost about the difficulties of equality and typechecking with dependent types. It’s aimed at people who have used dependently typed languages, but are still beginners.

Link:

Let me know what you think should be improved!