Thorsten Altenkirch: ‘A constructive justification of Homotopy Type Theory’
My main thesis is that Homotopy Type Theory is a foundation of mathematics that is constructive in two ways: not only is the platonic concept of mathematical truth replaced by evidence (via the proposition as types translation) but also collections of preexisting objects as in set theory are replaced by types which reflect the idea that they are created and not discovered. Applying a constructive form of extensionality we arrive at the univalence principle, because we cannot distinguish isomorphic structures in Type Theory.
Steve Awodey: ‘Univalence as a logical law’
David Corfield: ‘The modality of physical law in modal homotopy type theory’
For homotopy type theory (HoTT) to act as a useful formal language for gauge field theory it needs to be able to express naturally the constructions of modern differential topology and geometry. Since continuity and smoothness are not built into HoTT, Urs Schreiber looked to William Lawvere’s ideas to find a way to encode the necessary structures.
As he explained in a talk at Bristol last year [Sch 14], this amounts to defining a series of chains of adjunctions, each giving rise to several so-called ‘modalities’. These are named
for what they share with the structure of the classic modalities of possibility and necessity, as represented by categorical logicians in terms of ‘monads’ and ‘comonads’. A vast of modern gauge field theory can now be written out in modal homotopy type theory
[Sch 13].
In discussions with Schreiber, we noticed a way to make much clearer the parallel between
ordinary modal logic, as concerning variation over a type of worlds, and the theory of partial differential equations, as expressing infinitesimally local variation. For example, partial differential equations with variables varying over a domain find their analogues in the rigid designators of modal logic. In this talk I would like to take this analogy further, in particular, to investigate the modal quality of physical laws as expressions of kinds of invariance.
[Sch 13], Differential cohomology in a cohesive ∞-topos v2,
[Sch 14], ‘Modern Physics formalized in Modal Homotopy Type Theory’,
talk at the University of Bristol, 7 April 2015.
Ben Eva: ‘Q worlds: A guided tour’
The idea that, by using non-classical mathematics, we can hope to construct
a new, philosophically illuminating, language for non-relativistic quantum mechanics
(QM) has gained a signicant amount of attention in recent years. In
this presentation, I will aim to provide both a philosophical survey/analysis
of, and a new mathematical unifying framework for, two of the major research
projects in this area. In particular, I will argue that topos quantum theory
(TQT) and quantum set theory (QST) can be seen as sharing a common basic interpretational stance with regards to QM, and present a new formal framework that allows us to transfer concepts and results between these approaches in a new and exciting way. I will go on to use this framework to prove some physically important new results, including a logical characterization of operator inequalities in TQT. The central result of the presentation will be that for any xed Hilbert space H, it is possible to construct a non-classical set theoretic universe (a ‘Q world’), whose truth values correspond to the truth values of TQT, and in which the set of all Dedekind real numbers is in bijective correspondence with the self-adjoint operators on H. This leads naturally to the idea that it might be possible to construct, for any given physical system, a mathematical universe whose internal structure is uniquely well suited to describe the physics of that system.
Eleanor Knox: tba
James Ladyman and Stuart Presnell: ‘HoTT, Structure and Structuralism’
Vasiliki Nassiopoulou: ‘A dipolar relation between subject and object captured sheaf-theoretically’
Structural realism appears in two forms, the Epistemic Structural Realism (ESR) and the Ontic Structural Realism (OSR). They both focus on the structure of the unobservable world with the difference that ESR makes epistemological claims and OSR ontological ones. However, it has been claimed that in its current formulation OSR is like ESR; the elimination of relata or the endowment of relata with relational properties is epistemologically grounded. In this paper, I aim to present an approach where ontology involves the instantiation or realization of the structure of a given theory so that if epistemology rejects individuality, ontology introduces it.
In particular, the framework employed will be sheaf theory which can be used as a basis so that both the subject and the object participate in the interpretation of the structure of the world in an inseparable bidirectional way; this means that the objective world participates in the description of the structure (and it is not that the structure is found in the subject even if it is objective as structuralists may espouse). The relation between subject and object will be captured as bidirectional relation between whole and parts (actualized structures) so that none is prior. Sheaf theory provides an algebraic framework implementing a mereological treatment of regions, where these regions are not defined with respect to a background spacetime. Starting from the category of regions (or partially ordered sets, causal sets, manifolds etc.), one can obtain physical constructions that refer to other categories e.g. the category of algebras of differential k-forms on topological space, the category of Hilbert spaces etc. while the mereological relations are provided by (restriction) morphisms between objects (and elements of objects) of a category. Although category theory and sheaf theory provide the basis for an ontology of relations captured by morphisms, a notion of individuality is still recoverable.
Paige North: tba
Jaime Andrés Robayo Mesa: ‘An approximation of sheaves in HoTT’
HoTT appeared just a few years ago, but his evolution and advance are really amazing. When HoTT began with Vladimir Voevodsky’s works and the Univalent Program in IAS (2012-2013), the main problem was to translate to univalent foundation some notions of classical set theory and category theory.
Some recent works try to expand mathematical concepts to HoTT or go inside inner in the underlying logic for its HoTT. For example, the last papers of Michael Shulman about a notion of a synthetic topological space in HoTT, its obstructions and some relations with ∞-grupoids; the C-System, presented in the last papers of Voevodsky, like a univalent model that completes the model of inferences rules of Martin Löf of type theory, or the Awodey works about the univalent axiom.
Our goal in this contribution is to show a first version of Sheaves on HoTT, and describe some difficulties and advances to get it. Specially, for connections between category theory and HoTT logic, we explore the notion of sheaf from topos theory, in other words, through the functors on Grothendieck topology.
This notion is more likely to be extended or axiomatized in HoTT, because it has a closest connection between morphism, functors, category concepts and the logic of this new foundation.
Andrei Rodin: ‘HoTT and the Semantic View of Theories’
P. Suppes famously argued that a typical scientific theory should be identified not with any particular class of statements (formal or contentual) but rather with a certain class of models. On this basis Suppes and his followers designed a Bourbaki-style format of formal presentation where a scientific theory is presented through an appropriate class of its set-theoretic models.
Albeit such a Bourbaki-style presentation can be useful for purposes of logical and structural analysis, it appears to be useless as a practical tool, which may help working scientists to formulate and develop their theories in an axiomatic way. Such a limitation is hardly surprising given that the standard set-theoretic semantics of theories provides no formal means for building and operating with models other than by referring to the fact that a model in question satisfies such-and-such propositions. Differences in epistemological views on the roles of syntax and semantics affect the style of axiomatic presentation but not the axiomatic architecture itself. This is why in practice the usual non-statement approach to axiomatizing scientific theories demonstrates the same limitations as its syntactically oriented rival.
HoTT provides a novel notion – as well as an example – of theory, which does not reduce to a class of propositions but has a further higher-order non-propositional structure. The axiomatic basis of this theory consists of a system of rules, which apply both at the propositional and non-propositional levels. At the semantic level these rules apply as rules for constructing further semantic constructions from primitive semantic elements assigned to primitive syntactic types.
This new constructive notion of theory provides a precise sense in which a theory, generally, does not reduce to a class of its propositions. Thus it supplements the semantic aka non-statement view of theories in its usual form with a new axiomatic technique, which has a potential of applications in theoretical physics and perhaps some other scientific disciplines. In my talk I shall discuss how this potential is realized in recent works by Urs Schreiber in axiomatizing the Quantum Field theory.
Urs Schreiber: Formalizing higher Cartan geometry in modal HoTT
An elegant general theory capturing all flavors of geometry
(Riemannian, complex, symplectic, conformal, etc.) is “Cartan
geometry”, the theory of torsion-free G-structures on manifolds. Its
generalization to higher (i.e. stacky) geometry and to super-geometry,
turns out to encode 11-dimensional super-gravity, all the way from the
Einstein equations of motion to BPS states and brane charges. I have
shown earlier that all this has an elegant “synthetic” formulation in
higher toposes equipped with a progression of 9 adjoint idempotent
(co-)monads. The internal language of these is thought to be HoTT with
a system of modal operators added. Recently Felix Wellen, in his
thesis, has begun to fully formalize Cartan geometry in modal HoTT
along these lines. In the talk I give an introduction and present his
results.
Felix Wellen: ‘Synthetic differential geometry in homotopy type theory via a modal
operator’
We aim at developing synthetic differential geometry in homotopy type theory. Of particular interest are types locally modelled on group like types. Differential geometric
extra structure on types may be given by a modal operator resembling the infinitesimal shape monad of a differentially cohesive infinity topos, a notion introduced by Urs Schreiber to model aspects of modern physics.
We add axioms to homotopy type theory to ensure the existence of such a modal operator and refer to the types of this theory as differentially cohesive types. The modal operator allows to synthetically formulate a definition of a V-manifold as a type which is locally modelled on a differentially cohesive group V. These V-manifolds would already be locally trivial, if the bundle of infinitesimal neighbourhoods over a differentially cohesive group were trivial.
We outline a strategy to prove this last statement in general and give a proof of the already completed parts. Along the way are various opportunities to look at benefits gained from using homotopy type theory and differential cohesion to model the geometry underlying modern physics.
HoTT and Philosophy 