Cubical Versions Save

An experimental library for Cubical Agda

v0.7

4 months ago

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

v0.6

7 months ago

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<SomeAlgebraicStructure> 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<AlgebraicStructure> 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

v0.5

11 months ago

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

v0.4

1 year ago

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

v0.3

2 years ago

v0.2

4 years ago