GitLab Commit is coming up on August 3-4. Learn how to innovate together using GitLab, the DevOps platform. Register for free: gitlabcommitvirtual2021.com

README.md 2.42 KB
Newer Older
Paolo Capriotti's avatar
Paolo Capriotti committed
1
2
3
4
5
6
7
8
9
10
11
12
## 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.
13

Paolo Capriotti's avatar
Paolo Capriotti committed
14
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.
15

Paolo Capriotti's avatar
Paolo Capriotti committed
16
17
18
19
20
21
22
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.
Paolo Capriotti's avatar
Paolo Capriotti committed
23

Paolo Capriotti's avatar
Paolo Capriotti committed
24
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.
25

26
27
28
29
30
31
### Structure of the formalisation

 - modules `segal.composition.l<k>`, 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<k>`, 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.