V9.0

What's Changed

• github754: make this test work again by @jdchristensen in #2104
• ImpredicativeTruncation: redo using universe annotations by @jdchristensen in #2103
• fix coqdoc warnings by @Alizter in #2108
• Idempotent ring elements by @Alizter in #2105
• add note about building documentation locally to STYLE.md by @Alizter in #2109
• chore: remove Cubical.v indexing file by @Alizter in #2111
• istrunc_self_implies_istrunc by @ThomatoTomato in #2112
• rename istrunc_inhabited_istrunc by @Alizter in #2119
• small style tweaks in Loops.v by @Alizter in #2120
• demote priority of cocartesian monoidal structure by @Alizter in #2117
• Better ring constructors by @Alizter in #2114
• more polymorphic terminal unit and initial empty by @Alizter in #2116
• ind_homotopy lemma for FreeAbGroup by @Alizter in #2113
• cleanup: make into aliases: easy -> done, now -> by by @Alizter in #2122
• lax monoidal functors by @Alizter in #2115
• Equivalence cleanups by @jdchristensen in #2124
• subgroup and ideal preimage, ideal extension by @Alizter in #2118
• Constant.v: variants without Funext; cleanups by @jdchristensen in #2126
• Sequential.v Cocone.v Monoidal.v: small fixes to comments by @jdchristensen in #2125
• Prove Yoneda-like result for paths, and required lemmas by @jdchristensen in #2129
• Matrix: use strip_reflections to avoid extra universe variables by @jdchristensen in #2130
• Minor fixes to Truncations/Core, Ideal, Bool, Empty by @jdchristensen in #2131
• [coq] Overlay for rocq-prover/rocq#18385 by @ejgallego in #1951
• chore: update nix flake by @Alizter in #2110
• move twist construction into its own file by @Alizter in #2132
• cleanup: unused tactics by @Alizter in #2133
• Naturality of coequalizer universal property w.r.t. functor_coeq by @gio256 in #2106
• introduce implicit arguments for sig_rec by @Alizter in #2137
• generalise nat_mod_one_l to nat_mod_lt by @Alizter in #2139
• reorganise finite sums (in abgroups) into their own file by @Alizter in #2140
• Minor cleanups by @jdchristensen in #2142
• Overture: replace comment about Funext class by @jdchristensen in #2141
• cleanup in FinNat by @Alizter in #2138
• Theorem 5.8.2 from the book: characterizations of identity types by @ThomatoTomato in #2143
• Add variants of transport_paths_FlFr by @Alizter in #2150
• double recursion for join by @Alizter in #2151
• cleanup in CayleyDickson and fix #2149 by @Alizter in #2152
• functoriality of span pushouts by @Alizter in #2145
• Path spaces of graph quotients, coequalizers, and pushouts by @ThomatoTomato in #2147
• Misc cleanups by @jdchristensen in #2154
• cleanup: remove Misc.v by @Alizter in #2157
• move NullHomotopy.v to Homotopy/ by @Alizter in #2158
• Injective Types by @doolster in #2153
• remove NullHomotopy from STYLE.md by @Alizter in #2160
• functor_coeq_idmap by @Alizter in #2162
• functoriality lemmas for sum by @Alizter in #2161
• mathclasses improvements (^ for group inverses) by @Alizter in #2159
• add and use more Join_ind lemmas by @Alizter in #2165
• add implicit arguments to FreeGroup_rec by @Alizter in #2167
• better induction principles for FreeProduct + cleanup by @Alizter in #2168
• add transport_paths_FFr and remove unused arg in transport_paths_FFlFFr by @Alizter in #2166
• Functoriality results for Colimits by @ThomatoTomato in #2170
• forall y, Decidable (x = y) is an hprop by @jdchristensen in #2169
• make maximal_subgroup a printed coercion by @Alizter in #2177
• add more usable group cancellation lemmas by @Alizter in #2176
• remove implicit arguments in trivial_subgroup and maximal_subgroup by @Alizter in #2175
• abgroup_group is a functor by @Alizter in #2174
• complete and organise grp_moveL_1M type lemmas by @Alizter in #2173
• improve normal subgroup lemmas by @Alizter in #2179
• add functoriality lemmas for pushout by @Alizter in #2163
• fix notations in subgroup lemmas by @Alizter in #2182
• trivial and maximal subgroup are normal by @Alizter in #2181
• conjugation of group elements by @Alizter in #2178
• Improve mapping out of a generated subgroup by @Alizter in #2180
• group unit lemmas by @Alizter in #2189
• improvements to trivial group by @Alizter in #2186
• some helpful lemmas for FreeGroup by @Alizter in #2183
• group of maximal subgroup of a group is iso to said group by @Alizter in #2187
• quotient by a trivial group by @Alizter in #2188
• some remaining exercises in Chapter 2 by @Theongck in #2190
• Defining properties of maxima and minima, lemmas for the take operation in lists, lists from sequences. by @thchatzidiamantis in #2192
• Commutators, commutator subgroups and three subgroups lemma by @Alizter in #2185
• lemmas about subgroup product by @Alizter in #2193
• maximal subgroups by @Alizter in #2194
• subgroup_group iso lemmas and all trivial subgroups are iso by @Alizter in #2195
• definition of simple group by @Alizter in #2196
• Misc cleanups to PathGroupoids, Equiv, HProp and BoundedSearch by @jdchristensen in #2198
• quotient is trivial iff subgroup is maximal by @Alizter in #2197
• Variants of decidable_exists_nat by @jdchristensen in #2199
• minor cleanups in Groups/ by @Alizter in #2200
• cleanups and improvements to lagrange by @Alizter in #2203
• image of a subgroup by @Alizter in #2201

New Contributors

• @doolster made their first contribution in #2153
• @thchatzidiamantis made their first contribution in #2192

Full Changelog: V8.20...V9.0