projects
/
cubicaltt.git
/ shortlog
commit
grep
author
committer
pickaxe
?
search:
re
summary
| shortlog |
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
cubicaltt.git
2015-10-19
Daniel R. Grayson
Merge branch 'master' of github.com:mortberg/cubicaltt...
commit
|
commitdiff
|
tree
|
snapshot
2015-10-16
Anders Mörtberg
Remove some old tests
commit
|
commitdiff
|
tree
|
snapshot
2015-10-16
Anders Mörtberg
Patch and clean the torus example
commit
|
commitdiff
|
tree
|
snapshot
2015-10-15
Daniel R. Grayson
improve Makefile
commit
|
commitdiff
|
tree
|
snapshot
2015-10-14
Anders Mörtberg
Update cabal file (fix typo, remove old email address...
commit
|
commitdiff
|
tree
|
snapshot
2015-10-14
Anders Mörtberg
Merge pull request #19 from tulcod/haskell2010
commit
|
commitdiff
|
tree
|
snapshot
2015-10-14
Anders Mörtberg
Merge pull request #18 from tulcod/master
commit
|
commitdiff
|
tree
|
snapshot
2015-10-14
Auke Booij
Move to haskell 2010
commit
|
commitdiff
|
tree
|
snapshot
2015-10-14
Auke Booij
Populate extra-source-files
commit
|
commitdiff
|
tree
|
snapshot
2015-10-14
Auke Booij
Complete cubicaltt.cabal: list all generated modules...
commit
|
commitdiff
|
tree
|
snapshot
2015-10-14
Auke Booij
Rename executable to cubical (as in Makefile)
commit
|
commitdiff
|
tree
|
snapshot
2015-10-14
Auke Booij
Converted the project into a cabal project.
commit
|
commitdiff
|
tree
|
snapshot
2015-10-11
Daniel R. Grayson
improve Makefile
commit
|
commitdiff
|
tree
|
snapshot
2015-10-05
Anders Mörtberg
Reintroduce hdata
commit
|
commitdiff
|
tree
|
snapshot
2015-09-17
Simon Huber
Removed unGlue
commit
|
commitdiff
|
tree
|
snapshot
2015-09-10
Simon Huber
Merge branch 'mutual'
commit
|
commitdiff
|
tree
|
snapshot
2015-09-10
Simon Huber
Rename Simple into NonMutual and added sanity check
commit
|
commitdiff
|
tree
|
snapshot
2015-09-08
coquand
updated README
commit
|
commitdiff
|
tree
|
snapshot
2015-08-31
Simon Huber
Fixed and added comment for transpHIT
commit
|
commitdiff
|
tree
|
snapshot
2015-08-18
Simon Huber
Reintroduced mutual (wip)
commit
|
commitdiff
|
tree
|
snapshot
2015-08-11
Simon Huber
Fix squeezes
commit
|
commitdiff
|
tree
|
snapshot
2015-08-04
mortberg
Merge pull request #14 from vladimirias/master
commit
|
commitdiff
|
tree
|
snapshot
2015-08-02
Vladimir Voevodsky
The link to Voevodsky's webpage in README updated
commit
|
commitdiff
|
tree
|
snapshot
2015-07-14
Anders Mörtberg
Fix list
commit
|
commitdiff
|
tree
|
snapshot
2015-07-14
Anders Mörtberg
add link to hoq
commit
|
commitdiff
|
tree
|
snapshot
2015-07-03
coquand
update README
commit
|
commitdiff
|
tree
|
snapshot
2015-07-03
coquand
removed some examples (to be updated)
commit
|
commitdiff
|
tree
|
snapshot
2015-07-03
coquand
added some examples
commit
|
commitdiff
|
tree
|
snapshot
2015-07-03
coquand
Merge branch 'master' of https://github.com/mortberg...
commit
|
commitdiff
|
tree
|
snapshot
2015-07-03
coquand
minor changes
commit
|
commitdiff
|
tree
|
snapshot
2015-07-03
Anders Mörtberg
Update README
commit
|
commitdiff
|
tree
|
snapshot
2015-07-02
Anders Mörtberg
Add the proof of univalence using glue with isos
commit
|
commitdiff
|
tree
|
snapshot
2015-07-01
Anders Mörtberg
Fix imports
commit
|
commitdiff
|
tree
|
snapshot
2015-06-30
Anders Mörtberg
Fix typo in typechecker and redefine isoId using glue
commit
|
commitdiff
|
tree
|
snapshot
2015-06-30
Anders Mörtberg
Revert to using iso instead of equiv
commit
|
commitdiff
|
tree
|
snapshot
2015-06-29
Anders
Some lemmas about equivs
commit
|
commitdiff
|
tree
|
snapshot
2015-06-29
Anders
Update aim talk
commit
|
commitdiff
|
tree
|
snapshot
2015-06-28
Simon Huber
Fixed lemCompInv
commit
|
commitdiff
|
tree
|
snapshot
2015-06-24
Simon Huber
Equations for subst and J
commit
|
commitdiff
|
tree
|
snapshot
2015-06-22
Simon Huber
Fix typo in inferType
commit
|
commitdiff
|
tree
|
snapshot
2015-06-18
Anders
Restate univalence
commit
|
commitdiff
|
tree
|
snapshot
2015-06-18
Anders
Update susp
commit
|
commitdiff
|
tree
|
snapshot
2015-06-18
Anders
Update README and update demo.ctt
commit
|
commitdiff
|
tree
|
snapshot
2015-06-18
Anders
Cleaning and reorganization of files
commit
|
commitdiff
|
tree
|
snapshot
2015-06-18
Anders
Merge branch 'no_regular' into equiv
commit
|
commitdiff
|
tree
|
snapshot
2015-06-18
Anders
Cleaning
commit
|
commitdiff
|
tree
|
snapshot
2015-06-18
Anders
Add typechecking for glueElem
commit
|
commitdiff
|
tree
|
snapshot
2015-06-18
Anders
Remove old code for eqToIso and gradLemma for isos
commit
|
commitdiff
|
tree
|
snapshot
2015-06-18
Anders
Make more names unqualified when importing Map and...
commit
|
commitdiff
|
tree
|
snapshot
2015-06-18
Anders
Improve printing of fst and snd
commit
|
commitdiff
|
tree
|
snapshot
2015-06-18
Anders
Remove commented code for GlueLine, GlueLineElem, CompE...
commit
|
commitdiff
|
tree
|
snapshot
2015-06-18
Anders
Reintroduce transport
commit
|
commitdiff
|
tree
|
snapshot
2015-06-18
Anders
Reintroduce glueElem
commit
|
commitdiff
|
tree
|
snapshot
2015-06-17
Anders
Finish the proof of univalence
commit
|
commitdiff
|
tree
|
snapshot
2015-06-17
Anders Mörtberg
Start adding gradlemma to finish proof of univalence
commit
|
commitdiff
|
tree
|
snapshot
2015-06-16
Simon Huber
A proof of univalence (wip)
commit
|
commitdiff
|
tree
|
snapshot
2015-06-16
Simon Huber
Adds projections for equivs
commit
|
commitdiff
|
tree
|
snapshot
2015-06-16
Simon Huber
Typo
commit
|
commitdiff
|
tree
|
snapshot
2015-06-16
Simon Huber
Don't require equivalences to be eta-expanded
commit
|
commitdiff
|
tree
|
snapshot
2015-06-15
Simon Huber
Finished eqToEquiv
commit
|
commitdiff
|
tree
|
snapshot
2015-06-15
Simon Huber
Fix handling of neutral for composition in sums
commit
|
commitdiff
|
tree
|
snapshot
2015-06-13
Anders
Fix hisos''
commit
|
commitdiff
|
tree
|
snapshot
2015-06-12
Anders
Fix printing
commit
|
commitdiff
|
tree
|
snapshot
2015-06-10
Simon Huber
Convertability for HSum
commit
|
commitdiff
|
tree
|
snapshot
2015-06-09
Simon Huber
Rename hiso to equiv
commit
|
commitdiff
|
tree
|
snapshot
2015-06-09
Simon Huber
Equivalences instead of isos (wip)
commit
|
commitdiff
|
tree
|
snapshot
2015-06-08
Anders
Make bool, circle and integer compile
commit
|
commitdiff
|
tree
|
snapshot
2015-06-08
Anders
Add lemSimpl
commit
|
commitdiff
|
tree
|
snapshot
2015-06-08
Simon Huber
Convertability for hComp
commit
|
commitdiff
|
tree
|
snapshot
2015-06-06
Anders Mörtberg
Update aim.ctt again
commit
|
commitdiff
|
tree
|
snapshot
2015-06-06
Anders Mörtberg
Update aim.ctt
commit
|
commitdiff
|
tree
|
snapshot
2015-06-06
Anders Mörtberg
Add AIM talk
commit
|
commitdiff
|
tree
|
snapshot
2015-06-05
Simon Huber
Less definitional equalities for glue
commit
|
commitdiff
|
tree
|
snapshot
2015-06-05
Simon Huber
Throw out transport
commit
|
commitdiff
|
tree
|
snapshot
2015-06-05
Simon Huber
Merge branch 'hisoproj' into no_regular
commit
|
commitdiff
|
tree
|
snapshot
2015-06-05
Simon Huber
Finished eqToIso and removed constants for comp in U
commit
|
commitdiff
|
tree
|
snapshot
2015-06-04
Anders Mörtberg
Update squeezeHIT
commit
|
commitdiff
|
tree
|
snapshot
2015-06-04
Simon Huber
Equality to isomorphism (wip)
commit
|
commitdiff
|
tree
|
snapshot
2015-06-04
Anders Mörtberg
define trans in terms of gencomp
commit
|
commitdiff
|
tree
|
snapshot
2015-06-04
Simon Huber
Added fill as a term and comp is now genComp
commit
|
commitdiff
|
tree
|
snapshot
2015-06-04
Anders
Add genComp and some examples for debugging
commit
|
commitdiff
|
tree
|
snapshot
2015-06-04
Anders
remove commented code
commit
|
commitdiff
|
tree
|
snapshot
2015-06-04
Simon Huber
Adapted HITs
commit
|
commitdiff
|
tree
|
snapshot
2015-06-04
Simon Huber
Fix for neutral unglues
commit
|
commitdiff
|
tree
|
snapshot
2015-06-04
Simon Huber
Added neutral values for unglue
commit
|
commitdiff
|
tree
|
snapshot
2015-06-04
Simon Huber
Adapted
commit
|
commitdiff
|
tree
|
snapshot
2015-06-04
Simon Huber
Added constructor for comp in U
commit
|
commitdiff
|
tree
|
snapshot
2015-06-03
Simon Huber
Fix use of compLine
commit
|
commitdiff
|
tree
|
snapshot
2015-06-03
Anders Mörtberg
Fix add_comm
commit
|
commitdiff
|
tree
|
snapshot
2015-06-03
Anders
isNeutralComp, small fixes to comp and comment things...
commit
|
commitdiff
|
tree
|
snapshot
2015-06-03
Simon Huber
Adapted prelude
commit
|
commitdiff
|
tree
|
snapshot
2015-06-03
Simon Huber
Finished first version
commit
|
commitdiff
|
tree
|
snapshot
2015-06-03
Simon Huber
Adapted compGlue
commit
|
commitdiff
|
tree
|
snapshot
2015-06-02
Simon Huber
Started adapting for the non-regular setting (wip)
commit
|
commitdiff
|
tree
|
snapshot
2015-05-18
Anders
Add direct proof that s2 is trivial (for the HIT defini...
commit
|
commitdiff
|
tree
|
snapshot
2015-05-16
coquand
simple examples on nat and list
commit
|
commitdiff
|
tree
|
snapshot
2015-05-12
Anders
Isomorphism of the direct and the susp definition of S2
commit
|
commitdiff
|
tree
|
snapshot
2015-05-11
Anders
Fix the bug in transport and add optimizations to compE...
commit
|
commitdiff
|
tree
|
snapshot
2015-05-08
Anders
Add exchange law and genPiS3
commit
|
commitdiff
|
tree
|
snapshot
2015-05-08
Anders
Change order in checkPathSystem
commit
|
commitdiff
|
tree
|
snapshot
next