myuon-myon.hatenablog.com の続き. いくつか疑問が解消されたのでそれについて. var-free type theoryについて syntaxはcontext, type, term, substからなる. contextはtypeの有限列(通常はvariableとそのtypeの組の列だが, 今回はvariable-freeなのでtype…