Benedikt Ahrens
Benedikt Ahrens
On 22/04/2019 20:27, Daniel R. Grayson wrote: > This overrides the element of bool named "true": > > https://github.com/UniMath/UniMath/blob/10839eec83e48397b5544f249662d3b5d126b5cd/UniMath/CategoryTheory/SubobjectClassifier.v#L57 How about calling it `True` instead? Or is that too close?
In Circle2.v, the opposite effect happens: removing the local implicit argument settings, type-checking becomes very slow at `set (f := c p).` in ``` Theorem circle_induction : CircleInduction circle pt...
@DanGrayson : do you have any advice on this issue?
On 21/06/2019 17:11, Daniel R. Grayson wrote: > It has nothing to do with implicit arguments, as this code triggers it: > > |Require Import UniMath.Foundations.All. Require Import > UniMath.MoreFoundations.All....
When I do ``` Time Variables (X : circle → Type) (x : X pt). Time Variable (p : PathOver x x loop). ``` then the first is instantly, whereas...
On 23/06/2019 12:02, Daniel R. Grayson wrote: > I reported it as an issue in coq/coq#10421 > Thanks a lot!
It is completely unnecessary here. The construction becomes much smaller without destructing the pairs, since the proofs of the equalities do not need destructing the pairs when the functions are...
> Why do you need the long composition to compute? If you know the answer is a map f and can prove the answer is equal to the composition, then...
On 24/07/2019 15:31, Daniel R. Grayson wrote: > I'd be happy to rewrite the proofs of |weqtotal2dirprodassoc| and its > neighbors. They don't look very good, anyway. I filed a...
@siddharthist : would you be interested in upstreaming the category-theoretic part? I suggest merging your PR #955 first, and then you could replace, e.g., your composition-of-adj-eqs-is-adj-eq with the more general...