WIP: On the comparison to book project on higher cats

[samtoth]

This is work on progress on authoring a tree comparing the progress of this library to the foudations presented by Cisinski, Cnossen, Nguyen and Walde in their book project on presenting higher categories

[samtoth]

I thought this might be a useful tree to have - in particular making this library more accessible for people less familiar with type theory/simplicial type theory.

@fredrik-bakke @UlrikBuchholtz (@markrd-williams ?) I thought this may be of use regarding the workshop at Mittag-Leffler as I think it is a reasonable long term goal to have their axioms formalised/accounted for in this library, and could provide a nice high level overview of the progress of the project in general.

At the moment I have just written a very quick draft of the axioms in the introduction of that book, but would like to invite your contributions; there are a few axioms where I think others would be in a much better place to comment than me, e.g. the 'functoriality of universals' and 'exponentiability' axioms. See comments in code for some more details.

Happy to provide tech support if needs be.

(it's moments like these where it would be nice to have a PR preview functionality...)

best,
Sam

[samtoth]

(it's moments like these where it would be nice to have a PR preview functionality...)

... The moment has arrived!!

http://agda-synthetic-categories.toth.co.uk/preview/83/tot-0002/index.xml

[fredrik-bakke]

Your link sends me to a 404 😂

[samtoth]

So it does

Edit: It seems the server has run out of storage 😩

[samtoth]

So it does

Edit: It seems the server has run out of storage 😩

Another insentive to address #121

[samtoth]

Your link sends me to a 404 😂

@fredrik-bakke Fixed now!