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