Vladimir Voevodsky

Uniformity

14

We need uniformity in naming. It is crucial. 1. Now we have four different ways of forming a name from two (or more) words. Let's say monoidfun can be named...

Obligatory use of the existing definitions

22

I suggest the following addition to our rules: 1. Formalizing a result or a group of results one must use the existing definitions wherever they are available. For example, if...

eqtohomot

4

What if we make eqtohomot a coercion to Funclass?

Colimits in HSET

7

1. To construct colimits of arbitrary functors C -> HSET (using setquot) 2. To construct, for any h-set X an isomorphism between X and the colimit of its finite subsets...

exists tactic

5

While this is a small thing, I would like to raise the following issue for discussion. The concept of "exist" in the UF corresponds to the propositional truncation of a...

Capitalization

7

I suggest that we rename all the .v files in UniMath/UniMath into starting with a small letter and subdirectories into starting with a capital. This way files, as seen in...

UniMath rules - automatic verification

2

We need a script that can be included in the checks that a new contribution must pass before being accepted that verifies at least some of the rules. To start...