Unrestricted Quantification and the Structure of Type Theory. (8th August 2019)