本次报告首先介绍了 NA 的类型组合逻辑(Type Composition Logic, TLC)中与常见类型论不同的两点：点类型与量化类型。在量化类型方面，证明了 NA 的规则会产生矛盾，以及Ssher的类型在子类关系下将形成一个严格分叉的结构。报告人介绍了Asher 引入新类型的动机，对原来问题的解决，以及由此产生的后果。