cubicaltt.git
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 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 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 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

8 years agoMerge pull request #36 from georgydunaev/master
Anders Mörtberg [Sun, 6 Mar 2016 14:51:28 +0000 (09:51 -0500)]
Merge pull request #36 from georgydunaev/master

added imports and changed examples/collection.ctt (corrUniv B A)

8 years agoadded imports and changed collection.ctt (corrUniv B A)
Georgy Dunaev [Sun, 6 Mar 2016 09:06:12 +0000 (12:06 +0300)]
added imports and changed collection.ctt (corrUniv B A)

8 years agoFix squeezeHIT for non-recursive HITs
Simon Huber [Thu, 3 Mar 2016 16:31:39 +0000 (17:31 +0100)]
Fix squeezeHIT for non-recursive HITs

8 years agoAnders bugfix for squeezes
Simon Huber [Thu, 3 Mar 2016 12:38:15 +0000 (13:38 +0100)]
Anders bugfix for squeezes

8 years agoMerge pull request #29 from abooij/master
Anders Mörtberg [Thu, 18 Feb 2016 05:54:50 +0000 (00:54 -0500)]
Merge pull request #29 from abooij/master

Soften version constraints

8 years agoSoften version constraints
Auke Booij [Wed, 17 Feb 2016 15:46:18 +0000 (15:46 +0000)]
Soften version constraints

8 years agoFix printing of environments
Simon Huber [Thu, 11 Feb 2016 12:31:33 +0000 (13:31 +0100)]
Fix printing of environments

8 years agoTest for correct length in checks (Fixes #27)
Simon Huber [Wed, 10 Feb 2016 20:31:41 +0000 (21:31 +0100)]
Test for correct length in checks (Fixes #27)

8 years agoadd a small test of the grad lemma
Anders Mörtberg [Wed, 27 Jan 2016 20:35:27 +0000 (15:35 -0500)]
add a small test of the grad lemma

8 years agocleaning
Anders Mörtberg [Sat, 23 Jan 2016 17:51:36 +0000 (12:51 -0500)]
cleaning

8 years agoMerge branch 'nunivalence'
Anders Mörtberg [Sat, 23 Jan 2016 17:40:21 +0000 (12:40 -0500)]
Merge branch 'nunivalence'

8 years agocomment in nthmUniv
Anders Mörtberg [Sat, 23 Jan 2016 17:38:16 +0000 (12:38 -0500)]
comment in nthmUniv

8 years agoadd the correct normal form of univalence
Anders Mörtberg [Sat, 23 Jan 2016 17:36:05 +0000 (12:36 -0500)]
add the correct normal form of univalence

8 years agouse uahp' in setquot instead
Anders Mörtberg [Sat, 23 Jan 2016 17:32:56 +0000 (12:32 -0500)]
use uahp' in setquot instead

8 years agoFix ö
Anders Mörtberg [Wed, 20 Jan 2016 14:00:09 +0000 (09:00 -0500)]
Fix ö

8 years agoUpdated readme
Simon Huber [Wed, 20 Jan 2016 10:44:39 +0000 (11:44 +0100)]
Updated readme

8 years agoMissing case for checking GlueElem against VCompU
Simon Huber [Mon, 18 Jan 2016 10:42:15 +0000 (11:42 +0100)]
Missing case for checking GlueElem against VCompU

8 years agomove two lemmas to nat
Anders Mörtberg [Fri, 15 Jan 2016 21:29:06 +0000 (16:29 -0500)]
move two lemmas to nat

8 years agofinish the hz exercise
Anders Mörtberg [Fri, 15 Jan 2016 21:05:40 +0000 (16:05 -0500)]
finish the hz exercise

8 years agoFinish the last undefined in setquot
Anders Mörtberg [Fri, 15 Jan 2016 19:08:23 +0000 (14:08 -0500)]
Finish the last undefined in setquot

8 years ago"fix" bug
Anders Mörtberg [Fri, 15 Jan 2016 16:49:15 +0000 (11:49 -0500)]
"fix" bug

8 years agoBugfix in inferType
Simon Huber [Fri, 15 Jan 2016 16:38:32 +0000 (17:38 +0100)]
Bugfix in inferType

8 years agosetquot is a set
Anders Mörtberg [Fri, 15 Jan 2016 03:55:34 +0000 (22:55 -0500)]
setquot is a set

8 years agoone less undefined
Anders Mörtberg [Fri, 15 Jan 2016 03:44:12 +0000 (22:44 -0500)]
one less undefined

8 years agosquash some admits
Anders Mörtberg [Fri, 15 Jan 2016 03:22:41 +0000 (22:22 -0500)]
squash some admits

8 years agominor changes
Anders Mörtberg [Thu, 14 Jan 2016 23:21:50 +0000 (18:21 -0500)]
minor changes

8 years agomore on setquot. on the way to define an equality test for hz
Anders Mörtberg [Thu, 14 Jan 2016 21:56:45 +0000 (16:56 -0500)]
more on setquot. on the way to define an equality test for hz

8 years agoadd nlem1
Anders Mörtberg [Thu, 14 Jan 2016 15:36:33 +0000 (10:36 -0500)]
add nlem1