version 0.4, compatible with Agda-2.6.2.2

What's Changed

• Finitely presented algebras by @felixwellen in #582
• Fix ring solver (Issue #513) by @felixwellen in #530
• Syllepsis by @aljungstrom in #590
• Lattices and posets by @mzeuner in #593
• Use improved ringsolver by @mzeuner in #599
• Typo and consistent names by @HilpAlex in #586
• Emacs-lisp code for deleting whitespaces on save by @felixwellen in #588
• Delete --guardedness flag by @XiaohuWang0921 in #594
• Added uniqueness of initial and final objects by @kl-i in #601
• define plus to diffInt and prove diffInt is group by @hyleIndex in #603
• Add syntax typeclass for types with carriers. by @shlevy in #595
• More flexibel reflection solving by @felixwellen in #585
• Define spectra by @felixwellen in #589
• An n-type preservation property of pushouts by @felixwellen in #605
• Update naming convention by @felixwellen in #608
• Define the adjunction between suspension and loop by @ice1000 in #607
• fix merge conflict from ∙Susp → Susp∙ renaming by @ecavallo in #609
• If f is (n+1)-connected then cong f is n-connected by @ecavallo in #611
• Fixes for ZCohomology paper by @aljungstrom in #612
• Some modular arithmetic by @aljungstrom in #550
• Gysin sequence/Hopf invariant/Homotopy groups by @aljungstrom in #617
• Proof of Blakers-Massey Theorem by @kangrongji in #613
• Fundamental theorem of identity types by @felixwellen in #614
• Zariski Lattice by @mzeuner in #615
• Miscellaneous prelude cleaning by @ecavallo in #619
• Made the code compatible with the Agda branch issue4786 by @nad in #606
• Organize rings and commutative rings into categories by @mortberg in #618
• Combinatorics of Finite Sets by @kangrongji in #620
• [ testsuite ] turn off NoEquivWhenSplitting warning for make check by @Saizan in #627
• Clean category theory by @mortberg in #624
• Make library build with Agda 2.6.3-e2eb867 by @Saizan in #631
• Decouple Precategory from Category and use Category in the CT library by @mortberg in #629
• [ makefile ] added a build target for plain make without -W error by @Saizan in #639
• Add discrete categories by @barrettj12 in #638
• Add Ab as instance of category by @barrettj12 in #636
• Make the category C explicit by @barrettj12 in #634
• Poset and various lattice induced categories by @mortberg in #649
• Rename Obj -> Node and Hom -> Edge in Cubical.Data.Graph by @barrettj12 in #655
• Whitehead product by @aljungstrom in #640
• filled in an _ to please future Agda by @Saizan in #659
• Refactor pullbacks by @mortberg in #650
• Generalize binary set quotient operations + misc cleaning by @ecavallo in #660
• Category of categories by @barrettj12 in #642
• Quotient category by @barrettj12 in #653
• Add Hom as instance of AbGroup by @barrettj12 in #635
• Product of categories by @barrettj12 in #654
• Split initial and terminal objects into separate files and rewrite by @mortberg in #669
• Move FreeCommAlgebra by @felixwellen in #668
• Add instructions for getting make to work on Windows by @barrettj12 in #651
• Sheaves on distributive lattices by @mortberg in #671
• Clean up RingSolver and extract NatSolver by @felixwellen in #621
• Add initial commutative algebra by @felixwellen in #664
• Pointwise ring and algebra structure by @felixwellen in #667
• Add monoidal & enriched categories by @barrettj12 in #665
• Add (co)products by @barrettj12 in #637
• Good stuff from "Some finite limits" by @mzeuner in #679
• Terminal object and pullbacks in CommRings (i.e. trivial ring and fibered products) by @mortberg in #676
• Add transportComposite by @lpw25 in #681
• Html in gh-pages by @ice1000 in #687
• Refactor limits by @mortberg in #683
• Only htmlize on master branch by @ice1000 in #690
• Localization pullback by @mzeuner in #685
• Sheaf on a basis of a distributive lattice by @mzeuner in #692
• π₄(S³) ≅ π₃(S²×S² ← S²∨S² → S²) by @aljungstrom in #684
• Make cubical compatible with agda/agda#5716 by @L-TChen in #686
• [ ci ] Use the latest Agda but check cubical without NoEquivWhenSplitting warnings by @L-TChen in #697
• Revert "[ ci ] Use the latest Agda but check cubical without NoEquivWhenSplitting warnings" by @mortberg in #701
• Revert "Make cubical compatible with agda/agda#5716" by @mortberg in #702
• Small changes. by @xekoukou in #688
• Structure presheaf by @mzeuner in #699
• Clean the summary file for pi_4(S^3) = Z/2Z and prove two small general lemmas that were left as holes by @mortberg in #707
• Blakers Massey: Pushout-Pullback form by @aljungstrom in #704
• Long exact sequence of homotopy groups + Generator of π₃S² by @aljungstrom in #698
• Add 2 argument version of ua→ by @shlevy in #713
• π₄S³≡ℤ/2 by @aljungstrom in #715
• Clean the summary file by @mortberg in #716
• Don't claim cubical compiles with the latest agda development version by @felixwellen in #717
• Structure Sheaf on Basic Opens by @mzeuner in #728
• Polynomials over commutative rings added by @AkermanRydbeck in #714
• Some more helpful functions. by @xekoukou in #730
• remove obsolete definition of homotopy groups by @felixwellen in #725
• Terminal algebra by @felixwellen in #682
• Remove some unused imports by @MatthiasHu in #732
• A shorter definition of isHAEquiv.com-op by @howsiyu in #727
• Free Commutative Monoid by @guilhermehas in #719
• Cardinality and Quotients of Finite Sets by @kangrongji in #630
• Terminal objects in the categories of CommRings/Algebras by @mzeuner in #733
• Do not ask users to run make to install the library. by @Saizan in #696
• Dependent lists by @anuyts in #737
• Remove Product, which is a copy of BinProduct by @anuyts in #738
• Rijke Finite Types and the Number of Finite Groups by @kangrongji in #644
• Add 'debug' goal to GNUmakefile by @andreasabel in #744
• [ re #703, #743 ] Remove extend*Context by @L-TChen in #745
• Add direct sum by @thomas-lamiaux in #750
• Adding Nth-polynomials by @thomas-lamiaux in #740
• Maybe: elim. by @anuyts in #751
• Product of type-many categories by @anuyts in #739
• lookup for List and FinData. by @anuyts in #749
• Use CommIdeal everywhere by @felixwellen in #691
• Universal property of FreeCommAlgebra by @felixwellen in #678
• Compute free algebra on empty type by @felixwellen in #693
• Euclidean Algorithm and Bézout Identity for Integers by @kangrongji in #705
• Right Kan extension with an application to presheaves on DistLattices by @mzeuner in #735
• CommRing category is univalent and complete by @mortberg in #694
• Smith Normal Form by @kangrongji in #710
• Powers generating 1 by @mzeuner in #757
• Fix level-issue with Direct-sum : by @thomas-lamiaux in #758
• The Brunerie number is ±2 - direct proof by @aljungstrom in #741
• Abelianization of groups by @HilpAlex in #647
• Additive and abelian categories by @barrettj12 in #672
• General cohomology by @felixwellen in #723
• Grothendieck Groups of Commutative Monoids by @fabianmasato in #587
• Isomorphisms between hSets, isUnivalent SET by @marcinjangrzybowski in #734
• Improve and add a few path operators by @anuyts in #746
• fix ring solver README.md by @MatthiasHu in #762
• Naming convetion for universe levels by @felixwellen in #770
• Start working on some naming convention guidelines by @mortberg in #451
• Some useful transport results from the book by @Aqissiaq in #756
• Indexed W-types by @anuyts in #747
• MonoidSolver by @fabianmasato in #708
• Make the ring solver work in more situations by @felixwellen in #754
• Left adjoint functors preserve initial object. by @anuyts in #773
• Isomorphisms of precategories. by @anuyts in #768
• Computation of a simplified version of the Brunerie Number by @aljungstrom in #763
• Adding natural numbers defined by their associativity property by @guilhermehas in #720
• Internal monoids by @anuyts in #752
• Eliminators for Rationals HITQ by @guilhermehas in #766
• Re: #397 Modeling set theory by @WorldSEnder in #402
• Aspirational algebra naming conventions by @ecavallo in #775
• Monads, functor algebras, Eilenberg-Moore algebras by @anuyts in #764
• General Eilenberg-MacLane spaces (+ some theory) by @aljungstrom in #597
• Terminal Abelian category by @felixwellen in #695
• Some work related to countable types by @dolio in #514
• Define weak extensionality of a relation by @shlevy in #596
• Examples of finite presentations of CommAlgebra's by @felixwellen in #680
• Eilenberg-Moore adjunction by @anuyts in #772
• Contravariance of categories of algebras by @anuyts in #767
• James Construction (Only Basics) by @kangrongji in #718
• Update CI to use Agda v2.6.2.2 by @ecavallo in #778
• Create implementations for the Free Group and for the Bouquet types a… by @gmagaf in #721
• Rename RingSolver to CommRingSolver by @felixwellen in #777
• Free categories by @barrettj12 in #666
• Fix CI caching by @ecavallo in #780
• Work in progress on proving various things about equality as an inductive family by @mortberg in #309
• remove dependency on built-in pathToEquiv by @ecavallo in #782
• Issue #396: enforce import rules by @felixwellen in #783
• add caching of library build to CI by @ecavallo in #784
• Cohomology Rings by @thomas-lamiaux in #759
• Only htmlize on master branch, part II by @ecavallo in #787
• Fix ZGroup by @thomas-lamiaux in #786
• James Construction (Inductive Version) by @kangrongji in #722
• James Construction (Connectivity) by @kangrongji in #729
• Added ComMonoid instance of FreeComMonoid by @guilhermehas in #792
• Added Free Abelian Group by @guilhermehas in #793
• Adjoint: additional lemmas natural bijection. by @anuyts in #790
• Dl sheaves properly ordered by @mzeuner in #788
• Build cubical with latest Agda master (2022-05-09) by @andreasabel in #791
• Contravariance of Eilenberg-Moore category by @anuyts in #794
• Clean up library by @thomas-lamiaux in #789
• Remove an unnecessary argument in aurefl by @vikraman in #801
• Verification of Brunerie number computation by @aljungstrom in #802
• Update the summary file for pi_4(S^3) with the direct and computational proofs by @mortberg in #805
• Generalize universal property of quotient rings by @felixwellen in #809
• Describe kernel of ring and algebra quotient maps by @MatthiasHu in #816
• Added Field in Algebra by @guilhermehas in #797
• SIP for Fields by @kangrongji in #825
• ℚ is a Field by @kangrongji in #826
• Principal ideal quotient fp by @felixwellen in #818
• The abelianization of groups as a coequalizer of sets by @HilpAlex in #811
• Add non-dependent product special case to uarel automation by @ecavallo in #829
• More copatterns in Cubical.Algebra by @felixwellen in #821
• Write down our naming choices by @felixwellen in #834
• Upper natural numbers by @felixwellen in #602
• More induced structures by @mortberg in #827
• Enforcing the new algebra naming conventions for Algebraic Structures by @thomas-lamiaux in #824
• [ cosmetics ] Fix comments to address --two-levels by @ice1000 in #837
• Direct sum and gradedRing by @thomas-lamiaux in #798
• Rename, refactor, generalize one universe level by @felixwellen in #851
• FinVec is an instance of LeftModule by @guilhermehas in #850
• H-spaces and homogeneous types by @UlrikBuchholtz in #849
• Generalized an example for finitely presented algebra by @MatthiasHu in #852
• FinMatrix is an instance of LeftModule by @guilhermehas in #854
• Issue #831: move solvers by @felixwellen in #855
• Lookup & tabulate by @anuyts in #806
• Weak Equivalence between Categories by @kangrongji in #836
• Functor Category is Univalent if the Target Category is Univalent by @kangrongji in #839
• Some connectivity lemmas by @aljungstrom in #859
• Higher cohomology groups of real projective plane by @aljungstrom in #861
• markdown typo in NAMING.md by @MatthiasHu in #863
• Local rings by @MatthiasHu in #864
• abstractify QuotientAlgebra by @MatthiasHu in #857
• Cup product lemmas for CP2 by @aljungstrom in #862
• Simplify discreteSetQuotients by @MatthiasHu in #875
• Naive injectivity implies isEmbedding even if only B is a set by @MatthiasHu in #874
• Pulling back an equivalence relation along a function by @MatthiasHu in #876
• Freely pointed types by @MatthiasHu in #881
• Fin (suc n) ≡ Maybe (Fin n) by @MatthiasHu in #880
• Remove DecidableEq by @MatthiasHu in #866
• Dependent lists: mapOverSpan. by @anuyts in #878
• An Improvement for Cartesian Kan Operations by @kangrongji in #884
• Associativity of smash product by @aljungstrom in #860
• Characterization of Rezk Completion by @kangrongji in #841
• The Essential Image of Functor by @kangrongji in #842
• Rezk Completion by Yoneda Embedding by @kangrongji in #843
• Bump cabal version bound on base by @plt-amy in #890
• Clean up Cohomology Ring by @thomas-lamiaux in #845
• Image of a function by @felixwellen in #888
• Generalize some universe levels and add a function to pointwise algebra structure by @felixwellen in #889
• Remove redundant import by @Trebor-Huang in #901
• More on images by @felixwellen in #895
• A small lemma on equivalences by @felixwellen in #897
• Lemma on AlgebraEquivs by @felixwellen in #898
• clean up and comment RecordEquiv by @ecavallo in #893
• Ring properties of cup product by @aljungstrom in #869
• #885: Update README, inform about reviewing by @felixwellen in #887
• replace WithK with a file in Axiom containing statement and consequences of UIP/K by @ecavallo in #896
• Revert "Add syntax typeclass for types with carriers." by @felixwellen in #907
• generalize levels for some AlgebraHom operations by @MatthiasHu in #899
• List operations by @anuyts in #870
• Path operators by @anuyts in #807
• Examples for modalities by @MatthiasHu in #848
• Added FinWeak (isomorphic to Fin) by @guilhermehas in #867
• A Dependent Version of Univalence by @kangrongji in #900
• The Internal n-Cubes by @kangrongji in #902
• Cup product of klein bottle (Z coeffs) by @aljungstrom in #915
• Cubes in Path Type by @kangrongji in #903
• Filling Cubes and h-Level by @kangrongji in #904
• Dependent Cube Filling by @kangrongji in #909
• Add FreeCommAlgebra to 'Algebra.Polynomials' by @felixwellen in #918
• remove duplicate of Pushout.elimProp by @MatthiasHu in #923
• Cohomology (groups + cup product) + Klein bottle by @aljungstrom in #913
• Almost the structure sheaf property by @mzeuner in #920
• Lifting sheaves from the basis of a distributive lattice by @mzeuner in #877
• Alternative definition of the torus by @ncfavier in #912
• RP2 by @thomas-lamiaux in #847
• Cohomology Ring of S2 / S4 by @thomas-lamiaux in #879
• Algebra structure for UnivariateListPoly by @felixwellen in #916
• The FreeCommAlgebra on a coproduct of types by @felixwellen in #925
• Update install instructions by @felixwellen in #933
• Move and split FPAlgebra by @felixwellen in #924
• #930: Remove subtypePathReflection by @felixwellen in #935
• CP2 by @thomas-lamiaux in #846
• Cohomology Ring of the Klein Bottle by @thomas-lamiaux in #882
• H*(Kleinbottle,Z/2) by @aljungstrom in #928
• H*(RP2/S1, Z/2) by @thomas-lamiaux in #934
• Cohomology Ring of RP2 / S1 by @thomas-lamiaux in #883
• H*(RP²∨S¹,Z/2) by @aljungstrom in #936
• Add cohomology rings summary file by @apabepa10 in #937
• Added Unordered Pair by @guilhermehas in #891
• Graded commutativity of cup product by @aljungstrom in #938
• R is not zigzag complete if R<- and R-> are PERs. by @phadej in #940
• Allow nullification to take a family of types as input rather than just one type by @awswan in #939
• The Structure Sheaf by @mzeuner in #941
• Universal property of list-based polynomials by @felixwellen in #917
• X is a regular element in the ring of list-based polynomials by @felixwellen in #919
• Minor adjustment to universe level parameters and a correction by @awswan in #946
• Typevariate and list-based polynomials are isomorphic by @felixwellen in #922
• Quotient by sum of ideals by @felixwellen in #950
• Remove outdated comment by @felixwellen in #952
• Define profunctors and representability of profunctors in 2 ways by @maxsnew in #945
• Various functions that I found useful by @awswan in #951
• Add Nix flakes by @guilhermehas in #800

New Contributors

• @HilpAlex made their first contribution in #586
• @XiaohuWang0921 made their first contribution in #594
• @kl-i made their first contribution in #601
• @hyleIndex made their first contribution in #603
• @shlevy made their first contribution in #595
• @kangrongji made their first contribution in #613
• @barrettj12 made their first contribution in #638
• @lpw25 made their first contribution in #681
• @xekoukou made their first contribution in #688
• @AkermanRydbeck made their first contribution in #714
• @MatthiasHu made their first contribution in #732
• @howsiyu made their first contribution in #727
• @guilhermehas made their first contribution in #719
• @anuyts made their first contribution in #737
• @andreasabel made their first contribution in #744
• @thomas-lamiaux made their first contribution in #750
• @fabianmasato made their first contribution in #587
• @Aqissiaq made their first contribution in #756
• @gmagaf made their first contribution in #721
• @plt-amy made their first contribution in #890
• @Trebor-Huang made their first contribution in #901
• @ncfavier made their first contribution in #912
• @awswan made their first contribution in #939
• @maxsnew made their first contribution in #945

Full Changelog: v0.3...v0.4