1 citations · 1 across the 1 of their papers we have counts for
Showing 2024Show all
2 papers · 1 filter
cs.LO2024
Unifying cubical and multimodal type theory
Frederik Lerbjerg Aagaard, Magnus Baunsgaard Kristensen, Daniel Gratzer +1
In this paper we combine the principled approach to modalities from multimodal type theory (MTT) with the computationally well-behaved realization of identity types from cubical ty…
math.CT2024
Strict universes for Grothendieck topoi
Daniel Gratzer, Michael Shulman, Jonathan Sterling
Hofmann and Streicher famously showed how to lift Grothendieck universes into presheaf topoi, and Streicher has extended their result to the case of sheaf topoi by sheafification.…