projects
/
cubicaltt.git
/ shortlog
commit
grep
author
committer
pickaxe
?
search:
re
summary
| shortlog |
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
cubicaltt.git
2015-04-13
Anders Mörtberg
Update help message
commit
|
commitdiff
|
tree
|
snapshot
2015-04-13
Anders Mörtberg
Update README
commit
|
commitdiff
|
tree
|
snapshot
2015-04-13
Anders Mörtberg
Move stream to experiments
commit
|
commitdiff
|
tree
|
snapshot
2015-04-13
Anders
Add dependency graph script
commit
|
commitdiff
|
tree
|
snapshot
2015-04-13
Anders
Update README
commit
|
commitdiff
|
tree
|
snapshot
2015-04-13
Anders
Lots of cleaning in the examples
commit
|
commitdiff
|
tree
|
snapshot
2015-04-13
Anders
Add equiv and uafunext2
commit
|
commitdiff
|
tree
|
snapshot
2015-04-13
Anders
Reorganized and cleaned some examples
commit
|
commitdiff
|
tree
|
snapshot
2015-04-13
Anders
Update README
commit
|
commitdiff
|
tree
|
snapshot
2015-04-13
Anders
Fix README
commit
|
commitdiff
|
tree
|
snapshot
2015-04-13
Anders
Update README
commit
|
commitdiff
|
tree
|
snapshot
2015-04-13
Anders
Update the README and examples
commit
|
commitdiff
|
tree
|
snapshot
2015-04-13
Simon Huber
demo from the proglog talk
commit
|
commitdiff
|
tree
|
snapshot
2015-04-13
Simon Huber
use smart fst/snd in act
commit
|
commitdiff
|
tree
|
snapshot
2015-04-12
Simon Huber
added thierrys examples (funext from univalence,helix)
commit
|
commitdiff
|
tree
|
snapshot
2015-04-11
Simon Huber
fixing use of isNeutral
commit
|
commitdiff
|
tree
|
snapshot
2015-04-10
Anders
Fix parsing of trans, comp, etc.
commit
|
commitdiff
|
tree
|
snapshot
2015-04-10
Anders
Explicitly pass around the history
commit
|
commitdiff
|
tree
|
snapshot
2015-04-10
mortberg
Merge pull request #6 from nad/master
commit
|
commitdiff
|
tree
|
snapshot
2015-04-09
Anders Mörtberg
Start the proof that ua implies funext
commit
|
commitdiff
|
tree
|
snapshot
2015-04-09
Nils Anders...
Proved (?) that equality coincides with bisimilarity.
commit
|
commitdiff
|
tree
|
snapshot
2015-04-09
Anders
Clean examples
commit
|
commitdiff
|
tree
|
snapshot
2015-04-09
Anders
Add normalization function
commit
|
commitdiff
|
tree
|
snapshot
2015-04-09
Simon Huber
funext from interval
commit
|
commitdiff
|
tree
|
snapshot
2015-04-08
Simon Huber
don't crash the main loop if error in eval
commit
|
commitdiff
|
tree
|
snapshot
2015-04-08
Simon Huber
split annotation is now the type not the family; typo...
commit
|
commitdiff
|
tree
|
snapshot
2015-04-08
Simon Huber
evaluate undefined into a closure
commit
|
commitdiff
|
tree
|
snapshot
2015-04-08
Simon Huber
function should be known in def (for general recursion)
commit
|
commitdiff
|
tree
|
snapshot
2015-04-08
Anders
Cleaning
commit
|
commitdiff
|
tree
|
snapshot
2015-04-08
Simon Huber
added thierrys adapted files
commit
|
commitdiff
|
tree
|
snapshot
2015-04-07
Simon Huber
improve show of a sum
commit
|
commitdiff
|
tree
|
snapshot
2015-04-07
Simon Huber
analogous fix for pathUniv
commit
|
commitdiff
|
tree
|
snapshot
2015-04-07
Simon Huber
bugfix in pathUnivTrans
commit
|
commitdiff
|
tree
|
snapshot
2015-03-31
Simon Huber
reintroduce faceEnv
commit
|
commitdiff
|
tree
|
snapshot
2015-03-31
Anders
Cleaned and simplified type checker
commit
|
commitdiff
|
tree
|
snapshot
2015-03-30
Simon Huber
bugfix in simplify, conv; extended prelude
commit
|
commitdiff
|
tree
|
snapshot
2015-03-29
Anders
Fix parsing of /\
commit
|
commitdiff
|
tree
|
snapshot
2015-03-29
Anders Mörtberg
Fix error message when path constructors are written...
commit
|
commitdiff
|
tree
|
snapshot
2015-03-28
Anders Mörtberg
Cleaning
commit
|
commitdiff
|
tree
|
snapshot
2015-03-27
Anders
Update Makefile
commit
|
commitdiff
|
tree
|
snapshot
2015-03-27
Anders
readme
commit
|
commitdiff
|
tree
|
snapshot
2015-03-27
Anders
fix readme
commit
|
commitdiff
|
tree
|
snapshot
2015-03-27
Anders
fix readme
commit
|
commitdiff
|
tree
|
snapshot
2015-03-27
Anders
Update readme
commit
|
commitdiff
|
tree
|
snapshot
2015-03-27
Anders
Examples
commit
|
commitdiff
|
tree
|
snapshot
2015-03-27
Anders
app for VCompElem and VElimComp
commit
|
commitdiff
|
tree
|
snapshot
2015-03-27
Anders
Fix conversion of formulas
commit
|
commitdiff
|
tree
|
snapshot
2015-03-27
Anders
Fix isNeutral
commit
|
commitdiff
|
tree
|
snapshot
2015-03-26
Anders
Add more tests
commit
|
commitdiff
|
tree
|
snapshot
2015-03-26
Anders
Fix a bug in eqLemma
commit
|
commitdiff
|
tree
|
snapshot
2015-03-26
Anders
Add the circle (there is a bug)
commit
|
commitdiff
|
tree
|
snapshot
2015-03-26
Anders
Finish adding HITs
commit
|
commitdiff
|
tree
|
snapshot
2015-03-26
Anders
Add squeeze, fix some bugs and optimize(?) transport
commit
|
commitdiff
|
tree
|
snapshot
2015-03-26
Simon Huber
moved transGlue; typo in compGlue
commit
|
commitdiff
|
tree
|
snapshot
2015-03-25
Anders
Add HITs (parsing and resolver missing)
commit
|
commitdiff
|
tree
|
snapshot
2015-03-24
Simon Huber
examples
commit
|
commitdiff
|
tree
|
snapshot
2015-03-24
Simon Huber
bugfix in trans
commit
|
commitdiff
|
tree
|
snapshot
2015-03-24
Simon Huber
bugfix for act on a path
commit
|
commitdiff
|
tree
|
snapshot
2015-03-24
Simon Huber
added compElem and elimComp (still buggy)
commit
|
commitdiff
|
tree
|
snapshot
2015-03-24
Simon Huber
pairs now associate to the right
commit
|
commitdiff
|
tree
|
snapshot
2015-03-24
Simon Huber
lemTest not in prelude..
commit
|
commitdiff
|
tree
|
snapshot
2015-03-24
Simon Huber
added simplify for Trans and Comp
commit
|
commitdiff
|
tree
|
snapshot
2015-03-24
Simon Huber
removed Map. here and there
commit
|
commitdiff
|
tree
|
snapshot
2015-03-24
Simon Huber
fixed bug; switched a with b in hiso
commit
|
commitdiff
|
tree
|
snapshot
2015-03-24
Simon Huber
enhanced and renamed emacs mode
commit
|
commitdiff
|
tree
|
snapshot
2015-03-23
Anders
Finish adding glue
commit
|
commitdiff
|
tree
|
snapshot
2015-03-23
Anders
Add evaluation of Glue and GlueElem
commit
|
commitdiff
|
tree
|
snapshot
2015-03-20
Simon Huber
fixed compLine; improved error msg for @@
commit
|
commitdiff
|
tree
|
snapshot
2015-03-20
Simon Huber
dont crash the resolver if expression could not be...
commit
|
commitdiff
|
tree
|
snapshot
2015-03-20
Anders
Update .gitignore
commit
|
commitdiff
|
tree
|
snapshot
2015-03-20
Anders
Fix printing of formulas in AppFormula
commit
|
commitdiff
|
tree
|
snapshot
2015-03-20
Anders
Add support for multiple bindings of dimensions
commit
|
commitdiff
|
tree
|
snapshot
2015-03-20
Anders
Fix printing of systems
commit
|
commitdiff
|
tree
|
snapshot
2015-03-20
Anders
Fix bug in gensym and add Square
commit
|
commitdiff
|
tree
|
snapshot
2015-03-19
Anders
Finish implementing comp
commit
|
commitdiff
|
tree
|
snapshot
2015-03-19
Anders
Parsing of systems
commit
|
commitdiff
|
tree
|
snapshot
2015-03-19
Anders
Started adding comp
commit
|
commitdiff
|
tree
|
snapshot
2015-03-19
Simon Huber
the endpoints of a path should match the Id arguments...
commit
|
commitdiff
|
tree
|
snapshot
2015-03-19
Simon Huber
throw out Binder
commit
|
commitdiff
|
tree
|
snapshot
2015-03-19
Simon Huber
time to wake up
commit
|
commitdiff
|
tree
|
snapshot
2015-03-19
Simon Huber
reintroduced Convertible typeclass; fixed conv for...
commit
|
commitdiff
|
tree
|
snapshot
2015-03-19
Simon Huber
fixed support for Env
commit
|
commitdiff
|
tree
|
snapshot
2015-03-19
Anders Mörtberg
Start adding inferType
commit
|
commitdiff
|
tree
|
snapshot
2015-03-19
Anders Mörtberg
Add 0 and 1 to parser and resolver
commit
|
commitdiff
|
tree
|
snapshot
2015-03-19
Anders Mörtberg
Use checkPath when checking IdP
commit
|
commitdiff
|
tree
|
snapshot
2015-03-19
Anders Mörtberg
Add .gitignore
commit
|
commitdiff
|
tree
|
snapshot
2015-03-19
Anders Mörtberg
Names are now strings
commit
|
commitdiff
|
tree
|
snapshot
2015-03-19
Anders Mörtberg
Add J
commit
|
commitdiff
|
tree
|
snapshot
2015-03-19
Anders Mörtberg
Fix a typo in the parser
commit
|
commitdiff
|
tree
|
snapshot
2015-03-18
Simon Huber
added transport
commit
|
commitdiff
|
tree
|
snapshot
2015-03-18
Simon Huber
show transport like we parse it; whitespace
commit
|
commitdiff
|
tree
|
snapshot
2015-03-18
Simon Huber
added app of a formula
commit
|
commitdiff
|
tree
|
snapshot
2015-03-18
Anders
Add Id, Path, AppFormula and Trans.
commit
|
commitdiff
|
tree
|
snapshot
2015-03-18
Anders
Add Connections
commit
|
commitdiff
|
tree
|
snapshot
2015-03-18
Anders
Rename to cubical
commit
|
commitdiff
|
tree
|
snapshot
2015-03-18
Anders
Start adding Id types
commit
|
commitdiff
|
tree
|
snapshot
2015-03-18
Anders
Remove Neutral data type
commit
|
commitdiff
|
tree
|
snapshot
2015-03-18
Anders Mörtberg
Clean Resolver
commit
|
commitdiff
|
tree
|
snapshot
2015-03-18
Anders
Start working on cubical type theory
commit
|
commitdiff
|
tree
|
snapshot
2015-02-26
Anders
Initial commit
commit
|
commitdiff
|
tree
|
snapshot
next