I am mainly interested in topos theory and categorical logic. Currently I’m applying logical methods to construct synthetic environments for higher domain theory, higher category theory, and higher computability.
I now also maintain a logical-geometry note.
Published/Submitted
[2026] Craig Interpolation for Subgeometric Logics [arXiv]
An interpolation theorem for general subgeometric logics.
We show that a vast class of finitary fragments of geometric logic admit a form of Craig interpolation property. In doing so, we provide a new dictionary to import technology from algebraic logic to categorical logic.
[2025] Domains and Classifying Topoi [arXiv]
Synthetic domain theory via distributive lattice classifiers.
We explore a new connection between synthetic domain theory and Grothendieck topoi related to the distributive lattice classifier. In particular, all the axioms of synthetic domain theory (including the inductive fixed point object and the chain completeness of the dominance) emanate from a countable version of the synthetic quasi-coherence principle that has emerged as a central feature in the unification of synthetic algebraic geometry, synthetic Stone duality, and synthetic category theory. The duality between quasi-coherent algebras and affine spaces in a topos with a distributive lattice object provides a new set of techniques for reasoning synthetically about domain-like structures, and reveals a broad class of (higher) sheaf models for synthetic domain theory.
[2025] Logic and Concepts in the 2-category of Topoi [arxiv]
Study fragments of geometric logic via Kan injectivity in the 2-category of topoi; provide general classifying topos and syntactic category construction.
We use Kan injectivity to axiomatise concepts in the 2-category of topoi. We showcase the expressivity of this language through many examples. We use this technology to introduce fragments of geometric logic, and we accommodate essentially algebraic, disjunctive, regular, and coherent logic in our framework, together with some more exotic examples. We show that each fragment H in our sense identifies a lax-idempotent (relative) pseudomonad 𝖳 on 𝗅𝖾𝗑, the 2-category of finitely complete categories. We show that the algebras for 𝖳 admit a notion of classifying topos, for which we deliver several Diaconescu-type results. The construction of classifying topoi allows us to define conceptually complete fragments of geometric logic.
[2023] Categorical Structure in Coherent Theory of Arithmetic [arxiv, to appear in TCS]
Construct a coherent theory of arithmetic and prove its universal property, with applications to proof theory.
Constructed a coherent theory of arithmetic, whose syntactic category is the initial coherent category with a parametrised natural number object. Applied it to characterise provably total recursive functions in IΣ1, and study other proof-theoretic properties of arithmetic.
[2022] Varieties of Self-Reference in Meta-Mathematics [JPL]
Study canonical self-reference in meta-mathematics.
Defined uniform diagonal operators and studied naming relations on syntax of arithmetic. They are used to distinguish functional and accidental self-reference. Applied them to the study of Henkin sentences, as well as other self-referential sentences in meta-mathematics.
[2022] Unification of Modal Logic via Topological Categories [ACT 2022]
A unified semantics of general modal logics via topological categories.
Established a unified framework via topological categories encapsulating various existing semantics of modal logic. Obtained exact correspondence between fibrational structures of topological categories and syntactic features of modal logic. Based on my Bachelor thesis.
[2021] Towards a Relational Treating of Language and Logical System [AWPL]
Study universal properties of connectives via a “jointly consistent relation”.
Thesis
[Master] Algebraic Monoidal Model Categories and Path Category Structures for Effective Kan Fibrations [pdf]
A general framework to lift the pushout-product axioms in homotopy theory to the structured context of algebraic weak factorisation systems, with application to effective Kan fibrations.
We develop a general framework to lift the pushout-product axioms in classical homotopy theory to the structured context of algebraic weak factorisation systems. The outcome is a notion of an algebraic monoidal model category. Within this framework, we are able to formulate and prove a structured analogue of Joyal-Tierney calculus, with the help of which we put an algebraic monoidal structure on effective Kan fibrations.
Effective Kan fibration is a new notion of fibration to develop a constructive model of homotopy type theory on simplicial sets. We show there is a path category structure on the full subcategory of effective Kan fibrations over any object, using the algebraic monoidal structure constructed earlier. This brings us closer to showing the existence of a full model structure. Finally, we also identify a key semantic property, which we refer to as Moore equivalence extension. We are able to show that if simplicial sets satisfy this property, then there exists a full algebraic monoidal model category structure for effective Kan fibrations.
[Bachelor] A Structural Study of Information in a Logical Perspective [pdf]
A structural study of the “landscape of information”.
The thesis gives a structural study of the “landscape of information”. The general type of information structures we consider are those supporting the interpretation of certain (extensions of) modal systems. The project provides a precise description of the common mathematical background for all such types of models, and studies interactions between all these different types of semantics by considering functorial transformations between them.
Under Revision
[2024] Stack Representation of Finitely Presented Heyting Pretoposes [arxiv]
Present Heyting pretoposes as stacks over Krikpe frames.
This is the first of a series of papers on stack representation of finitely presented Heyting pretoposes. We have provided the first step by constructing a (2, 1)-site, which can be thought of as the site of finite Kripke frames, such that the (2,1)-category of finitely presented Heyting pretoposes contravariantly embeds into the (2,1)- topos of stacks on this (2, 1)-site.
[2024] Canonical Incompleteness [pdf]
Incompleteness via universal properties.
There are many “counterexamples” of second incompleteness theorem. This is a document explaining how categorical logic can help pin down what exactly it means to say “PA cannot prove its own consistency”, and provide a correct proof of second incompleteness theorem.
Notes
[2023] Ultraposet, Distributive Lattice, and Coherent Locale [arxiv]
[2023] Sheaf Representation of Heyting Algebras [pdf]
[2021] Complexity, Incompleteness, and Foundation of Mathematics [pdf]
[2021] Morse Method in Computing Persistent Cosheaf Homology [pdf]
[2020] Algebraic Investigations of Provability Logic and Paradoxes [pdf]
Lingyuan Ye 叶凌远 