Start / Iowa Type Theory Commute / The basic lemma

The Basic Lemma

15 min • 30 september 2020

Also known as the Fundamental Property, this is a theorem stating that for every well-typed term t : T, and every logical relation R between algebraic structures A and B, the meaning of t in A is related by R to the meaning of t in B. I view it as a straightforward semantic soundness property, but where the semantics of types is this somewhat interesting one that interprets types as binary relations on structures A and B. I muse on these matters a bit in the episode.