Dennis

Add a (work in progress) package on model categories / weak factorization systems

10

This is still a bit of a work in progress. I am also not 100% sure it will compile yet in UniMath. Suggestions are welcome of course. There is one...

Coqdoc generation documentation and reduction

1

Hello, yesterday I was messing around trying to get the standard coqdoc HTML documentation to generate after contributing the ModelCategories package, and I was wondering what your procedure was, or...

Hi all, It seems that creating and initializing an IOC takes up a crazy high amount of memory when ran under sudo. This is not the case when ran as...

Recursive tagged unions fail to create serializer

2

Hello again, We have stumbled upon another interesting edge case: we are trying to load a model which has a self-referential tagged union. I made a small example that fails:...

Homogeneous element of tagged unions stops on first failure

2

So I have a model which contains a list of a tagged union. However, I would really like to have some sort of catch-all or failure whenever a tagged-union element...