1. 11
  1.  

  2. 3

    I find it interesting that none of Martin Lof’s or Coquand’s works on their dependently typed calculi are on this.. Especially since most modern proof assistants..