Comments (51)
I usually use the MIT license:
https://github.com/mortberg/cubicaltt/blob/master/LICENSE
It gives people lots of freedom in using the software, but they still need to refer to the original authors.
from unimath.
This looks to me more suited for academic work than CC0. We can say Copyright (c) UniMath and/or we can use the names of the main contributors to each file.
On May 29, 2015, at 6:14 PM, mortberg [email protected] wrote:
I usually use the MIT license:
https://github.com/mortberg/cubicaltt/blob/master/LICENSE https://github.com/mortberg/cubicaltt/blob/master/LICENSE
It gives people lots of freedom in using the software, but they still need to refer to the original authors.—
Reply to this email directly or view it on GitHub #103 (comment).
from unimath.
A minor point: don't put "(c)" in copyright notices: it has no legal effect. Either use the word "copyright" or use the correct symbol ©; using both is okay but redundant.
from unimath.
Another point: "Copyright UniMath" won't work, for two reasons: the year is absent, and UniMath is not the owner of the rights. (UniMath isn't a person or a corporation.) See http://www.copyright.gov/circs/circ03.pdf
from unimath.
Did Bourbaki register their name in some way?
On May 29, 2015, at 7:31 PM, Daniel R. Grayson [email protected] wrote:
Another point: "Copyright UniMath" won't work, for two reasons: the year is absent, and UniMath is not the owner of the rights. (UniMath isn't a person or a corporation.)
—
Reply to this email directly or view it on GitHub #103 (comment).
from unimath.
The MIT license is nice, but I see no reason to include the disclaimer of warranty, since we aren't selling the product. See https://www.law.cornell.edu/ucc/2/2-315
from unimath.
The copyright in Bourbaki's Algebra was held by the publisher: https://archive.org/stream/ElementsOfMathematics-AlgebraPart1/Bourbaki-ElementsOfMathematicsAlgebraPart1#page/n5/mode/2up
from unimath.
Yes, but everybody cited Bourbaki. Can we make sure that everybody will be citing UniMath? Because individual authorship of the code will deteriorate very soon as more and more of us edit and improve each others code.
On May 29, 2015, at 7:51 PM, Daniel R. Grayson [email protected] wrote:
The copyright in Bourbaki's Algebra was held by the publisher: https://archive.org/stream/ElementsOfMathematics-AlgebraPart1/Bourbaki-ElementsOfMathematicsAlgebraPart1#page/n5/mode/2up https://archive.org/stream/ElementsOfMathematics-AlgebraPart1/Bourbaki-ElementsOfMathematicsAlgebraPart1#page/n5/mode/2up
—
Reply to this email directly or view it on GitHub #103 (comment).
from unimath.
To answer Benedikt's first question (Should all of UniMath be available under one license?): I think yes. We don't want people to have to read all the licenses attached to all the files, as it would be too painful.
from unimath.
Here's what we do about encouraging users to cite Macaulay2: http://www.math.illinois.edu/Macaulay2/Citing/
from unimath.
Here's how Singular encourages citation: http://www.singular.uni-kl.de/index.php/how-to-cite-singular.html
from unimath.
My goal is to make it eas{y,ier} to use the code for others, and to avoid bureaucratic hassle.
I chose CC0 for this reason, but if the MIT license is the freest option we can agree on, then that's fine with me for the sake of uniformity.
I like MIT's restriction to "substantial portions", and I like Dan's idea of removing the disclaimer.
from unimath.
Then let’s do the MIT license and maybe we can do something like the page for Macaulay2? I suggest that we start the list of authors in more or less historical sequence (which puts me first :)) and then it will expand as more people contribute. There can also be footnotes on at the names (as sometimes can be seen in journals like Nature on papers with many authors).
Vladimir.
On May 30, 2015, at 11:02 AM, Benedikt Ahrens [email protected] wrote:
My goal is to make it eas{y,ier} to use the code for others, and to avoid bureaucratic hassle.
I chose CC0 for this reason, but if the MIT license is the freest option we can agree on, then that's fine with me for the sake of uniformity.
I like MIT's restriction to "substantial portions", and I like Dan's idea of removing the disclaimer.—
Reply to this email directly or view it on GitHub #103 (comment).
from unimath.
I'll take a stab at an initial draft of a copyright notice and license agreement and let you take a look at it.
from unimath.
What about this?:
## UniMath license and copyright
The files in the various package subdirectories are mostly copyright as in the
following table; refer to individual files for any exceptions.
Package | Copyright
--------------- | --------------------------------------------------------------------------------
Foundations | Copyright 2015 Vladimir Voevodsky
RezkCompletion | Copyright 2015 Benedikt Ahrens
Ktheory | Copyright 2015 Daniel Grayson
PAdics | Copyright 2011 Alvaro Pelayo, Vladimir Voevodsky and Michael A. Warren
The following permission notice applies to all the files of UniMath; refer to
individual directories and files for any additional permissions.
Permission is hereby granted, free of charge, to any person obtaining a copy of
this software and associated documentation files (the "Software"), to deal in
the Software without restriction, including without limitation the rights to
use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies
of the Software, and to permit persons to whom the Software is furnished to do
so, subject to the following conditions:
The above copyright notice and this permission notice shall be included in all
copies or substantial portions of the Software.
from unimath.
And what about this for citing?
How to cite UniMath
If you use UniMath in a paper, please cite it. If you use latex, you may use
the following bibtex item.
@Misc{UniMath,
author = {Voevodsky, Vladimir and Ahrens, Benedikt and Grayson, Daniel and others},
title = {{\em UniMath}: {Univalent} {Mathematics}},
howpublished = {Available at \url{https://github.com/UniMath}}
}
Add this line to your preamble to provide the macro \url
.
\usepackage{hyperref}
from unimath.
Test it with foo.tex:
\documentclass{article}
\usepackage{hyperref}
\begin{document}
Refer to UniMath \cite{UniMath}.
\bibliographystyle{plain}
\bibliography{foo}
\end{document}
and foo.bib:
@Misc{UniMath,
author = {Voevodsky, Vladimir and Ahrens, Benedikt and Grayson, Daniel and others},
title = {{\em UniMath}: {Univalent} {Mathematics}},
howpublished = {Available at \url{https://github.com/UniMath}}
}
from unimath.
Here's the way the license would look when viewed on github (edited to remove the footnote example):
UniMath license and copyright
The files in the various package subdirectories are mostly copyright as in the
following table; refer to individual files for any exceptions.
Package | Copyright |
---|---|
Foundations | Copyright 2015 Vladimir Voevodsky |
RezkCompletion | Copyright 2015 Benedikt Ahrens, Chris Kapulkin, and Michael Shulman |
Ktheory | Copyright 2015 Daniel Grayson |
PAdics | Copyright 2011 Alvaro Pelayo, Vladimir Voevodsky, and Michael A. Warren |
The following permission notice applies to all the files of UniMath; refer to
individual directories and files for any additional permissions.
Permission is hereby granted, free of charge, to any person obtaining a copy of
this software and associated documentation files (the "Software"), to deal in
the Software without restriction, including without limitation the rights to
use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies
of the Software, and to permit persons to whom the Software is furnished to do
so, subject to the following conditions:
The above copyright notice and this permission notice shall be included in all
copies or substantial portions of the Software.
from unimath.
I just realized that another thing I dislike about the disclaimer paragraph in the MIT license is that it is in all caps, which has no legal significance.
from unimath.
This looks fine to me.
On May 30, 2015, at 5:29 PM, Daniel R. Grayson [email protected] wrote:
Test it with foo.tex:
\documentclass{article}
\usepackage{hyperref}
\begin{document}
Refer to UniMath \cite{UniMath}.
\bibliographystyle{plain}
\bibliography{foo}
\end{document}
and foo.bib:@misc{UniMath,
author = {Voevodsky, Vladimir and Ahrens, Benedikt and Grayson, Daniel and others},
title = {{\em UniMath}: {Univalent} {Mathematics}},
howpublished = {Available at \url{https://github.com/UniMath}},
year = {2015}
}
—
Reply to this email directly or view it on GitHub #103 (comment).
from unimath.
Hmm, maybe we want all those who copy UniMath to also copy the instructions about citing UniMath in papers.
from unimath.
Do you have any suggestions for initial footnote content? That way we would remember how to make footnotes, which I had to google to discover.
from unimath.
I don’t like this idea of many separate copyright holders. It is just not right and it will impend the development when one person works on a package started by another.
I would prefer things in the following order:
- To have UniMath as a registered entity that can hold the copyright.
- To have one of us (e.g. myself) to be the copyright holder for the whole library with the MIT license attached that requires to reproduce the notice where the name UniMath appears prominently while the name of the person who holds the copyright need not appear at all.
- To have all authors to be the copyright holders of the whole UniMath with the addition of new people as they contribute.
- To have it the way in which different packages have different copyright holders.
(There can and should of course be information about the main authors and smaller contributors as well as some info about the dates at the top of the individual files and in the package README’s).
On May 30, 2015, at 5:29 PM, Daniel R. Grayson [email protected] wrote:
Here's the way the license would look when viewed on github:
UniMath license and copyright
The files in the various package subdirectories are mostly copyright as in the
following table; refer to individual files for any exceptions.Package | Copyright
Foundations | Copyright 2015 Vladimir Voevodsky
RezkCompletion | Copyright 2015 Benedikt Ahrens
Ktheory | Copyright 2015 Daniel Grayson
PAdics | Copyright 2011 Alvaro Pelayo, Vladimir Voevodsky and Michael A. Warren
The following permission notice applies to all the files of UniMath; refer to
individual directories and files for any additional permissions.Permission is hereby granted, free of charge, to any person obtaining a copy of
this software and associated documentation files (the "Software"), to deal in
the Software without restriction, including without limitation the rights to
use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies
of the Software, and to permit persons to whom the Software is furnished to do
so, subject to the following conditions:The above copyright notice and this permission notice shall be included in all
copies or substantial portions of the Software.—
Reply to this email directly or view it on GitHub #103 (comment).
from unimath.
We may have a footnote on the names of Voevodsky, Ahrens and Grayson saying “Founding author of Foundations”, “Founding author of RezkCompletion”, “Founding author of Ktheory”. Or “founding author of and the main contributor to … “.
On May 30, 2015, at 5:48 PM, Daniel R. Grayson [email protected] wrote:
Do you have any suggestions for initial footnote content? That way we would remember how to make footnotes, which I had to google to discover.
—
Reply to this email directly or view it on GitHub #103 (comment).
from unimath.
The copyright owner of all the files in Foundations is of course also the author of the files, so the thing about founding author is implicit, and I don't need a footnote on my name.
We might want to keep the markup to a minimum, so the copyright notice is readable also in plain ascii.
from unimath.
Another issue is what to do about those who contribute amendments by github pull requests and additional code. One way would be to accept only minor pull requests that are accompanied by a release of their content into the public domain, so we can use it freely. For major ones only would we want to consider adding them to the list of authors.
from unimath.
I've just deleted the year from the bibtex entry, on the theory that UniMath will keep changing.
from unimath.
I did not mean a footnote at the copyright notice. Actually the whole idea of footnotes was not very relevant.
On May 30, 2015, at 5:57 PM, Daniel R. Grayson [email protected] wrote:
The copyright owner of all the files in Foundations is of course also the author of the files, so the thing about founding author is implicit, and I don't need a footnote on my name.
We might want to keep the markup to a minimum, so the copyright notice is readable also in plain ascii.
—
Reply to this email directly or view it on GitHub #103 (comment).
from unimath.
This sounds reasonable. Of course if someone submits many minor pull-requests he or she may also be added to the list of authors. How is it done with Coq or Agda?
On May 30, 2015, at 5:59 PM, Daniel R. Grayson [email protected] wrote:
Another issue is what to do about those who contribute amendments by github pull requests and additional code. One way would be to accept only minor pull requests that are accompanied by a release of their content into the public domain, so we can use it freely. For major ones only would we want to consider adding them to the list of authors.
—
Reply to this email directly or view it on GitHub #103 (comment).
from unimath.
A few comments:
- Core of RezkCompletion is authored by Ahrens, Kapulkin, Shulman
- Kapulkin and Shulman are ok with passing to MIT license
- Option 3 below is used by many free software projects. Advantage of
having many copyright holders is that it is difficult to change the
license, since for that all of the contributors would need to agree -
compare it to it being difficult to change a constitution.
Since the MIT license is very liberal, that does not impend further
development in case a contributor leaves, because a license once granted
cannot be revoked. However, a new contributor must agree to release
their contribution under the project's chosen license. - In analogy with a constitution, it is not a good idea to have just one
person holding the copyright.
On 05/30/2015 05:50 PM, Vladimir Voevodsky wrote:
I don’t like this idea of many separate copyright holders. It is just not right and it will impend the development when one person works on a package started by another.
I would prefer things in the following order:
- To have UniMath as a registered entity that can hold the copyright.
- To have one of us (e.g. myself) to be the copyright holder for the whole library with the MIT license attached that requires to reproduce the notice where the name UniMath appears prominently while the name of the person who holds the copyright need not appear at all.
- To have all authors to be the copyright holders of the whole UniMath with the addition of new people as they contribute.
- To have it the way in which different packages have different copyright holders.
(There can and should of course be information about the main authors and smaller contributors as well as some info about the dates at the top of the individual files and in the package README’s).
from unimath.
Re: "* In analogy with a constitution, it is not a good idea to have just one
person holding the copyright."
At least with a constitution, we can change it without getting permission from dead voters. Not so with a copyright.
from unimath.
I am fine with option n. 3 but I would like to check how it is done with projects such as Coq and Agda (e.g. with Coq standard library).
On May 31, 2015, at 11:20 AM, Benedikt Ahrens [email protected] wrote:
A few comments:
- Core of RezkCompletion is authored by Ahrens, Kapulkin, Shulman
- Kapulkin and Shulman are ok with passing to MIT license
- Option 3 below is used by many free software projects. Advantage of
having many copyright holders is that it is difficult to change the
license, since for that all of the contributors would need to agree -
compare it to it being difficult to change a constitution.
Since the MIT license is very liberal, that does not impend further
development in case a contributor leaves, because a license once granted
cannot be revoked. However, a new contributor must agree to release
their contribution under the project's chosen license.- In analogy with a constitution, it is not a good idea to have just one
person holding the copyright.On 05/30/2015 05:50 PM, Vladimir Voevodsky wrote:
I don’t like this idea of many separate copyright holders. It is just not right and it will impend the development when one person works on a package started by another.
I would prefer things in the following order:
- To have UniMath as a registered entity that can hold the copyright.
- To have one of us (e.g. myself) to be the copyright holder for the whole library with the MIT license attached that requires to reproduce the notice where the name UniMath appears prominently while the name of the person who holds the copyright need not appear at all.
- To have all authors to be the copyright holders of the whole UniMath with the addition of new people as they contribute.
- To have it the way in which different packages have different copyright holders.
(There can and should of course be information about the main authors and smaller contributors as well as some info about the dates at the top of the individual files and in the package README’s).
—
Reply to this email directly or view it on GitHub #103 (comment).
from unimath.
On 05/31/2015 07:55 PM, Vladimir Voevodsky wrote:
I am fine with option n. 3 but I would like to check how it is done with projects such as Coq and Agda (e.g. with Coq standard library).
I should have mentioned that I would also agree to option n. 1. But I
don't know how much effort it is to register such an entity.
Concerning the Coq copyright, you can have a look at the top directory
of the coq source tree, in particular file "COPYRIGHT":
The Coq proof assistant
Copyright 1999-2015 The Coq development team, INRIA, CNRS, University
Paris Sud, University Paris 7, Ecole Polytechnique.
This product includes also software developed by
Pierre Crégut, France Telecom R & D (plugins/omega and plugins/romega)
Pierre Courtieu and Julien Forest, CNAM (plugins/funind)
Claudio Sacerdoti Coen, HELM, University of Bologna, (plugins/xml)
Pierre Corbineau, Radboud University, Nijmegen (declarative mode)
John Harrison, University of Cambridge (csdp wrapper)
The file CREDITS contains a list of contributors.
The credits section in the Reference Manual details contributions.
The standard library seems to be the same, e.g., the header of
theories/Init/Datatypes.v is:
(*************************************************************)
( v * The Coq Proof Assistant / The Coq Development Team )
( <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 )
( \VV/ )
( // * This file is distributed under the terms of the )
( * GNU Lesser General Public License Version 2.1 )
()
from unimath.
Can we have the UniMath Team ?
On May 31, 2015, at 8:06 PM, Benedikt Ahrens [email protected] wrote:
On 05/31/2015 07:55 PM, Vladimir Voevodsky wrote:
I am fine with option n. 3 but I would like to check how it is done with projects such as Coq and Agda (e.g. with Coq standard library).
I should have mentioned that I would also agree to option n. 1. But I
don't know how much effort it is to register such an entity.Concerning the Coq copyright, you can have a look at the top directory
of the coq source tree, in particular file "COPYRIGHT":The Coq proof assistant
Copyright 1999-2015 The Coq development team, INRIA, CNRS, University
Paris Sud, University Paris 7, Ecole Polytechnique.This product includes also software developed by
Pierre Crégut, France Telecom R & D (plugins/omega and plugins/romega)
Pierre Courtieu and Julien Forest, CNAM (plugins/funind)
Claudio Sacerdoti Coen, HELM, University of Bologna, (plugins/xml)
Pierre Corbineau, Radboud University, Nijmegen (declarative mode)
John Harrison, University of Cambridge (csdp wrapper)The file CREDITS contains a list of contributors.
The credits section in the Reference Manual details contributions.The standard library seems to be the same, e.g., the header of
theories/Init/Datatypes.v is:(*************************************************************)
( v * The Coq Proof Assistant / The Coq Development Team )
( <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 )
( \VV/ )
( // * This file is distributed under the terms of the )
( * GNU Lesser General Public License Version 2.1 )
()—
Reply to this email directly or view it on GitHub #103 (comment).
from unimath.
... on the other hand, the license we currently have is permissive enough to allow almost everything, so it's hard to imagine that we would need to change something about it.
from unimath.
Re: "3. To have all authors to be the copyright holders of the whole UniMath with the addition of new people as they contribute."
It's easy to imagine new authors unwilling to cede copyright control over their contribution to the group as a whole. Indeed, I'm one, for I'm not copyrighting my code (see https://github.com/UniMath/UniMath/blob/master/UniMath/Ktheory/README.md).
from unimath.
It's interesting that someone can own the copyright of a collective work without owning the copyright of the individual components of the collection, see Section 201 at http://copyright.gov/title17/92chap2.pdf . Perhaps this can be used by us:
"(c) Contributions to Collective Works.—Copyright in each separate
contribution to a collective work is distinct from copyright in the collective work
as a whole, and vests initially in the author of the contribution. In the absence
of an express transfer of the copyright or of any rights under it, the owner of
copyright in the collective work is presumed to have acquired only the privilege
of reproducing and distributing the contribution as part of that particular collective
work, any revision of that collective work, and any later collective work
in the same series."
from unimath.
I suppose we can have the UniMath Team, but let's have the membership be public information, unlike the Coq Development Team, which seems to be opaque.
from unimath.
Sure.
On May 31, 2015, at 11:38 PM, Daniel R. Grayson [email protected] wrote:
I suppose we can have the UniMath Team, but let's have the membership be public information, unlike the Coq Development Team, which seems to be opaque.
—
Reply to this email directly or view it on GitHub #103 (comment).
from unimath.
Re: "I don’t like this idea of many separate copyright holders. It is just not right and it will impend the development when one person works on a package started by another."
How would having separate copyright holders impede development, so long as we receive from each copyright holder all the rights listed in our modified MIT license agreement? We'd be able to change and redistribute their code, and we'd be able to copyright the lines of code we add to their code.
from unimath.
Discussion on this topic seems to have died down. Shall we proceed to a final conclusion?
from unimath.
On 06/19/2015 07:36 PM, Daniel R. Grayson wrote:
Discussion on this topic seems to have died down. Shall we proceed
to a final conclusion?
Yes, that would be nice.
As mentioned before, I would be happy to have a unified license (e.g.,
MIT), with copyright holders being either some "organization" (whatever
that means) or all the contributors together.
from unimath.
I agree we should have a unified license for UniMath; the MIT license is fine. I suggest we permit individual components to have even more permissive licenses.
It's okay with me if UniMath is copyright as a collection of individual contributions, with the copyright holder held by an organization. I suggest that individual components could also be copyright or contributed to the public domain by individual authors, provided the licenses given by the authors to the organization are permissive enough; the copyright of the whole collection can be separate, as mentioned above.
I am yet to be convinced that it's a good idea for me to grant copyright in my code to an organization, since the rights I give to the whole world are so permissive that the organization will not be hindered in any way if I don't.
from unimath.
PS: Perhaps there is a good argument against having individual components with identifiable authors, as that makes one hesitant to move code around, blurring the boundaries of the components.
from unimath.
Yes, this was and remains my argument. I suggest one license (MIT license) for the whole of the UniMath and to have it copied to the subdirectories of each contribution.
I consider UniMath to be a piece of academic work and what worries me is not that we are not permissive enough but that people and groups of people will start copying code from uniMath and use it as their own without giving proper credit to the authors. This is what we should be worried about and that what we should work to avoid with licenses and with other means (such as timely publications of papers describing newly added sections of UniMath).
I do not want UniMath to be used for academic and administrative advancement by dishonest and incompetent people through claiming of our work for their own.
Vladimir.
On Jun 19, 2015, at 8:23 PM, Daniel R. Grayson [email protected] wrote:
PS: Perhaps there is a good argument against having individual components with identifiable authors, as that makes one hesitant to move code around, blurring the boundaries of the components.
—
Reply to this email directly or view it on GitHub #103 (comment).
from unimath.
Okay, I'm willing to go along with that.
from unimath.
On 06/20/2015 07:34 PM, Daniel R. Grayson wrote:
Okay, I'm willing to go along with that.
I am not quite sure what it means in practice: will we add an MIT
license notice on the top level of UniMath and a statement saying that
individual packages may come with more liberal conditions (refer to the
README of the individual packages)?
from unimath.
I'm willing to delete the notice about more liberal conditions from my
README, so
UniMath has a single unified license.
On Wed, Jun 24, 2015 at 8:32 AM Benedikt Ahrens [email protected]
wrote:
On 06/20/2015 07:34 PM, Daniel R. Grayson wrote:
Okay, I'm willing to go along with that.
I am not quite sure what it means in practice: will we add an MIT
license notice on the top level of UniMath and a statement saying that
individual packages may come with more liberal conditions (refer to the
README of the individual packages)?—
Reply to this email directly or view it on GitHub
https://urldefense.proofpoint.com/v2/url?u=https-3A__github.com_UniMath_UniMath_issues_103-23issuecomment-2D114850800&d=AwMCaQ&c=8hUWFZcy2Z-Za5rBPlktOQ&r=PAZ_jTPLrSb1btCfAu4RkycWe57N0sGyzbjgeOn2wN0&m=HjocIV0RsDK4XkHLZiRvX2Ugcuh36HgL0K57IyGqJdk&s=TGCze5zAay5WD4PugMLegHNeCNRagYX6ZGO-nwIRFIM&e=
.
from unimath.
On 06/24/2015 02:39 PM, Daniel R. Grayson wrote:
I'm willing to delete the notice about more liberal conditions from
my README, so UniMath has a single unified license.
Ok, I can do the same.
Would you mind preparing a PR in this vein?
from unimath.
Okay.
On Wed, Jun 24, 2015 at 8:42 AM Benedikt Ahrens [email protected]
wrote:
On 06/24/2015 02:39 PM, Daniel R. Grayson wrote:
I'm willing to delete the notice about more liberal conditions from
my README, so UniMath has a single unified license.Ok, I can do the same.
Would you mind preparing a PR in this vein?—
Reply to this email directly or view it on GitHub
https://urldefense.proofpoint.com/v2/url?u=https-3A__github.com_UniMath_UniMath_issues_103-23issuecomment-2D114854308&d=AwMCaQ&c=8hUWFZcy2Z-Za5rBPlktOQ&r=PAZ_jTPLrSb1btCfAu4RkycWe57N0sGyzbjgeOn2wN0&m=7BZAQcTJ7EnFS5TZ7sq9v7jGbSH32cjaq0XLp4iS2wQ&s=mojUEKGFyTmf3JKyY_Y-G-ogv6CvK4jx9oftC7ND8-s&e=
.
from unimath.
Resolved by #110
from unimath.
Related Issues (20)
- GrpdHITs currently not building over Coq dev HOT 3
- Should we replace `-type-in-type` with `Unset Universe Checking` in some way? HOT 21
- Commented material in `Foundations.NaturalNumbers` HOT 1
- A guide to new users on how to use UniMath
- Use access functions instead of projections in UniMath/Bicategories/Limits/Examples/LimitsStructuredCategories HOT 1
- Split the file DisplayedCats/BinProducts
- Beta-reduction for pairs is problematic
- New package: order theory HOT 10
- Get rid of UU : UU warning?
- Code should be reactivated [was: Compilation seems to hang at Qed.] HOT 9
- Using PathOver in definitions and constructions of displayed things? HOT 3
- Error `/bin/sh: Argument list too long` when doing `$ make install` HOT 13
- there are competing implementations of a full subcategory HOT 9
- how to keep track of which .v files of UniMath are being compiled?
- which version of Coq are we allowed to use? HOT 2
- Please pick the version you prefer for Coq 8.18 in Coq Platform 2023.10 HOT 4
- A warning HOT 4
- Defining objects, morphisms and categories separately or together HOT 3
- Error "Argument list too long" when running sanity checks HOT 3
- Who are contributors anonymous-1234567 and anonymous-13243557? HOT 3
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from unimath.