Test workflow_dispatch #1
Open
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
R is not zigzag complete if R<- and R-> are PERs.
Allow nullification to take a family of types as input rather than just one type
* use improved ringsolver * delete one more line * apply sing lemma * getting started on natural iso * general case of fully faithful cor * too many problems * almost global sections * make things compute * everything is small now * start with transport lemma * big transport lemma * some nasty paths * getting started with last proof * elegant lemma * back to nicer version * comm algs have limits * char of pres limits * preserving limits and lemma * lift sheaf diagrams * begin last lemma * last lemma * done * easy fixes * more fixes * loc master file * del comment
* scalar multiplication is homomorphic * CommAlgebra instance for list-based polynomials * refer to the new algebra structure * revert deleted line * elimProp2 for UnivariatePolyList * properties of list-based polynomials, related to the UMP of polynomials * property of algebras needed for the ump of the list-based polynomials * construct induced homomorphism * uniqueness part of the universal property of list-based polynomials * refactor: reduce noise * export all parts of the unviersal property * add a reference to the universal property, so make it easier to find * rename * add the implicit ring hom and use it to simplify the definition * refactor: rename according to conventions for algebra * deduplicate * reformulate ump
* scalar multiplication is homomorphic * CommAlgebra instance for list-based polynomials * refer to the new algebra structure * revert deleted line * elimProp2 for UnivariatePolyList * properties of list-based polynomials, related to the UMP of polynomials * property of algebras needed for the ump of the list-based polynomials * construct induced homomorphism * uniqueness part of the universal property of list-based polynomials * refactor: reduce noise * export all parts of the unviersal property * shift on sequence-based polynomials * add a reference to the universal property, so make it easier to find * x is regular in the list-based polynomials * rename * add the implicit ring hom and use it to simplify the definition * implement suggestion, rename
… the lemmas on PathSplit equivalences
…er to get modalities at all greater universe levels, and correct the definition of idemNull
Minor adjustment to universe level parameters and a correction
* scalar multiplication is homomorphic * CommAlgebra instance for list-based polynomials * refer to the new algebra structure * revert deleted line * elimProp2 for UnivariatePolyList * properties of list-based polynomials, related to the UMP of polynomials * property of algebras needed for the ump of the list-based polynomials * construct induced homomorphism * uniqueness part of the universal property of list-based polynomials * refactor: reduce noise * export all parts of the unviersal property * add stubs * add a reference to the universal property, so make it easier to find * export generator * uniqueness part of the universal property of FreeCommAlgebra * generator preserving isomorphism between typevariate and list-based polynomials * corollary easing isomorphism construction from ump * corollary easing isomorphism construction from ump * use new corollaries * rename * add the implicit ring hom and use it to simplify the definition * fix merge * introduce equalByUMP for UnivariateListPoly * fix indentation bug * export iso
* move and split ideal (Ring) * surjective image of an ideal is an ideal * reorganize Ideals in CommRings * rename CommRing.QuotientRing to CommRing.Quotient, create subfolder for Quotient * surjective image ideal for CommRings * fix renaming, expose quotientHom as surjection * ideal helper * lemma on surjections, refactor * CommIdeals are closed under - * new test cases for the solver * composition of surjections * describe fiber of ring-hom with kernel * wrap universal property of quotients for CommRings * add flag for faster checking * show isomorphism theorem on iterated quotients * export * improve comment * fix... * Update Cubical/Functions/Surjection.agda Co-authored-by: Matthias Hutzler <matthias-hutzler@posteo.net> * remove unneccessary lossy unification * introduce images of subsets * use images of subsets * specialize 'open' * organize imports, simplify rightFactorSurjective, use simplified * fix refactoring bug Co-authored-by: Matthias Hutzler <matthias-hutzler@posteo.net>
…a#945) * Define profunctors and define mappings between 2 notions of representability * add top-level description of profunctors file and delete trailing whitespace * Style fixes, improve description of universe levels in Profunctors 1. Line breaks added, though some lines are still 100+ 2. Equational reasoning proofs aligned 3. Re-written description of the choice of universe levels 4. Use an anonymous module 5. Some slightly different module opening to reduce number of projections 6. Comment on our convention for profunctors * Add Profunctor.agda file, and mnemonic notation for profunctor variance * delete trailing whitespace
* added various functions that I found useful * allow multiple universe levels in definition of JDep * remove unecessary implicit arguments from JDep
* added nix flake files
* added nix installation
* added install
* added default.nix
* added installPhase
* Renamed Build to Nix
* changed cubical derivation
* added FinWeak
* added more indentation
* removed useless {n}
* added more indentation
* added agdaWithCubical in flake.nix
* removed unnecessary FinWeak
* added nix flake in install.md
* changed CI to master
* changed name to nix flakes instructions
* improved nix flakes
* nixpkgs is referred to nixos-22.05
* changed defaultPackage to default
* updated flake.nix
* added install.md instruction
* updated nix flakes
* changed to flake-compat
* bump version number * update RELEASE instructions * update flake.lock * update README, use table for version info * improve update to README Co-authored-by: Matthias Hutzler <matthias-hutzler@posteo.net>
This reverts commit c00c032.
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.