/ Notes / Types Types Leonid Dubinsky Agda Introduction to Univalent Foundations of Mathematics with Agda Programming Language Foundations in Agda Agda mode for VSCode invitation to port it to intellij-dtlc Agda Documentation Learn You An Agda Haskell A Type of Programming Arend Theorem Prover HoTT Martin Escardo's course Andrei Bauer's course Egbert Rijke's course Homotopy type theory Homotopy Type System principle of equivalence in nLab Univalent Foundations: “No Comment.” | Mathematics without Apologies, by Michael Harris What is an explicit bijection? - Bauer The visitor pattern is essentially the same thing as Church encoding Type Theory I don't like judgemental equality - Martin Escardo Proof by contradiction - Martin Escardo ON THE MEANINGS OF THE LOGICAL CONSTANTS AND THE JUSTIFICATIONS OF THE LOGICAL LAWS - Per Martin Löf How did 'judgement' come to be a term of logic? - Per Martin Löf