cubicaltt.git
2016-09-15 Anders Mörtbergcleaning
2016-09-14 Anders Mörtbergvisible -> transparent
2016-09-14 Anders Mörtbergdirect definition of retract
2016-09-14 Anders Mörtbergadd Dan's proof of univalence from ua and uabeta
2016-08-10 Anders MörtbergMerge pull request #50 from david-christiansen/elisp...
2016-08-01 David ChristiansenEmacs mode: Update names for Customize
2016-08-01 David ChristiansenUpdate README for Emacs mode
2016-08-01 David ChristiansenRemove redundant comment command from Emacs mode
2016-08-01 David ChristiansenRemove CL-isms from Emacs mode
2016-08-01 David ChristiansenRename Emacs mode identifiers
2016-08-01 David ChristiansenBetter comment about space-escaping in Emacs mode
2016-07-29 Anders MörtbergMerge pull request #46 from david-christiansen/elisp...
2016-07-29 Anders MörtbergMerge pull request #45 from david-christiansen/emacs...
2016-07-29 Anders MörtbergMerge pull request #44 from gullcomb/opt-decl-cmp
2016-07-29 Anders Mörtbergchange back conversion
2016-07-29 Anders MörtbergMerge branch 'conv'
2016-07-26 David Raymond... Improve the display of Emacs customize
2016-07-26 David Raymond... Add imenu support to the Emacs mode
2016-07-26 David Raymond... Add support for completion
2016-07-26 David Raymond... Make the Emacs mode work for package.el
2016-07-25 David ChristiansenAdd subprocess to Emacs mode
2016-07-14 Anders Mörtbergminor changes
2016-07-12 Guillaume CombetteTag declarations with their location.
2016-07-12 Guillaume CombetteFix build for GHC 7.8
2016-07-11 Anders Mörtbergfix bug in printing
2016-07-11 Anders Mörtbergcleaning of binnat
2016-07-11 Anders MörtbergClean up of univalence and add the definition of unival...
2016-07-08 Rafaël BocquetMerge branch 'csystems'
2016-07-08 Rafaël BocquetFix conv
2016-07-08 Rafaël BocquetMerge branch 'master' into csystems
2016-07-07 Rafaël BocquetSpeed up conv
2016-07-07 Rafaël Bocquetadd some comments in category.ctt and csystem.ctt
2016-07-07 Anders Mörtbergrename visible to transparent and fix printing of glue
2016-07-07 Anders Mörtbergrename glue -> Glue, glueElem -> glue and unglueElem...
2016-07-07 Anders Mörtbergrename Id to Path
2016-07-07 Anders Mörtbergremove nthmUniv
2016-07-07 Anders Mörtbergrename Path to PLam and IdP to PathP
2016-07-07 Anders Mörtbergmake subset compile using opaque
2016-07-07 Anders Mörtbergmove testempty
2016-07-07 Anders Mörtbergmerge mult and multS1
2016-07-07 Anders Mörtbergmove context of indSusp to susp
2016-07-07 Anders Mörtbergmore duplicate definitions
2016-07-07 Anders Mörtbergmove ex1 into circle
2016-07-07 Anders Mörtbergremove duplicate code
2016-07-07 Anders Mörtbergadd a line without any specified points
2016-07-07 Anders MörtbergMerge branch 'csystems'
2016-07-06 Anders Mörtbergdon't hardcode list of ctt files in Makefile for genera...
2016-07-06 Anders Mörtbergcleaning in prelude
2016-07-06 Anders Mörtbergadd equalNat
2016-07-05 Anders Mörtbergfix name of local splits
2016-07-05 Anders Mörtbergadd local split
2016-07-05 Anders Mörtbergadd batch mode flag
2016-07-05 Anders Mörtbergwip
2016-07-05 Anders Mörtbergwip on an equivalent presentation of the circle as...
2016-07-05 Anders Mörtbergminor changes to circle
2016-07-01 Simon HuberMerge pull request #39 from abooij/prop-trunc
2016-06-20 Rafaël BocquetTwo equivalent categories are equal
2016-06-14 Rafaël Bocquetwip
2016-06-13 Rafaël Bocquetwip
2016-06-02 Auke BooijAdd warning about recursive HITs
2016-06-02 Auke BooijRename truncP to inh
2016-06-01 Auke Booijimplement propositional truncation
2016-05-31 Rafaël BocquetSplit csystem.ctt into category.ctt and csystem.ctt
2016-05-24 Anders Mörtbergadd reserved keywords to README
2016-05-23 Rafaël BocquetConstruction of a C0-System from a universe category
2016-05-23 Rafaël BocquetFix the module name
2016-05-23 Rafaël Bocquet(wip) construction of a C0-System from a universe category
2016-05-10 Rafaël BocquetBoth definitions of C systems; the second one implies...
2016-04-27 Thierry Coquandsmall change
2016-04-27 Thierry Coquandwe should improve the evaluator
2016-04-21 Rafaël BocquetMerge branch 'master' of github.com:mortberg/cubicaltt...
2016-04-21 Rafaël Bocquetdefinition of C systems
2016-04-14 Anders MörtbergFinish binnat example and add elimination principles...
2016-04-14 Rafaël Bocquetsimple computation using multZ
2016-04-14 Rafaël Bocquettorsor multiplication
2016-04-13 Rafaël Bocqueteval ignores opaqueness
2016-04-12 Anders MörtbergStart porting binnat
2016-04-12 Rafaël Bocquetvisible_all command
2016-04-12 Rafaël BocquetOpaque/Visible definitions
2016-04-08 Rafaël Bocquetsome proofs
2016-04-08 Rafaël Bocquetslow proof
2016-04-08 Thierry Coquandother proof of lemPropF
2016-04-07 Rafaël BocquetOnly ZEquiv : isEquiv (plus x) is not proven
2016-04-06 Rafaël BocquetS1 = BZ
2016-04-05 Rafaël BocquetMerge branch 'master' of https://github.com/mortberg...
2016-04-05 Rafaël BocquetZ = Id BZ ZBZ ZBZ
2016-04-04 Rafaël Bocquet.
2016-04-02 Thierry Coquandsome computations
2016-04-01 Thierry Coquandstudy of multiplication on S1
2016-04-01 Thierry Coquandproof that S1 is a groupoid
2016-03-06 Anders MörtbergMerge pull request #36 from georgydunaev/master
2016-03-06 Georgy Dunaevadded imports and changed collection.ctt (corrUniv...
2016-03-03 Simon HuberFix squeezeHIT for non-recursive HITs
2016-03-03 Simon HuberAnders bugfix for squeezes
2016-02-18 Anders MörtbergMerge pull request #29 from abooij/master
2016-02-17 Auke BooijSoften version constraints
2016-02-11 Simon HuberFix printing of environments
2016-02-10 Simon HuberTest for correct length in checks (Fixes #27)
2016-01-27 Anders Mörtbergadd a small test of the grad lemma
2016-01-23 Anders Mörtbergcleaning
next