Classically, derived functors are computed by projective or injective resolutions. For any ring R, the category of R-modules has enough projective and injective objects by the axiom of choice. However, this axiom is not assumed in Homotopy Type Theory (HoTT), preventing us from using the standard resolutions. Building upon earlier work by Yoneda and Buchsbaum, we present a constructive resolution-free approach to derived functors. Using this framework, we give a constructive derivation of Tor in HoTT.

A perennial question in type theory is how to do type theory within type theory. Rather than interpreting the syntax, which has proven very difficult even for simple type theories, one can attempt to internalize categorical models of type theory instead. We give a roadmap for formalizing the simplicial model of homotopy type theory (HoTT) inside HoTT, with particular emphasis on the first step: weak factorization systems and the small object argument.

Strong approximation is a technique in arithmetic geometry to find a k-point of a variety over a number field which is v-adically close to a finite number of local points. It is desirable to understand what the obstructions to strong approximation are and when they vanish. In this talk we will review several important concepts of strong approximation before then showing how one is able to extend these ideas from varieties to algebraic stacks. We will then apply these concepts to BG, the classifying stack of G-torsors, and see that the etale-Brauer-Manin obstruction is the only obstruction in this case.

Monodromy solving is the idea that for a parametrized polynomial system with a single known solution at a given parameter p, the other solutions can be found by tracking the solution along loops based at p. We extend this concept to the concept of fibre-preserving maps, and explore how adding in the option of tracking the solutions using fibre-preserving maps could help us make the algorithm faster.