projects
/
cubicaltt.git
/ shortlog
commit
grep
author
committer
pickaxe
?
search:
re
summary
| shortlog |
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
cubicaltt.git
2016-07-11
Anders Mörtberg
fix bug in printing
commit
|
commitdiff
|
tree
|
snapshot
2016-07-11
Anders Mörtberg
cleaning of binnat
commit
|
commitdiff
|
tree
|
snapshot
2016-07-11
Anders Mörtberg
Clean up of univalence and add the definition of unival...
commit
|
commitdiff
|
tree
|
snapshot
2016-07-07
Anders Mörtberg
rename visible to transparent and fix printing of glue
commit
|
commitdiff
|
tree
|
snapshot
2016-07-07
Anders Mörtberg
rename glue -> Glue, glueElem -> glue and unglueElem...
commit
|
commitdiff
|
tree
|
snapshot
2016-07-07
Anders Mörtberg
rename Id to Path
commit
|
commitdiff
|
tree
|
snapshot
2016-07-07
Anders Mörtberg
remove nthmUniv
commit
|
commitdiff
|
tree
|
snapshot
2016-07-07
Anders Mörtberg
rename Path to PLam and IdP to PathP
commit
|
commitdiff
|
tree
|
snapshot
2016-07-07
Anders Mörtberg
make subset compile using opaque
commit
|
commitdiff
|
tree
|
snapshot
2016-07-07
Anders Mörtberg
move testempty
commit
|
commitdiff
|
tree
|
snapshot
2016-07-07
Anders Mörtberg
merge mult and multS1
commit
|
commitdiff
|
tree
|
snapshot
2016-07-07
Anders Mörtberg
move context of indSusp to susp
commit
|
commitdiff
|
tree
|
snapshot
2016-07-07
Anders Mörtberg
more duplicate definitions
commit
|
commitdiff
|
tree
|
snapshot
2016-07-07
Anders Mörtberg
move ex1 into circle
commit
|
commitdiff
|
tree
|
snapshot
2016-07-07
Anders Mörtberg
remove duplicate code
commit
|
commitdiff
|
tree
|
snapshot
2016-07-07
Anders Mörtberg
add a line without any specified points
commit
|
commitdiff
|
tree
|
snapshot
2016-07-07
Anders Mörtberg
Merge branch 'csystems'
commit
|
commitdiff
|
tree
|
snapshot
2016-07-06
Anders Mörtberg
don't hardcode list of ctt files in Makefile for genera...
commit
|
commitdiff
|
tree
|
snapshot
2016-07-06
Anders Mörtberg
cleaning in prelude
commit
|
commitdiff
|
tree
|
snapshot
2016-07-06
Anders Mörtberg
add equalNat
commit
|
commitdiff
|
tree
|
snapshot
2016-07-05
Anders Mörtberg
fix name of local splits
commit
|
commitdiff
|
tree
|
snapshot
2016-07-05
Anders Mörtberg
add local split
commit
|
commitdiff
|
tree
|
snapshot
2016-07-05
Anders Mörtberg
add batch mode flag
commit
|
commitdiff
|
tree
|
snapshot
2016-07-05
Anders Mörtberg
wip
commit
|
commitdiff
|
tree
|
snapshot
2016-07-05
Anders Mörtberg
wip on an equivalent presentation of the circle as...
commit
|
commitdiff
|
tree
|
snapshot
2016-07-05
Anders Mörtberg
minor changes to circle
commit
|
commitdiff
|
tree
|
snapshot
2016-07-01
Simon Huber
Merge pull request #39 from abooij/prop-trunc
commit
|
commitdiff
|
tree
|
snapshot
2016-06-20
Rafaël Bocquet
Two equivalent categories are equal
commit
|
commitdiff
|
tree
|
snapshot
2016-06-14
Rafaël Bocquet
wip
commit
|
commitdiff
|
tree
|
snapshot
2016-06-13
Rafaël Bocquet
wip
commit
|
commitdiff
|
tree
|
snapshot
2016-06-02
Auke Booij
Add warning about recursive HITs
commit
|
commitdiff
|
tree
|
snapshot
2016-06-02
Auke Booij
Rename truncP to inh
commit
|
commitdiff
|
tree
|
snapshot
2016-06-01
Auke Booij
implement propositional truncation
commit
|
commitdiff
|
tree
|
snapshot
2016-05-31
Rafaël Bocquet
Split csystem.ctt into category.ctt and csystem.ctt
commit
|
commitdiff
|
tree
|
snapshot
2016-05-24
Anders Mörtberg
add reserved keywords to README
commit
|
commitdiff
|
tree
|
snapshot
2016-05-23
Rafaël Bocquet
Construction of a C0-System from a universe category
commit
|
commitdiff
|
tree
|
snapshot
2016-05-23
Rafaël Bocquet
Fix the module name
commit
|
commitdiff
|
tree
|
snapshot
2016-05-23
Rafaël Bocquet
(wip) construction of a C0-System from a universe category
commit
|
commitdiff
|
tree
|
snapshot
2016-05-10
Rafaël Bocquet
Both definitions of C systems; the second one implies...
commit
|
commitdiff
|
tree
|
snapshot
2016-04-27
Thierry Coquand
small change
commit
|
commitdiff
|
tree
|
snapshot
2016-04-27
Thierry Coquand
we should improve the evaluator
commit
|
commitdiff
|
tree
|
snapshot
2016-04-21
Rafaël Bocquet
Merge branch 'master' of github.com:mortberg/cubicaltt...
commit
|
commitdiff
|
tree
|
snapshot
2016-04-21
Rafaël Bocquet
definition of C systems
commit
|
commitdiff
|
tree
|
snapshot
2016-04-14
Anders Mörtberg
Finish binnat example and add elimination principles...
commit
|
commitdiff
|
tree
|
snapshot
2016-04-14
Rafaël Bocquet
simple computation using multZ
commit
|
commitdiff
|
tree
|
snapshot
2016-04-14
Rafaël Bocquet
torsor multiplication
commit
|
commitdiff
|
tree
|
snapshot
2016-04-13
Rafaël Bocquet
eval ignores opaqueness
commit
|
commitdiff
|
tree
|
snapshot
2016-04-12
Anders Mörtberg
Start porting binnat
commit
|
commitdiff
|
tree
|
snapshot
2016-04-12
Rafaël Bocquet
visible_all command
commit
|
commitdiff
|
tree
|
snapshot
2016-04-12
Rafaël Bocquet
Opaque/Visible definitions
commit
|
commitdiff
|
tree
|
snapshot
2016-04-08
Rafaël Bocquet
some proofs
commit
|
commitdiff
|
tree
|
snapshot
2016-04-08
Rafaël Bocquet
slow proof
commit
|
commitdiff
|
tree
|
snapshot
2016-04-08
Thierry Coquand
other proof of lemPropF
commit
|
commitdiff
|
tree
|
snapshot
2016-04-07
Rafaël Bocquet
Only ZEquiv : isEquiv (plus x) is not proven
commit
|
commitdiff
|
tree
|
snapshot
2016-04-06
Rafaël Bocquet
S1 = BZ
commit
|
commitdiff
|
tree
|
snapshot
2016-04-05
Rafaël Bocquet
Merge branch 'master' of https://github.com/mortberg...
commit
|
commitdiff
|
tree
|
snapshot
2016-04-05
Rafaël Bocquet
Z = Id BZ ZBZ ZBZ
commit
|
commitdiff
|
tree
|
snapshot
2016-04-04
Rafaël Bocquet
.
commit
|
commitdiff
|
tree
|
snapshot
2016-04-02
Thierry Coquand
some computations
commit
|
commitdiff
|
tree
|
snapshot
2016-04-01
Thierry Coquand
study of multiplication on S1
commit
|
commitdiff
|
tree
|
snapshot
2016-04-01
Thierry Coquand
proof that S1 is a groupoid
commit
|
commitdiff
|
tree
|
snapshot
2016-03-06
Anders Mörtberg
Merge pull request #36 from georgydunaev/master
commit
|
commitdiff
|
tree
|
snapshot
2016-03-06
Georgy Dunaev
added imports and changed collection.ctt (corrUniv...
commit
|
commitdiff
|
tree
|
snapshot
2016-03-03
Simon Huber
Fix squeezeHIT for non-recursive HITs
commit
|
commitdiff
|
tree
|
snapshot
2016-03-03
Simon Huber
Anders bugfix for squeezes
commit
|
commitdiff
|
tree
|
snapshot
2016-02-18
Anders Mörtberg
Merge pull request #29 from abooij/master
commit
|
commitdiff
|
tree
|
snapshot
2016-02-17
Auke Booij
Soften version constraints
commit
|
commitdiff
|
tree
|
snapshot
2016-02-11
Simon Huber
Fix printing of environments
commit
|
commitdiff
|
tree
|
snapshot
2016-02-10
Simon Huber
Test for correct length in checks (Fixes #27)
commit
|
commitdiff
|
tree
|
snapshot
2016-01-27
Anders Mörtberg
add a small test of the grad lemma
commit
|
commitdiff
|
tree
|
snapshot
2016-01-23
Anders Mörtberg
cleaning
commit
|
commitdiff
|
tree
|
snapshot
2016-01-23
Anders Mörtberg
Merge branch 'nunivalence'
commit
|
commitdiff
|
tree
|
snapshot
2016-01-23
Anders Mörtberg
comment in nthmUniv
commit
|
commitdiff
|
tree
|
snapshot
2016-01-23
Anders Mörtberg
add the correct normal form of univalence
commit
|
commitdiff
|
tree
|
snapshot
2016-01-23
Anders Mörtberg
use uahp' in setquot instead
commit
|
commitdiff
|
tree
|
snapshot
2016-01-20
Anders Mörtberg
Fix ö
commit
|
commitdiff
|
tree
|
snapshot
2016-01-20
Simon Huber
Updated readme
commit
|
commitdiff
|
tree
|
snapshot
2016-01-18
Simon Huber
Missing case for checking GlueElem against VCompU
commit
|
commitdiff
|
tree
|
snapshot
2016-01-15
Anders Mörtberg
move two lemmas to nat
commit
|
commitdiff
|
tree
|
snapshot
2016-01-15
Anders Mörtberg
finish the hz exercise
commit
|
commitdiff
|
tree
|
snapshot
2016-01-15
Anders Mörtberg
Finish the last undefined in setquot
commit
|
commitdiff
|
tree
|
snapshot
2016-01-15
Anders Mörtberg
"fix" bug
commit
|
commitdiff
|
tree
|
snapshot
2016-01-15
Simon Huber
Bugfix in inferType
commit
|
commitdiff
|
tree
|
snapshot
2016-01-15
Anders Mörtberg
setquot is a set
commit
|
commitdiff
|
tree
|
snapshot
2016-01-15
Anders Mörtberg
one less undefined
commit
|
commitdiff
|
tree
|
snapshot
2016-01-15
Anders Mörtberg
squash some admits
commit
|
commitdiff
|
tree
|
snapshot
2016-01-14
Anders Mörtberg
minor changes
commit
|
commitdiff
|
tree
|
snapshot
2016-01-14
Anders Mörtberg
more on setquot. on the way to define an equality test...
commit
|
commitdiff
|
tree
|
snapshot
2016-01-14
Anders Mörtberg
add nlem1
commit
|
commitdiff
|
tree
|
snapshot
2016-01-14
Anders Mörtberg
Change printing of environments
commit
|
commitdiff
|
tree
|
snapshot
2016-01-14
Anders Mörtberg
rename sig to Sigma and make setquot compile
commit
|
commitdiff
|
tree
|
snapshot
2016-01-14
Anders Mörtberg
make bool compile and move tests using univalence for...
commit
|
commitdiff
|
tree
|
snapshot
2016-01-14
Simon Huber
Bugfix in compU and compGlue
commit
|
commitdiff
|
tree
|
snapshot
2016-01-12
Simon Huber
Bugfix by Fabian Ruch
commit
|
commitdiff
|
tree
|
snapshot
2016-01-09
Anders Mörtberg
fix bug
commit
|
commitdiff
|
tree
|
snapshot
2016-01-08
Anders Mörtberg
cleaning
commit
|
commitdiff
|
tree
|
snapshot
2016-01-07
Anders Mörtberg
comment gradLemmaU
commit
|
commitdiff
|
tree
|
snapshot
2016-01-07
Anders Mörtberg
remove @@@
commit
|
commitdiff
|
tree
|
snapshot
2016-01-07
Anders Mörtberg
dont write to a file
commit
|
commitdiff
|
tree
|
snapshot
2016-01-07
Anders Mörtberg
"_" in constPath again
commit
|
commitdiff
|
tree
|
snapshot
next