What would be interesting and relevant would be a formalization of the different types of theories of types applied to lambda calculus. At the moment we have the Simple Type Theory (i.e. HOL) developed by Mario Carneiro but there are many type theories. Dependent Type Theory is only one of them. Of course it would need a lot of commentary and references to book sources.
-- FL -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/2337506c-0c61-4269-be58-cde052ed7ec7%40googlegroups.com.
