Abstract: 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.

Abstract: 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.