Benedikt Ahrens
Benedikt Ahrens
We could try to set up alectryon for UniMath. The source of alectryon is at https://github.com/cpitclaudel/alectryon.
It would be great to have UniMath in jsCoq. The overall process is described in https://github.com/jscoq/jscoq/blob/v8.16/docs/build.md.
In a discussion during TYPES, @ppedrot suggested we could/should change our build system to allow the building in "stages". I have not understood what this means, and what we would...
We currently have ``` Definition idtoiso {C : precategory} {a b : ob C}: a = b -> iso a b. ``` but we should have ``` Definition idtoiso {C...
@jozefg wrote some code on Grothendieck universes, available at https://github.com/unimath2019-tt/UniMath/pull/1. Can it get merged into UniMath? @mortberg
People get massively confused over types from the standard library, such as `prod` (instead of UniMath's `dirprod`). This causes frustration over weird error messages at `Qed` time. We should not...
PR #1469 introduced some quite unreadable code with the goal of making UniMath available with the Coq development version. Once UniMath uses a Coq version with the modified coercion mechanism,...
VSCode seems to be emerging as the code editor of the future. It would be good to provide configuration files that make UniMath work with VSCode, similiar to how we...
The construction `smf_from_param_distr` in `ActionBasedStrongFunctorsMonoidal.v` is unsuited for use, since the proofs of properties are transparent. Similar for `parameterized_distributivity_nat_as_instance`.