Naive Type Theory (NTT)
Material related to my course at the Midland Graduate School in Birmingham, 11 - 15 April 2016
1st lecture:
intro
,
function types
1st set of exercises
2nd lecture
2nd set of exercises
3rd lecture
Pi and Sigma types
,
propositions as types for predicate logic
3rd set of exercises
4th lecture
universes
,
eliminators
4th set of exercises
Last modified: Thu Apr 14 15:47:36 BST 2016