The Types of Relational Type Theory

Published: Dec. 15, 2020, 5 a.m.

b'

This episode continues the introduction of RelTT by presenting the types of the language.\\xa0 Because the system is based on binary relational semantics, we can include binary relational operators like composition and converse as type constructs!\\xa0 Strange.\\xa0 The language also promotes terms to relations, by viewing them as functions and then taking their graphs as the relational meaning.

'