cubicaltt.git
8 years agoadd a small puzzle due to Andrew Polonsky
Anders Mörtberg [Thu, 22 Sep 2016 20:33:24 +0000 (16:33 -0400)]
add a small puzzle due to Andrew Polonsky

8 years agoMerge pull request #49 from mortberg/defeqJ
Anders Mörtberg [Thu, 22 Sep 2016 20:02:51 +0000 (16:02 -0400)]
Merge pull request #49 from mortberg/defeqJ

Add Id types

8 years agoFix insertSystem to maintain invariant for systems
Simon Huber [Mon, 19 Sep 2016 09:26:00 +0000 (11:26 +0200)]
Fix insertSystem to maintain invariant for systems

Closes #52.

8 years agocleaning
Anders Mörtberg [Thu, 15 Sep 2016 17:31:47 +0000 (13:31 -0400)]
cleaning

8 years agocleaning
Anders Mörtberg [Thu, 15 Sep 2016 16:56:15 +0000 (12:56 -0400)]
cleaning

8 years agovisible -> transparent
Anders Mörtberg [Wed, 14 Sep 2016 20:56:58 +0000 (16:56 -0400)]
visible -> transparent

8 years agodirect definition of retract
Anders Mörtberg [Wed, 14 Sep 2016 20:56:15 +0000 (16:56 -0400)]
direct definition of retract

8 years agoadd Dan's proof of univalence from ua and uabeta
Anders Mörtberg [Wed, 14 Sep 2016 20:48:21 +0000 (16:48 -0400)]
add Dan's proof of univalence from ua and uabeta

8 years agoMerge pull request #50 from david-christiansen/elisp-conventions
Anders Mörtberg [Wed, 10 Aug 2016 07:38:27 +0000 (09:38 +0200)]
Merge pull request #50 from david-christiansen/elisp-conventions

Emacs mode updates

8 years agoEmacs mode: Update names for Customize
David Christiansen [Mon, 1 Aug 2016 13:11:38 +0000 (09:11 -0400)]
Emacs mode: Update names for Customize

Now Customize uses the updated names consistently.

8 years agoUpdate README for Emacs mode
David Christiansen [Mon, 1 Aug 2016 13:08:52 +0000 (09:08 -0400)]
Update README for Emacs mode

8 years agoRemove redundant comment command from Emacs mode
David Christiansen [Mon, 1 Aug 2016 13:04:14 +0000 (09:04 -0400)]
Remove redundant comment command from Emacs mode

It is sufficient to set a couple of variables to make the built-in
commenting command work for cubical.

8 years agoRemove CL-isms from Emacs mode
David Christiansen [Mon, 1 Aug 2016 13:02:30 +0000 (09:02 -0400)]
Remove CL-isms from Emacs mode

*foo* is Common Lisp for special variables, while foo is Emacs Lisp for
 the same.

8 years agoRename Emacs mode identifiers
David Christiansen [Mon, 1 Aug 2016 13:01:20 +0000 (09:01 -0400)]
Rename Emacs mode identifiers

Now, the identifiers match the mode filename, per Elisp convention.

8 years agoBetter comment about space-escaping in Emacs mode
David Christiansen [Mon, 1 Aug 2016 12:58:22 +0000 (08:58 -0400)]
Better comment about space-escaping in Emacs mode

The behavior of :cd at the cubical shell is now better described in a
comment, so as to not surprise Elisp hackers.

8 years agodefine equivalence using Id and prove univalence with Id everywhere
Anders Mörtberg [Fri, 29 Jul 2016 12:12:07 +0000 (14:12 +0200)]
define equivalence using Id and prove univalence with Id everywhere

8 years agominor changes
Anders Mörtberg [Tue, 26 Jul 2016 15:26:34 +0000 (17:26 +0200)]
minor changes

8 years agocleaning and a version of univalence for Id
Anders Mörtberg [Tue, 26 Jul 2016 15:18:54 +0000 (17:18 +0200)]
cleaning and a version of univalence for Id

8 years agorename Eq to Id
Anders Mörtberg [Tue, 26 Jul 2016 14:53:35 +0000 (16:53 +0200)]
rename Eq to Id

8 years agoSome experiments with Eq
Simon Huber [Mon, 14 Sep 2015 12:59:00 +0000 (14:59 +0200)]
Some experiments with Eq

8 years agoAdded Eq types with definitional equality for J
Simon Huber [Mon, 31 Aug 2015 14:19:16 +0000 (16:19 +0200)]
Added Eq types with definitional equality for J

8 years agoMerge pull request #46 from david-christiansen/elisp-conventions
Anders Mörtberg [Fri, 29 Jul 2016 09:35:58 +0000 (11:35 +0200)]
Merge pull request #46 from david-christiansen/elisp-conventions

Emacs mode: completion, imenu, and friendlier Customize

8 years agoMerge pull request #45 from david-christiansen/emacs-update
Anders Mörtberg [Fri, 29 Jul 2016 09:35:24 +0000 (11:35 +0200)]
Merge pull request #45 from david-christiansen/emacs-update

Add subprocess to Emacs mode

8 years agoMerge pull request #44 from gullcomb/opt-decl-cmp
Anders Mörtberg [Fri, 29 Jul 2016 09:18:03 +0000 (11:18 +0200)]
Merge pull request #44 from gullcomb/opt-decl-cmp

Speed up comparison of environments

8 years agochange back conversion
Anders Mörtberg [Fri, 29 Jul 2016 09:16:48 +0000 (11:16 +0200)]
change back conversion

8 years agoMerge branch 'conv'
Anders Mörtberg [Fri, 29 Jul 2016 09:09:06 +0000 (11:09 +0200)]
Merge branch 'conv'

8 years agoImprove the display of Emacs customize
David Raymond Christiansen [Tue, 26 Jul 2016 15:39:50 +0000 (11:39 -0400)]
Improve the display of Emacs customize

The customization options in Emacs are now shown with friendlier names.

8 years agoAdd imenu support to the Emacs mode
David Raymond Christiansen [Tue, 26 Jul 2016 15:37:04 +0000 (11:37 -0400)]
Add imenu support to the Emacs mode

imenu is a general-purpose index for things in a buffer, used by a
variety of Emacs tools to give a list of definitions in the buffer.
This adds support for it to the Emacs mode.

8 years agoAdd support for completion
David Raymond Christiansen [Tue, 26 Jul 2016 15:26:34 +0000 (11:26 -0400)]
Add support for completion

Define a completion function and add it to completion-at-point-functions
in ctt-mode. This function is used by many different completion systems
in Emacs, including company-mode and the built-in simple
completion-at-point.

Completion uses a regexp to attempt to find names defined in the current
buffer as well as using the language keywords as sources of completion.

8 years agoMake the Emacs mode work for package.el
David Raymond Christiansen [Tue, 26 Jul 2016 14:43:48 +0000 (10:43 -0400)]
Make the Emacs mode work for package.el

Modify the Emacs mode to make it follow typical Elisp conventions, as
well as adding the necessary headers to make it work in the package
system.

Additionally, the mode is now derived from prog-mode, which will enable
hooks that should work for all programming language modes to run.

8 years agoAdd subprocess to Emacs mode
David Christiansen [Mon, 25 Jul 2016 13:29:07 +0000 (09:29 -0400)]
Add subprocess to Emacs mode

The Emacs mode for cubical can now run cubical as a subprocess. The
keybinding "C-c C-l", which is the same as Agda and Idris, saves the
current buffer and loads it in cubical.

Additionally, a Customize setting is added to allow users to easily
customize the command to be used to invoke cubical.

8 years agominor changes
Anders Mörtberg [Thu, 14 Jul 2016 13:30:54 +0000 (15:30 +0200)]
minor changes

8 years agoTag declarations with their location.
Guillaume Combette [Tue, 12 Jul 2016 15:58:52 +0000 (17:58 +0200)]
Tag declarations with their location.

This speeds up the comparison of environments in the common case of
identical declarations.

8 years agoFix build for GHC 7.8
Guillaume Combette [Tue, 12 Jul 2016 14:42:19 +0000 (16:42 +0200)]
Fix build for GHC 7.8

This version does not implement the Foldable/Traversable in Prelude
proposal thus `elem` does not work on Sets.

8 years agofix bug in printing
Anders Mörtberg [Mon, 11 Jul 2016 21:25:19 +0000 (23:25 +0200)]
fix bug in printing

8 years agocleaning of binnat
Anders Mörtberg [Mon, 11 Jul 2016 20:22:21 +0000 (22:22 +0200)]
cleaning of binnat

8 years agoClean up of univalence and add the definition of univalence using the map defined...
Anders Mörtberg [Mon, 11 Jul 2016 19:32:40 +0000 (21:32 +0200)]
Clean up of univalence and add the definition of univalence using the map defined using J

8 years agoMerge branch 'csystems'
Rafaël Bocquet [Fri, 8 Jul 2016 07:58:02 +0000 (09:58 +0200)]
Merge branch 'csystems'

8 years agoFix conv
Rafaël Bocquet [Fri, 8 Jul 2016 07:30:49 +0000 (09:30 +0200)]
Fix conv

8 years agoMerge branch 'master' into csystems
Rafaël Bocquet [Fri, 8 Jul 2016 07:29:45 +0000 (09:29 +0200)]
Merge branch 'master' into csystems

8 years agoSpeed up conv
Rafaël Bocquet [Thu, 7 Jul 2016 15:34:29 +0000 (17:34 +0200)]
Speed up conv

8 years agoadd some comments in category.ctt and csystem.ctt
Rafaël Bocquet [Thu, 7 Jul 2016 15:33:06 +0000 (17:33 +0200)]
add some comments in category.ctt and csystem.ctt

8 years agorename visible to transparent and fix printing of glue
Anders Mörtberg [Thu, 7 Jul 2016 14:14:51 +0000 (16:14 +0200)]
rename visible to transparent and fix printing of glue

8 years agorename glue -> Glue, glueElem -> glue and unglueElem -> unglue
Anders Mörtberg [Thu, 7 Jul 2016 14:03:02 +0000 (16:03 +0200)]
rename glue -> Glue, glueElem -> glue and unglueElem -> unglue

8 years agorename Id to Path
Anders Mörtberg [Thu, 7 Jul 2016 13:57:52 +0000 (15:57 +0200)]
rename Id to Path

8 years agoremove nthmUniv
Anders Mörtberg [Thu, 7 Jul 2016 13:47:07 +0000 (15:47 +0200)]
remove nthmUniv

8 years agorename Path to PLam and IdP to PathP
Anders Mörtberg [Thu, 7 Jul 2016 13:43:11 +0000 (15:43 +0200)]
rename Path to PLam and IdP to PathP

8 years agomake subset compile using opaque
Anders Mörtberg [Thu, 7 Jul 2016 12:06:08 +0000 (14:06 +0200)]
make subset compile using opaque

8 years agomove testempty
Anders Mörtberg [Thu, 7 Jul 2016 11:57:41 +0000 (13:57 +0200)]
move testempty

8 years agomerge mult and multS1
Anders Mörtberg [Thu, 7 Jul 2016 11:47:31 +0000 (13:47 +0200)]
merge mult and multS1

8 years agomove context of indSusp to susp
Anders Mörtberg [Thu, 7 Jul 2016 11:43:02 +0000 (13:43 +0200)]
move context of indSusp to susp

8 years agomore duplicate definitions
Anders Mörtberg [Thu, 7 Jul 2016 11:38:21 +0000 (13:38 +0200)]
more duplicate definitions

8 years agomove ex1 into circle
Anders Mörtberg [Thu, 7 Jul 2016 11:34:56 +0000 (13:34 +0200)]
move ex1 into circle

8 years agoremove duplicate code
Anders Mörtberg [Thu, 7 Jul 2016 11:32:35 +0000 (13:32 +0200)]
remove duplicate code

8 years agoadd a line without any specified points
Anders Mörtberg [Thu, 7 Jul 2016 10:58:21 +0000 (12:58 +0200)]
add a line without any specified points

8 years agoMerge branch 'csystems'
Anders Mörtberg [Thu, 7 Jul 2016 10:34:12 +0000 (12:34 +0200)]
Merge branch 'csystems'

# Conflicts:
# cubicaltt.el
# examples/helix.ctt

8 years agodon't hardcode list of ctt files in Makefile for generating TAGS file
Anders Mörtberg [Wed, 6 Jul 2016 11:39:38 +0000 (13:39 +0200)]
don't hardcode list of ctt files in Makefile for generating TAGS file

8 years agocleaning in prelude
Anders Mörtberg [Wed, 6 Jul 2016 11:17:13 +0000 (13:17 +0200)]
cleaning in prelude

8 years agoadd equalNat
Anders Mörtberg [Wed, 6 Jul 2016 11:06:00 +0000 (13:06 +0200)]
add equalNat

8 years agofix name of local splits
Anders Mörtberg [Tue, 5 Jul 2016 14:06:27 +0000 (16:06 +0200)]
fix name of local splits

8 years agoadd local split
Anders Mörtberg [Tue, 5 Jul 2016 13:42:30 +0000 (15:42 +0200)]
add local split

8 years agoadd batch mode flag
Anders Mörtberg [Tue, 5 Jul 2016 12:09:46 +0000 (14:09 +0200)]
add batch mode flag

8 years agowip
Anders Mörtberg [Tue, 5 Jul 2016 11:57:49 +0000 (13:57 +0200)]
wip

8 years agowip on an equivalent presentation of the circle as a quotient of unit
Anders Mörtberg [Tue, 5 Jul 2016 11:41:10 +0000 (13:41 +0200)]
wip on an equivalent presentation of the circle as a quotient of unit

8 years agominor changes to circle
Anders Mörtberg [Tue, 5 Jul 2016 11:35:23 +0000 (13:35 +0200)]
minor changes to circle

8 years agoMerge pull request #39 from abooij/prop-trunc
Simon Huber [Fri, 1 Jul 2016 12:34:42 +0000 (14:34 +0200)]
Merge pull request #39 from abooij/prop-trunc

implement propositional truncation

8 years agoTwo equivalent categories are equal
Rafaël Bocquet [Fri, 17 Jun 2016 15:07:49 +0000 (17:07 +0200)]
Two equivalent categories are equal

8 years agowip
Rafaël Bocquet [Tue, 14 Jun 2016 08:51:29 +0000 (10:51 +0200)]
wip

8 years agowip
Rafaël Bocquet [Mon, 13 Jun 2016 15:16:35 +0000 (17:16 +0200)]
wip

8 years agoAdd warning about recursive HITs
Auke Booij [Thu, 2 Jun 2016 22:47:41 +0000 (23:47 +0100)]
Add warning about recursive HITs

8 years agoRename truncP to inh
Auke Booij [Thu, 2 Jun 2016 22:44:11 +0000 (23:44 +0100)]
Rename truncP to inh

8 years agoimplement propositional truncation
Auke Booij [Wed, 1 Jun 2016 14:41:30 +0000 (15:41 +0100)]
implement propositional truncation

8 years agoSplit csystem.ctt into category.ctt and csystem.ctt
Rafaël Bocquet [Tue, 31 May 2016 15:00:01 +0000 (17:00 +0200)]
Split csystem.ctt into category.ctt and csystem.ctt

8 years agoadd reserved keywords to README
Anders Mörtberg [Tue, 24 May 2016 15:58:53 +0000 (11:58 -0400)]
add reserved keywords to README

8 years agoConstruction of a C0-System from a universe category
Rafaël Bocquet [Mon, 23 May 2016 14:50:54 +0000 (16:50 +0200)]
Construction of a C0-System from a universe category

8 years agoFix the module name
Rafaël Bocquet [Mon, 23 May 2016 13:58:51 +0000 (15:58 +0200)]
Fix the module name

8 years ago(wip) construction of a C0-System from a universe category
Rafaël Bocquet [Mon, 23 May 2016 13:55:06 +0000 (15:55 +0200)]
(wip) construction of a C0-System from a universe category

8 years agoBoth definitions of C systems; the second one implies the first one
Rafaël Bocquet [Tue, 10 May 2016 10:06:41 +0000 (12:06 +0200)]
Both definitions of C systems; the second one implies the first one

8 years agosmall change
Thierry Coquand [Wed, 27 Apr 2016 09:27:47 +0000 (11:27 +0200)]
small change

8 years agowe should improve the evaluator
Thierry Coquand [Wed, 27 Apr 2016 09:22:34 +0000 (11:22 +0200)]
we should improve the evaluator

8 years agoMerge branch 'master' of github.com:mortberg/cubicaltt into torsor
Rafaël Bocquet [Thu, 21 Apr 2016 14:33:08 +0000 (16:33 +0200)]
Merge branch 'master' of github.com:mortberg/cubicaltt into torsor

8 years agodefinition of C systems
Rafaël Bocquet [Thu, 21 Apr 2016 14:33:01 +0000 (16:33 +0200)]
definition of C systems

8 years agoFinish binnat example and add elimination principles for equivalences and isomorphisms
Anders Mörtberg [Thu, 14 Apr 2016 18:13:02 +0000 (14:13 -0400)]
Finish binnat example and add elimination principles for equivalences and isomorphisms

8 years agosimple computation using multZ
Rafaël Bocquet [Thu, 14 Apr 2016 12:17:08 +0000 (14:17 +0200)]
simple computation using multZ

8 years agotorsor multiplication
Rafaël Bocquet [Thu, 14 Apr 2016 10:13:34 +0000 (12:13 +0200)]
torsor multiplication

8 years agoeval ignores opaqueness
Rafaël Bocquet [Wed, 13 Apr 2016 08:48:59 +0000 (10:48 +0200)]
eval ignores opaqueness
Proof of BZ = (X : (A:U) * (A->A)) * inh (X = (Z, sucZ))

8 years agoStart porting binnat
Anders Mörtberg [Tue, 12 Apr 2016 21:50:54 +0000 (17:50 -0400)]
Start porting binnat

8 years agovisible_all command
Rafaël Bocquet [Tue, 12 Apr 2016 15:29:34 +0000 (17:29 +0200)]
visible_all command

8 years agoOpaque/Visible definitions
Rafaël Bocquet [Tue, 12 Apr 2016 13:02:26 +0000 (15:02 +0200)]
Opaque/Visible definitions

8 years agosome proofs
Rafaël Bocquet [Fri, 8 Apr 2016 12:22:03 +0000 (14:22 +0200)]
some proofs

8 years agoslow proof
Rafaël Bocquet [Fri, 8 Apr 2016 11:35:53 +0000 (13:35 +0200)]
slow proof

8 years agoother proof of lemPropF
Thierry Coquand [Fri, 8 Apr 2016 07:09:00 +0000 (09:09 +0200)]
other proof of lemPropF

8 years agoOnly ZEquiv : isEquiv (plus x) is not proven
Rafaël Bocquet [Thu, 7 Apr 2016 09:19:36 +0000 (11:19 +0200)]
Only ZEquiv : isEquiv (plus x) is not proven

8 years agoS1 = BZ
Rafaël Bocquet [Wed, 6 Apr 2016 14:42:27 +0000 (16:42 +0200)]
S1 = BZ

8 years agoMerge branch 'master' of https://github.com/mortberg/cubicaltt
Rafaël Bocquet [Tue, 5 Apr 2016 09:30:19 +0000 (11:30 +0200)]
Merge branch 'master' of https://github.com/mortberg/cubicaltt

8 years agoZ = Id BZ ZBZ ZBZ
Rafaël Bocquet [Tue, 5 Apr 2016 09:30:13 +0000 (11:30 +0200)]
Z = Id BZ ZBZ ZBZ

8 years ago.
Rafaël Bocquet [Mon, 4 Apr 2016 07:12:04 +0000 (09:12 +0200)]
.

8 years agosome computations
Thierry Coquand [Sat, 2 Apr 2016 11:49:45 +0000 (13:49 +0200)]
some computations

8 years agostudy of multiplication on S1
Thierry Coquand [Fri, 1 Apr 2016 10:26:27 +0000 (12:26 +0200)]
study of multiplication on S1

8 years agoproof that S1 is a groupoid
Thierry Coquand [Fri, 1 Apr 2016 10:22:28 +0000 (12:22 +0200)]
proof that S1 is a groupoid