version 0.8, compatible with Agda-2.7.0.1

What's Changed

• (C ≃ᶜ C') ≃ (C ≡ C') for univalent categories by @marcinjangrzybowski in #1091
• Simplify (and generalize) invElPropElimN by @MatthiasHu in #1102
• move precategories to separate folder and rename to wild categories by @felixwellen in #1103
• Well-orderings and Ordinals by @LuuBluum in #1072
• Functorial qcqs-schemes by @mzeuner in #1086
• Added transportIsoToPath and transportIsoToPath⁻ by @oisdk in #1109
• elimGpd by @aljungstrom in #1112
• Open subschemes by @mzeuner in #1096
• Summary paper qcqs-schemes by @mzeuner in #1113
• Update agda version table by @felixwellen in #1114
• Normal form of FreeGroup by @marcinjangrzybowski in #1099
• Algebraic geometry directory, take 2 by @mzeuner in #1121
• Preorder structure on the category of subobjects by @rahulc29 in #1115
• CW complexes, cellular homology + a lot more by @aljungstrom in #1111
• Topological modalities by @awswan in #1125
• Properties of the lifting functor by @mzeuner in #1123
• Refactor and extend the path-graph by @felixwellen in #1116
• Construct 'the' free wild category on a graph by @felixwellen in #1117
• Simplify Embedding-into-hLevel→hLevel by @MatthiasHu in #1107
• Clean up: Remove Foundation/Everything and outdated stuff by @felixwellen in #1127
• Displayed Category Constructions by @stschaef in #1108
• Simplify CartesianKanOps/FunExtEquiv using "interpolation" on I by @pi3js2 in #1001
• Update summary file for qcqs-schemes paper by @mzeuner in #1131
• Add Π-contractDom by @ncfavier in #1132
• Simplify proof that cong ⟨_⟩ is injective on groups by @ecavallo in #1134
• Add credit to @Schippmunk for Displayed by @ecavallo in #1136
• Add a generic UARel lemma to prove EquivJ for groups by @ecavallo in #1135
• Another minor universe level generalisation by @awswan in #1138
• Containers (and W and M) by @stefaniatadama in #1129
• Supply implicit argument for agda/agda#7390 by @andreasabel in #1143
• Add comment on our notion of field by @felixwellen in #1142
• Pi4S3 Paper by @aljungstrom in #1151
• Add Boolean Rings by @Freek98 in #1146
• Base change, sliced adjoints by @marcinjangrzybowski in #1120
• (Displayed) Category Theory: Sections of displayed categories, Free Category 3.0 and UMPs are Props by @maxsnew in #1149
• Minor fix: improved definition of whitehead products by @aljungstrom in #1155
• Rework displayed category reasoning. by @jpoiret in #1153
• Remove redundant clause for agda/agda#7496 by @szumixie in #1156
• Connected CW complexes by @aljungstrom in #1133
• Category of elements as a wild functor to CAT. by @anuyts in #1160
• Fix compilation with agda/agda#7581 by @UlfNorell in #1168
• fix incorrectly named isIsoToIso, add IsoToIsIso by @maxsnew in #1173
• Indexed W-types: hlevel without univalence. by @anuyts in #1172
• A few minor utility functions by @awswan in #1174
• Another minor universe level generalisation by @awswan in #1177
• Basic Order Theory by @LuuBluum in #1154
• Remove duplicated factorial function by @anshwad10 in #1183
• Fix missed rename of StrictPoset to Quoset by @LuuBluum in #1185
• Move factorial from Cubical.Data.Fin.LehmerCode to Cubical.Data.Nat.Properties by @anshwad10 in #1184
• Reduced homology of CW complexes by @loic-p in #1175
• Devalapurkar & Haine by @Trebor-Huang in #1157
• Prep for Agda 2.8.0: remove some spurious private by @andreasabel in #1205
• Release for agda 2.7 by @felixwellen in #1206

New Contributors

• @rahulc29 made their first contribution in #1115
• @stschaef made their first contribution in #1108
• @pi3js2 made their first contribution in #1001
• @stefaniatadama made their first contribution in #1129
• @Freek98 made their first contribution in #1146
• @szumixie made their first contribution in #1156
• @UlfNorell made their first contribution in #1168
• @anshwad10 made their first contribution in #1183

Full Changelog: v0.7...v0.8