Vladimir Voevodsky

No, but it is not a duplication since we don’t have this concept anywhere else. Right? I am a little concerned with the use of the capital letter as a...

I doubt that we should be overly concerned with having too few contributions to UniMath. I am more worried that in a few years we will have too many and...

I guess so.

> But "given" is the English synonym for the tactic intro > What does this mean? > On Feb 21, 2017, at 9:02 AM, Daniel R. Grayson wrote: > >...

I am with Dan on this question. At the same time I think we should start prodding Matthew Sozeau to introduce a “transparent” for Qed. There is one additional reason...

The argument against opaque is that it does not solve the problem of slow code. I commented that this may be a signal that the code can be re-arranged to...

> which does not have any access You mean does not need to have any access? > On Jan 21, 2017, at 7:42 AM, Jason Gross wrote: > > I...

We made a lot of effort to make UniMath run on the of-the-shelf Coq and we certainly don’t want to get back to the state where we are on a...

This is not very surprising. In general, given P: A -> A -> Type such that forall a : A , iscontr ( { a’ : A | P a...

Why not to create a special section or sections where these issues will be discussed and move them from the introduction to these sections? Having something in the narrative and...