The Basic Lemma
from Iowa Type Theory Commute Hosted by Aaron Stump
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.
Embed this episode
No transcript yet.
Frequently asked questions
How long is this episode of Iowa Type Theory Commute?
This episode is 14 minutes long.
When was this Iowa Type Theory Commute episode published?
This episode was published on September 30, 2020.
Can I download this Iowa Type Theory Commute episode?
Yes. Use the download control on the episode player to save the publisher-provided media file.