UniMath/UniMath issues and pull requests

#1397 - WIP: identifies developments that can be done with CAT

Pull Request - State: open - Opened by rmatthes about 3 years ago - 10 comments

#1349 - Move some files

Issue - State: closed - Opened by DanGrayson over 3 years ago - 2 comments

#1231 - simplify some proofs

Issue - State: open - Opened by DanGrayson over 5 years ago - 1 comment

#1228 - Implicit Arguments settings slow down Coq by a huge factor

Issue - State: open - Opened by benediktahrens over 5 years ago - 9 comments

#1220 - better name for proof irrelevance

Issue - State: open - Opened by DanGrayson over 5 years ago - 1 comment

#1186 - remove Circle.v

Issue - State: closed - Opened by DanGrayson over 5 years ago - 2 comments
Labels: pull request submitted

#1096 - Unify names of builder functions

Issue - State: closed - Opened by benediktahrens almost 6 years ago - 7 comments
Labels: code change - just do, good first issue

#1092 - duplication

Issue - State: closed - Opened by DanGrayson almost 6 years ago
Labels: pull request submitted

#1069 - Put headers into new files on bicategories

Issue - State: open - Opened by benediktahrens almost 6 years ago - 1 comment

#1067 - Move material on partially ordered sets to its own file

Issue - State: open - Opened by langston-barrett almost 6 years ago - 3 comments

#1064 - Check and fix notation levels in CT/Bicategories

Issue - State: open - Opened by benediktahrens almost 6 years ago - 2 comments

#1000 - setquot3

Issue - State: open - Opened by DanGrayson about 6 years ago - 2 comments

#984 - Reading Group Suggestions

Issue - State: closed - Opened by gilbo over 6 years ago - 5 comments

#980 - Upstream code on foundations and categories from UniMath/TypeTheory

Issue - State: closed - Opened by benediktahrens over 6 years ago - 4 comments
Labels: code change - just do, good first issue

#979 - Relative monads (and modules over them) should be formalized as functors with structure

Issue - State: open - Opened by benediktahrens over 6 years ago - 5 comments
Labels: code change - just do, good first issue

#968 - Activate all warnings

Issue - State: closed - Opened by benediktahrens over 6 years ago - 7 comments

#951 - Remove duplicates invmap_eq and pathsweq1

Issue - State: closed - Opened by langston-barrett over 6 years ago - 2 comments
Labels: good first issue

#947 - Remove duplicates weq_pathscomp0r and transitive_paths_weq

Issue - State: open - Opened by langston-barrett over 6 years ago - 4 comments
Labels: good first issue

#881 - useful notations

Issue - State: open - Opened by DanGrayson almost 7 years ago
Labels: code change - just do

#880 - notation declarations

Issue - State: open - Opened by DanGrayson almost 7 years ago - 1 comment

#873 - `map_on_two_paths` and `two_arg_paths` are the same modulo order of arguments

Issue - State: closed - Opened by benediktahrens almost 7 years ago - 1 comment
Labels: good first issue

#846 - po (preorders) should be renamed to PreOrder

Issue - State: open - Opened by Chgrau almost 7 years ago - 4 comments

#823 - On the definition of BinDirectSums (biproducts)

Issue - State: closed - Opened by mortberg almost 7 years ago - 7 comments

#805 - Host coqdoc documentation online

Issue - State: open - Opened by langston-barrett almost 7 years ago - 23 comments

#780 - a tool for asynchronous processing of proof files

Issue - State: closed - Opened by DanGrayson about 7 years ago - 3 comments

#765 - add links

Issue - State: open - Opened by DanGrayson about 7 years ago - 2 comments

#763 - rework Foundations

Issue - State: open - Opened by DanGrayson about 7 years ago - 25 comments

#686 - Capitalization

Issue - State: closed - Opened by vladimirias over 7 years ago - 7 comments

#664 - associativity of implication

Issue - State: open - Opened by DanGrayson over 7 years ago - 1 comment
Labels: code change - just do

#543 - revisit some proofs in CategoryTheory

Issue - State: closed - Opened by benediktahrens almost 8 years ago - 1 comment
Labels: code change - just do

#463 - company-coq

Issue - State: open - Opened by DanGrayson about 8 years ago - 1 comment
Labels: code change - just do

#412 - UniMath rules - automatic verification

Issue - State: open - Opened by vladimirias over 8 years ago - 2 comments

#400 - complicated `intros` patterns

Issue - State: open - Opened by DanGrayson over 8 years ago - 10 comments

#233 - Minimize dependencies

Issue - State: closed - Opened by benediktahrens about 9 years ago - 11 comments

#203 - decidable propositions

Issue - State: open - Opened by DanGrayson about 9 years ago - 1 comment
Labels: reorganization

#197 - Inductive type bool from Coq's Init.Datatypes

Issue - State: closed - Opened by benediktahrens about 9 years ago - 6 comments
Labels: code change - just do

#192 - Mirroring UniMath

Issue - State: closed - Opened by benediktahrens about 9 years ago - 2 comments

#191 - Backup of UniMath

Issue - State: open - Opened by benediktahrens about 9 years ago - 11 comments

#175 - free commutative monoids on X, implemented as unordered lists

Issue - State: closed - Opened by DanGrayson about 9 years ago

#139 - Colimits in HSET

Issue - State: open - Opened by vladimirias about 9 years ago - 7 comments
Labels: code change - just do

#100 - Vladimir update

Pull Request - State: closed - Opened by DanGrayson over 9 years ago - 2 comments

#99 - Changes to hnat and changes to functors_transformations

Pull Request - State: closed - Opened by vladimirias over 9 years ago - 2 comments

#98 - Some updates to hnat.v

Pull Request - State: closed - Opened by vladimirias over 9 years ago - 6 comments

#97 - Put opposite category in a separate file and minor changes

Pull Request - State: closed - Opened by mortberg over 9 years ago - 3 comments

#96 - Show that post-composition with f in a precategory is an equivalence iff pre-composition is

Issue - State: closed - Opened by benediktahrens over 9 years ago - 1 comment
Labels: code change - just do

#95 - added some comments about the two definitions of iso in a precategory

Pull Request - State: closed - Opened by benediktahrens over 9 years ago - 4 comments

#94 - For coq trunk unpatched

Pull Request - State: closed - Opened by DanGrayson over 9 years ago - 5 comments

#93 - Update Makefile

Pull Request - State: closed - Opened by mortberg over 9 years ago - 7 comments

#92 - Switch to Coq 8.5

Issue - State: closed - Opened by benediktahrens over 9 years ago - 46 comments

#91 - Issue 40.1

Pull Request - State: closed - Opened by DanGrayson over 9 years ago - 1 comment

#90 - Issue 40

Pull Request - State: closed - Opened by DanGrayson over 9 years ago - 5 comments

#89 - Fewer assumptions in constructions on functors and natural transformations

Pull Request - State: closed - Opened by benediktahrens over 9 years ago - 2 comments

#88 - Revert "changed parameters of type of natural transformations"

Pull Request - State: closed - Opened by benediktahrens over 9 years ago - 1 comment

#87 - Change "isaprop" to "isatruthvalue"

Issue - State: closed - Opened by vladimirias over 9 years ago - 31 comments

#86 - Coproducts

Pull Request - State: closed - Opened by benediktahrens over 9 years ago - 1 comment