theories/Algebra/AbGroups/AbelianGroup.v | 2 1 + 1 - 0 !
theories/Algebra/AbGroups/Abelianization.v | 2 1 + 1 - 0 !
theories/Algebra/AbGroups/FreeAbelianGroup.v | 2 1 + 1 - 0 !
theories/Algebra/AbSES/Core.v | 6 3 + 3 - 0 !
theories/Algebra/Groups/Group.v | 2 1 + 1 - 0 !
theories/Algebra/Groups/Subgroup.v | 10 5 + 5 - 0 !
theories/Algebra/Rings/Ring.v | 3 1 + 2 - 0 !
theories/Algebra/Universal/Algebra.v | 6 3 + 3 - 0 !
theories/Algebra/Universal/Congruence.v | 6 3 + 3 - 0 !
theories/Algebra/Universal/Homomorphism.v | 2 1 + 1 - 0 !
theories/Algebra/ooGroup.v | 2 1 + 1 - 0 !
theories/Basics/Decidable.v | 4 2 + 2 - 0 !
theories/Basics/Overture.v | 8 4 + 4 - 0 !
theories/Basics/Trunc.v | 4 2 + 2 - 0 !
theories/Categories/Category/Core.v | 2 1 + 1 - 0 !
theories/Categories/Category/Morphisms.v | 2 1 + 1 - 0 !
theories/Categories/Functor/Attributes.v | 7 2 + 5 - 0 !
theories/Classes/interfaces/abstract_algebra.v | 179 67 + 112 - 0 !
theories/Classes/interfaces/canonical_names.v | 31 12 + 19 - 0 !
theories/Classes/interfaces/integers.v | 7 3 + 4 - 0 !
theories/Classes/interfaces/naturals.v | 7 3 + 4 - 0 !
theories/Classes/interfaces/orders.v | 90 37 + 53 - 0 !
theories/Classes/interfaces/rationals.v | 7 3 + 4 - 0 !
theories/Classes/interfaces/ua_algebra.v | 2 1 + 1 - 0 !
theories/Classes/interfaces/ua_congruence.v | 6 3 + 3 - 0 !
theories/Classes/interfaces/ua_setalgebra.v | 2 1 + 1 - 0 !
theories/Classes/theory/premetric.v | 19 6 + 13 - 0 !
theories/Classes/theory/ua_homomorphism.v | 4 2 + 2 - 0 !
theories/Classes/theory/ua_isomorphic.v | 4 2 + 2 - 0 !
theories/Classes/theory/ua_subalgebra.v | 2 1 + 1 - 0 !
theories/Colimits/Colimit.v | 5 1 + 4 - 0 !
theories/Diagrams/Cocone.v | 5 1 + 4 - 0 !
theories/Diagrams/Cone.v | 5 1 + 4 - 0 !
theories/Diagrams/DDiagram.v | 3 1 + 2 - 0 !
theories/Equiv/Relational.v | 4 2 + 2 - 0 !
theories/Factorization.v | 4 2 + 2 - 0 !
theories/Homotopy/CayleyDickson.v | 50 16 + 34 - 0 !
theories/Homotopy/ExactSequence.v | 4 2 + 2 - 0 !
theories/Homotopy/HSpace/Coherent.v | 6 3 + 3 - 0 !
theories/Homotopy/HSpace/Core.v | 7 3 + 4 - 0 !
theories/Limits/Limit.v | 5 1 + 4 - 0 !
theories/Modalities/Descent.v | 4 2 + 2 - 0 !
theories/Modalities/Modality.v | 4 2 + 2 - 0 !
theories/Modalities/ReflectiveSubuniverse.v | 16 8 + 8 - 0 !
theories/Pointed/Core.v | 2 1 + 1 - 0 !
theories/Sets/Ordinals.v | 20 7 + 13 - 0 !
theories/Spaces/No/Addition.v | 4 2 + 2 - 0 !
theories/Spaces/No/Negation.v | 2 1 + 1 - 0 !
theories/Spectra/Spectrum.v | 4 2 + 2 - 0 !
theories/Universes/DProp.v | 6 3 + 3 - 0 !
theories/WildCat/Adjoint.v | 4 2 + 2 - 0 !
theories/WildCat/Core.v | 12 6 + 6 - 0 !
theories/WildCat/Displayed.v | 18 9 + 9 - 0 !
theories/WildCat/DisplayedEquiv.v | 2 1 + 1 - 0 !
theories/WildCat/EquivGpd.v | 2 1 + 1 - 0 !
theories/WildCat/FunctorCat.v | 4 2 + 2 - 0 !
theories/WildCat/Monoidal.v | 7 2 + 5 - 0 !
theories/WildCat/NatTrans.v | 2 1 + 1 - 0 !
theories/WildCat/PointedCat.v | 8 4 + 4 - 0 !
theories/WildCat/TwoOneCat.v | 18 9 + 9 - 0 !
theories/WildCat/ZeroGroupoid.v | 6 3 + 3 - 0 !
61 files changed, 275 insertions(+), 398 deletions(-)

 fix compilation with coq/rocq 9.1