Post 1550096 by dek@niu.moe
 (DIR) More posts by dek@niu.moe
 (DIR) Post #1550095 by abs@niu.moe
       2018-11-28T06:57:01Z
       
       0 likes, 0 repeats
       
       Kinda sad about yesterday's talk about Martin Löf Type Theory. There were so many things that could've been explained better. I'm worried many students that that don't have experience with the TT haven't really seen what's different/special about it.
       
 (DIR) Post #1550096 by dek@niu.moe
       2018-11-28T08:06:33Z
       
       0 likes, 0 repeats
       
       @abs nothing! :D
       
 (DIR) Post #1550737 by abs@niu.moe
       2018-11-28T09:22:09Z
       
       0 likes, 0 repeats
       
       @dek Well, you have an explicit equality judgement, which can get very exiting, which you don't have in CIC, for example.