Author Archives: Sam Speight
Impredicative Encodings of Inductive Types in HoTT
I recently completed my master’s thesis under the supervision of Steve Awodey and Jonas Frey. A copy can be found here. Known impredicative encodings of various inductive types in System F, such as the type of natural numbers do not … Continue reading
Posted in Applications, Foundations, Uncategorized
5 Comments