-
Propositional Resizing [dsp-9M7X]
-
Internal ∞-Categorical Models of Dependent Type Theory [dsp-7Z0O]
-
The Real Numbers, Propositionally [dsp-0016]
-
Type Theory for The Working Rustacean [dsp-0033]
-
Proof Theory Impressionism: Blurring the Curry-Howard Line [dsp-0030]