In this article the author endows the functor category [B(Z2),Gpd] with the structure of a type-theoretic fibration category with a univalent universe using the so-called injective model structure. It gives us a new model of Martin-Löf type theory with dependent sums, dependent products, identity types and a univalent universe. This model, together with the model (developed by the author in an other work) in the same underlying category together with the very same universe that turned out to be provably not univalent with respect to projective fibrations, provides an example of two Quillen equivalent model categories that host different models of type theory. Thus, we provide a counterexample to the model invariance problem formulated by Michael Shulman.
In this paper we give an algorithmic description of Freyd categories that subsumes and enhances the usual approach to finitely presented modules in computer algebra. The upshot is a constructive approach to finitely presented functors that only relies on a few basic algorithms.
We construct Quillen equivalent semi-model structures on the categories of dg-Lie algebroids and $L_\infty$-algebroids over a commutative dg-algebra in characteristic zero. This allows one to apply the usual methods of homotopical algebra to dg-Lie algebroids: for example, every Lie algebroid can be resolved by dg-Lie algebroids that arise from dg-Lie algebras, i.e. that have a null-homotopic anchor map. As an application, we show how Lie algebroid cohomology is represented by an object in the homotopy category of dg-Lie algebroids.
We develop the theory of weak Fraisse categories, where the crucial concept is the weak amalgamation property, discovered relatively recently in model theory. We show that, in a suitable framework, every weak Fraisse category has its unique limit, a special object in a bigger category, characterized by certain variant of injectivity. This significantly extends the known theory of Fraisse limits.