2 citations · 2 across the 3 of their papers we have counts for
Showing math.CTShow all
2 papers · 1 filter
math.CT2024
A Type Theory with a Tiny Object
Mitchell Riley
We present an extension of Martin-Löf Type Theory that contains a tiny object; a type for which there is a right adjoint to the formation of function types as well as the expected…
math.CT2023★ 2 cited
Commuting Cohesions
David Jaz Myers, Mitchell Riley
Shulman's spatial type theory internalizes the modalities of Lawvere's axiomatic cohesion in a homotopy type theory, enabling many of the constructions from Schreiber's modal appro…