Benedikt Ahrens
Benedikt Ahrens
+1 for `make_` +1 for fixing this issue as soon as possible On 26/11/2018 18:14, Langston Barrett wrote: > Don't forget the the |*pair| names, like |weqpair| and |iscontrpair|. >...
The guidelines that you suggest sound very good to me; classifying a piece of commented-out code according to them might not be straightforward. NB: Recovering deleted code from a repository...
@peterlefanulumsdaine @DanGrayson Thanks for your work on this PR so far. I would like to suggest using the easier installation route that @DanGrayson uses in https://github.com/UniMath/UniMath/pull/1437: 1. Install Coq via...
On 10/11/2018 09:20, Daniel R. Grayson wrote: > These definitions should be changed so the equations are part of the > property: > > |Definition isCokernel {x y z :...
On 10/11/2018 15:11, Daniel R. Grayson wrote: > Yes, but traditional practice in category theory tells both what it > means for a cone to be universal and what it...
On 12/11/2018 09:02, Daniel R. Grayson wrote: > The reason the second version below is clearer applies generally when > doing big diagram chases. Various parts of the diagram form...
@rmatthes : This issue seems to be resolved through your overhauling of monoidal categories - can you confirm?
On 18/01/18 14:27, Daniel R. Grayson wrote: > One of things about to go away, since it comes from Coq's init, is the > tactic "easy". I am very much...
Done in #876, closing.
@DanGrayson : what do you think about this issue? Its original goal was to allow the use of `-noinit`, which has been achieved. Another goal was then added to do...