BEGIN:VCALENDAR VERSION:2.0 PRODID:researchseminars.org CALSCALE:GREGORIAN X-WR-CALNAME:researchseminars.org BEGIN:VEVENT SUMMARY:Peter LeFanu Lumsdaine (Stockholm University) DTSTART:20200615T143000Z DTEND:20200615T153000Z DTSTAMP:20260409T094011Z UID:HoTTEST2020/1 DESCRIPTION:Title: What are we thinking when we present a type theory?\nby Peter LeFa nu Lumsdaine (Stockholm University) as part of The HoTTEST conference of 2 020\n\n\nAbstract\nPresentations of dependent type theories\, as tradition ally written\, are deceptively simple: a collection of rules specifying an inductively defined derivability relation on judgments (or some variation on such a setup).\n\nHowever\, in writing these rules\, we usually follow various guiding principles — or at least\, we have these principles in mind\, and depart from them only with good cause and extra care. Some of these principles are (sometimes) explicitly stated: “all rules hold over an arbitrary ambient context”\, for instance. Other principles almost always remain implicit — “the rules are ordered\, and each rule may ma ke use of earlier-introduced constructions\, but not later ones” — but become apparent through our reliance on them in later definitions and pro ofs.\n\nI will present a careful analysis of these implicit principles\, a nd how they contribute to the well-behavedness properties we expect our ty pe theories to enjoy.\n\n(Based on joint work with Andrej Bauer and Philip p Haselwarter\, forthcoming since 2016.)\n LOCATION:https://researchseminars.org/talk/HoTTEST2020/1/ END:VEVENT BEGIN:VEVENT SUMMARY:Brandon Doherty (University of Western Ontario) DTSTART:20200615T160000Z DTEND:20200615T170000Z DTSTAMP:20260409T094011Z UID:HoTTEST2020/2 DESCRIPTION:Title: Cubical models of (∞\,1)-categories\nby Brandon Doherty (Univers ity of Western Ontario) as part of The HoTTEST conference of 2020\n\n\nAbs tract\nWe discuss the construction of a new model structure on the categor y of cubical sets with connections whose cofibrations are the monomorphism s and whose fibrant objects are defined by the right lifting property with respect to inner open boxes\, the cubical analogue of inner horns. We als o discuss the proof that this model structure is Quillen equivalent to the Joyal model structure on simplicial sets via the triangulation functor. T his talk is based on joint work with Chris Kapulkin\, Zachery Lindsey\, an d Christian Sattler\, arXiv:2005.04853.\n LOCATION:https://researchseminars.org/talk/HoTTEST2020/2/ END:VEVENT BEGIN:VEVENT SUMMARY:Valery Isaev (JetBrains Research and Higher School of Economics) DTSTART:20200616T143000Z DTEND:20200616T153000Z DTSTAMP:20260409T094011Z UID:HoTTEST2020/3 DESCRIPTION:Title: Indexed type theories\nby Valery Isaev (JetBrains Research and Hig her School of Economics) as part of The HoTTEST conference of 2020\n\n\nAb stract\nIndexed type theory is a version of homotopy type theory which rep resents indexed ∞-categories. It has two levels of types: the first leve l correspond to ordinary homotopy type theory and the second one represent s indexed objects. Indexed type theories generalize other similar two-leve l systems such as a form of cohesive homotopy type theory and certain line ar dependent type theories. It can be used to reason directly in ∞-categ ories which do not have all the structure required by homotopy type theory .\n\nIn this talk\, I define indexed type theory and describe various cons tructions in it including finite and infinite (co)limits and object classi fiers. I will give several examples of models of indexed type theory inclu ding spectra and quasicategories. I will also prove a special case of the indexed adjoint functor theorem using the language of indexed type theorie s.\n LOCATION:https://researchseminars.org/talk/HoTTEST2020/3/ END:VEVENT BEGIN:VEVENT SUMMARY:David Jaz Myers (Johns Hopkins University) DTSTART:20200616T160000Z DTEND:20200616T170000Z DTSTAMP:20260409T094011Z UID:HoTTEST2020/4 DESCRIPTION:Title: Higher Scheier theory\nby David Jaz Myers (Johns Hopkins Universit y) as part of The HoTTEST conference of 2020\n\n\nAbstract\nIn a 1926 arti cle\, Otto Schreier gave a classification of all extensions of a group G b y a (non-abelian) group K. This classification of extensions has come to b e known as Schreier theory\, and has been reformulated many times by many authors since. Just as central extensions by an abelian group are classifi ed by group cohomology in degree 2\, Schreier theory can be seen as an exa mple of a classification by non-abelian group cohomology.\n\nHigher Schrei er theory concerns the classification of extensions of higher groups. Bree n has generalized Schreier theory to sheaves of 2-groups. In this talk\, w e will give a proof of Schreier theory for oo-groups in homotopy type theo ry - and therefore for sheaves of ∞-groups by interpreting in various oo -toposes. Our main theorem is:\n\nLet G and K be ∞-groups. Then the type of extensions of G by K is equivalent to the type of actions of G on the delooping BK.\n\nOne can immediately see the resemblence of this formulati on of higher Schreier theory to the classification of split extensions of G by K by the homomorphic actions of G on K. We can derive this classifica tion\, and some others\, as an immediate corollary.\n\nWe will also discus s the notion of central extensions\, and navigate some subtleties concerni ng the notion of centrality for higher groups.\n LOCATION:https://researchseminars.org/talk/HoTTEST2020/4/ END:VEVENT BEGIN:VEVENT SUMMARY:Taichi Uemura (University of Amsterdam) DTSTART:20200617T143000Z DTEND:20200617T153000Z DTSTAMP:20260409T094011Z UID:HoTTEST2020/5 DESCRIPTION:Title: Abstract type theories\nby Taichi Uemura (University of Amsterdam) as part of The HoTTEST conference of 2020\n\n\nAbstract\nMany variants of dependent type theory admit the semantics based on categories with famili es (CwFs). I introduce an abstract notion of a type theory to give a unifi ed account of the CwF-semantics of type theory. The key idea is to regard a CwF-model of a type theory as a functor to a presheaf category preservin g certain structures. Basic results in the semantics of type theory are th en stated and proved in a purely categorical way. In this talk I will expl ain motivations and intuitions behind my definition of a type theory.\n LOCATION:https://researchseminars.org/talk/HoTTEST2020/5/ END:VEVENT BEGIN:VEVENT SUMMARY:Paige Randall North (Ohio State University) DTSTART:20200617T160000Z DTEND:20200617T170000Z DTSTAMP:20260409T094011Z UID:HoTTEST2020/6 DESCRIPTION:Title: A higher structure identity principle\nby Paige Randall North (Ohi o State University) as part of The HoTTEST conference of 2020\n\n\nAbstrac t\nThe Structure Identity Principle (SIP) is an informal principle asserti ng that isomorphic structures are equal. In univalent foundations\, the SI P can be formally stated and proved for a variety of mathematical structur es. This means that any statement that can be expressed in univalent found ations is invariant under isomorphism\, or\, put differently\, that only s tructural properties can be stated in univalent foundations.\n\nThe SIP on ly applies to objects that naturally form a 1-category. In this talk\, I w ill discuss a Higher Structure Identity Principle in univalent foundations for structures that naturally form a higher category (e.g.\, categories t hemselves).\n\nThis is joint work with Benedikt Ahrens\, Mike Shulman\, an d Dimitris Tsementzis.\n LOCATION:https://researchseminars.org/talk/HoTTEST2020/6/ END:VEVENT BEGIN:VEVENT SUMMARY:Mitchell Riley (Wesleyan University) DTSTART:20200618T143000Z DTEND:20200618T153000Z DTSTAMP:20260409T094011Z UID:HoTTEST2020/7 DESCRIPTION:Title: Synthetic spectra via a monadic and comonadic modality\nby Mitchel l Riley (Wesleyan University) as part of The HoTTEST conference of 2020\n\ n\nAbstract\n"Spectra" are the central objects of study in stable homotopy theory\, and it is easy to define them internally in HoTT as Ω-spectra: a spectrum is a sequence of types with an equivalence between each type an d the loop-space of the next. Working with these spectra in type theory ca n be quite difficult\, however. In this talk we describe an extension of H oTT intended to be modeled in the category of "parameterised spectra"\, wh ere a modality is used to identify the types that correspond to individual spectra. A pair of axioms are considered that internalise some features o f the intended model\, and which fix the "homotopy groups" (appropriately defined) of the sphere spectrum to be the stable homotopy groups of the or dinary higher inductive spheres.\n LOCATION:https://researchseminars.org/talk/HoTTEST2020/7/ END:VEVENT BEGIN:VEVENT SUMMARY:Anja Petković (University of Ljubljana) DTSTART:20200618T160000Z DTEND:20200618T170000Z DTSTAMP:20260409T094011Z UID:HoTTEST2020/8 DESCRIPTION:Title: Equality checking for finitary type theories\nby Anja Petković (U niversity of Ljubljana) as part of The HoTTEST conference of 2020\n\n\nAbs tract\nEquality checking algorithms are essential components of proof assi stants based on type theories\, since they free users from the burden of p roving judgemental equalities\, and provide computation-by-normalization e ngines. Indeed\, the type theories found in the most popular proof assista nts are designed to provide such algorithms.\n\nHowever\, in a proof assis tant that supports arbitrary user-definable theories\, such as Andromeda 2 \, there may not be an equality checking algorithm available in general.\n \nI will discuss the design of a user-extensible judgemental equality chec king algorithm for finitary type theories that supports computation rules and extensionality rules. The user needs only provide the equality rules t hey wish to use\, after which the algorithm devises an appropriate notion of normal form. We will also take a peek at how the implementation of the equality checking algorithm is used in the Andromeda 2 prover.\n LOCATION:https://researchseminars.org/talk/HoTTEST2020/8/ END:VEVENT BEGIN:VEVENT SUMMARY:Eric Finster (University of Birmingham) DTSTART:20200619T143000Z DTEND:20200619T153000Z DTSTAMP:20260409T094011Z UID:HoTTEST2020/9 DESCRIPTION:Title: Weak structures from strict ones\nby Eric Finster (University of B irmingham) as part of The HoTTEST conference of 2020\n\n\nAbstract\nI will describe a technique for defining various weak higher structures by exten ding type theory with a universe of strict polynomial monads. Furthermore \, I will describe implementation of the proposed theory in Agda using rew rite rules.\n LOCATION:https://researchseminars.org/talk/HoTTEST2020/9/ END:VEVENT BEGIN:VEVENT SUMMARY:Michael Shulman (University of San Diego) DTSTART:20200619T160000Z DTEND:20200619T170000Z DTSTAMP:20260409T094011Z UID:HoTTEST2020/10 DESCRIPTION:Title: Type-theoretic model toposes\nby Michael Shulman (University of S an Diego) as part of The HoTTEST conference of 2020\n\n\nAbstract\nStartin g with the Awodey-Warren interpretation of identity types by path objects and Voevodsky's model of univalence in simplicial sets\, various kinds of Quillen model categories have been used to interpret homotopy type theory. A "type-theoretic model topos" is a Quillen model category that is optim al for this purpose in many respects. On one hand\, it has sufficient str ucture to interpret essentially all of "Book" HoTT\, including in strict u nivalent universes and most higher inductive types. On the other hand\, i t is sufficiently general that any Rezk-Lurie-Grothendieck (∞\,1)-topos can be presented by a type-theoretic model topos. This talk will sketch t he definition of type-theoretic model topos and the proofs of these facts\ , including some variations of the definition that apply to models of cubi cal type theory.\n LOCATION:https://researchseminars.org/talk/HoTTEST2020/10/ END:VEVENT END:VCALENDAR