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

definitional inductives #2

Merged
merged 23 commits into from
Apr 1, 2019
Merged

definitional inductives #2

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
23 commits
Select commit Hold shift + click to select a range
106800e
Start of Inductives.
LuisScoccola Dec 12, 2017
5c000de
Modified travis and Makefile.
LuisScoccola Dec 12, 2017
918e13c
Merged travis.
LuisScoccola Dec 12, 2017
205f3c2
Added a bit on coalgebras, added polynomial functors.
LuisScoccola Dec 12, 2017
77661cb
Trying to prove Lemma 5.1.8 in Felix's thesis.
LuisScoccola Dec 13, 2017
f6ebfab
Finished the proof of 5.1.8
LuisScoccola Dec 13, 2017
73a69c2
Closer to proving that WHom'(W, C) is contractible for every C.
LuisScoccola Dec 14, 2017
8d3d189
Proved that WHom'(W,C) is contractible for every C
LuisScoccola Dec 14, 2017
c4486e9
Proving WHom' is equivalent to WHom.
LuisScoccola Dec 14, 2017
6f69d5b
Finished proof that W is an initial algebra.
LuisScoccola Dec 16, 2017
7ca97ed
Fixed some typos.
LuisScoccola Dec 17, 2017
7e46c64
Cleaning algebras.v a bit
LuisScoccola Dec 24, 2017
5d51473
Cleaning addresses.v a bit
LuisScoccola Dec 24, 2017
116c4d7
Construct M-types from nat
s9ferech Jan 21, 2018
eaeaa40
Make M-types indexed
s9ferech Feb 8, 2018
2af232b
Extend M-types for judgmental computation rule
s9ferech Mar 7, 2018
5182d39
WIP: Make W-types indexed
s9ferech Apr 1, 2019
4353399
WIP: Define mu- and nu-containers
s9ferech Apr 1, 2019
3f48ece
resolved conflicts
Apr 1, 2019
7dad77c
Merge branch 'LuisScoccola-master' into restorescoccolarech
Apr 1, 2019
ef9c646
most recent version of felix
Apr 1, 2019
d232b69
compiling version
Apr 1, 2019
39d8c34
epsilon
Apr 1, 2019
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 2 additions & 0 deletions .travis.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -19,10 +19,12 @@ env:
- PACKAGES=Tactics BUILD_COQIDE=yes BUILD_ALSO=TAGS
- PACKAGES=Folds
- PACKAGES=Induction
- PACKAGES=Inductives
- PACKAGES="Foundations Combinatorics Algebra NumberSystems" COQ_BRANCH=master

# The "docker run" command will pull if needed.
# Running this first gives two tries in case of network lossage.

before_script:
- timeout 5m docker pull palmskog/xenial-unimath || timeout 5m docker pull palmskog/xenial-unimath || timeout 5m docker pull palmskog/xenial-unimath

Expand Down
1 change: 1 addition & 0 deletions Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -25,6 +25,7 @@ PACKAGES += Folds
PACKAGES += HomologicalAlgebra
PACKAGES += Paradoxes
PACKAGES += Induction
PACKAGES += Inductives
############################################
# other user options; see also build/Makefile-configuration-template
BUILD_COQ ?= yes
Expand Down
9 changes: 9 additions & 0 deletions UniMath/CONTENTS.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -431,3 +431,12 @@ The packages and files are listed here in logical order: each file depends only
- [W/Uniqueness.v](Induction/W/Uniqueness.v)
- [M/Chains.v](Induction/M/Chains.v)
- [All.v](Induction/All.v)
## Package Inductives
- [functors.v](Inductives/functors.v)
- [auxiliary_lemmas.v](Inductives/auxiliary_lemmas.v)
- [containers.v](Inductives/containers.v)
- [algebras.v](Inductives/algebras.v)
- [M_from_nat.v](Inductives/M_from_nat.v)
- [addresses.v](Inductives/addresses.v)
- [W_from_M.v](Inductives/W_from_M.v)
- [All.v](Inductives/All.v)
7 changes: 7 additions & 0 deletions UniMath/Inductives/.package/files
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
functors.v
auxiliary_lemmas.v
containers.v
algebras.v
M_from_nat.v
addresses.v
W_from_M.v
Loading