Informal Workshop on Algebraic Weak Factorisation Systems
John Bourke: An orthogonal approach to algebraic weak factorisation systems
Abstract: Factorisation systems (both weak and strong) are commonly defined as consisting of two classes of maps satisfying a certain orthogonality relation and a factorisation axiom. The standard definition of algebraic weak factorisation system, involving comonads and monads, is rather different. The goal of this talk will be to describe an equivalent definition of algebraic weak factorisation system emphasising orthogonality and factorisation.
Wijnand van Woerkom: The Frobenius property for algebraic weak factorisation systems
Abstract: In the interpretation of type theory using WFS the dependent types are interpreted as the right maps of the WFS. The product types are interpreted using pushforward functors, so for this interpretation the WFS should satisfy the condition that pushforward along right maps preserves right maps. This property is generally hard to prove for a particular instance of a WFS. Luckily it is equivalent to the so-called ‘Frobenius property’ that is easier to prove, which states that pullback along a right map preserves left maps.
Recently efforts are made to interpret type theory using AWFS. Since the interpretation follows largely the same schema as with WFS, this requires us to phrase Frobenius and pushforward properties for AWFS, and to show they are equivalent. This talk is about sketching how this is done.
Nicola Gambino: The effective model structure on simplicial objects
Abstract: I will describe joint work with S. Henry, C. Sattler and K. Szumiło in which we construct a Qullen model structure on the category of simplicial objects in a category with finite limits and well-behaved countable coproducts. This work originates from the constructive version of the Kan-Quillen model structure on simplicial sets obtained by Henry and re-obtained with different methods by Sattler, Szumiło and me, by observing that the constructive arguments used in these proofs admitted a generalisation, obtained by replacing the category of sets with a category with finite limits and well-behaved countable coproducts. In particular, I will try to explain how some steps in the proof can be carried over even with a paucity of assumptions on the ambient category, as well as links with the theory of exact completions and Homotopy Type Theory.
References:
[1] N. Gambino, C. Sattler and K. Szumiło, The constructive Kan-Quillen model structure: two new proofs, The Quarterly Journal of Mathematics (to appear), arXiv:1907.05394
[2] N. Gambino, S. Henry, C. Sattler and K. Szumiło, The effective model structure and ∞-groupoid objects, Forum of Mathematics, Sigma (to appear), arXiv:2102.06146
[3] S. Henry, A constructive account of the Kan-Quillen model structure and of Kan's Ex^∞ functor, arXiv:1905.06160
Benno van den Berg: Effective Kan fibration in simplicial sets
Abstract: In this talk I will discuss ongoing work with Eric Faber where we also try to retrieve the Kan-Quillen model structure on simplicial sets in a constructive metatheory (in a manner different from that in the previous talk). The key definition is that of an ``effective Kan fibration'' which should be understood as a structure on a map of simplicial sets, rather than a property of a map of simplicial sets. We show (in a classical metatheory) that a map of simplicial sets can be equipped with this structure precisely when it is a Kan fibration. Furthermore, in a constructive metatheory the effective Kan fibrations are closed under pushforward (which is not true for the usual Kan fibrations), while also being ``local'' (unlike the ``uniform Kan fibrations'' of Gambino and Sattler), where both these requirements are important for modelling Homotopy Type Theory. In this talk I will explain our definition and give some idea of why it has the properties it has.
Reference:
B. van den Berg and E. Faber. Effective Kan fibration in simplicial sets. arXiv:2009.12670
Paige North: Two-sided and other generalizations of weak factorization systems
Abstract: This talk will be on one aspect of a project to develop a directed version of homotopy type theory. Homotopy type theory has semantics in (some) weak factorization systems, and so we first alter the notion of weak factorization systems to produce a directed version, which we call two-sided weak factorization systems, and which is the intended semantics for directed homotopy type theory. We also formulate a general notion, of which weak factorization systems and two-sided weak factorization systems are instances.
This is joint work with Benno van den Berg and Erin McCloskey.