pi4s3 (first 5 maps)

move girard

Merge pull request #40 from abooij/girard

Implement girard's paradox to show impredicativity of cubicaltt

Merge pull request #65 from mortberg/fiximporterrors

Proper error handling when importing files

Merge pull request #70 from Sobernard/master

Constant cubes in 2D, 3D and 4D

more explanations

update README

update README

update README

add README for the lectures

lecture 4

update lectures

comments

general constcubes 2-3-4D

constcubes in n dimensions

spurious import

proper error handling when importing files

add first version of lecture 4

Merge pull request #66 from mortberg/shadowed

Check if some names were shadowed while loading a file

move test up

remove empty lines

Check if some names were shadowed while loading the file

fix typos

add lecture 3

minor

minor

minor update to lecture 2

Add lecture 2

update lecture1

lecture1

update lecture

first lecture

Allow overlapping Arbitrary for Face and System

Boxing Env to prevent Show conflicts with newer versions of haskell packages

minor change

Merge pull request #60 from Rotsor/more-parens-in-goal

More parentheses when printing values

Merge pull request #59 from Rotsor/checkPLam-error-message

better error message from checkPLam

Fix printing of idC and idJ also for values

Don't use smart-constructors when normalizing values

Show idC and idJ as we parse them

More parentheses when printing values

Fixes a bug where not enough parentheses would be printed.
Previously if a function F is defined by split, `F (F x)` would be printed as `F F x`.
Now it's printed as `F (F x)` as it should.

better error message from checkPLam

Merge pull request #58 from Rotsor/patch-1

Emacs mode: ignore backslash character

Emacs mode: ignore backslash character

Emacs treats the '\' as an escape character by default, which means it sees `\(foo : x) -> bar` as having unbalanced parentheses and therefore `forward-sexp` and related functions don't work.

minor changes to bool

experiment with Id

Merge pull request #56 from linuborj/cubicaltt_grothendieck

Added a formalisation of the Grothendieck group and a proof that a family of universal arrows gives rise to an adjunction.

Uncommented slow function.

Added definitions of algebraic structures in algstruct.ctt, a construction of the Grothendieck group in grothendieck.cct, definitions of natural transformations, universal arrows, and adjunctions in univprop as well as a proof that a family of universal arrows gives rise to an adjunction.

swap direction of equality to match order in comment

add opposite category

add a comment to category

readme

update demo

readme

readme

README

update readme

doc

doc

test

test

add a readme for the examples folder

add summary file

doc

move graph script

comment

add a script for loading all files

comments

move implicit point

a lot of comments

remove undefined and make csystem compile

comments

update category

comments

add transparent_all to keywords in emacs file

remove examples/aim.ctt as it is subsumed by examples/demo.ctt

add a small puzzle due to Andrew Polonsky

Merge pull request #49 from mortberg/defeqJ

Add Id types

Fix insertSystem to maintain invariant for systems

Closes #52.

cleaning

cleaning

visible -> transparent

direct definition of retract

add Dan's proof of univalence from ua and uabeta

Merge pull request #50 from david-christiansen/elisp-conventions

Emacs mode updates

Emacs mode: Update names for Customize

Now Customize uses the updated names consistently.

Update README for Emacs mode

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.

Remove CL-isms from Emacs mode

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

Rename Emacs mode identifiers

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

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.

define equivalence using Id and prove univalence with Id everywhere

minor changes

cleaning and a version of univalence for Id

rename Eq to Id

Some experiments with Eq

Added Eq types with definitional equality for J

Merge pull request #46 from david-christiansen/elisp-conventions

Emacs mode: completion, imenu, and friendlier Customize

Merge pull request #45 from david-christiansen/emacs-update

Add subprocess to Emacs mode