Iowa Type Theory Commute
In this episode, I discuss the semantics of the proposed six type constructors of RelTT.