version 0.7, compatible with Agda 2.6.4.1

What's Changed

• ℤ-Functors by @mzeuner in #1068
• Whitehead's Lemma by @owen-fool in #1067
• CI: set heap size to 6G by @felixwellen in #1073
• CI: bump GHC to recommended version (9.4.7) by @andreasabel in #1075
• Generalized Universe Levels in 'substInPaths' by @kesleta in #1076
• Rational order by @LuuBluum in #1071
• Dependent Version of Bi-Invertible Equivalences by @kangrongji in #1062
• 'congR' and 'congL' by @eqNat in #1064
• funExt is an equivalence. by @smimram in #1070
• A direct proof of univalence from uaβ and uaη by @phijor in #1069
• Some recursive Fin functions by @dolio in #1077
• Bump cubical-utils to GHC 9.8 by @andreasabel in #1079
• opaque instead of abstract in QuotientAlgebra by @MatthiasHu in #1078
• Category of groups, uniqness of adjunctions by @marcinjangrzybowski in #1065
• Sites, sheaves and sheafification as a QIT by @MatthiasHu in #1031
• add proof that Sigma preserves null types by @awswan in #1085
• Remove redundant third constructor to replacement by @ecavallo in #1087
• Summary file/missing cohomology lemmas by @aljungstrom in #1092
• Triangular numbers by @felixwellen in #1044
• Placeholder for paper in progress by @aljungstrom in #1094
• Check all agda files by @felixwellen in #1058
• Induction principle for smash product by @aljungstrom in #1098
• Zariski coverage on CommRing^op by @mzeuner in #1082
• Refactor and improve CommRingSolver by @felixwellen in #1093
• Release for agda 2.6.4.1 by @felixwellen in #1083

New Contributors

• @owen-fool made their first contribution in #1067
• @kesleta made their first contribution in #1076
• @eqNat made their first contribution in #1064

Full Changelog: v0.6...v0.7

version 0.6, compatible with Agda 2.6.4

What's Changed

• Localization algebra by @jpoiret in #1007
• #1018: Note licence exceptions by @felixwellen in #1021
• Representable Presheaves, Free Category, Functor and Associated solvers by @maxsnew in #988
• Define displayed categories, functors, natural transformations, adjoints by @ecavallo in #986
• Make ∥∥-rec and ∥∥-elim more general by @choukh in #1023
• Type-theoretic replacement with higher induction-recursion by @ecavallo in #972
• Categorical bits and pieces by @jpoiret in #1008
• fix outdated comments in FreeCommAlgebra by @MatthiasHu in #1032
• simplify isSet by @MatthiasHu in #1033
• Improve definitional behavior of the category of elements by @jpoiret in #1024
• elimProp for the FreeCommAlgebra HIT by @MatthiasHu in #1035
• +Int≡+ by @timorl in #1028
• Add opcartesian fibrations by @jpoiret in #1026
• Some miscellaneous separated/stable type facts by @dolio in #1030
• Make variables names ∙∙_∙∙ consistent with those in doubleComp-faces and remove an unnecessary space by @ShreckYe in #1029
• remove isSet accessors by @MatthiasHu in #1040
• Avoid unnecessary syntax declarations by @MatthiasHu in #1038
• ·Int≡· by @timorl in #1039
• Introduce Semiring and refactor finite sums by @felixwellen in #1042
• Remove commutativity assumption to bigOpSplit++ by @jpoiret in #1045
• Renaming to Sequential Colimits by @kangrongji in #1047
• Mayer-Vietoris by @aljungstrom in #954
• #1015: CITATION.cff by @felixwellen in #1049
• NatSolver should be able to deal with 'suc's by @felixwellen in #1043
• Move Rationals around by @timorl in #1027
• Remove mentions of the Id type by @plt-amy in #1005
• Generalize types of inspect idiom by @dolio in #1041
• Ordering over Int by @LuuBluum in #985
• Ganea's theorem by @aljungstrom in #1055
• Reduced cohomology+Eilenberg-Steenrod axioms by @aljungstrom in #955
• Cardinality and Order by @LuuBluum in #969
• Filling Cubes in a Few Lines of Code by @kangrongji in #1053
• Fix a minor grammar mistake in Structure.agda by @ShreckYe in #1060
• Gysin by @aljungstrom in #965
• more connectivity lemmas by @rwbarton in #1063
• Direct proof of uaOver from Glue types by @phijor in #1066
• Release v0.6 for agda 2.6.4 by @felixwellen in #1050

New Contributors

• @jpoiret made their first contribution in #1007
• @choukh made their first contribution in #1023
• @timorl made their first contribution in #1028
• @ShreckYe made their first contribution in #1029
• @phijor made their first contribution in #1066

Full Changelog: v0.5...v0.6

version 0.5, compatible with Agda 2.6.3

What's Changed

• remove isTruncatedFun (duplicate of isOfHLevelFun) by @rwbarton in #964
• Affine schemes paper by @mzeuner in #966
• New rec for EM-spaces by @felixwellen in #968
• Closed Modality by @markrd-williams in #970
• Presheaves, BinProd, Elements, TwistedArrow, Constant by @anuyts in #872
• Add a 'beta' for the fundamental theorem of identity types by @felixwellen in #949
• Move $ from Reflection.Base to Foundations.Function by @ecavallo in #971
• Pi4S3 stuff by @aljungstrom in #974
• [ re agda/#6368 ] Add blanket instance for TypeWithStr by @jespercockx in #976
• Prepare for Agda 2.6.3 by @felixwellen in #948
• Simpler bool by @phadej in #981
• Make triangle identities in definition of unit-counit adjunction pointwise by @ecavallo in #980
• Add implicitFunExt⁻. by @smimram in #990
• Generalize funTypeTransp. by @smimram in #991
• swap the argument order in equational reasoning by @maxsnew in #999
• Refactor CI actions by @cmcmA20 in #1000
• Minor update allowing different universe levels in isPropIsPathSplitEquiv by @awswan in #984
• Add link to arXiv preprint of affine schemes paper by @mzeuner in #1003
• agda/agda#6663: Fix fst f → fst g in HopfInvariant by @plt-amy in #1006
• add Bool.elim by @maxsnew in #996
• Add isPropIsEquivOver. by @smimram in #993
• Add invIsoOver. by @smimram in #992
• connectivity of the induced map between joins by @rwbarton in #963
• Smash products - symmetric monoidal structure by @aljungstrom in #973
• Define submodules by @felixwellen in #967
• Lindenbaum-Tarski algebra by @croos90 in #1012
• Comparison lemma for distributive lattice by @mzeuner in #1013
• Add more results for inductively defined equality type by @JonasHoefer in #1011
• Remove cong′, duplicate of congS from Prelude by @ecavallo in #994

New Contributors

• @rwbarton made their first contribution in #964
• @markrd-williams made their first contribution in #970
• @smimram made their first contribution in #990
• @cmcmA20 made their first contribution in #1000
• @croos90 made their first contribution in #1012
• @JonasHoefer made their first contribution in #1011

Full Changelog: v0.4...v0.5

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 Int...

version 0.3, compatible with Agda-2.6.2

Update contributing guidelines wrt flags (#584)

* update guidelines

* oops

version 0.2, compatible with Agda-2.6.1.3

Added construction of M-types from Signatures/Containers (#245)

* Added construction of M-types from Signatures/Containers

* Added files

* No longer 'Unresolved Metas', but some postulates

* Removed trailing whitespace

* Fixed name collision

* Making progress on postulates

* Making progress on postulates

* removed whitespace

* Trying to fix computation problems

* Reduced shift definition, to pure iso's

* Fixed naming collsion (again...)

* Fixed naming collision (again...)

* Updated files to use iso more, and made proofs more readable

* Update

* Removed whitespace

* Update

* Small step towards removing all postulates.

* Update

* Finished proving lemma11-Iso

* All postulates cleared in M-types

* Pushed abstract

* Uncomment

* Working but with some 'abstract'

* Pushed abstract

* Updated to newest version of Cubical Agda

* Renamed some theorems

* Renamed some theorems

* Getting closer to removing all postulates

* Clared the last postulate for construction of M-types

* Updated folder structure

* Updated infrastructure

* Moved proofs

* Added missing files

* Working on pull request comments

* Working on pull request comments

* Working on pull request comments

* Restructure

* Restructure

* Restructure

* Updates based on PR comments

* Working on comments on PR

* Trying to simplify definition of shift

* Simplifying shift definition

* Working on PR comments

* Working on PR comments

* Working on PR comments

* Working on PR comments

* Working on PR comments

* Rename M-type to M, and moved files