iiinova — where your digital self keeps evolving

David Corfield

@davidcorfield.bsky.social

Philosopher interested in mathematics, especially category theory, and psychoanalysis. Author of 'Modal Homotopy Type Theory: The prospect of a new tool for philosophy' (OUP, 2020) and 'Why do people get ill? (Hamish Hamilton 2007)

Posts Replies Media

David Corfield @davidcorfield.bsky.social · 08/05/2026

Luckily we now know what they are: arxiv.org/abs/2504.12158

040

David Corfield @davidcorfield.bsky.social · 23/12/2025

Yes, the work was done while the others were on the ARIA project. Their goal was to provide a graded monad understanding of dl.acm.org/doi/10.1145/..., and related work. I'm not working on that now, but what we did is being written up and has nearly reached first draft phase.

dl.acm.org

A unifying type-theory for higher-order (amortized) cost analysis | Proceedings of the ACM on Programming Languages

This paper presents λ-amor, a new type-theoretic framework for amortized cost analysis of higher-order functional programs and shows that existing type systems for cost analysis can be embedded in it....

010

David Corfield @davidcorfield.bsky.social · 23/12/2025

Then set-indexed families of Psh(M), as Riley notes. But then this is Psh(M+), where the + adjoins an initial object.

000

David Corfield @davidcorfield.bsky.social · 22/12/2025

Suddenly, we seemed very close to this section of Riley's thesis, but we didn't push things far in this direction:

110

David Corfield @davidcorfield.bsky.social · 22/12/2025

My interest derived at first from the role of linear HoTT in the Sati-Schreiber program: ncatlab.org/schreiber/sh.... But then, oddly, working with Rajani and Orchard on a type theory for amortization, we found ourselves looking at models which were families of copresheaves on an ordered monoid.

ncatlab.org

The Quantum Monadology in Schreiber

120

David Corfield @davidcorfield.bsky.social · 22/12/2025

Bunched dependent types, like Mitchell Riley: ncatlab.org/nlab/show/Mi...?

ncatlab.org

Mitchell Riley in nLab

110

David Corfield @davidcorfield.bsky.social · 04/11/2025

I hope you find inspiration and an outlet. Nothing has come close for me to the thrill of writing on the n-Category Cafe c. 2006-2013.

020

David Corfield @davidcorfield.bsky.social · 24/09/2025

Linked to "The unreasonable power of the lifting property in elementary mathematics"? Penultimate reference on 'nLab: factorization system': ncatlab.org/nlab/show/fa...

ncatlab.org

030

David Corfield @davidcorfield.bsky.social · 07/06/2025

The CW01 mentioned in the footnote is Caccamo & Winskel: A Higher-Order Calculus for Categories www.brics.dk/RS/01/27/BRI.... It has rules such as

120

David Corfield @davidcorfield.bsky.social · 06/06/2025

Maybe via ends/coends and this?: arxiv.org/abs/1501.02503

110