Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Clean up Cohomology Ring #845

Merged
merged 129 commits into from
Aug 16, 2022
Merged

Clean up Cohomology Ring #845

merged 129 commits into from
Aug 16, 2022

Commits on Apr 6, 2022

  1. Fix Direct-sum : 

    The index and the groups were at the same level.
The should be at different one, for instance if the index is Nat, and the group something else
    @thomas-lamiaux
    thomas-lamiaux committed Apr 6, 2022
    Configuration menu
    Copy the full SHA
    3f62a82 View commit details
    Browse the repository at this point in the history

  2. Merge branch 'agda:master' into master

    @thomas-lamiaux
    thomas-lamiaux committed Apr 6, 2022
    Configuration menu
    Copy the full SHA
    620bfc5 View commit details
    Browse the repository at this point in the history

  3. add the definition of the cohomology ring

    @thomas-lamiaux
    thomas-lamiaux committed Apr 6, 2022
    Configuration menu
    Copy the full SHA
    1f12e1f View commit details
    Browse the repository at this point in the history

Commits on Apr 7, 2022

  1. some progress for the graded property

    @thomas-lamiaux
    thomas-lamiaux committed Apr 7, 2022
    Configuration menu
    Copy the full SHA
    3bee7f0 View commit details
    Browse the repository at this point in the history

  2. module name changes

    @thomas-lamiaux
    thomas-lamiaux committed Apr 7, 2022
    Configuration menu
    Copy the full SHA
    a075003 View commit details
    Browse the repository at this point in the history

  3. Add gradedComm proof : 

    -> Modify some notions in gradedCommutativity
-> new lemme for the "good" -h^
-> proof
    @thomas-lamiaux
    thomas-lamiaux committed Apr 7, 2022
    Configuration menu
    Copy the full SHA
    0ee0210 View commit details
    Browse the repository at this point in the history

  4. uniformisation of the notation

    @thomas-lamiaux
    thomas-lamiaux committed Apr 7, 2022
    Configuration menu
    Copy the full SHA
    015710b View commit details
    Browse the repository at this point in the history

Commits on Apr 8, 2022

  1. Computation of H*(Unit) cong Z

    @thomas-lamiaux
    thomas-lamiaux committed Apr 8, 2022
    Configuration menu
    Copy the full SHA
    ecad958 View commit details
    Browse the repository at this point in the history

Commits on Apr 9, 2022

  1. Proof in a more general setting : 

    -> Because this case is so degenerated, things compute.
   This new proof is forgetting some of the computation
   to have proof that will rise better to non-degenerated case
    @thomas-lamiaux
    thomas-lamiaux committed Apr 9, 2022
    Configuration menu
    Copy the full SHA
    d4adcc7 View commit details
    Browse the repository at this point in the history

  2. Simplification

    @thomas-lamiaux
    thomas-lamiaux committed Apr 9, 2022
    Configuration menu
    Copy the full SHA
    37342d4 View commit details
    Browse the repository at this point in the history

  3. Renaming

    @thomas-lamiaux
    thomas-lamiaux committed Apr 9, 2022
    Configuration menu
    Copy the full SHA
    22f07e7 View commit details
    Browse the repository at this point in the history

  4. correct trailing-whitespaces and one path

    @thomas-lamiaux
    thomas-lamiaux committed Apr 9, 2022
    Configuration menu
    Copy the full SHA
    4e45548 View commit details
    Browse the repository at this point in the history

  5. Fix dependencies : 

    -> changing gradedComm by gradedCom' to account
   the previuous change
    @thomas-lamiaux
    thomas-lamiaux committed Apr 9, 2022
    Configuration menu
    Copy the full SHA
    67d21cf View commit details
    Browse the repository at this point in the history

  6. Fix dependecies

    @thomas-lamiaux
    thomas-lamiaux committed Apr 9, 2022
    Configuration menu
    Copy the full SHA
    d38d370 View commit details
    Browse the repository at this point in the history

  7. fix dependecies

    @thomas-lamiaux
    thomas-lamiaux committed Apr 9, 2022
    Configuration menu
    Copy the full SHA
    53d1962 View commit details
    Browse the repository at this point in the history

  8. fix dependencies

    @thomas-lamiaux
    thomas-lamiaux committed Apr 9, 2022
    Configuration menu
    Copy the full SHA
    c3ea1cb View commit details
    Browse the repository at this point in the history

  9. Fix dependency brunerie

    @thomas-lamiaux
    thomas-lamiaux committed Apr 9, 2022
    Configuration menu
    Copy the full SHA
    cb88096 View commit details
    Browse the repository at this point in the history

  10. Add a recursor for the special case A / < a, ..., c >

    @thomas-lamiaux
    thomas-lamiaux committed Apr 9, 2022
    Configuration menu
    Copy the full SHA
    b21dc11 View commit details
    Browse the repository at this point in the history

  11. moved files

    @thomas-lamiaux
    thomas-lamiaux committed Apr 9, 2022
    Configuration menu
    Copy the full SHA
    39ccad1 View commit details
    Browse the repository at this point in the history

  12. Add a special recursor for polynomes : 

    -> There is a need of the special as on the left we need the
   CommRing to take A / < a, ..., b > and we nedd a ring on
   the right as H*(X) is not a CommRing but a gradedComm Ring
    @thomas-lamiaux
    thomas-lamiaux committed Apr 9, 2022
    Configuration menu
    Copy the full SHA
    7721b8b View commit details
    Browse the repository at this point in the history

  13. delete trailing-white-spaces

    @thomas-lamiaux
    thomas-lamiaux committed Apr 9, 2022
    Configuration menu
    Copy the full SHA
    3b1e38c View commit details
    Browse the repository at this point in the history

Commits on Apr 10, 2022

  1. Begining to build a general framework ot the example of unit

    @thomas-lamiaux
    thomas-lamiaux committed Apr 10, 2022
    Configuration menu
    Copy the full SHA
    b4b3685 View commit details
    Browse the repository at this point in the history

  2. H*-Unit->Z[x] is a ring morphism

    @thomas-lamiaux
    thomas-lamiaux committed Apr 10, 2022
    Configuration menu
    Copy the full SHA
    1167e9c View commit details
    Browse the repository at this point in the history

  3. Add functions H* Unit <-> Z[X]/X

    @thomas-lamiaux
    thomas-lamiaux committed Apr 10, 2022
    Configuration menu
    Copy the full SHA
    4df89fa View commit details
    Browse the repository at this point in the history

  4. Builds all the framework except e-sect

    @thomas-lamiaux
    thomas-lamiaux committed Apr 10, 2022
    Configuration menu
    Copy the full SHA
    6c385a4 View commit details
    Browse the repository at this point in the history

  5. Fix : commented a part

    @thomas-lamiaux
    thomas-lamiaux committed Apr 10, 2022
    Configuration menu
    Copy the full SHA
    5696cae View commit details
    Browse the repository at this point in the history

  6. Compute H* Unit in a generalisable way

    @thomas-lamiaux
    thomas-lamiaux committed Apr 10, 2022
    Configuration menu
    Copy the full SHA
    c24276c View commit details
    Browse the repository at this point in the history

Commits on Apr 12, 2022

  1. A simplification

    @thomas-lamiaux
    thomas-lamiaux committed Apr 12, 2022
    Configuration menu
    Copy the full SHA
    86af319 View commit details
    Browse the repository at this point in the history

  2. Add the functions for S1 in both sens and stat proving some properties

    @thomas-lamiaux
    thomas-lamiaux committed Apr 12, 2022
    Configuration menu
    Copy the full SHA
    a1861b2 View commit details
    Browse the repository at this point in the history

Commits on Apr 13, 2022

  1. Add the following : 

    -> A cleaner way to deal with the cup product
-> Finish all the structure except some cases of the cup-product
-> Prove the retraction property
    @thomas-lamiaux
    thomas-lamiaux committed Apr 13, 2022
    Configuration menu
    Copy the full SHA
    f3d2c17 View commit details
    Browse the repository at this point in the history

  2. Add a proof of e-sect

    @thomas-lamiaux
    thomas-lamiaux committed Apr 13, 2022
    Configuration menu
    Copy the full SHA
    1938cb6 View commit details
    Browse the repository at this point in the history

Commits on Apr 14, 2022

  1. Proof of the ring morphism for the case H0 H0

    @thomas-lamiaux
    thomas-lamiaux committed Apr 14, 2022
    Configuration menu
    Copy the full SHA
    5b5d11f View commit details
    Browse the repository at this point in the history

  2. stuck on filing squares in the ring morphism part

    @thomas-lamiaux
    thomas-lamiaux committed Apr 14, 2022
    Configuration menu
    Copy the full SHA
    a17e98f View commit details
    Browse the repository at this point in the history

Commits on Apr 15, 2022

  1. First complete computation of H*(S¹) equiv Z[X]/X²

    @thomas-lamiaux
    thomas-lamiaux committed Apr 15, 2022
    Configuration menu
    Copy the full SHA
    e4815fc View commit details
    Browse the repository at this point in the history

  2. clean up

    @thomas-lamiaux
    thomas-lamiaux committed Apr 15, 2022
    Configuration menu
    Copy the full SHA
    c3419d7 View commit details
    Browse the repository at this point in the history

Commits on Apr 18, 2022

  1. Add direct prod for rings

    @thomas-lamiaux
    thomas-lamiaux committed Apr 18, 2022
    Configuration menu
    Copy the full SHA
    49ed72d View commit details
    Browse the repository at this point in the history

  2. Add Direct Prod for CommRing

    @thomas-lamiaux
    thomas-lamiaux committed Apr 18, 2022
    Configuration menu
    Copy the full SHA
    d7c30ea View commit details
    Browse the repository at this point in the history

Commits on Apr 20, 2022

  1. Merge branch 'agda:master' into master

    @thomas-lamiaux
    thomas-lamiaux committed Apr 20, 2022
    Configuration menu
    Copy the full SHA
    d6d6104 View commit details
    Browse the repository at this point in the history

  2. Partially add Coproduct

    @thomas-lamiaux
    thomas-lamiaux committed Apr 20, 2022
    Configuration menu
    Copy the full SHA
    6dcf4b0 View commit details
    Browse the repository at this point in the history

  3. Coproduct : add proof of sect

    @thomas-lamiaux
    thomas-lamiaux committed Apr 20, 2022
    Configuration menu
    Copy the full SHA
    11c9cce View commit details
    Browse the repository at this point in the history

  4. Add morphism on the cup product

    @thomas-lamiaux
    thomas-lamiaux committed Apr 20, 2022
    Configuration menu
    Copy the full SHA
    7d4284f View commit details
    Browse the repository at this point in the history

  5. Coproduct : Add H*(X coprod Y) equiv H*(X) x H*(Y) 

    -> add the morphism
-> add the equivalence of ring
    @thomas-lamiaux
    thomas-lamiaux committed Apr 20, 2022
    Configuration menu
    Copy the full SHA
    efc74ed View commit details
    Browse the repository at this point in the history

  6. Coproduct : clean up

    @thomas-lamiaux
    thomas-lamiaux committed Apr 20, 2022
    Configuration menu
    Copy the full SHA
    2ad2efb View commit details
    Browse the repository at this point in the history

  7. small clean up Unit

    @thomas-lamiaux
    thomas-lamiaux committed Apr 20, 2022
    Configuration menu
    Copy the full SHA
    05ae65d View commit details
    Browse the repository at this point in the history

  8. S0 : refine doesn't type check in time

    @thomas-lamiaux
    thomas-lamiaux committed Apr 20, 2022
    Configuration menu
    Copy the full SHA
    514a50f View commit details
    Browse the repository at this point in the history

Commits on Apr 21, 2022

  1. Same issue

    @thomas-lamiaux
    thomas-lamiaux committed Apr 21, 2022
    Configuration menu
    Copy the full SHA
    d763231 View commit details
    Browse the repository at this point in the history

  2. Clean up but still fails computing : 

    -> Add some lemma for computing better
    @thomas-lamiaux
    thomas-lamiaux committed Apr 21, 2022
    Configuration menu
    Copy the full SHA
    dc1dd58 View commit details
    Browse the repository at this point in the history

Commits on Apr 22, 2022

  1. Uniformisation of the files

    @thomas-lamiaux
    thomas-lamiaux committed Apr 22, 2022
    Configuration menu
    Copy the full SHA
    fc7902c View commit details
    Browse the repository at this point in the history

  2. Clean up : 

    -> rename smething ill named and fix dependencies
-> Add a packaging for Hn-Sn
-> Used it to clean H*-S1
    @thomas-lamiaux
    thomas-lamiaux committed Apr 22, 2022
    Configuration menu
    Copy the full SHA
    8e41dad View commit details
    Browse the repository at this point in the history

  3. clean up on S0, still issue

    @thomas-lamiaux
    thomas-lamiaux committed Apr 22, 2022
    Configuration menu
    Copy the full SHA
    fb60c60 View commit details
    Browse the repository at this point in the history

  4. Fix for S0 !

    @thomas-lamiaux
    thomas-lamiaux committed Apr 22, 2022
    Configuration menu
    Copy the full SHA
    67ce7d3 View commit details
    Browse the repository at this point in the history

  5. Add notation for the polynomial ring

    @thomas-lamiaux
    thomas-lamiaux committed Apr 22, 2022
    Configuration menu
    Copy the full SHA
    78d5668 View commit details
    Browse the repository at this point in the history

  6. Fix : forgot to add a file

    @thomas-lamiaux
    thomas-lamiaux committed Apr 22, 2022
    Configuration menu
    Copy the full SHA
    4e4c217 View commit details
    Browse the repository at this point in the history

Commits on Apr 23, 2022

  1. Sn : Partition + transport + functions in both sens

    @thomas-lamiaux
    thomas-lamiaux committed Apr 23, 2022
    Configuration menu
    Copy the full SHA
    2e0cea6 View commit details
    Browse the repository at this point in the history

  2. S1 : Big issue what to do in the case 0 < k < Sn and 0 < l < Sn ?

    @thomas-lamiaux
    thomas-lamiaux committed Apr 23, 2022
    Configuration menu
    Copy the full SHA
    9ee3cd1 View commit details
    Browse the repository at this point in the history

Commits on Apr 24, 2022

  1. Sn : Fix the wronfull traduction + Add / Miss : 

      Add :
-> add the framework for the cup product
-> do the proof up to the missing lemma

(Things that used to hold by computation)

  Miss :
-> map1
-> computation of T0 on Z
-> cancel X²
    @thomas-lamiaux
    thomas-lamiaux committed Apr 24, 2022
    Configuration menu
    Copy the full SHA
    6e2aa4b View commit details
    Browse the repository at this point in the history

Commits on Apr 25, 2022

  1. Sn : Add secction and retraction, Missing computation rule

    @thomas-lamiaux
    thomas-lamiaux committed Apr 25, 2022
    Configuration menu
    Copy the full SHA
    72941a6 View commit details
    Browse the repository at this point in the history

  2. Sn : change the partition

    @thomas-lamiaux
    thomas-lamiaux committed Apr 25, 2022
    Configuration menu
    Copy the full SHA
    0e1dadd View commit details
    Browse the repository at this point in the history

  3. Sn : change the partition

    @thomas-lamiaux
    thomas-lamiaux committed Apr 25, 2022
    Configuration menu
    Copy the full SHA
    774f49a View commit details
    Browse the repository at this point in the history

  4. Sn : computed !

    @thomas-lamiaux
    thomas-lamiaux committed Apr 25, 2022
    Configuration menu
    Copy the full SHA
    e4a40da View commit details
    Browse the repository at this point in the history

Commits on Apr 26, 2022

  1. CP2 : All but cup product morpism on H2 -> H2 -> H4

    @thomas-lamiaux
    thomas-lamiaux committed Apr 26, 2022
    Configuration menu
    Copy the full SHA
    afed64c View commit details
    Browse the repository at this point in the history

  2. CP2 : All except but cup product morphism H2 -> H2 -> H4

    @thomas-lamiaux
    thomas-lamiaux committed Apr 26, 2022
    Configuration menu
    Copy the full SHA
    516c5ae View commit details
    Browse the repository at this point in the history

Commits on Apr 27, 2022

  1. Renaming + add some encode-decode proof

    @thomas-lamiaux
    thomas-lamiaux committed Apr 27, 2022
    Configuration menu
    Copy the full SHA
    1cf0b2b View commit details
    Browse the repository at this point in the history

Commits on Apr 28, 2022

  1. Remove CP2 from pull request + Continue adding lemma

    @thomas-lamiaux
    thomas-lamiaux committed Apr 28, 2022
    Configuration menu
    Copy the full SHA
    28c243d View commit details
    Browse the repository at this point in the history

  2. add a file

    @thomas-lamiaux
    thomas-lamiaux committed Apr 28, 2022
    Configuration menu
    Copy the full SHA
    4a95228 View commit details
    Browse the repository at this point in the history

Commits on Apr 29, 2022

  1. Adding lemma for vec to prove the equivalence

    @thomas-lamiaux
    thomas-lamiaux committed Apr 29, 2022
    Configuration menu
    Copy the full SHA
    42b6e63 View commit details
    Browse the repository at this point in the history

Commits on Apr 30, 2022

  1. Add PA->A-cancel

    @thomas-lamiaux
    thomas-lamiaux committed Apr 30, 2022
    Configuration menu
    Copy the full SHA
    b306cc7 View commit details
    Browse the repository at this point in the history

  2. Add lemma -> entirely prove PA->A-cancel

    @thomas-lamiaux
    thomas-lamiaux committed Apr 30, 2022
    Configuration menu
    Copy the full SHA
    559a91a View commit details
    Browse the repository at this point in the history

Commits on May 2, 2022

  1. Fit an offet issue between 1k0 on Vec and FinVec

    @thomas-lamiaux
    thomas-lamiaux committed May 2, 2022
    Configuration menu
    Copy the full SHA
    4e3b821 View commit details
    Browse the repository at this point in the history

Commits on May 3, 2022

  1. Complete the proof of A[X1,...,Xn]/<X1,...,Xn> equiv A

    @thomas-lamiaux
    thomas-lamiaux committed May 3, 2022
    Configuration menu
    Copy the full SHA
    eaaceda View commit details
    Browse the repository at this point in the history

  2. Merge branch 'agda:master' into master

    @thomas-lamiaux
    thomas-lamiaux committed May 3, 2022
    Configuration menu
    Copy the full SHA
    574ce6d View commit details
    Browse the repository at this point in the history

  3. Merge branch 'master' into cup-product

    @thomas-lamiaux
    thomas-lamiaux committed May 3, 2022
    Configuration menu
    Copy the full SHA
    7b14401 View commit details
    Browse the repository at this point in the history

  4. Fix some merging issues

    @thomas-lamiaux
    thomas-lamiaux committed May 3, 2022
    Configuration menu
    Copy the full SHA
    99c9d7a View commit details
    Browse the repository at this point in the history

  5. Add an explicit equivalence for the previous commit

    @thomas-lamiaux
    thomas-lamiaux committed May 3, 2022
    Configuration menu
    Copy the full SHA
    8a0291a View commit details
    Browse the repository at this point in the history

Commits on May 4, 2022

  1. Add A[X]/X equiv A

    @thomas-lamiaux
    thomas-lamiaux committed May 4, 2022
    Configuration menu
    Copy the full SHA
    5678778 View commit details
    Browse the repository at this point in the history

  2. Add a H*(Unit) = Z + fix a bug

    @thomas-lamiaux
    thomas-lamiaux committed May 4, 2022
    Configuration menu
    Copy the full SHA
    3283566 View commit details
    Browse the repository at this point in the history

Commits on May 5, 2022

  1. Merge branch 'agda:master' into master

    @thomas-lamiaux
    thomas-lamiaux committed May 5, 2022
    Configuration menu
    Copy the full SHA
    64efe74 View commit details
    Browse the repository at this point in the history

  2. Merge branch 'master' into cup-product

    @thomas-lamiaux
    thomas-lamiaux committed May 5, 2022
    Configuration menu
    Copy the full SHA
    a1a5e86 View commit details
    Browse the repository at this point in the history

  3. Enfonce new convention for importing module

    @thomas-lamiaux
    thomas-lamiaux committed May 5, 2022
    Configuration menu
    Copy the full SHA
    f53b681 View commit details
    Browse the repository at this point in the history

  4. Enforce module import convention

    @thomas-lamiaux
    thomas-lamiaux committed May 5, 2022
    Configuration menu
    Copy the full SHA
    1eb2d11 View commit details
    Browse the repository at this point in the history

  5. Enforcing using bot.rec rather then rec-bot

    @thomas-lamiaux
    thomas-lamiaux committed May 5, 2022
    Configuration menu
    Copy the full SHA
    b52322f View commit details
    Browse the repository at this point in the history

  6. clean up importing module + enforcing rec, elim import

    @thomas-lamiaux
    thomas-lamiaux committed May 5, 2022
    Configuration menu
    Copy the full SHA
    41fe5b1 View commit details
    Browse the repository at this point in the history

  7. clean up

    @thomas-lamiaux
    thomas-lamiaux committed May 5, 2022
    Configuration menu
    Copy the full SHA
    0802720 View commit details
    Browse the repository at this point in the history

  8. enforce notation pred...

    @thomas-lamiaux
    thomas-lamiaux committed May 5, 2022
    Configuration menu
    Copy the full SHA
    e182ade View commit details
    Browse the repository at this point in the history

  9. Enforece pres... notation

    @thomas-lamiaux
    thomas-lamiaux committed May 5, 2022
    Configuration menu
    Copy the full SHA
    f8cd307 View commit details
    Browse the repository at this point in the history

  10. Enforce pres... notation

    @thomas-lamiaux
    thomas-lamiaux committed May 5, 2022
    Configuration menu
    Copy the full SHA
    9cbb571 View commit details
    Browse the repository at this point in the history

  11. Enforcing Algebra convention

    @thomas-lamiaux
    thomas-lamiaux committed May 5, 2022
    Configuration menu
    Copy the full SHA
    0b29d54 View commit details
    Browse the repository at this point in the history

Commits on May 6, 2022

  1. Fix pull request

    @thomas-lamiaux
    thomas-lamiaux committed May 6, 2022
    Configuration menu
    Copy the full SHA
    06fe36e View commit details
    Browse the repository at this point in the history

  2. fix trailing white spaces

    @thomas-lamiaux
    thomas-lamiaux committed May 6, 2022
    Configuration menu
    Copy the full SHA
    fc4d006 View commit details
    Browse the repository at this point in the history

Commits on May 7, 2022

  1. Merge branch 'agda:master' into master

    @thomas-lamiaux
    thomas-lamiaux committed May 7, 2022
    Configuration menu
    Copy the full SHA
    a4fa9af View commit details
    Browse the repository at this point in the history

  2. Merge branch 'master' into cup-product

    @thomas-lamiaux
    thomas-lamiaux committed May 7, 2022
    Configuration menu
    Copy the full SHA
    e833b03 View commit details
    Browse the repository at this point in the history

  3. Merge branch 'agda:master' into master

    @thomas-lamiaux
    thomas-lamiaux committed May 7, 2022
    Configuration menu
    Copy the full SHA
    e711dde View commit details
    Browse the repository at this point in the history

  4. Merge branch 'master' into cup-product

    @thomas-lamiaux
    thomas-lamiaux committed May 7, 2022
    Configuration menu
    Copy the full SHA
    48480fc View commit details
    Browse the repository at this point in the history

  5. Add theframework around CP2

    @thomas-lamiaux
    thomas-lamiaux committed May 7, 2022
    Configuration menu
    Copy the full SHA
    30e5f5e View commit details
    Browse the repository at this point in the history

Commits on May 9, 2022

  1. Merge branch 'agda:master' into master

    @thomas-lamiaux
    thomas-lamiaux committed May 9, 2022
    Configuration menu
    Copy the full SHA
    fdf9af8 View commit details
    Browse the repository at this point in the history

Commits on May 13, 2022

  1. Merge branch 'agda:master' into master

    @thomas-lamiaux
    thomas-lamiaux committed May 13, 2022
    Configuration menu
    Copy the full SHA
    39c4855 View commit details
    Browse the repository at this point in the history

  2. Merge branch 'master' into cup-product

    @thomas-lamiaux
    thomas-lamiaux committed May 13, 2022
    Configuration menu
    Copy the full SHA
    1c66581 View commit details
    Browse the repository at this point in the history

  3. update CP2

    @thomas-lamiaux
    thomas-lamiaux committed May 13, 2022
    Configuration menu
    Copy the full SHA
    99f978c View commit details
    Browse the repository at this point in the history

Commits on May 29, 2022

  1. Merge branch 'agda:master' into master

    @thomas-lamiaux
    thomas-lamiaux committed May 29, 2022
    Configuration menu
    Copy the full SHA
    79538ca View commit details
    Browse the repository at this point in the history

  2. Merge branch 'master' into cup-product

    @thomas-lamiaux
    thomas-lamiaux committed May 29, 2022
    Configuration menu
    Copy the full SHA
    737cef0 View commit details
    Browse the repository at this point in the history

Commits on May 30, 2022

  1. A sketch of proof for CP2

    @thomas-lamiaux
    thomas-lamiaux committed May 30, 2022
    Configuration menu
    Copy the full SHA
    db9a22b View commit details
    Browse the repository at this point in the history

Commits on May 31, 2022

  1. Try introducing notation

    @thomas-lamiaux
    thomas-lamiaux committed May 31, 2022
    Configuration menu
    Copy the full SHA
    271992c View commit details
    Browse the repository at this point in the history

  2. Why isn't working ?

    @thomas-lamiaux
    thomas-lamiaux committed May 31, 2022
    Configuration menu
    Copy the full SHA
    aff3c90 View commit details
    Browse the repository at this point in the history

  3. Improve package of the proof

    @thomas-lamiaux
    thomas-lamiaux committed May 31, 2022
    Configuration menu
    Copy the full SHA
    4b7bc8d View commit details
    Browse the repository at this point in the history

Commits on Jun 1, 2022

  1. Add a lemma file

    @thomas-lamiaux
    thomas-lamiaux committed Jun 1, 2022
    Configuration menu
    Copy the full SHA
    5a11c79 View commit details
    Browse the repository at this point in the history

  2. Weird issue

    @thomas-lamiaux
    thomas-lamiaux committed Jun 1, 2022
    Configuration menu
    Copy the full SHA
    71204a1 View commit details
    Browse the repository at this point in the history

Commits on Jun 3, 2022

  1. Merge branch 'agda:master' into master

    @thomas-lamiaux
    thomas-lamiaux committed Jun 3, 2022
    Configuration menu
    Copy the full SHA
    4bb13ca View commit details
    Browse the repository at this point in the history

Commits on Jun 8, 2022

  1. Merge branch 'agda:master' into master

    @thomas-lamiaux
    thomas-lamiaux committed Jun 8, 2022
    Configuration menu
    Copy the full SHA
    53d8b56 View commit details
    Browse the repository at this point in the history

Commits on Jun 13, 2022

  1. Merge branch 'agda:master' into master

    @thomas-lamiaux
    thomas-lamiaux committed Jun 13, 2022
    Configuration menu
    Copy the full SHA
    b02cd00 View commit details
    Browse the repository at this point in the history

Commits on Jun 16, 2022

  1. Merge branch 'agda:master' into master

    @thomas-lamiaux
    thomas-lamiaux committed Jun 16, 2022
    Configuration menu
    Copy the full SHA
    58c0b83 View commit details
    Browse the repository at this point in the history

Commits on Jun 17, 2022

  1. Merge branch 'master' into cup-product

    @thomas-lamiaux
    thomas-lamiaux committed Jun 17, 2022
    Configuration menu
    Copy the full SHA
    9c0b869 View commit details
    Browse the repository at this point in the history

Commits on Jun 19, 2022

  1. Adding CP2 + cleaning Unit

    @thomas-lamiaux
    thomas-lamiaux committed Jun 19, 2022
    Configuration menu
    Copy the full SHA
    11a976f View commit details
    Browse the repository at this point in the history

  2. cleaning S1

    @thomas-lamiaux
    thomas-lamiaux committed Jun 19, 2022
    Configuration menu
    Copy the full SHA
    d7fbba6 View commit details
    Browse the repository at this point in the history

  3. Fix a dependency

    @thomas-lamiaux
    thomas-lamiaux committed Jun 19, 2022
    Configuration menu
    Copy the full SHA
    250ad2b View commit details
    Browse the repository at this point in the history

  4. Begin doing Sn

    @thomas-lamiaux
    thomas-lamiaux committed Jun 19, 2022
    Configuration menu
    Copy the full SHA
    e7b9a9e View commit details
    Browse the repository at this point in the history

  5. Clean Sn

    @thomas-lamiaux
    thomas-lamiaux committed Jun 19, 2022
    Configuration menu
    Copy the full SHA
    c2112bc View commit details
    Browse the repository at this point in the history

  6. Delete useless diff

    @thomas-lamiaux
    thomas-lamiaux committed Jun 19, 2022
    Configuration menu
    Copy the full SHA
    13514c9 View commit details
    Browse the repository at this point in the history

  7. Delete CP2

    @thomas-lamiaux
    thomas-lamiaux committed Jun 19, 2022
    Configuration menu
    Copy the full SHA
    5f2ff89 View commit details
    Browse the repository at this point in the history

  8. Fix issue

    @thomas-lamiaux
    thomas-lamiaux committed Jun 19, 2022
    Configuration menu
    Copy the full SHA
    660f800 View commit details
    Browse the repository at this point in the history

  9. Forgot to delete something

    @thomas-lamiaux
    thomas-lamiaux committed Jun 19, 2022
    Configuration menu
    Copy the full SHA
    f11e34c View commit details
    Browse the repository at this point in the history

Commits on Jul 22, 2022

  1. Merge branch 'agda:master' into master

    @thomas-lamiaux
    thomas-lamiaux committed Jul 22, 2022
    Configuration menu
    Copy the full SHA
    8d4ffb8 View commit details
    Browse the repository at this point in the history

Commits on Aug 14, 2022

  1. Cosmetic changes

    @thomas-lamiaux
    thomas-lamiaux committed Aug 14, 2022
    Configuration menu
    Copy the full SHA
    01df9d9 View commit details
    Browse the repository at this point in the history

Commits on Aug 15, 2022

  1. Some renaming

    @thomas-lamiaux
    thomas-lamiaux committed Aug 15, 2022
    Configuration menu
    Copy the full SHA
    5fbf63e View commit details
    Browse the repository at this point in the history

  2. Small fix

    @thomas-lamiaux
    thomas-lamiaux committed Aug 15, 2022
    Configuration menu
    Copy the full SHA
    303e1a6 View commit details
    Browse the repository at this point in the history

  3. reverse a change

    @thomas-lamiaux
    thomas-lamiaux committed Aug 15, 2022
    Configuration menu
    Copy the full SHA
    bd1891c View commit details
    Browse the repository at this point in the history

  4. Issue version ?

    @thomas-lamiaux
    thomas-lamiaux committed Aug 15, 2022
    Configuration menu
    Copy the full SHA
    388b834 View commit details
    Browse the repository at this point in the history

Commits on Aug 16, 2022

  1. Merge branch 'agda:master' into master

    @thomas-lamiaux
    thomas-lamiaux committed Aug 16, 2022
    Configuration menu
    Copy the full SHA
    a8c066a View commit details
    Browse the repository at this point in the history

  2. Merge branch 'master' into cup-product

    @thomas-lamiaux
    thomas-lamiaux committed Aug 16, 2022
    Configuration menu
    Copy the full SHA
    7753250 View commit details
    Browse the repository at this point in the history

  3. Fix all dep ?

    @thomas-lamiaux
    thomas-lamiaux committed Aug 16, 2022
    Configuration menu
    Copy the full SHA
    0b6cd3e View commit details
    Browse the repository at this point in the history