#39 Equality, Quotation, Bidirectional Type Checking - David Christiansen
Type Theory Forall
00:00
Exploring Equality and Judgments in Type Theory
The chapter delves into the intricacies of equality in type theory, discussing different types of equality, the evolution of terminology, and the importance of judgments in systems. It also explores the concept of equality in verifying mathematical proofs, the complexity of dependent types, and the understanding of the eliminator for equality.
Transcript
Play full episode
