PAdics does not compile at the moment. It should be adapted to compile with latest Coq/UniMath.
Some beautification would also be beneficial.

Anyone starting to work on this should comment in this issue, as to avoid duplication of efforts.

uu0a.v says, "Coconuses: spaces of paths which begin (coconusfromt) or end (coconustot) at a given point" . Why are these types called "coconuses"? Something to do with cocones?

In general, it'd be great to have a small comment explaining the etymology/motivation/purpose of each definition and theorem. I understand it's a lot of work, and teaching isn't necessarily an aim of the UniMath library, but it'd be a tremendous help to people trying to learn about it.

The current precedence levels are

Notation "g 'circ' f" := (funcomp f g) (at level 80, right associativity).

and

Notation "f ~ g" := (homot f g) (at level 70, right associativity).

Perhaps it would be better to give circ a smaller precedence level than ~, so that we can write, e.g.,

p circ s ~ idfun X

instead of

(p circ s) ~ idfun X.

There are comments in uuu.v saying:

"It contains some new notations for constructions defined in Coq.Init library as well as the definition of dependent sum as a record."

"One could use "Inductive" instead of "Record" here but using "Record" which is equivalent to "Structure" allows us later to use the mechanism of canonical structures with total2."

They give the impression that dependent sums will be defined as records. However the current definition of total2 uses Inductive, not Record. Perhaps these comments can be removed or corrected.

If the commit number recorded in UniMath for the submodule sub/coq
changes, and a user uses "git pull" to get that change, it may be that
"git submodule update ..." is required to update the submodule. If so,
add that to the top level Makefile somehow, in such a way that it doesn't
interfere with developers of UniMath who are trying to work with a different
commit of coq.

I have recently messed up a .package/files file in an attempt to avoid a Coq file being compiled by prepending the corresponding line with a hash.
Turns out that that does not work, leaving you with an ill-formed Makefile.
But then fixing the .packages/files should give you back a well-formed Makefile, which it doesn't - for this the helper file .coq_makefile_input would need to be recreated, which it does not seem to be.
make clean does not delete this file, nor does git clean (since it it listed in .gitignore).

I am not sure what the proper fix is - having a target depending on the .package/files files for the file .coq_makefile_input ?

The definition of a set-category should include the condition that the hom-types are sets.

I sugest we add a directory called Documentation (or something similar) and start by adding the pdf file from http://arxiv.org/abs/1401.0053 to it.

Suggestion: put Coq commands

• Proof
• Qed and
• Defined

on their own line.
Advantages:

• provides visual separation between statement (type) and proof (term).
• allows postprocessing of HTML to allow for collapsing and expanding of proofs. See for example
  https://benediktahrens.github.io/coinductives/html/Cat.Category.TriMat.Terminality.html
  for this feature

minusgeh0 is useless because every nat is ge 0.

Definition minusgeh0 ( n m : nat ) ( is : natgeh n m ) : natgeh ( n - m ) 0%nat.

See

https://github.com/UnivalentMathematics/Foundations/blob/master/Packages/Foundations/hlevel2/hnat.v#L636

can we replace "make coqbinaries" by something less, e.g., by
make coqbinaries && make tools ?

I have a branch where the condition of hom-types being sets is factored out, i.e. a precategory now has mor: ob -> ob -> UU. Hence an assumption (hs: has_homsets C) has to be added wherever necessary.
https://github.com/benediktahrens/UniMath/tree/hom-hset-explicit
Most constructions actually need that assumption of hom-types being sets; or at least I have not made an effort to do without. That makes the code a bit cumbersome.
Also, the definition of isomorphism is not the right one without that assumption, but I have not given another one yet.
I am not sure whether this change should go into UniMath.
On the other hand, the hom-set condition is part of a more general "saturation" condition, see https://github.com/benediktahrens/folds .
In that spirit, it would make sense to have it separated from the definition of a precategory.

I suggest to change all of the occurrences of "isaprop" throughout UniMath to "isatruthvalue".

This will make some things a little long - later we can come up with convenient abbreviation - tvalue?

I think it is philosophically correct to call types of h-level 1 truth-values (or even univalent truth-values as later we may also have strict truth values as types where all object are definitionally equal).

If set up correctly, Travis checks that pull requests do indeed compile, so that reviewing can focus on other aspects.

Some setup information is here:
http://docs.travis-ci.com/user/getting-started/
and looking at how it is done in HoTT
https://github.com/HoTT/HoTT
might also be useful.

as suggested by DG

... and record a few of them somewhere

Since Vladimir mentioned it in an email, I would like to suggest a couple more notations for UniMath.
I am using these notations in a formalization of FOLDS-categories in UF [1], based on UniMath.

Notation "∀ x .. y , P" := (forall x, .. (forall y, P) ..)
(at level 200, x binder, y binder, right associativity) : type_scope.
Notation "'Σ' x .. y , P" := (total2 (fun x => .. (total2 (fun y => P)) ..))
(at level 200, x binder, y binder, right associativity) : type_scope.
Notation "A × B" := (dirprod A B) (at level 80, no associativity) : type_scope.
Notation "X ≃ Y" := (weq X Y) (at level 80, no associativity) : type_scope.
Notation "x → y" := (x -> y)
(at level 90, y at level 200, right associativity): type_scope.
Notation "'λ' x .. y , t" := (fun x => .. (fun y => t) ..)
(at level 200, x binder, y binder, right associativity).
Notation "∥ A ∥" := (ishinh A) (at level 200) : type_scope.

An argument against Unicode notation is that inputting Unicode can be difficult, e.g., I have no clue how to get it to work using CoqIDE.

Any thoughts?

[1] https://github.com/benediktahrens/folds

The toggling of the display of proofs behaves miserably on my machine, for when the proofs
are hidden, many other parts of the page are hidden, too, if there's just one proof in
the file, such as Magma.v. Here's the view with proofs hidden:

And here's the view with proofs shown:

from what I understand, -Q only adds one directory to the search path under the given name, whereas -R adds the directory and all its subdirectories.

Maybe it would be safer to use -Q ?
As a consequence, Imports would always need to use the fully qualified name UniMath.Package.file, but we are doing this anyway.

This would allow having files of the same name in different packages without the risk of confounding them.

Goal: make the definitions and results of a file accessible to a new user without the user having to read the whole file.
Possible solution: use ssreflect's documentation style, as e.g. shown here:
http://ssr.msr-inria.inria.fr/doc/mathcomp-1.5/MathComp.poly.html
The beginning of the file explains the important constants of the file.
Improvement compared to shown example: In a comment, enclosing an identifier in brackets as in [ident] will turn it into a link in the html documentation. This allows jumping from the summary to the implementation of ident.

In uu0a.v, in the comment

"Note that we do no need [pathscomp0lid] since the corresponding
two terms are convertible to each other due to our definition of
[pathscomp0]. If we defined it by inductioning [q] and applying
[p] then [pathsinv0rid] would be trivial but [pathsinv0lid] would
require a proof."

I think [pathsinv0rid] and [pathsinv0lid] need to be replaced with [pathscomp0rid] and [pathscomp0lid], respectively.

Is it too early to think about switching to Coq 8.5?
Using the type-in-type flag (and -indices-matter), it should be possible to stick to vanilla Coq.
Maybe we should start a branch to gather some work towards that switch? It might take a while to adapt all the packages.

I suggest to create a branch of the UniMath called UniMath-edu (or something better) for the version of UniMath and of individual files of UniMath that are oriented towards teaching of UniMath and its style of formalization to mathematicians. There we will keep total2 to be an "Inductive", will avoid destruct (until a good explanation of the "match" to mathematicians can be found) etc.

On the main UniMath we will switch to total2 being a record, use primitive projections and start using canonical structures. Also on the main branch we will start using more advance features of Coq in the newer files (under the condition that the use of any such feature is explicitly described in the README of the corresponding directory!).

Having defined colimits let us define a finitary functor HSET -> HSET as follows.

1. For any functor F: C -> HSET and any functor G : HSET -> HSET define a function

colimcompare: colim ( F compose G ) -> G ( colim F ) .

1. Let

FromFinSub: FinSub X -> HSET be the obvious functor from the category of finite subsets of X to HSET.

Definition. isfinitary { C : precategory ) ( F : [ C , HSET ] ) : forall X : HSET , isweq ( colimcompare F ( FrromFinSub X ) ) .

1. Using colimits and FromFinSub it should be easy to define for any functor from finite sets to sets an extension to a functor from all sets to sets.
2. The function (3) and the obvious restriction function should provide an equivalence between the type of finitary functors from HSET to HSET and all functors from finite sets to HSET.

Paige has just compiled UniMath from scratch on MacOS 10.10, following the instructions in the README.
She had to

brew install ocaml camlp4 camlp5

rather than just

brew install ocaml 

Not having MacOS myself, I am reluctant to modify the installation instructions myself. Could you confirm and amend, if necessary?

I recalled the reason why I prefer to insert spaces around parenthesis as well as around all other strings:
when I want to replace throughout the text "i" with "n" (or some other similar replacement) as the name used for a variable of type nat, it is very easy to do when all uses of "i" as a complete name are surrounded by spaces and very inconvenient to do otherwise. This does not disallow using ((( and ))) but does exclude (i and i).

Add a target to the UniMath Makefile that builds coqide.

At least the fix from [1] will need to be incorporated.

[1] https://github.com/benediktahrens/substitution/blob/master/Makefile#L48

I.e., (xy)z would be xy*z* and x(yz) would be xyz**.

Implement such strings as functions (coprod (stn n) unit) -> X satisfying a certain condition, n:nat.

Do not assume X is a set.

I think the Arguments declaration for tpair in uuu.v is superfluous, because T is already declared implicit in the definition of total2. Perhaps it can be removed.

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 (a finite subset is defined as S : X -> hProp such that isfinite ( carrier S ) ) .

I have looked through it on paper and it seems to work.

There are several files which contain instances of terminal white space, i.e., white space after periods, etc. Perhaps these can be removed.

Those Requires might load the wrong module (aka file) when there are several modules (aka files) of the same name. This potential pitfall can probably be avoided by using "-I . UniMath" instead of "-R . UniMath", which would require all Requires to be fully qualified, as far as I understand.

For instance, fix

AffineLine.v:Require Import Utilities algebra1b funextfun GroupAction hz Integers Nat UniMath.Ktheory.Equivalences.
Circle.v:Require Import Utilities.
Equivalences.v:Require Import Utilities funextfun.
GroupAction.v:Require Import algebra1b funextfun Utilities UniMath.Ktheory.Equivalences.
Halfline.v:Require Import funextfun Utilities.
Integers.v:Require Import algebra1b funextfun Utilities total2_paths GroupAction hz.

In my last PR there is the usual uu0 and also four files uu0a uu0b uu0c and uu0d that are the result of separating uu0 into four parts for easier editing in the future.

I did not know how to change the Makefile to switch from the uu0 to these four files. I think we should do it and then continue the overhaul.

The files UniMath/*/.package/files specify a linear ordering of the *.v files in our formalization, crafted by hand, whereas "make" computes a partial ordering of the files based on dependencies. We should verify, in the Makefile, whether the two orderings are compatible.

(The linear ordering is used for making the TAGS file and for displaying line and word counts in the files.)

As far as I recall, total2 was, at some point, defined as a record type. At the moment, it is defined as an inductive type. (The comments in uuu.v still say that a record type is used.)
What was the reason for changing from record to an ordinary inductive?

If we switched back to total2 being defined as a record type, we could use the "Set Primitive Projections" option which, as @JasonGross told me, would provide significant speedup of compilation (at least it did for HoTT/HoTT).
It would also provide eta for dependent pairs, which might or might not be something we want.

Coqdoc wrongly pretty-prints the homotopy infix operator ~ as the negation symbol ¬ in the HTML documentation created by "make doc". Section 15.4.1 of the Coq manual says that this translation is specified by the current pretty-printing table. To correct it, it appears that one has to write

(** printing ~ #~# *)

or perhaps

(** remove printing ~ *)

in each file that uses the ~ notation.

I've submitted a bug report here: https://coq.inria.fr/bugs/show_bug.cgi?id=4275

Following from recent lectures based on UniMath, I feel that a good part of Foundations, and especially uu0.v, could benefit from the following superficial changes in syntax:

• Consistently replacing notations with the newly introduced set (@, =, !).
• Perhaps introducing a new notation f ~ g for homotopies between functions.
• Standardising the spacing in implicit and non-implicit arguments, e.g. (f : X -> Y) and { X Y : UU }, which may be slightly easier to read on a projector.
• Word-wrapping at 95 or 100 characters per line.
• Adhere to a stricter format of proofs, as exemplified in the example script in issue #33.

Here are some things I'd like to rename:

setwithbinop -> magma
invmaponpathsincl -> an_inclusion_is_injective
total2 -> totalSpace

I didn't know it before, but "magma" is used that way in Bourbaki's Algebra.

Does anyone else have proposals?

Can we agree on any of them?

I suggest to rename functors_transformations in RezkCompletion into functor_categories.

Licensing was mentioned in #102 - let's continue discussion here.
Some questions that might be considered:

• Should all of UniMath be available under one license?
• If so, which one?

The recursion principle for "identity" on the trunk has been weakened so that even our simplest
proofs by induction no longer work:

$ /usr/local/bin/coqtop
Welcome to Coq 8.4pl4 (June 2014)

Coq < Check identity_rect.
identity_rect
     : forall (A : Type) (a : A) (P : forall a0 : A, identity a a0 -> Type),
       P a (identity_refl a) -> forall (y : A) (i : identity a y), P y i


$ ~/src/HoTT/UniMath/sub/coq/bin/coqtop
Welcome to Coq 8.5beta1 (January 2015)

Coq < Check identity_rect.
identity_rect
     : forall (A : Type) (a : A) (P : A -> Type),
       P a -> forall y : A, identity a y -> P y

Starting from a fresh clone of the UniMath repository, typing "make" builds just "Coq", and
"make" must be run again to compile our files.

Someone should port omega (see http://coq.inria.fr/refman/Reference-Manual023.html) to unimath.

It would clean up hnat.v and my code considerably.

Implement free monoids on a set X as lists of elements in the set.

Implement lists as functions from standard finite sets to X, without assuming X is a set.

It is a good idea to start converting the files to use unicode. I've started that off
with #168 . There is more to do. I suggest assigning
the issue to yourself temporarily if you want to work on that, continuing with the rest of PartA.

uu0a.v has the comment

`We now define different homotopies and maps between the paths spaces corresponding to a weak equivalence. What may look like unnecessary complexity in the definition of weqgf is due to the fact that the "naive" definition, that of weqgf00 , needs to be corrected in order for lemma weqfgf to hold. '

The identifiers weqgf and weqgf00 don't seem to occur anywhere in the library, and can perhaps be removed.

Is there a book on homotopy theory or model categories that'd be good to keep in mind when reading the material on homotopy fibre triangles, fibration sequences, etc., in uu0a.v?

see http://www.conifersystems.com/whitepapers/gnu-make/ for justification