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

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