markwilliams @markwilliams@types.pl

Ext groups are fundamental objects from homological algebra which underlie important computations in homotopy theory. We formalise the theory of Yoneda Ext groups in homotopy type theory (HoTT) using the Coq-HoTT library. This is a constructive approach to Ext which does not require projective or injective resolutions. Using univalence, we show how these Ext groups can be naturally represented in HoTT. We give a novel proof and formalisation of the usual six-term exact sequence via a fibre sequence of 1-types (or groupoids), along with an application. In addition, we discuss our formalisation of the contravariant long exact sequence of Ext, an important computational tool. Along the way we implement and explain the Baer sum of extensions and how Ext is a bifunctor.
[https://arxiv.org/abs/2302.12678v1]

Last night I put up a new blog post on how you can build objects using category theory!

The adjoint functor theorems can let you show a functor is representable without needing to build the representing object by hand. This has pros and cons compared to building the object directly. We use tensor products as a case study:

https://grossack.site/2023/02/20/abstract-tensor-products.html

I have posts in the pipeline about 2-categories, clue, what ~are~ categories, and some topos case studies, so look forward to those too ^_^

@andrejbauer gave a very entertaining and thought provoking talk on all the “invisible” parts of a mathematical statement that human mathematicians implicitly fill in when communicating with each other, but which formal proof assistants can struggle with.

The #IPAM workshop on #MachineAssistedProofs (which I am the lead organizer of) starts in less than an hour: http://www.ipam.ucla.edu/programs/workshops/machine-assisted-proofs/ . As an experiment, I plan to make some occasional posts on the workshop as comments to this post. (UPDATE: the workshop has now concluded, and videos of the talks are available at https://www.youtube.com/@IPAMUCLA/videos .)