Podcasts Technology Iowa Type Theory Commute Begin chapter on extensionality

Begin chapter on extensionality

Published: Jan. 25, 2023, 5 a.m.

b'

This episode begins a new chapter on extensionality in type theory, where we seek to equate terms in different ways based on their types.\\xa0 The basic example is function extensionality, where we would like to equate functions from A to B if given equal inputs at type A, they produce equal outputs at type B.\\xa0 With this definition, quicksort and mergesort are equal, even though their codes are not syntactically equivalent.\\xa0 The episode begins by reviewing the distinction between definitional and propositional equality.

Also, I am still seeking your small donations ($5 or $10 would be awesome) to pay my podcast-hosting fees at Buzzsprout.\\xa0 To donate, click here, and then under "Gift details" select "Search for additional options" and then search for Computer Science.\\xa0 Select the Computer Science Development Fund, College of Liberal Arts and Sciences.\\xa0 Then add gift instructions saying that this is to support the Iowa Type Theory Commute podcast of Aaron Stump.\\xa0 Sorry it's that complicated.

'