Michael Lindgren

I think this can be closed. Fixed by #950 and #952.

Can we try and merge master into this and see if it compiles with the recent changes to UniMath?

In a private repo / external to UniMath I have proof that every set is a filtered colimit of its K-finite subsets. I can maybe try to integrate it with...

@rmatthes In my suggestion `coq-unimath-substitution-systems` would depend on both `coq-unimath-bicategories` and `coq-unimath`, and that wouldn't require any changes, or am I missing something?

Completed by #1520.

This looks completed with #1507 to me, but I haven't looked closely. @rmatthes you did the hard work on this, is there anything left that needs to be done? If...

The main objections to this PR seems to have been that the material should be placed in `MoreFoundations` and not in `SyntheticHomotopyTheory` and if the proofs should be self-contained or...

Thanks to @Skantz for providing #1674 and #1653 building on #1643 `Coq.Init.Logic` is now removed from UniMath.

Cool that you're working on adding alectryon support, that is very welcome! So UniMath currently has two build systems in use, `dune` and `make` that work independently of each other....

> * Alectryon needs all of the files to be compiled passed to it, in the right order. So I think one way of doing this with dune would be...