Subtyping and Type Calculus

This lecture covers the concepts of subtyping and type calculus, focusing on calculating least upper bounds and greatest lower bounds of types in a system extended with subtyping. The instructor walks through exercises involving STLC extended with subtyping, explaining the rules and guiding the audience through solving the exercises step by step. The session also addresses questions about function types, variance, and the application of type parameters. Additionally, the lecture delves into proving the equivalence between excluded middle and double negation in a system extended with subtyping. The instructor provides detailed explanations, encourages critical thinking, and guides the audience in understanding and applying the concepts effectively.