V9.1

What's Changed

• basics on homotopy cofibers by @Alizter in #2171
• Sequences, uniform structures by @thchatzidiamantis in #2210
• ci: fix permission issues in dev by @Alizter in #2212
• more on commutator subgroups by @Alizter in #2205
• Group: Make isunitpreserving_grp_homo opaque by @jdchristensen in #2218
• Misc fixes to comments, spacing and some proofs by @jdchristensen in #2216
• surjective_factor: cleanup by @jdchristensen in #2217
• HoTT.v: add (some) missing Exports by @jdchristensen in #2219
• Exercise 2.17: type formers respect equivalences and the coherences between proofs by @Theongck in #2220
• fix: change Warnings Append -> Warnings by @Alizter in #2221
• move Constant.v to Truncations/ by @Alizter in #2222
• move BoundedSearch.v to Misc/ by @Alizter in #2231
• Adapt to rocq#19987 by @Tragicus in #2223
• WildCat/Core: reduce is1cat_is1cat_strong to a hint to avoid loops by @jdchristensen in #2228
• generate_coqproject: remove duplicates from list of .v files by @jdchristensen in #2236
• Remove reference to now-patched bug by @patrick-nicodemus in #2237
• more transport_paths lemmas by @Alizter in #2232
• Exercises from Chapter 3 by @Theongck in #2242
• Change Global instances to #[export] by @patrick-nicodemus in #2239
• Remove all remaining Global Instances. by @patrick-nicodemus in #2244
• Replace *rapply, *refine and apply with exact when possible by @jdchristensen in #2245
• Join/Core, ImpredicativeTruncation: fix typos in comments by @jdchristensen in #2246
• Rings.v: add missing Exports by @jdchristensen in #2247
• Miscellaneous minor fixes by @jdchristensen in #2248
• Bundled categories by @patrick-nicodemus in #2238
• Alternate definitions of rapply by @patrick-nicodemus in #2241
• remove mention of travis in STYLE.md and replace with GitHub actions by @Alizter in #2251
• EMSpace: add #[export] to the instances by @jdchristensen in #2252
• reorganise transport_paths lemmas and add tests by @Alizter in #2253
• Spelling and style changes by @patrick-nicodemus in #2249
• nat: least common multiple by @Alizter in #2207
• chore: fix warnings in test/ by @Alizter in #2255
• Cleanup in ClassifyingSpace.v by @Alizter in #2213
• connectivity of wedge inclusion by @Alizter in #2211
• Elimination principles for GroupCoeq by @Alizter in #2184
• Add things related to suspensions and joins by @jdchristensen in #2259
• Typeclass hints by @patrick-nicodemus in #2254
• ci: fix docker-coq-action to 1.5.1 by @Alizter in #2268
• Clean annotations by @patrick-nicodemus in #2267
• cleanup some unused files by @Alizter in #2260
• Using new syntax for projection instance declarations by @patrick-nicodemus in #2263
• Make A and B implicit arguments in Build_{pMap,pEquiv,pEquiv'}; add/adjust bidirectionality hint & by @jdchristensen in #2270
• unboxed HasMorExt and IsUnivalent1Cat by @patrick-nicodemus in #2266
• Miscellaneous clean ups and fixes by @jdchristensen in #2275
• Make f and g explicit arguments to isequiv_compose by @jdchristensen in #2276
• Formalisation of bar induction axioms, first steps towards formalising the fan theorem and its consequences by @thchatzidiamantis in #2274
• Add and use concat_l, concat_r and concat_lr by @jdchristensen in #2277
• Improvements to Truncations/Core by @jdchristensen in #2278
• Connectivity by @jdchristensen in #2279
• Generalize lhs and rhs tactics to other relations by @jdchristensen in #2281
• Cofiber: add isconnmap_isconnected_cofiber, converse of isconnected_cofiber by @jdchristensen in #2280
• Miscellaneous improvements by @jdchristensen in #2282
• Adapt to rocq-prover/rocq#20601 by @proux01 in #2283
• Update Book.py by @CharlesCNorton in #2286
• Update coqcreplace.py by @CharlesCNorton in #2287
• Update INSTALL.md by @CharlesCNorton in #2289
• Add canonical morphism helpers to Objects.v by @CharlesCNorton in #2291
• Category/Objects: use path_contr by @jdchristensen in #2292
• Add zero objects infrastructure for stable categories by @CharlesCNorton in #2293
• Adapt to rocq-prover/rocq#20813 (Update default hypothesese names in generated schemes) by @dhalilov in #2294
• associativity of ideal product by @Alizter in #2121
• The wedge of n-connected types is n-connected by @jdchristensen in #2295
• Add transport lemmas for morphisms to Category/Core by @CharlesCNorton in #2299
• Various typo fixes in ci.yml by @CharlesCNorton in #2301
• typo fix: instutitions -> institutions by @CharlesCNorton in #2302
• Add "ghcup install cabal" to work around error by @jdchristensen in #2303
• [WIP] Add biproduct infrastructure for additive categories by @CharlesCNorton in #2300
• Various typo fixes by @CharlesCNorton in #2307
• Add results on compact and searchable types (mostly following Escardo), lemmas for HProps by @thchatzidiamantis in #2309
• Adapt to rocq-prover/rocq#20614 (induction finds registered schemes) by @SkySkimmer in #2311
• Add "From HoTT" before many "Require" commands by @jdchristensen in #2312
• chore: update nix flake by @Alizter in #2314
• don't depend on coq stdlib by @Alizter in #2297
• Changes for Rocq PR#21164 by @jdchristensen in #2318
• Miscellaneous small changes by @jdchristensen in #2319
• Briefly mention Rocq in INSTALL.md by @jdchristensen in #2321
• HSpaceS1: move Univalence assumption to just where needed by @jdchristensen in #2326
• Edit diagram in comments in Cubical/PathSquare.v by @marcbezem in #2327
• Cubical/PathSquare.v: edit diagram in comment + formulate interchange lemma by @marcbezem in #2325
• An interchange law for squares and cleanups to Cubical/PathSquare.v by @marcbezem in #2328
• SetoidRewrite: various cleanups and simplifications by @jdchristensen in #2329
• Adapt with respect to rocq-prover/rocq#21098 by @tabareau in #2331
• Adapt with respect to rocq-prover/rocq#21371 by @tabareau in #2332
• Wildcat pullbacks by @jdchristensen in #2333
• move SetoidRewrite to main library and other changes in preparation for diagram chasing by @jdchristensen in #2334
• AbEnriched: wild categories enriched in abelian groups by @jdchristensen in #2335
• EpiStable.v: categories in which one can do diagram chasing by @jdchristensen in #2336
• nix: update flake and rocq by @Alizter in #2337
• ci: bump minimal rocq version and improve ci by @Alizter in #2338
• chore: bump minimal rocq version by @Alizter in #2339
• Homological Algebra: Diagram chasing in practice by @ThomatoTomato in #2344
• opam: require >= 9.0, instead of >= 8.19.0 by @jdchristensen in #2347
• The wild category AbGroup satisfies IsAbEpiStable by @jdchristensen in #2346
• Update explanation of workarounds in WildCat/Equiv.v by @jdchristensen in #2349
• Adapt to rocq-prover/rocq#21852 by @proux01 in #2350
• Fix Proof command incorrectly used after tactic by @SkySkimmer in #2351
• Ltac2 by @jdchristensen in #2348
• Syllepsis: use Ltac2 for slight speed up; reverts #1628 by @jdchristensen in #2352
• Adapt to rocq-prover/rocq#21947 by @proux01 in #2353
• chore: put asymmetric patterns commands on separate lines by @Alizter in #2356
• chore: update nix flake by @Alizter in #2357
• chore: add .*.aux to makefile clean targets by @Alizter in #2360
• chore: add Rocq 9.2 to CI by @Alizter in #2359
• basics on perfect groups by @Alizter in #2214
• Adapt to Rocq#21180 by @Tragicus in #2315
• fix and update alectryon by @Alizter in #2340
• chore: HoTT.Tests -> HoTT_Tests, HoTT.Contrib -> HoTT_Contrib by @Alizter in #2342
• Basics/Settings: globally set "-notation-for-abbreviation" for now by @jdchristensen in #2361
• Updated BiInv.v and related files by @maxipetro in #2362
• README.md: point to documentation links on wiki; update URLs by @jdchristensen in #2366
• Minor cleanups to homotopy groups, etc by @jdchristensen in #2367
• Adapt to rocq-prover/rocq#21987 (destruct clears non section variable even when reusing a section variable's name) by @SkySkimmer in #2363
• Cleanups to Syllepsis.v by @jdchristensen in #2368
• prove twist hexagon in twist construction by @Alizter in #2135
• symmetric monoidal categories satisfy the other hexagon by @Alizter in #2191
• Add semi-additive categories infrastructure by @CharlesCNorton in #2305
• Add additive categories infrastructure by @CharlesCNorton in #2304
• Adapt to rocq-prover/rocq#22124 by @proux01 in #2370
• Modalities: generalize OO_conn_map_isconnected and other results by @jdchristensen in #2371
• Descent: strengthen OO_cancelL_conn_map ("if" dir of CORS 2.31) by @jdchristensen in #2372
• Connectedness: remove one universe variable from conn_point_incl by @jdchristensen in #2373

New Contributors

• @Tragicus made their first contribution in #2223
• @CharlesCNorton made their first contribution in #2286
• @dhalilov made their first contribution in #2294
• @tabareau made their first contribution in #2331
• @maxipetro made their first contribution in #2362

Full Changelog: V9.0...V9.1