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 ofabstract
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