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

Computational M-types #1233

Merged
merged 61 commits into from Jun 6, 2019
Merged

Computational M-types #1233

merged 61 commits into from Jun 6, 2019

Commits on Dec 12, 2017

  1. Start of Inductives.

    @LuisScoccola
    LuisScoccola committed Dec 12, 2017
    Configuration menu
    Copy the full SHA
    106800e View commit details
    Browse the repository at this point in the history

  2. Modified travis and Makefile.

    @LuisScoccola
    LuisScoccola committed Dec 12, 2017
    Configuration menu
    Copy the full SHA
    5c000de View commit details
    Browse the repository at this point in the history

  3. Merged travis.

    @LuisScoccola
    LuisScoccola committed Dec 12, 2017
    Configuration menu
    Copy the full SHA
    918e13c View commit details
    Browse the repository at this point in the history

  4. Added a bit on coalgebras, added polynomial functors.

    @LuisScoccola
    LuisScoccola committed Dec 12, 2017
    Configuration menu
    Copy the full SHA
    205f3c2 View commit details
    Browse the repository at this point in the history

Commits on Dec 13, 2017

  1. Trying to prove Lemma 5.1.8 in Felix's thesis.

    @LuisScoccola
    LuisScoccola committed Dec 13, 2017
    Configuration menu
    Copy the full SHA
    77661cb View commit details
    Browse the repository at this point in the history

  2. Finished the proof of 5.1.8

    @LuisScoccola
    LuisScoccola committed Dec 13, 2017
    Configuration menu
    Copy the full SHA
    f6ebfab View commit details
    Browse the repository at this point in the history

Commits on Dec 14, 2017

  1. Closer to proving that WHom'(W, C) is contractible for every C.

    @LuisScoccola
    LuisScoccola committed Dec 14, 2017
    Configuration menu
    Copy the full SHA
    73a69c2 View commit details
    Browse the repository at this point in the history

  2. Proved that WHom'(W,C) is contractible for every C

    @LuisScoccola
    LuisScoccola committed Dec 14, 2017
    Configuration menu
    Copy the full SHA
    8d3d189 View commit details
    Browse the repository at this point in the history

  3. Proving WHom' is equivalent to WHom.

    @LuisScoccola
    LuisScoccola committed Dec 14, 2017
    Configuration menu
    Copy the full SHA
    c4486e9 View commit details
    Browse the repository at this point in the history

Commits on Dec 16, 2017

  1. Finished proof that W is an initial algebra.

    @LuisScoccola
    LuisScoccola committed Dec 16, 2017
    Configuration menu
    Copy the full SHA
    6f69d5b View commit details
    Browse the repository at this point in the history

Commits on Dec 17, 2017

  1. Fixed some typos.

    @LuisScoccola
    LuisScoccola committed Dec 17, 2017
    Configuration menu
    Copy the full SHA
    7ca97ed View commit details
    Browse the repository at this point in the history

Commits on Dec 24, 2017

  1. Cleaning algebras.v a bit

    @LuisScoccola
    LuisScoccola committed Dec 24, 2017
    Configuration menu
    Copy the full SHA
    7e46c64 View commit details
    Browse the repository at this point in the history

  2. Cleaning addresses.v a bit

    @LuisScoccola
    LuisScoccola committed Dec 24, 2017
    Configuration menu
    Copy the full SHA
    5d51473 View commit details
    Browse the repository at this point in the history

Commits on Feb 7, 2018

  1. Construct M-types from nat

    @s9ferech
    s9ferech committed Feb 7, 2018
    Configuration menu
    Copy the full SHA
    116c4d7 View commit details
    Browse the repository at this point in the history

Commits on Feb 12, 2018

  1. Make M-types indexed

    @s9ferech
    s9ferech committed Feb 12, 2018
    Configuration menu
    Copy the full SHA
    eaeaa40 View commit details
    Browse the repository at this point in the history

Commits on Mar 7, 2018

  1. Extend M-types for judgmental computation rule

    @s9ferech
    s9ferech committed Mar 7, 2018
    Configuration menu
    Copy the full SHA
    2af232b View commit details
    Browse the repository at this point in the history

Commits on Apr 1, 2019

  1. the base file with the project context

    @rmatthes
    rmatthes committed Apr 1, 2019
    Configuration menu
    Copy the full SHA
    54b9d06 View commit details
    Browse the repository at this point in the history

  2. WIP: Make W-types indexed

    @s9ferech
    s9ferech committed Apr 1, 2019
    Configuration menu
    Copy the full SHA
    5182d39 View commit details
    Browse the repository at this point in the history

  3. WIP: Define mu- and nu-containers

    @s9ferech
    s9ferech committed Apr 1, 2019
    Configuration menu
    Copy the full SHA
    4353399 View commit details
    Browse the repository at this point in the history

  4. resolved conflicts

    Dominik Kirst committed Apr 1, 2019
    Configuration menu
    Copy the full SHA
    3f48ece View commit details
    Browse the repository at this point in the history

  5. Merge branch 'LuisScoccola-master' into restorescoccolarech

    Dominik Kirst committed Apr 1, 2019
    Configuration menu
    Copy the full SHA
    7dad77c View commit details
    Browse the repository at this point in the history

  6. most recent version of felix

    Dominik Kirst committed Apr 1, 2019
    Configuration menu
    Copy the full SHA
    ef9c646 View commit details
    Browse the repository at this point in the history

  7. compiling version

    Dominik Kirst committed Apr 1, 2019
    Configuration menu
    Copy the full SHA
    d232b69 View commit details
    Browse the repository at this point in the history

  8. epsilon

    Dominik Kirst committed Apr 1, 2019
    Configuration menu
    Copy the full SHA
    39d8c34 View commit details
    Browse the repository at this point in the history

  9. my slides at the EUTYPES workshop in Nijmegen 2018 with comments on R… 

    …ech's construction (see p. 22)
    @rmatthes
    rmatthes committed Apr 1, 2019
    Configuration menu
    Copy the full SHA
    62c9fc3 View commit details
    Browse the repository at this point in the history

  10. Merge pull request #2 from unimath2019-ri/restorescoccolarech 

    definitional inductives
    @dominik-kirst
    dominik-kirst committed Apr 1, 2019
    Configuration menu
    Copy the full SHA
    a68437a View commit details
    Browse the repository at this point in the history

  11. Merge branch 'dev' of https://github.com/unimath2019-ri/UniMath into dev

    @rmatthes
    rmatthes committed Apr 1, 2019
    Configuration menu
    Copy the full SHA
    91d228c View commit details
    Browse the repository at this point in the history

  12. Merge branch 'master' into dev

    @rmatthes
    rmatthes committed Apr 1, 2019
    Configuration menu
    Copy the full SHA
    cea58a0 View commit details
    Browse the repository at this point in the history

  13. independence of propositional resizing rule mentioned

    @rmatthes
    rmatthes committed Apr 1, 2019
    Configuration menu
    Copy the full SHA
    2417afc View commit details
    Browse the repository at this point in the history

  14. forgotten commenting of non-compiling code

    @rmatthes
    rmatthes committed Apr 1, 2019
    Configuration menu
    Copy the full SHA
    80f406d View commit details
    Browse the repository at this point in the history

  15. Merge pull request #3 from unimath2019-ri/commentnoncompilingpart 

    forgotten commenting of non-compiling code
    @rmatthes
    rmatthes committed Apr 1, 2019
    Configuration menu
    Copy the full SHA
    26de029 View commit details
    Browse the repository at this point in the history

Commits on Apr 2, 2019

  1. Added missing statements from Felix without proof.

    Christian Uldal Graulund committed Apr 2, 2019
    Configuration menu
    Copy the full SHA
    8ce0ddf View commit details
    Browse the repository at this point in the history

  2. Merge branch 'dev' of https://github.com/unimath2019-ri/UniMath into dev

    Christian Uldal Graulund committed Apr 2, 2019
    Configuration menu
    Copy the full SHA
    409da2c View commit details
    Browse the repository at this point in the history

  3. Proof of Lemma 11 from Non-wellfounded trees. 

    (Adapted from Felix Rech).
    Christian Uldal Graulund committed Apr 2, 2019
    Configuration menu
    Copy the full SHA
    c101d8d View commit details
    Browse the repository at this point in the history

  4. starting on ComputationalM.v

    Dominik Kirst committed Apr 2, 2019
    Configuration menu
    Copy the full SHA
    2fd92b7 View commit details
    Browse the repository at this point in the history

  5. Merge branch 'dev' of https://github.com/unimath2019-ri/UniMath into dev

    Dominik Kirst committed Apr 2, 2019
    Configuration menu
    Copy the full SHA
    d0a9431 View commit details
    Browse the repository at this point in the history

  6. minor improvements 

    - Chains.v now compiles with closing section
- newlines at the end of three files
- identify some of the redundant auxiliary lemmas of Felix Rech
    @rmatthes
    rmatthes committed Apr 2, 2019
    Configuration menu
    Copy the full SHA
    48f9819 View commit details
    Browse the repository at this point in the history

  7. Merge pull request #4 from unimath2019-ri/minorimprovementsoninductives 

    Minor improvements on inductives
    @rmatthes
    rmatthes committed Apr 2, 2019
    Configuration menu
    Copy the full SHA
    3b9fbe2 View commit details
    Browse the repository at this point in the history

  8. corecursive equation

    @dominik-kirst
    dominik-kirst committed Apr 2, 2019
    Configuration menu
    Copy the full SHA
    e693b75 View commit details
    Browse the repository at this point in the history

Commits on Apr 3, 2019

  1. morphism equation and refactoring

    @dominik-kirst
    dominik-kirst committed Apr 3, 2019
    Configuration menu
    Copy the full SHA
    27cf1ce View commit details
    Browse the repository at this point in the history

Commits on Apr 4, 2019

  1. carriers are equal

    @dominik-kirst
    dominik-kirst committed Apr 4, 2019
    Configuration menu
    Copy the full SHA
    f46e0cf View commit details
    Browse the repository at this point in the history

  2. still working on equations

    @dominik-kirst
    dominik-kirst committed Apr 4, 2019
    Configuration menu
    Copy the full SHA
    331188f View commit details
    Browse the repository at this point in the history

Commits on Apr 5, 2019

  1. proved finality plus cleanup

    @dominik-kirst
    dominik-kirst committed Apr 5, 2019
    Configuration menu
    Copy the full SHA
    54c3deb View commit details
    Browse the repository at this point in the history

Commits on Apr 6, 2019

  1. inform makefile about ComputationalM.v, replace reflexivity by apply … 

    …idpath
    @rmatthes
    rmatthes committed Apr 6, 2019
    Configuration menu
    Copy the full SHA
    00aa48b View commit details
    Browse the repository at this point in the history

Commits on May 16, 2019

  1. replaces some projections by accessors (very shallow contribution)

    @rmatthes
    rmatthes committed May 16, 2019
    Configuration menu
    Copy the full SHA
    5f49e04 View commit details
    Browse the repository at this point in the history

  2. Merge branch 'master' into computationalM

    @rmatthes
    rmatthes committed May 16, 2019
    Configuration menu
    Copy the full SHA
    e48805d View commit details
    Browse the repository at this point in the history

  3. shallow changes to reestablish compilation

    @rmatthes
    rmatthes committed May 16, 2019
    Configuration menu
    Copy the full SHA
    3882ba9 View commit details
    Browse the repository at this point in the history

  4. wip on establishing isprop for the crucial property P 

    this is by transfer of the already formalized proof by Felix Rech
    @rmatthes
    rmatthes committed May 16, 2019
    Configuration menu
    Copy the full SHA
    78858b7 View commit details
    Browse the repository at this point in the history

  5. fills the gaps in the development: P proven a proposition, fine-tunin… 

    …g for proper behaviour
    @rmatthes
    rmatthes committed May 16, 2019
    Configuration menu
    Copy the full SHA
    242397f View commit details
    Browse the repository at this point in the history

Commits on Jun 3, 2019

  1. epsilon

    @dominik-kirst
    dominik-kirst committed Jun 3, 2019
    Configuration menu
    Copy the full SHA
    94893bd View commit details
    Browse the repository at this point in the history

  2. delta

    @dominik-kirst
    dominik-kirst committed Jun 3, 2019
    Configuration menu
    Copy the full SHA
    e771582 View commit details
    Browse the repository at this point in the history

Commits on Jun 4, 2019

  1. Merge branch 'master' into computationalM

    @rmatthes
    rmatthes committed Jun 4, 2019
    Configuration menu
    Copy the full SHA
    ade382c View commit details
    Browse the repository at this point in the history

  2. corrects a left-over from the merge process

    @rmatthes
    rmatthes committed Jun 4, 2019
    Configuration menu
    Copy the full SHA
    b55caed View commit details
    Browse the repository at this point in the history

  3. some cleanup 

    - uses function composition more often
- upstream lemmas were mostly in the library, one moved to MoreFoundations/PartA.v
- extended header information about the UniMath schools that contributed to the present file
    @rmatthes
    rmatthes committed Jun 4, 2019
    Configuration menu
    Copy the full SHA
    5912b8a View commit details
    Browse the repository at this point in the history

Commits on Jun 5, 2019

  1. erased remaining two upstream lemmas

    @dominik-kirst
    dominik-kirst committed Jun 5, 2019
    Configuration menu
    Copy the full SHA
    af3c4cd View commit details
    Browse the repository at this point in the history

  2. modifies list of authors after email exchange with Dominik

    @rmatthes
    rmatthes committed Jun 5, 2019
    Configuration menu
    Copy the full SHA
    8a00fc4 View commit details
    Browse the repository at this point in the history

  3. leaves out material on which project work at UniMathSchool 2019 was b… 

    …ased

this does not give a clean commit history, but at least, the overall diff for the PR under construction will be readable
    @rmatthes
    rmatthes committed Jun 5, 2019
    Configuration menu
    Copy the full SHA
    2473613 View commit details
    Browse the repository at this point in the history

  4. tiny changes to minimize number of modified files in PR

    @rmatthes
    rmatthes committed Jun 5, 2019
    Configuration menu
    Copy the full SHA
    6e37919 View commit details
    Browse the repository at this point in the history

Commits on Jun 6, 2019

  1. description of PR integrated into introductory comments

    @rmatthes
    rmatthes committed Jun 6, 2019
    Configuration menu
    Copy the full SHA
    5d19115 View commit details
    Browse the repository at this point in the history

  2. Defined replaces Qed everywhere, except for the lemma proved by idpath

    @rmatthes
    rmatthes committed Jun 6, 2019
    Configuration menu
    Copy the full SHA
    f6af06a View commit details
    Browse the repository at this point in the history

  3. last Qed turned into Defined

    @rmatthes
    rmatthes committed Jun 6, 2019
    Configuration menu
    Copy the full SHA
    efb26ef View commit details
    Browse the repository at this point in the history