Releases · HoTT/Coq-HoTT

27 Sep 21:06

63a47b4

Summary

This update of the Coq-HoTT library brings together the culmination of much work over the last few months. Major additions include theory on bifunctors, monoidal categories, non-commutative rings, matrices, modules and general improvements to the algebra library. There was also a systematic effort to improve the definition and theory of various types such as Int, nat and list. Theory about divisibility and prime numbers was developed leading to a partially finished proof of the fundamental theorem of arithmetic.

New Contributors

@ThomatoTomato made their first contribution in #1991
@ndcroos made their first contribution in #2050

Full Changelog: V8.19...V8.20

What's Changed

(2,1)-cat structure for paths by @Alizter in #1902
better definition of monoidal 1-category by @Alizter in #1894
pointed truncation preserves products by @Alizter in #1906
more movement lemmas for WildCat/Equiv.v by @Alizter in #1914
cleanup and document Group.v by @Alizter in #1911
I-indexed coproducts in pType by @Alizter in #1907
Add missing coherences from WildCat/Paths.v to PathGroupoids.v by @Alizter in #1908
noncommutative rings by @Alizter in #1912
truncation level of lists by @Alizter in #1917
left R-module basics by @Alizter in #1916
coproduct-product inclusion map by @Alizter in #1919
cleanup lists by @Alizter in #1920
bifunctor improvements by @Alizter in #1925
Symmetric Monoidal Categories by @Alizter in #1915
Trick to make Is1Cat definitionally involutive by @jdchristensen in #1934
bump to dune 3.13 by @Alizter in #1910
opposite rings by @Alizter in #1940
cleanup Basics/ by @Alizter in #1942
shorter proofs of monoidal structure in Products.v by @Alizter in #1943
Monoidal: convenient naturality lemmas by @Alizter in #1944
rename cat_coprod_prod_incl -> cat_coprod_prod by @Alizter in #1946
Opposite pointed category by @Alizter in #1948
cleanup in AbGroups by @Alizter in #1949
Bool: add convenient variant of negb_ne by @Alizter in #1947
redefine Bifunctor by @Alizter in #1952
JoinAssoc: tiny fix to join_associator by @jdchristensen in #1955
WildCat: generalize a couple of proofs from Bifunctor.v to Prod.v by @jdchristensen in #1954
monoids and comonoids in a monoidal category by @Alizter in #1953
Prove coproduct type ap functoriality by @Theongck in #1960
move Int/ -> BinInt/ by @Alizter in #1962
abstract out some idioms for dealing with decidable types by @Alizter in #1956
finite sums of ring elements by @Alizter in #1959
more theory about lists by @Alizter in #1957
Prove that the universal property of pullback is an equivalence by @Theongck in #1966
Unary integers by @Alizter in #1964
chore: cleanup 8.11 compat by @Alizter in #1967
Matrix Rings by @Alizter in #1965
cleanup NatTrans.v by @Alizter in #1968
make opposite Is1Natural definitionally involutive by @Alizter in #1969
further coherence conditions for monoidal categories by @Alizter in #1970
fix notation warnings in 8.20 by @Alizter in #1972
subrings by @Alizter in #1971
finite sums and modules by @Alizter in #1975
left action on negation by @Alizter in #1974
injectivity of nat addition by @Alizter in #1973
more lemmas about matrix transpose by @Alizter in #1978
interaction of scalar and matrix multiplication by @Alizter in #1976
fix universes in Vector.v by @Alizter in #1980
theory of diagonal matrices by @Alizter in #1977
more theory about matrix traces by @Alizter in #1979
bump min version to 8.19 by @Alizter in #1985
[8.19] fix % in Arguments warnings by @Alizter in #1862
fix universes in list library by @Alizter in #1984
drop extra universe in istrunc_sigma by @Alizter in #1986
nix: add coq master to nix flake by @Alizter in #1989
chore(ci): update to checkout@v4 by @Alizter in #1990
fix universes in vector by @Alizter in #1987
Rings: remove some universe variables by @jdchristensen in #1993
More flexible WildCat.Paths instances by @Alizter in #1994
recommend coq-lsp over vscoq by @Alizter in #1996
1-Cat instance for MatrixCat by @ThomatoTomato in #1991
integer group powers by @Alizter in #1995
Make some WildCat.Path instances Global, and use them by @jdchristensen in #1997
fix nix flake by @Alizter in #1998
fix universes in Matrix.v by @Alizter in #1999
upper/lower triangular matrix rings by @Alizter in #1981
symmetric matrices by @Alizter in #2001
skew-symmetric matrices by @Alizter in #2002
comonoid objects in opposite category are monoids by @Alizter in #2004
invertible ring elements by @Alizter in #2005
add comment to Products.v by @Alizter in #2010
composed bifunctor instances by @Alizter in #2011
rename opposite initial/terminal instances by @Alizter in #2012
opposite monoidal categories by @Alizter in #2013
switch to Int in cring_Z by @Alizter in #2000
more on coproducts by @Alizter in #2014
drop HasEquiv instance by @Alizter in #2017
fix naming of monoidal instances in (co)products.v by @Alizter in #2018
right R-modules by @Alizter in #2019
free abelian groups by @Alizter in #2020
notations for left and right module actions by @Alizter in #2024
abgroup coequalizers by @Alizter in #2023
move SuccessorStructure.v over to using Int by @Alizter in #2027
consolidate injectivity predicate by @Alizter in #2025
fix induction principles for nat by @Alizter in #2026
remove IsUnitPreserving from GroupHomomorphism by @Alizter in #2029
tensor products of abelian groups by @Alizter in #2021
Minor updates to comments and whitespace by @jdchristensen in #2032
introduce Coeq_ind_hprop and use it by @Alizter in #2033
better looking terms in presentation test by @Alizter in #2031
revise definition of normal subgroup by @Alizter in #2030
ci: python -> python3 by @Alizter in #2036
Fix binding of type_scope to Sortclass by @Alizter in #2038
Cleanup of Nat.v part 1 by @Alizter in #2028
Use lemmas from Nat.Core in Colimits/Sequential instead of custom ones by @jdchristensen in #2039
Cleanup of Nat.v part 2 by @Alizter in #2040
EMSpace: every n-connected and (n+1)-truncated type is an EM space by @jdchristensen in #204...

Contributors

jdchristensen, Alizter, and 3 other contributors

Assets 2

26 Mar 10:34

Alizter

V8.19

1c3dd70

V8.19

Release Highlights

Yoneda lemma using 0-groupoids by @jdchristensen in #1745
HITs: fix inconsistencies from several HITs by @jdchristensen in #1758
Wildcat improvements by @jdchristensen in #1766
Associativity of Join, and lots more by @jdchristensen in #1768
Susp is a 1-functor; Join Bool A <~> Susp A; etc. by @jdchristensen in #1771
Naturality of join_assoc and trijoin_twist by @jdchristensen in #1783
wildcat: show Universe is a 2-cat by @Alizter in #1778
Join: prove unitors, triangle law, and hexagon law by @jdchristensen in #1784
trijoin_id_sym is natural; export more from HSpace/Core by @jdchristensen in #1786
2-cat of pointed types by @Alizter in #1795
Updates to EMSpace, Join/Core, HSpaces/* and other things by @jdchristensen in #1796
pHomotopy, pmap_postwhisker by @jdchristensen in #1797
1-category of successor structures by @Alizter in #1799
πₙ(Sⁿ) = Z, and other cleanups by @jdchristensen in #1800
CayleyDickson: some cleanups, remove funext by @Alizter in #1801
Add pmap_from_psphere_iterated_loops, and needed lemmas by @jdchristensen in #1803
wildcat: binary products by @Alizter in #1804
Make IsTrunc an inductive type by @jdchristensen in #1806
symmetry and associativity of products by @Alizter in #1813
A strengthening of Freudenthal's theorem for H-spaces by @jarlg in #1814
add prod_0gpd_corec by @Alizter in #1815
Hartogs: improve speed, reorganize by @jdchristensen in #1816
Truncatedness of pointed maps and pForall by @jdchristensen in #1819
New proof and generalization of Licata-Finster theorem by @jdchristensen in #1821
coproduct symmetry and associativity by @Alizter in #1828
Wedge of a family of pType by @Alizter in #1829
Displayed Wild Categories by @gio256 in #1832
flattening for pushouts + total space of Hopf construction by @Alizter in #1840
Colimits and Hopf: clean up and speed up by @jdchristensen in #1843
wedge projections by @Alizter in #1844
pinch map of suspension by @Alizter in #1845
functoriality of binary coproducts by @Alizter in #1847
characterize fiber of loop-susp counit by @Alizter in #1850
transport011: transport over 2 1-paths and lemmas about them by @Alizter in #1853
Flattening lemma for GraphQuotient by @Alizter in #1851
functoriality of GraphQuotient by @Alizter in #1856
flattening lemma for Coeq, Pushout and improvements to Hopf by @Alizter in #1857
Equivalences for displayed wild categories by @gio256 in #1859
add universe constraints in GraphQuotient by @Alizter in #1812
Improvements to make_equiv by @jdchristensen in #1869
Clean-ups to Spaces/Int/ and Spaces/Pos/ by @jdchristensen in #1870
Add instances isconnected_em' and is_minus_one_connected_pointed by @jdchristensen in #1871
Pointed/Core and Classes/theory/groups by @jdchristensen in #1872
HIT/quotient: fix universe variables, and uses in Classes by @jdchristensen in #1873
Generalize quotient_kernel_factor, and use it in Ordinals.v by @jdchristensen in #1874
Groups for a pointed wildcat, and other things about pointedness by @jdchristensen in #1876
redefine DPath as transport and cleanup proofs by @Alizter in #1880
Indexed products and coproducts by @gio256 in #1878
add missing coherence for TwoOneCat by @Alizter in #1897
Update bifunctors by @gio256 in #1886
[Chapter 1 Exercise] Solved by @MintChocoManju in #1901
functoriality of smash by @Alizter in #1892
Zero-groupoid universal property for coequalizers by @gio256 in #1900