Merge #7
Merged
Merge #7
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
* expand explanation of Glue * fixing language, keeping more closely to the typing rules in the paper * copy over invEq for readability * use transport from Prelude
* BiInvInt as a CommRing * Remove unused imports Co-authored-by: Felix Cherubini <felix.cherubini@posteo.de>
* Add some lemmas and definitions about embeddings and surjections * Add definition of subfinite sets * Add definition of finitely indexed types * Add module summary for Data.FinInd and Data.SubFinSet
* stubs and explanation in readme * define AlmostRing, throw away SemiRing (forgot why I wanted that) * forgot commutativity in the definition of almost ring * try to figure out what the whitespace problem is * try to figure out what the whitespace problem is * roll back * fix names Co-authored-by: Felix Cherubini <felix.cherubini@posteo.de>
* add syntax for 1 * split Algebra into Module and Algebra * Also: generalize to non commutative scalars * apply the SIP to algebras * use improved notation * consistent notation * refactor * adapt modules to new structure style * try to adapt algebra structure and get confused at some point * evan-style names for left modules * evan-style names for algebras * make-functions for modules and algebras * the polynomials over a commutative ring * variables are indexed by an arbitrary type * show it is a commutative algebra * algebra homomorphisms * fix isSet extractors * universal property of polynomial ring: induced map on types * universal property of polynomial ring: induced homomorphism * universal property of polynomial ring: easy half of equiv * fix quotient rings * adapt new automatic univalent str style * prove not so easy half of ump of polynomials * fix renaming * fix renaming again, remove unsolved problem * beautification * option --no-import-sorts everywhere * fix sigma-theory of left-modules * refactor algebras, hopefully this will admit an easier sigma-theory * apply SIP to R-algebras * start work on comm-algebras * make equivalence to sigma-definitio of comm-rings compositional * cleanup * apply SIP to commutative R-algebras * composition of algebra homomorphisms * prove what is left from the universal property of the free commutative algebra * make instances used in some records private * homomorphisms of rings * kernel ideal of a ring homomorphism * induced map on the quotient * Fixes after merge * Finish universal property * Clean up my mess... * move Kernel, Ideal and QuotientRing to Ring/ * Nice Carrier Co-authored-by: Felix Cherubini <felix.cherubini@posteo.de>
* Level lifting for isOfHLevelDep * Alternate Σ level proof with isOfHLevelDep * Add some lemmas about involutions * Use isOfHLevelRetract in isOfHLevelΣ' * Some involution cleanup
* Makefile: add "timings" target, clean up. * Makefile: add gen-everythings as a dependency of check and timings.
* First update * Minor fixes * Cleanup * Cleanup * fixes * fixes1 * Pointed funs change * remove bool import * newline * delete everything @:-) * whitespace... * Update 8-6-1.agda * testing * Application * updated Trunc * move some things into ZCohomology.Properties + comments * K-algebra * K algebra laws done * smash sphere * push * smash-assoc * K-grousp * K-alg * whitespace etc * merge main * minor fixes * delete abgroup * rename * renaming * whitespace... * MVunreduced * MV-almostDone * MV done * finalbackup * backup before merge * injectivity * cohom1-S1 * S1-done * basechange-morph * cohom1Torus-maps+rinv * moreTorusStuff * newBranchBackup * moreCopatterns * coHom-restructuring * backup_before_merge * private * emptylines * whitespace:-) * backup * last fixes * merge * whiteSpaceFiller3 * whiteSpaceFiller4 * fixes * anders+whitespace * fixes * h1-sn * cleanup * cleanup2 * cleanup * remove substs * comment * removeTransps * fix * space * deeperInduction * ConnectedFixed * cohomRewrite * newTruncInZCohom * fix * done * hej * changedef * onsdag * wed * . * hej * Sn-finished * newMinus * sillyStuff * guillaumeTest * silly loopstuff * stuf * finally... * fix * whitespace * sillyStuff * reviewFix * whitespace Co-authored-by: Axel Ljungström <axlj4439@r11a.math.su.se> Co-authored-by: aljungstrom <axel.ljungstrom@math.su.se> Co-authored-by: Axel Ljungström <axlj4439@r11f.math.su.se>
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
No description provided.