version 0.2, compatible with Agda-2.6.1.3
Saizan
released this
18 May 09:10
Added construction of M-types from Signatures/Containers (#245)
* Added construction of M-types from Signatures/Containers
* Added files
* No longer 'Unresolved Metas', but some postulates
* Removed trailing whitespace
* Fixed name collision
* Making progress on postulates
* Making progress on postulates
* removed whitespace
* Trying to fix computation problems
* Reduced shift definition, to pure iso's
* Fixed naming collsion (again...)
* Fixed naming collision (again...)
* Updated files to use iso more, and made proofs more readable
* Update
* Removed whitespace
* Update
* Small step towards removing all postulates.
* Update
* Finished proving lemma11-Iso
* All postulates cleared in M-types
* Pushed abstract
* Uncomment
* Working but with some 'abstract'
* Pushed abstract
* Updated to newest version of Cubical Agda
* Renamed some theorems
* Renamed some theorems
* Getting closer to removing all postulates
* Clared the last postulate for construction of M-types
* Updated folder structure
* Updated infrastructure
* Moved proofs
* Added missing files
* Working on pull request comments
* Working on pull request comments
* Working on pull request comments
* Restructure
* Restructure
* Restructure
* Updates based on PR comments
* Working on comments on PR
* Trying to simplify definition of shift
* Simplifying shift definition
* Working on PR comments
* Working on PR comments
* Working on PR comments
* Working on PR comments
* Working on PR comments
* Rename M-type to M, and moved files