V8.20

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 #2041
• Cleanup of Nat.v part 3 by @Alizter in #2042
• Fix: proof of equiv_leq_lt_or_eq by @Alizter in #2043
• Nat: distributivity of multiplication over subtraction by @Alizter in #2049
• Added definition for cyclic' to AbGroups/Cyclic.v by @ndcroos in #2050
• Nat: basics on mod, div and divisibility by @Alizter in #2052
• Added proof for ab_mul_cyclic_in by @ndcroos in #2056
• Int: conversion lemmas with nat by @Alizter in #2055
• replace cyclic with cyclic' by @Alizter in #2053
• QuotientGroup: remove unused context variables and add comments by @jdchristensen in #2057
• Prime numbers by @Alizter in #2058
• Primes: division lemma for primes by @Alizter in #2061
• Functoriality of abelianization by @Alizter in #2064
• prime factorization by @Alizter in #2062
• Functoriality of FreeGroup by @Alizter in #2066
• add quotient cancelling and nat_mul divisibility monotonicty by @Alizter in #2063
• tensor preserves coequalizers by @Alizter in #2034
• Nat: theory about factorials by @Alizter in #2065
• doc: update INSTALL.md about opam and platform versions by @Alizter in #2047
• Nat: binomial coefficients by @Alizter in #2070
• update download-artifact: v3 -> v4 by @Alizter in #2076
• update README on editors by @Alizter in #2077
• ci: fix upload of documentation by @Alizter in #2078
• Basics on monoids by @Alizter in #2072
• free abelian groups take products to tensor products by @Alizter in #2068
• prove nat_div_div_r by @Alizter in #2074
• fix version of upload artifact in alectryon job by @Alizter in #2081
• Factorial: except for 0! = 1!, factorial is strictly monotone by @jdchristensen in #2082
• Work on issue #2015: grp_pow and related things by @ndcroos in #2071
• tensor product distributes over direct sum by @Alizter in #2079
• cleanup FreeProduct.v by @Alizter in #2083
• fix comment and simplify intros in Group.v by @Alizter in #2084
• Replace ab_biprod_corec_eta with grp_prod_corec_natural by @jdchristensen in #2085
• add lemma turning 0 < n -> n.+1 by @Alizter in #2086
• update nix flake to 8.20 by @Alizter in #2088
• STYLE.md: many updates throughout by @jdchristensen in #2090
• More STYLE.md updates by @jdchristensen in #2092
• localizations of commutative rings by @Alizter in #2089
• fix notations for 8.20 by @Alizter in #2087
• silence "From Coq" warning by @Alizter in #2095
• bump delete-artifact by @Alizter in #2097
• Misc cleanups to Overture, Colimits/Quotient by @jdchristensen in #2096
• Basics and Types cleanup by @jdchristensen in #2099
• Smallness by @Alizter in #1867
• Smallness: export in HoTT.v and rename a few things by @jdchristensen in #2101
• Remove emacs headers and put visual-line-mode in .dir-locals.el by @jdchristensen in #2102