issues
search
HoTT
/
Coq-HoTT
A Coq library for Homotopy Type Theory
http://homotopytypetheory.org/
Other
1.23k
stars
185
forks
source link
issues
Newest
Newest
Most commented
Recently updated
Oldest
Least commented
Least recently updated
Idempotent ring elements
#2009
Alizter
opened
2 days ago
0
Prime numbers
#2008
Alizter
opened
2 days ago
0
Finite fields (Galois fields)
#2007
Alizter
opened
2 days ago
0
General Linear group
#2006
Alizter
opened
2 days ago
1
invertible ring elements
#2005
Alizter
closed
15 minutes ago
1
comonoid objects in opposite category are monoids
#2004
Alizter
closed
2 days ago
1
centrosymmetric matrices
#2003
Alizter
opened
2 days ago
0
skew-symmetric matrices
#2002
Alizter
closed
2 days ago
0
symmetric matrices
#2001
Alizter
closed
3 days ago
0
switch to Int in cring_Z
#2000
Alizter
opened
4 days ago
10
fix universes in Matrix.v
#1999
Alizter
closed
5 days ago
3
fix nix flake
#1998
Alizter
closed
5 days ago
2
Make some WildCat.Path instances Global, and use them
#1997
jdchristensen
closed
1 week ago
0
recommend coq-lsp over vscoq
#1996
Alizter
closed
2 weeks ago
2
integer group powers
#1995
Alizter
closed
2 weeks ago
9
More flexible WildCat.Paths instances
#1994
Alizter
closed
2 weeks ago
1
Rings: remove some universe variables
#1993
jdchristensen
closed
2 weeks ago
1
Z-module structure on abelian groups
#1992
ThomatoTomato
opened
3 weeks ago
7
1-Cat instance for MatrixCat
#1991
ThomatoTomato
closed
2 weeks ago
1
chore(ci): update to checkout@v4
#1990
Alizter
closed
3 weeks ago
0
nix: add coq master to nix flake
#1989
Alizter
closed
3 weeks ago
1
fix universes in vector
#1988
Alizter
closed
3 weeks ago
0
fix universes in vector
#1987
Alizter
closed
3 weeks ago
3
drop extra universe in istrunc_sigma
#1986
Alizter
closed
3 weeks ago
9
bump min version to 8.19
#1985
Alizter
closed
3 weeks ago
8
fix universes in list library
#1984
Alizter
closed
3 weeks ago
13
Define matrices as a collection of columns rather than a collection of rows
#1983
Alizter
opened
1 month ago
0
Define matrices as functions
#1982
Alizter
opened
1 month ago
2
upper/lower triangular matrix rings
#1981
Alizter
closed
3 days ago
16
fix universes in Vector.v
#1980
Alizter
closed
1 month ago
0
more theory about matrix traces
#1979
Alizter
closed
4 weeks ago
0
more lemmas about matrix transpose
#1978
Alizter
closed
1 month ago
0
theory of diagonal matrices
#1977
Alizter
closed
4 weeks ago
0
interaction of scalar and matrix multiplication
#1976
Alizter
closed
1 month ago
1
finite sums and modules
#1975
Alizter
closed
1 month ago
0
left action on negation
#1974
Alizter
closed
1 month ago
0
injectivity of nat addition
#1973
Alizter
closed
1 month ago
1
fix notation warnings in 8.20
#1972
Alizter
closed
1 month ago
0
subrings
#1971
Alizter
closed
1 month ago
0
further coherence conditions for monoidal categories
#1970
Alizter
closed
1 month ago
6
make opposite Is1Natural definitionally involutive
#1969
Alizter
closed
1 month ago
2
cleanup NatTrans.v
#1968
Alizter
closed
1 month ago
2
chore: cleanup 8.11 compat
#1967
Alizter
closed
1 month ago
0
Prove that the universal property of pullback is an equivalence
#1966
MintChocoManju
closed
1 month ago
0
Matrix Rings
#1965
Alizter
closed
1 month ago
4
Unary integers
#1964
Alizter
closed
1 month ago
15
Locator: Require can be combined again
#1963
Alizter
closed
1 month ago
0
move Int/ -> BinInt/
#1962
Alizter
closed
1 month ago
0
more opposite tests
#1961
Alizter
closed
1 month ago
0
Prove coproduct type ap functoriality
#1960
MintChocoManju
closed
1 month ago
1
Next