What's Changed
- Add missing minus symbol by @LeeeeT in #1207
- Add inducedFun for EM1 by @anshwad10 in #1208
- Strict order equational reasoning by @LorenzoMolena in #1203
- Remove duplicated lemma by @anshwad10 in #1189
- Composition of left module homomorphisms by @mzhang28 in #1176
- Formalize Theorem 7.2.2 in the HoTT Book by @anshwad10 in #1180
- Five lemma by @mzhang28 in #1166
- Fix makefile race condition by @pthariensflame in #1210
- Add Rezk Completion by HIT by @anshwad10 in #1188
- Fix typo
indcuedHomEquivalenceby @anshwad10 in #1221 - Add Posetal Reflections by @anshwad10 in #1191
- Decidable reachability for finite quivers by @stschaef in #1198
- Rationals as localization by @anshwad10 in #1220
- Membership relation by @anshwad10 in #1217
- Do not use idfun for the typing annotation by @felixwellen in #1223
- typo by @Freek98 in #1225
- Rename lemma in boolean rings by @Freek98 in #1227
- Theory of Symmetric Groups by @anshwad10 in #1187
- WellFounded: Well-founded relations are irreflexive. by @shlevy in #1158
- Define the downward and upward closure of a subset by @anshwad10 in #1235
- CommAlgebras as CommRingHoms by @felixwellen in #1145
- Define the category of posets by @anshwad10 in #1232
- Strict monoidal categories are strict categories by @anshwad10 in #1196
- Release for Agda 2.8.0 by @felixwellen in #1222
New Contributors
- @LeeeeT made their first contribution in #1207
- @LorenzoMolena made their first contribution in #1203
- @mzhang28 made their first contribution in #1176
- @pthariensflame made their first contribution in #1210
Full Changelog: v0.8...v0.9
Contributors
shlevy, mzhang28, and 7 other contributors