Michael Lindgren

Create separate opam packages of UniMath.

2

Currently the opam package `coq-unimath` contains all of UniMath, except for the satellites. UniMath should offer smaller packages so that users don't have to compile everything to have access to...

WIP: Smarter cache management for CI.

4

This is a work in progress trying to make the cache management a bit smarter. Currently a PR can easily consume all 10 GB available because on each run the...

Have CI generate CONTENTS.md when a PR is merged

2

As I understand it the file `CONTENTS.md` is only used as a table of contents, linked from the main page of [UniMath](http://github.com/UniMath/UniMath/). It's very common to forget to commit these...

Restore EquivalencMonCatNonCurried.v

4

As part of refactoring monoidal categories (#1646 and originally #1644) , the material in [EquivalenceMonCatNonCurried.v](https://github.com/UniMath/UniMath/blob/70f0cd4e03cbc888b796bb0f6744f59956f8855a/UniMath/Bicategories/MonoidalCategories/UnivalenceMonCat/EquivalenceMonCatNonCurried.v) got commented out.

Remove dependency on Coq.Init.Logic

2

After merging #234 two files still unfortunately imports `Coq.Init.Logic`: - Initiality/Interpretation.v - TypeCat/General.v It's currently unclear to me if it's easy to fix or requires a more involved patch, so...