michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions
8744 commits 3 branches 0 tags 28 MiB
Commit graph

626 commits

Author SHA1 Message Date
Jakob von Raumer
a5fe82f177 feat(hott) add carrier and hom set of rezk completion 2016-07-09 10:31:41 -07:00
Floris van Doorn
2cc8914874 feat(homotopy): add results about infty-connectedness and loops of EM-spaces 2016-07-09 10:20:22 -07:00
Floris van Doorn
3213b1b3b0 feat(EM): Prove some corollaries of Whitehead's principle, and prove that K(G,1) is unique. 
Also reorder the arguments of is_equiv_compose
 2016-07-09 10:20:22 -07:00
Floris van Doorn
17ccc283a9 feat(hott): move basic theorems from colimit development to library. 
Most notable changes:
rename apo011 -> apd011 and apd011 -> apdt011
make an argument of pathover_of_eq explicit
 2016-07-09 10:20:22 -07:00
Floris van Doorn
ae1b2e854c feat(hott): various minor changes 2016-07-09 10:20:21 -07:00
Floris van Doorn
fcf06ae2f5 feat(vankampen): prove the van Kampen theorem with basepoints 2016-07-09 10:20:21 -07:00
Floris van Doorn
15cdd593c1 feat(init.{equiv|ua}): remove duplicated theorem 2016-07-09 10:20:21 -07:00
Floris van Doorn
41de1a8271 feat(hit): add construction of propositional truncation to the library 2016-07-09 10:20:21 -07:00
Floris van Doorn
735230ad07 feat(hott): small changes, simplify van Kampen 2016-07-09 10:20:21 -07:00
Floris van Doorn
e96e4a677d feat(homotopy): prove the naive Seifert-Van Kampen theorem 
Also define the pushout of categories and the pushout of groupoids
 2016-07-09 10:20:21 -07:00
Floris van Doorn
61848c4a2e feat(hott): define pushout of groupoids 2016-07-09 10:20:21 -07:00
Floris van Doorn
9f13527c25 chore(hott): update default files and some markdown files 2016-07-09 10:20:21 -07:00
Floris van Doorn
dd5dcb1dd1 feat(hott): prove something without using ua and update book.md 2016-07-09 10:20:21 -07:00
Floris van Doorn
66ec690061 feat(book): add new theorems to book.md 2016-05-06 14:27:27 -07:00
Floris van Doorn
52dd6cf90b feat(hott): Port files from other repositories to the HoTT library. 
This commit adds truncated 2-quotients, groupoid quotients, Eilenberg MacLane spaces, chain complexes, the long exact sequence of homotopy groups, the Freudenthal Suspension Theorem, Whitehead's principle, and the computation of homotopy groups of almost all spheres which are known in HoTT.
 2016-05-06 14:27:27 -07:00
Floris van Doorn
ab7adf3084 fix(pathover): remove unused argument of loop_pathover 2016-05-06 14:27:27 -07:00
Floris van Doorn
2afdaf6906 fix(groupoid): redefine groupoid given by a group 
The composition was in the reverse order
 2016-05-06 14:27:27 -07:00
Floris van Doorn
1135d80266 feat(hott): use group isomorphisms instead of equality between groups 2016-05-06 14:27:27 -07:00
Floris van Doorn
8db4676c46 feat(hott): various changes and additions in the HoTT library 
Add more theorems about mapping cylinders, fibers, truncated 2-quotient, truncated univalence, pre/postcomposition with an iso in a precategory.

renamings: equiv.refl -> equiv.rfl and equiv_eq <-> equiv_eq'
 2016-05-06 14:27:27 -07:00
Floris van Doorn
a6b5191be6 feat(pushout/susp): change definition of elim_type, so that flattening is easier to prove 2016-05-06 14:26:46 -07:00
Jakob von Raumer
651df51cb7 chore(hott) the coercion doesn't seem to be the problem 2016-04-11 09:45:59 -07:00
Jakob von Raumer
7a9e1c7f4f chore(hott) fix sum proof by adding manual coercions 2016-04-11 09:45:59 -07:00
Floris van Doorn
a6319118e3 feat(types.pointed): small additions 2016-04-11 09:45:59 -07:00
Floris van Doorn
f983724cf6 feat(pointed): merge pointed2 into pointed 
We move the basic notions of pointed types into init.pointed, to avoid cycles in the import graph. Also adds pointed versions of pi and sigma, with corresponding notation
 2016-04-11 09:45:59 -07:00
Floris van Doorn
4895726c54 feat(connectedness): show that if f is n-connected, then trunc_functor k f is so, too 2016-04-11 09:45:59 -07:00
Floris van Doorn
54da5bcbda feat(hott): add some [constructor] attributes 2016-04-11 09:45:59 -07:00
Floris van Doorn
3887efa7c1 feat(hott): some renamings in init.path 2016-04-11 09:45:59 -07:00
Floris van Doorn
3240df6020 feat(book): add comments about chapter 10 2016-04-11 09:45:59 -07:00
Floris van Doorn
dc37ec954d refactor(hott): rename apdo to apd 2016-04-11 09:45:59 -07:00
Floris van Doorn
80a2e285cb feat(init/ua): add ua_symm and ua_trans 2016-04-11 09:45:59 -07:00
Floris van Doorn
05b59aecf8 refactor(hott): rename apd to apdt 2016-04-11 09:45:59 -07:00
Floris van Doorn
b1ed69f621 feat(hott): small changes, mostly in pointed2 2016-04-11 09:45:59 -07:00
Leonardo de Moura
226f8bafeb fix(library/tactic/rewrite_tactic): do not allow projections to be unfolded 
fixes #1032

This is just a workaround. A better fix has been implemented in the
lean3 branch.
 2016-03-28 13:02:57 -07:00
Ulrik Buchholtz
1c52062f1e chore(hott): standardize names of homotopy_of_inv_homotopy_post and friends 2016-03-23 09:22:55 -07:00
Ulrik Buchholtz
5257e282aa feat(hott/homotopy): additions to sphere and susp, improve quaternionc_hopf 2016-03-23 09:22:55 -07:00
Ulrik Buchholtz
7e8ba1440f feat(hott): update book.md and homotopy.md to reflect additions 2016-03-23 09:22:55 -07:00
Ulrik Buchholtz
f11169b8f2 feat(hott): the quaternionic hopf fibration 2016-03-23 09:22:55 -07:00
Ulrik Buchholtz
89296ec52a feat(hott): the complex hopf fibration S3 to S2 2016-03-23 09:22:55 -07:00
Ulrik Buchholtz
d53320cb0f feat(hott): the imaginaroid version of the cayley dickson construction 2016-03-23 09:22:55 -07:00
Ulrik Buchholtz
0b9084c7d2 feat(hott): hopf construction and delooping of K(G,1)s 2016-03-23 09:22:55 -07:00
Ulrik Buchholtz
bb64913e50 feat(hott): flattening lemma for susp 2016-03-23 09:22:55 -07:00
Ulrik Buchholtz
bd9e47c82c feat(hott): functoriality of pushout; connectedness in is_conn namespace 
other changes:
- move result about connectedness of susp to homotopy.susp
- improved definition of circle multiplication
- improved the interface to join
 2016-03-23 09:22:55 -07:00
Leonardo de Moura
5e14b4ebe8 fix(library,hott): avoid rewrite with patterns of the form (?M ...) 2016-03-09 15:39:17 -08:00
Floris van Doorn
003c11c917 feat(connectedness): is_conn_map -> is_conn_fun, and unbundle the P in elimination principles 2016-03-06 13:03:31 -05:00
Floris van Doorn
1e10810a1e feat(init/funext): add function extensionality as an axiom. 
This allows us to keep track of theorems which use function extensionality, but not full univalence
 2016-03-06 13:03:31 -05:00
Floris van Doorn
2d9c3985c9 feat(square): add variants of eq_pathover 2016-03-06 13:03:31 -05:00
Floris van Doorn
671ef077b9 feat(hott): additions, mostly to types.trunc 2016-03-06 13:03:31 -05:00
Floris van Doorn
5cacebcf86 feat(hott): replace assert by have and merge namespace equiv.ops into equiv 
The coercion A ≃ B -> (A -> B) is now in namespace equiv. The notation ⁻¹ for symmetry of equivalences is not supported anymore. Use ⁻¹ᵉ
 2016-03-03 10:13:21 -08:00
Floris van Doorn
058000f61d feat(homotopy/homotopy_group): add theorems in section 8.3 of the HoTT book 2016-03-03 10:13:21 -08:00
Floris van Doorn
1903601ba5 refactor(trunc): rename namespace is_trunc.trunc_index to trunc_index 2016-03-03 10:13:20 -08:00
Floris van Doorn
e2b31a9b33 feat(hott): remove multiple_instances attribute 2016-03-03 10:13:20 -08:00
Floris van Doorn
af4ba3d2fb feat(hott): prove that the (n+1)-sphere is n-connected 2016-03-03 10:13:20 -08:00
Floris van Doorn
e515875464 feat(hott): various additions 2016-03-03 10:13:20 -08:00
Floris van Doorn
c6e628da12 feat(hott): more computation rules for trunc_index and use nats for Lemma 8.6.2 2016-03-03 10:13:20 -08:00
Floris van Doorn
e5d5ef9d55 feat(hott/library): various changes and additions. 
Most notably:
Give le.refl the attribute [refl]. This simplifies tactic proofs in various places.
Redefine the order of trunc_index, and instantiate it as weak order.
Add more about pointed equivalences.
 2016-03-03 10:13:20 -08:00
Floris van Doorn
65b367ddff feat(fin): port more parts of fin from the standard library 2016-03-03 10:13:20 -08:00
Floris van Doorn
bf403e124a feat(nat/div): port to HoTT library 2016-03-03 10:13:20 -08:00
Floris van Doorn
4238fdd3d8 fix(hott): add missing links to markdown files 2016-03-03 10:13:20 -08:00
Jakob von Raumer
1104537d02 chore(hott) adjust to new naming for pointed types and truncated types 2016-03-01 13:52:53 -08:00
Jakob von Raumer
2b13777bbe feat(hott) add type functors, maybe they should be changed to be un-funexted. 2016-03-01 13:52:53 -08:00
Jakob von Raumer
11458f64fe feat(hott/algebra) add order categories 2016-03-01 13:52:53 -08:00
Leonardo de Moura
fbe5188480 refactor(frontends/lean): remove 'by+' and 'begin+' tokens 2016-02-29 13:45:43 -08:00
Leonardo de Moura
faa0031d4e refactor(library,hott): remove 'by+' and 'begin+' 2016-02-29 13:15:48 -08:00
Leonardo de Moura
b41c65f549 feat(frontends/lean): remove '[visible]' annotation, remove 'is_visible' tracking 2016-02-29 12:31:23 -08:00
Leonardo de Moura
cc8d9bc7ff refactor(hott): replace 'assert'-expr with 'have'-expr 2016-02-29 12:11:17 -08:00
Leonardo de Moura
101cf1ec4c feat(frontends/lean): remove difference between 'have' and 'assert' 2016-02-29 11:28:20 -08:00
Leonardo de Moura
5a4dd3f237 feat(library/reducible): remove [quasireducible] annotation 2016-02-25 17:42:44 -08:00
Leonardo de Moura
d501295ec1 refactor(algebra/binary): remove unnecessary annotations 2016-02-25 15:11:52 -08:00
Leonardo de Moura
768ba1c363 refactor(library/hott): remove more unnecessary annotations 2016-02-25 14:30:00 -08:00
Leonardo de Moura
510168a387 refactor(library,hott): remove unnecessary annotations 2016-02-25 12:26:20 -08:00
Leonardo de Moura
146edde5b3 feat(library/class): mark instances as quasireducible by default 
quasireducible are also known as lazyreducible.

There is a lot of work to be done.
We still need to revise blast, and add a normalizer for type class
instances. This commit worksaround that by eagerly unfolding
quasireducible.
 2016-02-25 12:11:29 -08:00
Leonardo de Moura
1924b2884c refactor(library/tactic): remove 'append' and 'interleave' tacticals 
Preparation for major refactoring in the tactic framework.
 2016-02-24 16:02:16 -08:00
Sebastian Ullrich
3de216d302 chore(*.md): fix/remove broken links 2016-02-23 10:11:24 -08:00
Floris van Doorn
6cdbc0f79f feat(pointed/equiv): add more theorems 
The theorems are mostly about the interaction between pointed equivalences and pointed homotopies
Some of these theorems were missing for (unpointed) equivalences, so I also added them there
 2016-02-22 11:15:39 -08:00
Floris van Doorn
eea2a1ac91 feat(hott): add some more abstracts 2016-02-22 11:15:39 -08:00
Floris van Doorn
facd94a1b4 feat(hott): various changes 
more about pointed truncated types, including pointed sets.
also increase the priority of some basic instances that nat/num/pos_num/trunc_index have 0, 1 and + (in both libraries)
also move the notation + for sum into the namespace sum, to (sometimes) avoid overloading with add
 2016-02-22 11:15:38 -08:00
Floris van Doorn
087c44d614 style(hott): rename instances of pType using pfoo instead of Foo 
For example, the pointed suspension operation was called Susp before this commit, but now is called psusp
 2016-02-22 11:15:38 -08:00
Floris van Doorn
c64e5a114c feat(circle): add missing facts that the circle is 1-truncated and 0-connected 2016-02-22 11:15:38 -08:00
Floris van Doorn
bac6d99cc7 style(hott): rename Pointed to pType 
also rename sigma_equiv_sigma_id to sigma_equiv_sigma_right and similarly for pi
 2016-02-22 11:15:38 -08:00
Floris van Doorn
43cf2ad23d style(hott): replace all other occurrences of hprop/hset 
They are replaced by either Prop/Set or prop/set
 2016-02-22 11:15:38 -08:00
Floris van Doorn
4e2cc66061 style(*): rename is_hprop/is_hset to is_prop/is_set 2016-02-22 11:15:38 -08:00
Floris van Doorn
816237315c feat(hott): various additions, especially for pointed maps/homotopies/equivalences 2016-02-22 11:15:38 -08:00
Floris van Doorn
ecc141779a feat(init.path): update init.path to use tactics, also some additions 
Now the file hardly uses eq.rec explicitly anymore.
Also add the fact that horizontal and vertical inverses of paths are equal
Make one more argument explicit in eq.cancel_left and eq.cancel_right (to make it nicer to write 'apply cancel_right p')
 2016-02-22 11:15:38 -08:00
Floris van Doorn
7f09ba328e feat(hott): small changes 2016-02-22 11:15:38 -08:00
Floris van Doorn
78092af27f feat(hott): add some attributes 2016-02-22 11:15:38 -08:00
Floris van Doorn
cd74b6bff0 fix(hott): abstract some equivalence proofs 
Note: this is important. I proved a quite complicated equivalence with calc, by chaining these
equivalences. Now if I want to know the underlying function of this composite equivalence, I have to
unfold all these instances. Without the abstracts, this took 14 seconds, and afterwards, it took 2
seconds.
 2016-02-22 11:15:38 -08:00
Floris van Doorn
42b78962f9 feat(init/wf): simplify definition acc.drec 2016-02-09 10:03:48 -08:00
Floris van Doorn
e14d4a4c0c feat(init/wf): port from standard library to HoTT library 
After this commit we need some more advanced theorems in init/wf, notably function extenstionality.
For this reason I had to refactor the init folder a little bit.
To keep the init folders in both libraries similar, I did the same refactorization in the standard library, even though that was not required for the standard library
 2016-02-09 10:03:48 -08:00
Jakob von Raumer
c0abcc7722 chore(hott): fix signature of previous lemma 2016-02-09 09:59:03 -08:00
Jakob von Raumer
3c7536cff8 chore(hott): clean up cancellability proof a bit 2016-02-09 09:58:57 -08:00
Jakob von Raumer
4d6c516c01 feat(hott): add lemma: equivalent fin sets come from equal numbers, sums with fin sets are cancellable 2016-02-09 09:58:52 -08:00
Jakob von Raumer
4edb6d7765 feat(hott): finish cancelling law for sums with unit 2016-02-09 09:58:31 -08:00
Jakob von Raumer
0ad8131985 feat(hott): start cancellation proof for sums 2016-02-09 09:58:24 -08:00
Jakob von Raumer
62e1431f04 chore(hott): delay lemmas about smash product until I have more ideas on how to tackle the coherence there. 2016-02-09 09:58:17 -08:00
Jakob von Raumer
1042f6c29d feat(hott): port finite ordinal sets from the std library, with all things related to nat.mod and to fintype still missing. 
create a logic.hlean file for further extension of the logic theory in the prelude. add distributivity lemmas for products and sums.
 2016-02-09 09:58:10 -08:00
Jakob von Raumer
cb3bc1a311 feat(hott): add another constructor for pointed equivalences 2016-02-09 09:57:59 -08:00
Jakob von Raumer
23dec19aa7 feat(hott): start lemma about smashing with bool 2016-02-09 09:57:52 -08:00
Jakob von Raumer
8bc4206c62 feat(hott): add custom recursors for cofiber type 2016-02-09 09:57:47 -08:00
Jakob von Raumer
31e2653e58 feat(hott): add lemma: cofiber of terminal morphism is suspension 2016-02-09 09:57:39 -08:00
Jakob von Raumer
7e02ea6cab feat(hott): add smash product of pointed types 2016-02-09 09:57:33 -08:00
Jakob von Raumer
ce8ca64771 feat(hott): adjust small things in wedge theory 2016-02-09 09:57:27 -08:00
Jakob von Raumer
56cd88267c feat(hott): add cofiber of a function, prove lemma that cofibers of equivalences are contractible 2016-02-09 09:57:21 -08:00
Floris van Doorn
ec38ee8df8 fix(hott/init/tactic): add replace 2016-02-07 14:06:28 -08:00
Leonardo de Moura
30d6853ffd refactor(hott,tests): make sure HoTT library and tests still work if we introduce checkpoints in have-expressions 2016-02-04 16:58:32 -08:00
Leonardo de Moura
42fbc63bb6 fix(library/tc_multigraph): avoid name collisions 
@avigad, @fpvandoorn, @rlewis1988, @dselsam

I changed how transitive instances are named.
The motivation is to avoid a naming collision problem found by Daniel.
Before this commit, we were getting an error on the following file
tests/lean/run/collision_bug.lean.

Now, transitive instances contain the prefix "_trans_".
It makes it clear this is an internal definition and it should not be used
by users.

This change also demonstrates (again) how the `rewrite` tactic is
fragile. The problem is that the matching procedure used by it has
very little support for solving matching constraints that involving type
class instances. Eventually, we will need to reimplement `rewrite`
using the new unification procedure used in blast.

In the meantime, the workaround is to use `krewrite` (as usual).
 2016-02-04 13:15:42 -08:00
Ulrik Buchholtz
dcb35008e1 feat(hott/homotopy): general connectivity elimination and the wedge connectivity lemma 2016-02-04 11:07:22 -08:00
Floris van Doorn
29c84aad19 fix(book.md): add types.arrow to 2.9 
closes #976
 2016-01-26 20:40:22 -08:00
Floris van Doorn
3409deecdb chore(hott): update md files, move port.md 2016-01-24 16:34:45 -08:00
Floris van Doorn
8eab58f41a fix(choice): make some style changes 2016-01-24 16:34:45 -08:00
seulbaek
92d6806073 refactor(hott/choice): rename 3.8.5 2016-01-24 16:34:35 -08:00
seulbaek
107550238b refactor(hott/choice): rename lemmas for 3.8.2 2016-01-24 16:34:23 -08:00
seulbaek
d42f3d313f feat(hott): add choice.hlean 2016-01-24 16:34:12 -08:00
seulbaek
2c81c93d69 feat(hott/types/equiv): add is_trunc_equiv to equiv.hlean 2016-01-24 16:33:59 -08:00
Jakob von Raumer
aa5e188179 feat(hott): add symmetry of pushouts and pointed pushouts 2016-01-24 16:30:26 -08:00
Jakob von Raumer
d8d3b0c0b2 feat(hott): add wedge sum of pointed types, neutrality of wedging with the unit type 2016-01-24 16:30:21 -08:00
Jakob von Raumer
664132b845 feat(hott): add calc lemmas for pointed equivalences, make pinl and pinr constructors 2016-01-24 16:30:16 -08:00
Jakob von Raumer
8d22e454e7 feat(hott): add theory about pointed pushouts 2016-01-24 16:30:12 -08:00
Leonardo de Moura
66a722ff5a feat(library/unifier): remove "eager delta hack", use is_def_eq when delta-constraint does not have metavariables anymore 
The "eager-delta hack" was added to minimize problems in the interaction
between coercions and delta-constraints.
 2016-01-03 12:39:32 -08:00
Leonardo de Moura
b117a10f82 refactor(library/blast/simplifier): use priority_queue to store simp/congr lemmas, use name convention used at forward/backward lemmas, normalize lemmas when blast starts, cache get_simp_lemmas 2015-12-28 17:52:57 -08:00
Leonardo de Moura
f177082c3b refactor(*): normalize metaclass names 
@avigad and @fpvandoorn, I changed the metaclasses names. They
were not uniform:
- The plural was used in some cases (e.g., [coercions]).
- In other cases a cryptic name was used (e.g., [brs]).

Now, I tried to use the attribute name as the metaclass name whenever
possible. For example, we write

   definition foo [coercion] ...
   definition bla [forward] ...

and

  open [coercion] nat
  open [forward] nat

It is easier to remember and is uniform.
 2015-12-28 10:39:15 -08:00
Ulrik Buchholtz
b09fdc8c61 feat(hott/hit): flattening lemmas for coeq and pushout 2015-12-28 09:06:13 -08:00
Ulrik Buchholtz
f3b2c7010f feat(hott): functoriality of quotients 2015-12-28 09:06:13 -08:00
Leonardo de Moura
128b557d37 refactor(frontends/lean): use attribute_manager to simplify decl_attributes 2015-12-17 22:28:53 -08:00
Floris van Doorn
74366aa061 fix(hott): change some theorems to definitions 
This ensures that the HoTT library compiles with the option --to_axiom
 2015-12-17 12:46:16 -08:00
Floris van Doorn
c852f7bc71 feat(hott): use the induction tactic for trunc at some places 2015-12-17 12:46:16 -08:00
Floris van Doorn
da5f10ce63 feat(hott): minor fixes. allow the usage of numerals for trunc_index 2015-12-17 12:46:16 -08:00
Leonardo de Moura
61ecf018e9 feat(frontends/lean,library/tactic): add easy tactic parsing support for at ... and with ... 2015-12-17 12:18:32 -08:00
Leonardo de Moura
c824a0e050 chore(library,hott): enforce naming conventions 2015-12-17 11:36:58 -08:00
Leonardo de Moura
13419d1561 chore(hott/library): cleanup 2015-12-17 11:31:07 -08:00
Sebastian Ullrich
2185ee7e95 feat(library/tactic): make let tactic transparent, introduce new opaque note tactic 
The new let tactic is semantically equivalent to let terms, while `note`
preserves its old opaque behavior.
 2015-12-14 10:14:02 -08:00
Leonardo de Moura
e3a35ba4fd feat(frontends/lean): add 'with_attributes' tactical 
closes #494
 2015-12-13 18:27:44 -08:00
Leonardo de Moura
d4e49a8434 feat(library/tactic/intros_tactic): intro without argument should introduce a single variable 
see #695
 2015-12-13 16:28:39 -08:00
Floris van Doorn
4ef58f1ba5 chore(hott): more cleanup. 
Make zero and one reducible (see algebra/port.md)
Change some theorems which need to compute into definitions
 2015-12-10 10:42:16 -08:00
Floris van Doorn
c968f920ba chore(hott): cleanup 2015-12-10 10:42:16 -08:00
Floris van Doorn
65c93b180d fix(types.md): add num 2015-12-09 12:36:11 -08:00
Floris van Doorn
2325d23f68 feat(hott): port nat and int from the standard library 2015-12-09 12:36:11 -08:00
Floris van Doorn
46739c8b70 feat(hott/algebra): port abstract structures 2015-12-09 12:34:06 -08:00
Floris van Doorn
14a2c8e444 fix(init/nat): add spaces around inequalities 2015-12-09 12:34:06 -08:00
Floris van Doorn
377755e5ab feat(types/sigma): add lemma 2015-12-09 12:34:06 -08:00
Leonardo de Moura
6404c3c014 chore(hott/types/nat/order): remove occurrence of "migrate" command 2015-12-08 15:37:13 -08:00
Leonardo de Moura
85379b7706 feat(library/blast/actions/simple_actions): make sure contradiction action works even if classical logic support is not enabled 
not (not (not a)) -> not a
 2015-12-07 09:30:14 -08:00
Jakob von Raumer
cc8a5581d6 chore(hott/cubical): add lost space hints around square concatenations 2015-12-02 23:13:25 -08:00
Jakob von Raumer
68901c7788 feat(hott/homotopy): complete join associativity proof, helper lemmas for squares 2015-12-02 23:13:21 -08:00
Jakob von Raumer
bd064ef9c8 feat(hott/homotopy): prove missing helper lemmas up to cube massaging 2015-12-02 23:13:17 -08:00
Jakob von Raumer
811f3067ff feat(hott): join associativity proof done up to small auxiliary lemmas, add transposition, inversion of cubes 2015-12-02 23:13:12 -08:00
Jakob von Raumer
1d68d57bb9 chore(hott/cubical): adapt cubovers to new order of faces 2015-12-02 23:13:07 -08:00
Jakob von Raumer
e481e541a2 feat(hott/homotopy): more progress on join associativity 2015-12-02 23:13:03 -08:00
Jakob von Raumer
6c6dde7e48 feat(hott/homotopy): progress on join associativity, many coherence lemmas about square operations needed 2015-12-02 23:12:59 -08:00
Jakob von Raumer
1b52ae8858 feat(hott/cubical): add cube concatenations 2015-12-02 23:12:54 -08:00
Jakob von Raumer
3f1cf3835f chore(hott/cubical): change order of visible arguments in cube 2015-12-02 23:12:50 -08:00