Agda formalisation to accompany the paper ``Triangulating Context Lemmas" by Craig McLaughlin, James McKinna and Ian Stark.
Dependencies:
- Agda version 2.5.1, 2.5.2 or 2.5.3
- Agda standard library v0.12, v0.13 or v0.14
Agda 2.5.2 is compatible with GHC 8.0.2 and is available through the latest Long-Term Support release of the Haskell Tool Stack, with the following command line.
stack --resolver=lts-9.10 install Agda-2.5.2
The main results are summarised in triangulating-context-lemmas.agda.