Daniel R. Grayson
Daniel R. Grayson
That's pretty close. And something in Coq already has that name, though we don't use it. And I like to reserve capitalized identifiers for types.
`true_arrow` sounds good.
It looks like we can rather easily build UniMath using jscoq, but a procedure for getting it included in their distribution doesn't seem to be described at that link.
It has nothing to do with implicit arguments, as this code triggers it: ``` Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.SyntheticHomotopyTheory.Circle2. Section A. Context (circle_induction_function : ∏ (C...
I reported it as an issue in https://github.com/coq/coq/issues/10421
Why is relying on eta for pairs a problem?
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 the...
I'd be happy to rewrite the proofs of `weqtotal2dirprodassoc` and its neighbors. They don't look very good, anyway.
Let's not implement a change to the code without first agreeing on what it should be. It should be part of a comprehensive proposal about how identifiers should be named,...