cubical - version 0.9, compatible with Agda-2.8.0

What's Changed

• Add missing minus symbol by @LeeeeT in https://github.com/agda/cubical/pull/1207
• Add inducedFun for EM1 by @anshwad10 in https://github.com/agda/cubical/pull/1208
• Strict order equational reasoning by @LorenzoMolena in https://github.com/agda/cubical/pull/1203
• Remove duplicated lemma by @anshwad10 in https://github.com/agda/cubical/pull/1189
• Composition of left module homomorphisms by @mzhang28 in https://github.com/agda/cubical/pull/1176
• Formalize Theorem 7.2.2 in the HoTT Book by @anshwad10 in https://github.com/agda/cubical/pull/1180
• Five lemma by @mzhang28 in https://github.com/agda/cubical/pull/1166
• Fix makefile race condition by @pthariensflame in https://github.com/agda/cubical/pull/1210
• Add Rezk Completion by HIT by @anshwad10 in https://github.com/agda/cubical/pull/1188
• Fix typo indcuedHomEquivalence by @anshwad10 in https://github.com/agda/cubical/pull/1221
• Add Posetal Reflections by @anshwad10 in https://github.com/agda/cubical/pull/1191
• Decidable reachability for finite quivers by @stschaef in https://github.com/agda/cubical/pull/1198
• Rationals as localization by @anshwad10 in https://github.com/agda/cubical/pull/1220
• Membership relation by @anshwad10 in https://github.com/agda/cubical/pull/1217
• Do not use idfun for the typing annotation by @felixwellen in https://github.com/agda/cubical/pull/1223
• typo by @Freek98 in https://github.com/agda/cubical/pull/1225
• Rename lemma in boolean rings by @Freek98 in https://github.com/agda/cubical/pull/1227
• Theory of Symmetric Groups by @anshwad10 in https://github.com/agda/cubical/pull/1187
• WellFounded: Well-founded relations are irreflexive. by @shlevy in https://github.com/agda/cubical/pull/1158
• Define the downward and upward closure of a subset by @anshwad10 in https://github.com/agda/cubical/pull/1235
• CommAlgebras as CommRingHoms by @felixwellen in https://github.com/agda/cubical/pull/1145
• Define the category of posets by @anshwad10 in https://github.com/agda/cubical/pull/1232
• Strict monoidal categories are strict categories by @anshwad10 in https://github.com/agda/cubical/pull/1196
• Release for Agda 2.8.0 by @felixwellen in https://github.com/agda/cubical/pull/1222

New Contributors

• @LeeeeT made their first contribution in https://github.com/agda/cubical/pull/1207
• @LorenzoMolena made their first contribution in https://github.com/agda/cubical/pull/1203
• @mzhang28 made their first contribution in https://github.com/agda/cubical/pull/1176
• @pthariensflame made their first contribution in https://github.com/agda/cubical/pull/1210

Full Changelog: https://github.com/agda/cubical/compare/v0.8...v0.9

- Agda
Published by felixwellen 7 months ago

cubical - version 0.8, compatible with Agda-2.7.0.1

What's Changed

• (C ≃ᶜ C') ≃ (C ≡ C') for univalent categories by @marcinjangrzybowski in https://github.com/agda/cubical/pull/1091
• Simplify (and generalize) invElPropElimN by @MatthiasHu in https://github.com/agda/cubical/pull/1102
• move precategories to separate folder and rename to wild categories by @felixwellen in https://github.com/agda/cubical/pull/1103
• Well-orderings and Ordinals by @LuuBluum in https://github.com/agda/cubical/pull/1072
• Functorial qcqs-schemes by @mzeuner in https://github.com/agda/cubical/pull/1086
• Added transportIsoToPath and transportIsoToPath⁻ by @oisdk in https://github.com/agda/cubical/pull/1109
• elimGpd by @aljungstrom in https://github.com/agda/cubical/pull/1112
• Open subschemes by @mzeuner in https://github.com/agda/cubical/pull/1096
• Summary paper qcqs-schemes by @mzeuner in https://github.com/agda/cubical/pull/1113
• Update agda version table by @felixwellen in https://github.com/agda/cubical/pull/1114
• Normal form of FreeGroup by @marcinjangrzybowski in https://github.com/agda/cubical/pull/1099
• Algebraic geometry directory, take 2 by @mzeuner in https://github.com/agda/cubical/pull/1121
• Preorder structure on the category of subobjects by @rahulc29 in https://github.com/agda/cubical/pull/1115
• CW complexes, cellular homology + a lot more by @aljungstrom in https://github.com/agda/cubical/pull/1111
• Topological modalities by @awswan in https://github.com/agda/cubical/pull/1125
• Properties of the lifting functor by @mzeuner in https://github.com/agda/cubical/pull/1123
• Refactor and extend the path-graph by @felixwellen in https://github.com/agda/cubical/pull/1116
• Construct 'the' free wild category on a graph by @felixwellen in https://github.com/agda/cubical/pull/1117
• Simplify Embedding-into-hLevel→hLevel by @MatthiasHu in https://github.com/agda/cubical/pull/1107
• Clean up: Remove Foundation/Everything and outdated stuff by @felixwellen in https://github.com/agda/cubical/pull/1127
• Displayed Category Constructions by @stschaef in https://github.com/agda/cubical/pull/1108
• Simplify CartesianKanOps/FunExtEquiv using "interpolation" on I by @pi3js2 in https://github.com/agda/cubical/pull/1001
• Update summary file for qcqs-schemes paper by @mzeuner in https://github.com/agda/cubical/pull/1131
• Add Π-contractDom by @ncfavier in https://github.com/agda/cubical/pull/1132
• Simplify proof that cong ⟨_⟩ is injective on groups by @ecavallo in https://github.com/agda/cubical/pull/1134
• Add credit to @Schippmunk for Displayed by @ecavallo in https://github.com/agda/cubical/pull/1136
• Add a generic UARel lemma to prove EquivJ for groups by @ecavallo in https://github.com/agda/cubical/pull/1135
• Another minor universe level generalisation by @awswan in https://github.com/agda/cubical/pull/1138
• Containers (and W and M) by @stefaniatadama in https://github.com/agda/cubical/pull/1129
• Supply implicit argument for agda/agda#7390 by @andreasabel in https://github.com/agda/cubical/pull/1143
• Add comment on our notion of field by @felixwellen in https://github.com/agda/cubical/pull/1142
• Pi4S3 Paper by @aljungstrom in https://github.com/agda/cubical/pull/1151
• Add Boolean Rings by @Freek98 in https://github.com/agda/cubical/pull/1146
• Base change, sliced adjoints by @marcinjangrzybowski in https://github.com/agda/cubical/pull/1120
• (Displayed) Category Theory: Sections of displayed categories, Free Category 3.0 and UMPs are Props by @maxsnew in https://github.com/agda/cubical/pull/1149
• Minor fix: improved definition of whitehead products by @aljungstrom in https://github.com/agda/cubical/pull/1155
• Rework displayed category reasoning. by @jpoiret in https://github.com/agda/cubical/pull/1153
• Remove redundant clause for agda/agda#7496 by @szumixie in https://github.com/agda/cubical/pull/1156
• Connected CW complexes by @aljungstrom in https://github.com/agda/cubical/pull/1133
• Category of elements as a wild functor to CAT. by @anuyts in https://github.com/agda/cubical/pull/1160
• Fix compilation with agda/agda#7581 by @UlfNorell in https://github.com/agda/cubical/pull/1168
• fix incorrectly named isIsoToIso, add IsoToIsIso by @maxsnew in https://github.com/agda/cubical/pull/1173
• Indexed W-types: hlevel without univalence. by @anuyts in https://github.com/agda/cubical/pull/1172
• A few minor utility functions by @awswan in https://github.com/agda/cubical/pull/1174
• Another minor universe level generalisation by @awswan in https://github.com/agda/cubical/pull/1177
• Basic Order Theory by @LuuBluum in https://github.com/agda/cubical/pull/1154
• Remove duplicated factorial function by @anshwad10 in https://github.com/agda/cubical/pull/1183
• Fix missed rename of StrictPoset to Quoset by @LuuBluum in https://github.com/agda/cubical/pull/1185
• Move factorial from Cubical.Data.Fin.LehmerCode to Cubical.Data.Nat.Properties by @anshwad10 in https://github.com/agda/cubical/pull/1184
• Reduced homology of CW complexes by @loic-p in https://github.com/agda/cubical/pull/1175
• Devalapurkar & Haine by @Trebor-Huang in https://github.com/agda/cubical/pull/1157
• Prep for Agda 2.8.0: remove some spurious private by @andreasabel in https://github.com/agda/cubical/pull/1205
• Release for agda 2.7 by @felixwellen in https://github.com/agda/cubical/pull/1206

New Contributors

• @rahulc29 made their first contribution in https://github.com/agda/cubical/pull/1115
• @stschaef made their first contribution in https://github.com/agda/cubical/pull/1108
• @pi3js2 made their first contribution in https://github.com/agda/cubical/pull/1001
• @stefaniatadama made their first contribution in https://github.com/agda/cubical/pull/1129
• @Freek98 made their first contribution in https://github.com/agda/cubical/pull/1146
• @szumixie made their first contribution in https://github.com/agda/cubical/pull/1156
• @UlfNorell made their first contribution in https://github.com/agda/cubical/pull/1168
• @anshwad10 made their first contribution in https://github.com/agda/cubical/pull/1183

Full Changelog: https://github.com/agda/cubical/compare/v0.7...v0.8

- Agda
Published by felixwellen 9 months ago

cubical - version 0.7, compatible with Agda 2.6.4.1

What's Changed

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

New Contributors

• @owen-fool made their first contribution in https://github.com/agda/cubical/pull/1067
• @kesleta made their first contribution in https://github.com/agda/cubical/pull/1076
• @eqNat made their first contribution in https://github.com/agda/cubical/pull/1064

Full Changelog: https://github.com/agda/cubical/compare/v0.6...v0.7

- Agda
Published by felixwellen about 2 years ago

cubical - version 0.6, compatible with Agda 2.6.4

What's Changed

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

New Contributors

• @jpoiret made their first contribution in https://github.com/agda/cubical/pull/1007
• @choukh made their first contribution in https://github.com/agda/cubical/pull/1023
• @timorl made their first contribution in https://github.com/agda/cubical/pull/1028
• @ShreckYe made their first contribution in https://github.com/agda/cubical/pull/1029
• @phijor made their first contribution in https://github.com/agda/cubical/pull/1066

Full Changelog: https://github.com/agda/cubical/compare/v0.5...v0.6

- Agda
Published by felixwellen over 2 years ago

cubical - version 0.5, compatible with Agda 2.6.3

What's Changed

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

New Contributors

• @rwbarton made their first contribution in https://github.com/agda/cubical/pull/964
• @markrd-williams made their first contribution in https://github.com/agda/cubical/pull/970
• @smimram made their first contribution in https://github.com/agda/cubical/pull/990
• @cmcmA20 made their first contribution in https://github.com/agda/cubical/pull/1000
• @croos90 made their first contribution in https://github.com/agda/cubical/pull/1012
• @JonasHoefer made their first contribution in https://github.com/agda/cubical/pull/1011

Full Changelog: https://github.com/agda/cubical/compare/v0.4...v0.5

- Agda
Published by felixwellen over 2 years ago

cubical - version 0.4, compatible with Agda-2.6.2.2

What's Changed

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

New Contributors

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

Full Changelog: https://github.com/agda/cubical/compare/v0.3...v0.4

- Agda
Published by felixwellen about 3 years ago

cubical - version 0.3, compatible with Agda-2.6.2

- Agda
Published by mortberg over 4 years ago

cubical - version 0.2, compatible with Agda-2.6.1.3

- Agda
Published by Saizan almost 6 years ago