michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Commit graph

  • 3c0e5f5226 fix compile error mzhang/fix Michael Zhang 2024-08-09 04:21:21 -0500
  • 8d72008ca0 add .cache to .gitignore Michael Zhang 2024-08-09 04:21:09 -0500
  • ee53cc032b add compile_commands Michael Zhang 2024-08-09 03:52:49 -0500
  • 025a115c0e
         Merge 09b316ce75 into 8072fdf9a0 Mauricio Collares 2022-03-18 21:24:28 -0500
  • 09b316ce75 chore(lp): fix compilation error Mauricio Collares 2022-03-18 18:28:08 -0300
  • 8072fdf9a0 linkfix master Floris van Doorn 2018-10-01 16:13:23 -0400
  • 070d687c7f add functoriality of gloopn' Floris van Doorn 2018-09-24 17:29:16 +0200
  • f2dfca25f9 refactor: use notation for trunc_index Floris van Doorn 2018-09-20 16:03:32 +0200
  • 3468ab8a9f rename nondep to constant Floris van Doorn 2018-09-20 15:53:05 +0200
  • 98fb55e428 fix two errors in the hott library Floris van Doorn 2018-09-20 01:48:55 +0200
  • 183ca62cc1 reverse sigma_assoc_equiv, and add variant Floris van Doorn 2018-09-14 19:32:02 +0200
  • 4b603990fc make instances in sigma explicit Floris van Doorn 2018-09-14 17:56:25 +0200
  • 609da93df0 small additions to group theory Floris van Doorn 2018-09-14 17:56:16 +0200
  • c534985d3f move files from Spectral Floris van Doorn 2018-09-11 18:57:19 +0200
  • 9a17a244c9 move more results and make arguments explicit Floris van Doorn 2018-09-11 16:45:30 +0200
  • 14c8fbfea3 homomorphisms of abelian groups form an abelian group Floris van Doorn 2018-09-10 15:09:37 +0200
  • 2b722b3e34 use psquare for naturality squares consistently Floris van Doorn 2018-09-10 14:29:06 +0200
  • a7b69aeb60 remove connectivity requirement for elimination out of an K(G,n) Floris van Doorn 2018-09-10 13:15:04 +0200
  • 3d0d0947d6 various cleanup changes in library Floris van Doorn 2018-09-07 16:30:58 +0200
  • afdcf7cb71 backport some changes from lean 3 Floris van Doorn 2018-09-07 15:57:43 +0200
  • 04c80c477f add psquares with two constant sides Floris van Doorn 2018-09-05 17:58:38 +0200
  • 86c375b0c4 make apd10_eq_of_homotopy a homotopy Floris van Doorn 2018-09-05 15:24:07 +0200
  • a69a4226c6 reorder arguments of definitions about squares and squareovers Floris van Doorn 2018-09-05 15:11:35 +0200
  • 8d2da84b61 make arguments of some definitions implicit in cubical.square Floris van Doorn 2018-09-05 14:45:03 +0200
  • c5d31f76d7 move definitions from spectral repository here Floris van Doorn 2018-08-19 13:51:12 +0200
  • 5333dcfa02 remove print command in hott/init imp_hott Floris van Doorn 2018-01-25 17:33:18 -0500
  • d68cdae2f3 Imp hott (#10) jonas-frey 2018-01-25 18:08:17 -0500
  • 38e3e8c5ae amending last patch Jonas Frey 2018-01-25 17:24:31 -0500
  • 0990473390 finished proof in nat.hlean Jonas Frey 2018-01-25 17:16:23 -0500
  • 5a60e2c99f removing sorrys Jonas Frey 2018-01-25 14:53:40 -0500
  • 227fcad22a feat(hott): various small changes Floris van Doorn 2017-08-04 15:07:56 +0100
  • 34dbd6c3ae fix(homotopy_group): remove type class proof which was synthesized Floris van Doorn 2017-07-22 15:03:54 +0100
  • c8477d28ba generalize many results about pointed homotopies of nondependent maps to dependent maps Floris van Doorn 2017-07-21 15:03:17 +0100
  • 1a26d405ef define pmap in terms of ppi Floris van Doorn 2017-07-21 13:35:23 +0100
  • 27cde0aeae feat(hott): rename ppi_gen to ppi Floris van Doorn 2017-07-20 22:04:05 +0100
  • 9e3611fe3e move naturality of loop-susp-adjunction to standard library Floris van Doorn 2017-07-20 18:55:31 +0100
  • 64327eb804 fix precedence of ->* Floris van Doorn 2017-07-20 15:13:43 +0100
  • ddef24223b make pointed suspensions, wedges and spheres the default (in contrast to the unpointed ones), remove sphere_index Floris van Doorn 2017-07-20 15:01:40 +0100
  • a02ea6b751 Unfold macros using the full typechecker in normalize. Floris van Doorn 2017-07-18 22:53:03 +0100
  • 519dcee739 fix(hott/algebra/homomorphism): fix typos Jeremy Avigad 2017-06-30 16:21:23 +0100
  • d550afc384 fix(hott/algebra/homomorphism): fix typos Jeremy Avigad 2017-06-30 16:21:23 +0100
  • 39a8c7fef4 feat(pointed): define phomotopy as a dependent pointed function Floris van Doorn 2017-06-17 17:20:04 -0400
  • a1126cfcf2 feat(trunc): simplify proof further Floris van Doorn 2017-06-16 14:38:46 -0400
  • 9066ee4801 feat(trunc): simplify proof Floris van Doorn 2017-06-16 14:34:52 -0400
  • d38979f783 fix(util/trie): compilation issue Leonardo de Moura 2017-05-30 10:57:59 -0700
  • 3e429f0368 fix(util/trie): fix the build Leonardo de Moura 2017-05-23 13:23:19 -0700
  • 123ef6ab67 fix(datatypes): further fix incorrect comment Floris van Doorn 2017-06-15 15:24:00 -0400
  • cad1ed3395 fix(hott/init/datatypes): incorrect comment ia0 2017-06-02 00:22:55 +0200
  • 5259289eba Merge 0768724265 into 5ad4443237 Julien Cretin 2017-06-15 18:57:50 +0000
  • 5ad4443237 feat(pointed): rename pequiv.MK2 to pequiv.MK, it is the more natural constructor Floris van Doorn 2017-06-14 21:56:23 -0400
  • 9265094f96 feat(pointed): redefine pequiv Floris van Doorn 2017-06-14 21:28:31 -0400
  • 66ea4a4725 fix(LES_of_homotopy_groups): make LES of homotopy groups more usable Floris van Doorn 2017-06-14 20:03:35 -0400
  • 8a7319244f fix(group_theory): make group_fun an abbreviation Floris van Doorn 2017-06-14 18:41:35 -0400
  • 7d0eecc449 feat(hott): move basic lemmas from the spectral repository to the main repository Floris van Doorn 2017-06-02 12:13:20 -0400
  • 0768724265 fix(hott/init/datatypes): incorrect comment ia0 2017-06-02 00:22:55 +0200
  • 76e56d0198 Merge 75fd816248 into d86284da63 Sayantan Khan 2017-05-29 06:26:09 +0000
  • d86284da63 doc(ubuntu/emacs): update installation instructions Floris van Doorn 2017-05-25 18:23:27 -0400
  • e522343c88 doc(emacs): move configurations to emacs readme and expand try it out section Floris van Doorn 2017-05-24 20:51:09 -0400
  • 0de635a6c9 doc(ubuntu/emacs): update installation instructions Floris van Doorn 2017-05-24 20:38:05 -0400
  • 76a8dd1816 fix(prod): revert change with unintended consequence Floris van Doorn 2017-05-24 17:12:26 -0400
  • ba5368c4ae feat(hott): various small changes Floris van Doorn 2017-05-19 14:44:39 -0400
  • 2227d9d1be feat(group_power): add some facts Floris van Doorn 2017-05-19 14:26:01 -0400
  • 0cf04ed3f2 feat(hott): port group_power and int/order from standard library. Update markdown files Floris van Doorn 2017-05-19 13:36:43 -0400
  • a588c0f205 chore(algebra): clean up some imports Floris van Doorn 2017-04-10 20:33:30 -0400
  • 75fd816248 Ready for pull request? Sayantan Khan 2017-05-03 03:55:22 +0530
  • d5d004ad6c almost done Sayantan Khan 2017-05-03 03:41:34 +0530
  • 5dbd0d5ade First stage done Sayantan Khan 2017-05-02 23:24:19 +0530
  • e0531d1432 some progress on the four lemma Sayantan Khan 2017-05-02 17:31:34 +0530
  • b35e187114 Added one more easy theorem Sayantan Khan 2017-04-30 16:09:44 +0530
  • b658bdb377 Removed unnecessary definition Sayantan Khan 2017-04-20 11:28:54 +0530
  • f3fee8e15d Proved a couple of elementary lemmas Sayantan Khan 2017-04-19 22:09:18 +0530
  • 5c376434c0 doing homological algebra instead Sayantan Khan 2017-04-19 12:49:45 +0530
  • ad3338d5e7 reduced suspensions are frustrating Sayantan Khan 2017-04-18 11:46:03 +0530
  • 916ae39692 Added incomplete suspension axiom Sayantan Khan 2017-04-14 17:04:30 +0530
  • 815f530e13 Fixed import error Sayantan Khan 2017-04-13 23:37:08 +0530
  • 43a7a84bec Fixed a botch up Sayantan Khan 2017-04-13 23:23:40 +0530
  • 4a04aab8e3 Temporary cleanup Sayantan Khan 2017-04-13 23:05:45 +0530
  • 3f3fc5c785 Added the definition of the contravariant functors to abelian groups. Sayantan Khan 2017-04-13 22:23:34 +0530
  • dff24cc9e2 Merge branch 'master' of https://github.com/leanprover/lean2 Sayantan Khan 2017-04-13 18:17:13 +0530
  • b998a49ec4 feat(red_susp): define pelim Floris van Doorn 2017-04-10 20:33:14 -0400
  • e3495e8362 Fixed some imports Sayantan Khan 2017-04-07 11:15:55 +0530
  • c268731093 fix(hott): small changes to pointed and susp and book.md Floris van Doorn 2017-03-22 20:34:25 -0600
  • 8e2adaa5ba feat(pointed): generalize the definition of ap1 so that we can use path induction to prove properties about it Floris van Doorn 2017-03-22 18:35:35 -0400
  • 540d451e01 fix(hott): small fixes Floris van Doorn 2017-03-07 22:49:06 -0500
  • 8bdd699fca feat(functor.adjoint): give another way to construct an adjunction Floris van Doorn 2017-02-28 19:22:09 -0500
  • 916bde4050 feat(pointed): make the definition of ap1 and ap1_con more convenient to use Floris van Doorn 2017-02-18 17:09:16 -0500
  • 7430d2c73b fix(hott): fix cofiber.elim and redefine cofiber as the symmetric pushout Floris van Doorn 2017-02-16 23:31:58 -0500
  • 7411011340 remove HoTT library (except init) Floris van Doorn 2017-02-10 12:07:22 -0500
  • 18313bfab0 feat(hott): make Type.{0} impredicative Floris van Doorn 2017-02-10 12:04:08 -0500
  • 5eafb1f6b2 feat(algebra): use infinity groups Floris van Doorn 2017-02-02 21:38:48 -0500
  • 25ab404781 feat(algebra): define the infinity-version of algebraic structures with one binary operator Floris van Doorn 2017-02-02 17:23:23 -0500
  • eedbd197dc doc(README/make): correct some build instructions Floris van Doorn 2017-01-18 22:54:46 +0100
  • 97065119b0 doc(ubuntu-12.04-detailed): update installation instructions Floris van Doorn 2017-01-17 20:32:27 +0100
  • 2d918bafaa feat(pointed): some definition changes to make reasoning about them easier Floris van Doorn 2017-01-17 20:32:55 +0100
  • 914addc66c feat(homotopy): introduce notation for topological type constructors Floris van Doorn 2017-01-08 22:47:48 +0100
  • 249d57cd02 feat(hott): small additions and fixes Floris van Doorn 2017-01-07 14:53:15 +0100
  • 55bdf2764b feat(homotopy/red_susp): prove that reduced suspension is equivalent to suspension, and some small things Floris van Doorn 2017-01-06 19:02:13 +0100
  • 217035b06c feat(hott): minor changes Floris van Doorn 2016-12-26 22:07:57 +0100
  • dbe4856cbd fix(nat/hott): add constructor attribute for is_succ Floris van Doorn 2016-11-29 20:13:44 -0500
  • f87210fcf6 feat(hott): various small changes Floris van Doorn 2016-11-27 17:13:38 -0500