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