The Types of Relational Type Theory

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