Types

• 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](https://mathematicswithoutapologies.wordpress.com/2015/05/13/univalent-foundations-no-comment/)

  • 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