## Semi-Segal types and wild semicategories
A formalisation of the equivalence between (restricted) semi-Segal types and wild semicategories:
| level | semi-Segal | semicategory |
| ----- | ---------- | ------------ |
| 1 | edges | graph |
| 2 | triangles | transitive graph |
| 3 | tetrahedra | wild semicategory |
| 4 | 4-simplices | wild 2-semicategory |
A wild semicategory is a structure comprised of objects, morphisms and an associative composition operation. A wild 2-semicategory is a wild semicategory where the associator satisfies the pentagon identity.
A [browsable version](https://pcapriotti.gitlab.io/agda-segal) of the formalisation is available. This makes it possible to view the formalisation with complete syntax-highlighting and cross-referencing without having Agda installed on your machine.
Alternatively, the formalisation can be built with Agda 2.5.2 or 2.6.0. Since not many special features of Agda are used in this code, similar versions of Agda will likely work too. To build, run:
```bash
agda -i . README.agda
```
Note that the [`agda-base`](http://github.com/pcapriotti/agda-base) library is required. See [this page](http://agda.readthedocs.io/en/latest/tools/package-system.html) for instructions on how to install Agda libraries.
A note about the postulates contained in `agda-base`: besides the *univalence* axiom, core to HoTT, the only postulates are those related to inductive and coinductive types, such as homotopy-terminality of M-types and induction principles for higher inductive types. Those do not affect the present development, since it does not make use of (co)inductive types at all.
### Structure of the formalisation
- modules `segal.composition.l`, for `k = 1,2,3,4` contain the definitions of `k`-restricted *semi-Segal types* and wild `(k-2)`-*semicategories* and a proof of their equivalence;
- modules `segal.identities.l`, for `k = 1,2,3` contain the definitions of `k`-*degeneracy* and `k`-*identity* structures for semi-Segal types and wild semicategories respectively, and a proof of their equivalence;
- module `segal.univalence` contains a definition of *univalence* for wild precategories;
- module `segal.equivalences` is a summary of the notions and equivalences proved, and contains a definition of semi-Segal types with degeneracies (denoted `SegalDeg`) and wild precategories (denoted `WildId`), and their equivalences.