Mitchell Riley, April 17
12 views
Skip to first unread message
Dan Christensen
Apr 15, 2025, 9:28:42 AMApr 15
to hott-electroni...@googlegroups.com
This week the HoTTEST seminar presents:
Mitchell Riley
Tiny types and cubical type theory
The talk is at 11:30am EDT (15:30 UTC) on Thursday, April 17. The talk will be 60 minutes long, followed by up to 30 minutes for questions. See https://www.uwo.ca/math/faculty/kapulkin/seminars/hottest.html for the Zoom link and a list of all upcoming talks.
All are welcome!
Abstract:
I will present an extension of Martin-Löf Type Theory that contains a tiny object; a type for which there is an "amazing" right adjoint to the formation of function types as well as the expected left adjoint. A primary aim of the theory is to be simple enough to be used both by hand and in a (hypothetical) proof assistant. I will sketch a normalisation algorithm and discuss a few potential applications, in particular, to implementations of Cubical Type Theory.
Mitchell Riley
Tiny types and cubical type theory
The talk is at 11:30am EDT (15:30 UTC) on Thursday, April 17. The talk will be 60 minutes long, followed by up to 30 minutes for questions. See https://www.uwo.ca/math/faculty/kapulkin/seminars/hottest.html for the Zoom link and a list of all upcoming talks.
All are welcome!
Abstract:
I will present an extension of Martin-Löf Type Theory that contains a tiny object; a type for which there is an "amazing" right adjoint to the formation of function types as well as the expected left adjoint. A primary aim of the theory is to be simple enough to be used both by hand and in a (hypothetical) proof assistant. I will sketch a normalisation algorithm and discuss a few potential applications, in particular, to implementations of Cubical Type Theory.
Reply all
Reply to author
Forward
0 new messages