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

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