comments

simplify more

improve uaret

update lectures

unfolded version of propIsEquivDirect

direct proof that being an equiv is a prop

delete 'primitive' keyword from emacs mode

rudimentary vim syntax file

plug functor to recursion schemes

Create lambek.ctt

Add recursion schemes as examples of cubicaltt usage

Create control.ctt

update lectures

direct proofs that things are sets

test travis for PRs

test travis

.gitignore .stack-work, vim swap files

Build with stack LTS 9.5 resolver

use foldrWithKey instead of foldWithKey to eliminate warnings

cleaning

A small simplification on binnat.ctt

update lectures

Add stack build instructions to the README.md file.

Remove cruft from stack.yaml

Add support for Travis CI

Use cubicaltt syntax table in the process buffer.

This way forward-sexp and backward-sexp work there too, despite
the use of backslash for lambda.

separate syntax highlighting for keywords and builtins

Merge pull request #77 from mikeshulman/nograd

Remove one more instance of "graduate lemma"

Remove one more instance of "graduate lemma"

rename gradLemma to isoToEquiv

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