This repository mainly contains material related to section 5 of the paper Formalising Yoneda Ext in Univalent Foundations (doi) which pertains to the long exact sequence of Ext groups. Our formalisation follows the proof of theorem XII.5.1 in Mac Lane's "Homology". The following is a brief overview of the files:

• Lemmas.v contains two general lemmas, and a proof that loops_abses is a group isomorphism along with related facts.
• EquivalenceRelation.v contains basic results we need about the equivalence relation generated from a relation
• ES.v contains the definition and basic theory of the type ES n whose quotient is Ext n
• HigherExt.v contains the definition of Ext n using ES.v
• XII_5.v contains the key lemmas (XII.5.3-5) which go into proving the long exact sequence; they are first proved on the level of ES n and then deduced for Ext n
• LES.v contains the proof of exactness of the long exact sequence

This version has been tested with Coq 8.16.1 against commit 3062f0a15 of HoTT-Coq from Feb 19, 2023.

1. Install Coq 8.16.1.

The can be done by first installing opam (see https://opam.ocaml.org/) and then running opam install coq. If the current version is no longer 8.16.1, then you need to run opam pin add coq 8.16.1 before the install command. (Though things may well work with a newer version of Coq.)

2. Build the Coq-HoTT library.

It will probably work to install the Coq-HoTT library through opam, as described here. If not, follow the instructions there for manually buildling the library, and use commit 3062f0a15 from Feb 19, 2023.

3. Clone and set up this repository.

Run git clone https://github.com/jarlg/Yoneda-Ext, then remove the second line of _CoqProject if you installed coq-hott via opam or change it to point to your local copy of the Coq-HoTT library if you built it manually.

4. Build this project by running make.

After make has finished, you can step through the various files using e.g. coqide or Emacs with Proof General.