BEGIN:VCALENDAR
VERSION:2.0
PRODID:researchseminars.org
CALSCALE:GREGORIAN
X-WR-CALNAME:researchseminars.org
BEGIN:VEVENT
SUMMARY:Peter LeFanu Lumsdaine (Stockholm University)
DTSTART;VALUE=DATE-TIME:20200615T143000Z
DTEND;VALUE=DATE-TIME:20200615T153000Z
DTSTAMP;VALUE=DATE-TIME:20240328T102022Z
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;VALUE=DATE-TIME:20200615T160000Z
DTEND;VALUE=DATE-TIME:20200615T170000Z
DTSTAMP;VALUE=DATE-TIME:20240328T102022Z
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;VALUE=DATE-TIME:20200616T143000Z
DTEND;VALUE=DATE-TIME:20200616T153000Z
DTSTAMP;VALUE=DATE-TIME:20240328T102022Z
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;VALUE=DATE-TIME:20200616T160000Z
DTEND;VALUE=DATE-TIME:20200616T170000Z
DTSTAMP;VALUE=DATE-TIME:20240328T102022Z
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;VALUE=DATE-TIME:20200617T143000Z
DTEND;VALUE=DATE-TIME:20200617T153000Z
DTSTAMP;VALUE=DATE-TIME:20240328T102022Z
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;VALUE=DATE-TIME:20200617T160000Z
DTEND;VALUE=DATE-TIME:20200617T170000Z
DTSTAMP;VALUE=DATE-TIME:20240328T102022Z
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;VALUE=DATE-TIME:20200618T143000Z
DTEND;VALUE=DATE-TIME:20200618T153000Z
DTSTAMP;VALUE=DATE-TIME:20240328T102022Z
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;VALUE=DATE-TIME:20200618T160000Z
DTEND;VALUE=DATE-TIME:20200618T170000Z
DTSTAMP;VALUE=DATE-TIME:20240328T102022Z
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;VALUE=DATE-TIME:20200619T143000Z
DTEND;VALUE=DATE-TIME:20200619T153000Z
DTSTAMP;VALUE=DATE-TIME:20240328T102022Z
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;VALUE=DATE-TIME:20200619T160000Z
DTEND;VALUE=DATE-TIME:20200619T170000Z
DTSTAMP;VALUE=DATE-TIME:20240328T102022Z
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