Niels van der Weide
Niels van der Weide
> > The sanity checks passed, but the build script failed with the message "Error: Universe inconsistency." I don't think I did anything strange. No error occurs when I run...
I use `Let` for abbreviations. I don't use it with arguments and I don't use it for stuff that is supposed to be opaque (I prefer `Local Lemma` for that)....
> I would like to attract attention to [my commit](https://github.com/UniMath/UniMath/commit/a8ce0401) that would need help from an expert in displayed categories - just to fix proof parts of a definition where...
> It is rather a request for comments. No conflict with #1391 envisaged. > > The main question: is it good to have two separate strands instead of first developing...
> It is a bit unfortunate that dialgebras have their characteristic equality oriented differently from the comma category of which they are a special case. Good point. Do you think...
> I think there is an easier way than directly work all the details out, as sometimes details could be too overwhelming. > > notice that completeness is just the...
> @nmvdw > > > Since the equalizer diagram is required to commute up to the setoid equality and since the setoid equality in `Cats` is natural isomorphism, I think...
That helped! Thank you
Should this page only contain publications that describe specific parts of UniMath/UniMath or also code not in UniMath/UniMath?
I think the truncation would be a counterexample. I will check that.