unimath / unimath Goto Github PK
View Code? Open in Web Editor NEWThis coq library aims to formalize a substantial body of mathematics using the univalent point of view.
Home Page: http://unimath.org/
License: Other
This coq library aims to formalize a substantial body of mathematics using the univalent point of view.
Home Page: http://unimath.org/
License: Other
I've submitted a bug report here: https://coq.inria.fr/bugs/show_bug.cgi?id=4275
minusgeh0 is useless because every nat is ge 0.
Definition minusgeh0 ( n m : nat ) ( is : natgeh n m ) : natgeh ( n - m ) 0%nat.
See
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.)
At least the fix from [1] will need to be incorporated.
[1] https://github.com/benediktahrens/substitution/blob/master/Makefile#L48
I suggest to rename functors_transformations in RezkCompletion into functor_categories.
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.
Starting from a fresh clone of the UniMath repository, typing "make" builds just "Coq", and
"make" must be run again to compile our files.
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.
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.
Add a target to the UniMath Makefile that builds coqide.
Having defined colimits let us define a finitary functor HSET -> HSET as follows.
colimcompare: colim ( F compose G ) -> G ( colim F ) .
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 ) ) .
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?
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
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!).
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.
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.
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.
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 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).
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.
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 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).
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:
I have looked through it on paper and it seems to work.
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.
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.
see http://www.conifersystems.com/whitepapers/gnu-make/ for justification
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.
can we replace "make coqbinaries" by something less, e.g., by
make coqbinaries && make tools ?
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?
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.
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.
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?
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.
Suggestion: put Coq commands
on their own line.
Advantages:
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.
Licensing was mentioned in #102 - let's continue discussion here.
Some questions that might be considered:
as suggested by DG
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.
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.
The definition of a set-category should include the condition that the hom-types are sets.
... and record a few of them somewhere
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.
There are several files which contain instances of terminal white space, i.e., white space after periods, etc. Perhaps these can be removed.
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.
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.
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.
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.
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 ?
A declarative, efficient, and flexible JavaScript library for building user interfaces.
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google ❤️ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.