理論計算機科学と圏論ワークショップ CSCAT 2026
本研究集会は科研費JP24K23867の支援により開催されます．
CSCAT（理論計算機科学と圏論ワークショップ）は、数学の分野である圏論の情報科学への応用に関心を持つ研究者による研究集会です。 通常の学会では、時間の制約などのため研究の詳細にまで立ち入った発表と議論はなかなかむずかしいのが実情です。 本研究集会は、１つ１つの発表に長い時間を割り当て、じっくりと話を聞き議論する場を提供することを目的としています。
We provide a general semantic treatment of univalence at the level of Voevodsky's universe categories by providing a lightweight formulation that is easy to check across various models. The upshot of our formulation is that, when verifying univalence in a universe category model, one does not need to work with syntax at all. To arrive at such a formulation, we give a version of univalence, which we refer to as pointed univalence, that is stronger than the one commonly used and given in the HoTT Book, which we refer to as book univalence.
While book univalence asks for a certain commutative square to admit a diagonal filler making only the lower triangle commute, pointed univalence requires that both resulting triangles commute. As such, pointed univalence is very natural to verify in models coming from Quillen model categories. Furthermore, since maps from the left class to fibrations axiomatise pattern-matching, pointed univalence is also computationally desirable, as it justifies performing pattern matching on equivalences. Thus, we believe this strengthening constitutes a new notion of independent interest with strong semantic justification. Our semantic study of pointed univalence includes studying closure properties of models under two fundamental constructions: Artin--Wraith gluing and inverse diagrams. For book univalence, these were verified in the seminal work of Shulman [Shu15], and we provide the "pointed counterpart" of his results.
This talk is based on joint work with Krzysztof Kapulkin from [KL25].
[KL25] Krzysztof Kapulkin and Yufeng Li, (Pointed) Univalence in Universe Category Models of Type Theory. 2025. arXiv: 2512.16697 [CS.LO]. [Shu15] Michael Shulman. "Univalence for inverse diagrams and homotopy canonicity'". In: Mathematical Structures in Computer Science 25.5 (2015), pp. 1203--1277.
The \(\Sigma\)-module semantics of linear logic provides a unified linear-algebraic account of a wide range of webbed models, including coherence, finiteness, and probabilistic coherence spaces. Its distinctive feature is that addition is partial: sums may be undefined, for example when a sum exceeds \(1\) in probabilistic models. This partiality is central to the directness of the semantics: for example, it directly enforces the constraint that total probability does not exceed \(1\). Technically, however, it makes concrete reasoning about sums delicate.
We provide an alternative technical basis for Σ-module semantics by recasting this partiality in Hyland--Schalk's more classical and widely applicable framework of glueing (logical predicates) and orthogonality. Instead of treating undefined sums as partial algebraic operations, we pass from a coefficient \(\Sigma\)-semiring to its completion, where addition becomes total, and express the original restriction via a focused orthogonality, yielding a tight orthogonality model. For an arbitrary coefficient \(\Sigma\)-semiring \(R\) satisfying a suitable assumption, we construct a new linear model structure on the category of \(R\)-modules via the tight orthogonality model. We then show that the resulting linear model structures coincide with the original ones for principal examples of \(\Sigma\)-semirings whose \(\Sigma\)-module semantics recover the known models listed above. Our construction of the linear exponential comonad slightly generalizes the well-known construction from an LNL adjunction and may be of independent interest.
Given a cartesian monad T on a finitely complete category E, the slice category E/T1 carries a monoidal structure, and a T-operad is defined to be a monoid in this category. For example, when T is the free monoid monad on Set, the category Set/T1 may be viewed as the category of sets of function symbols, and a T-operad is precisely a planar operad. A T-operad induces a monad on E; equivalently, it may be described as a monad P on E equipped with a monad morphism ar : P → T. This suggests that T-operads should be regarded as one instance of a general notion of “theory”, alongside monads, Lawvere theories, finitely complete categories, and others. In this talk, we present several results on the structure–semantics adjunction for T-operads, viewed as a synthetic criterion for being a notion of “theory”. We also give a sufficient condition on the pair (T, E) under which this structure–semantics adjunction is particularly well behaved in comparison with the corresponding adjunction for monads. We call this property strong subgenericity.
This work is based on several joint works with Soichiro Fujii and Yuki Maehara.
Persistent homology provides topological descriptors for the configuration of point clouds in metric spaces and is used in topological data analysis to detect features such as local dimensionality and isotropy. Over the past decade, the application of persistent homology to point clouds that vary according to extra parameters has been extensively studied, leading to various formulations including multiparameter persistent homology.
In this talk, we introduce a formulation of persistent homology within the framework of topos theory. We demonstrate that the dependency of a point cloud on its parameters can be characterized through the axioms of the internal logic of an associated topos. As an application, we define a notion of infinitesimal parameter-dependent persistent homology and discuss barcode decomposition.
コンウェイのライフゲームでは，「グライダーが右上に向かって移動している」といった現象を観察することができます．でもそもそも，「グライダーが右上に向かって移動している」という言明は，格子ℤ^2の持つどのような空間的構造によって可能になっているのでしょうか．
本発表では，ライフゲームなどのセルオートマトンを例にとって，「時間発展に依存した空間概念」を離散力学系トポスSet^ℕ上のrelative topos of internal presheafとして捉えるというアイデアを紹介し，CSCATの皆さんに興味を持っていただけるかもしれない発展の方向性をいくつか提示します．