mathematical logic deduction system, natural deduction, sequent calculus, lambda-calculus, judgment type theory, simple type theory, dependent type theory collection, object, type, term, set, element equality, judgmental equality, typal equality universe, size issues higher-order logic This page is to record the reference: William Lawvere, Robert Rosebrugh: Sets for Mathematics Cambridge University Press (2003) doi:10.1017/CBO9780511755460 webpage, GoogleBooks, pdf which introduces set theory and the foundations of mathematics from a practical and category theoretic point of view known as structural set theory (“informal ETCS”). Paul Taylor Practical Foundations of Mathematics (web) Robert Harper, Practical Foundations for Programming Languages, Cambridge University Press (2016), (webpage)