mortberg / cubicaltt Goto Github PK

View Code? Open in Web Editor NEW

566.0 45.0 76.0 2.49 MB

Experimental implementation of Cubical Type Theory

Home Page: https://arxiv.org/abs/1611.02108

License: MIT License

Emacs Lisp 6.18% Makefile 2.43% Haskell 90.72% Vim Script 0.67%

cubical-type-theory type-theory homotopy-type-theory univalent-foundations

cubicaltt's Introduction

Cubical Type Theory

Experimental implementation of Cubical Type Theory in which the user can directly manipulate n-dimensional cubes. The language extends type theory with:

Path abstraction and application
Composition and transport
Equivalences can be transformed into equalities (and univalence can be proved, see "examples/univalence.ctt")
Identity types (see "examples/idtypes.ctt")
Some higher inductive types (see "examples/circle.ctt" and "examples/integer.ctt")

Because of this it is not necessary to have a special file of primitives (like in cubical), for instance function extensionality is directly provable in the system:

funExt (A : U) (B : A -> U) (f g : (x : A) -> B x)
       (p : (x : A) -> Id (B x) (f x) (g x)) :
       Id ((y : A) -> B y) f g = <i> \(a : A) -> (p a) @ i

For examples, including a demo ("examples/demo.ctt"), see the examples folder. For a summary of where to find the main results of the cubical type theory paper in the examples folder see "examples/summary.ctt".

The following keywords are reserved:

module, where, let, in, split, with, mutual, import, data, hdata,
undefined, PathP, comp, transport, fill, Glue, glue, unglue, U,
opaque, transparent, transparent_all, Id, idC, idJ

Install

You can compile the project using either cabal, make, or stack.

Cabal

To compile the project using cabal, first install the build-time dependencies (either globally or in a cabal sandbox):

cabal install alex happy bnfc

Then the project can be built (and installed):

cabal install

Make

Alternatively, a Makefile is provided:

    make

This assumes that the following Haskell packages are installed using cabal:

  mtl, haskeline, directory, BNFC, alex, happy, QuickCheck

To build the TAGS file, run:

    make TAGS

This assumes that hasktags has been installed.

To clean up, run:

    make clean

Stack

To compile and install the project using stack, run:

    stack setup
    stack install

Usage

To run the system type

cubical <filename>

To see a list of options add the --help flag. In the interaction loop type :h to get a list of available commands. Note that the current directory will be taken as the search path for the imports.

When using cabal sandboxes, cubical can be invoked using

cabal exec cubical <filename>

To enable emacs to edit *.ctt files in cubicaltt-mode, add the following line to your .emacs file:

(autoload 'cubicaltt-mode "cubicaltt" "cubical editing mode" t)
(setq auto-mode-alist (append auto-mode-alist '(("\\.ctt$" . cubicaltt-mode))))

and ensure that the file cubicaltt.el is visible in one of the diretories on emacs' load-path, or else load it in advance, either manually with M-x load-file, or with something like the following line in .emacs:

(load-file "cubicaltt.el")

When using cubicaltt-mode in Emacs, the command cubicaltt-load will launch the interactive toplevel in an Emacs buffer and load the current file. It is bound to C-c C-l by default. If cubical is not on Emacs's exec-path, then set the variable cubicaltt-command to the command that runs it.

References and notes

Cubical Type Theory: a constructive interpretation of the univalence axiom, Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mörtberg. This paper describes the type theory and its model.
Canonicity for Cubical Type Theory, Simon Huber. Proof of canonicity for the type theory.
Voevodsky's lectures and texts on univalent foundations
HoTT book and webpage: http://homotopytypetheory.org/
Cubical Type Theory - Old version of the typing rules of the system. See this for a variation using isomorphisms instead of equivalences.
Internal version of the uniform Kan filling condition
A category of cubical sets - main definitions towards a formalization
hoq - A language based on homotopy type theory with an interval (documentation available here).
A Cubical Approach to Synthetic Homotopy Theory, Dan Licata, Guillaume Brunerie.
Type Theory in Color, Jean-Philippe Bernardy, Guilhem Moulin.
A simple type-theoretic language: Mini-TT, Thierry Coquand, Yoshiki Kinoshita, Bengt Nordström and Makoto Takeyama - This presents the type theory that the system is based on.
A cubical set model of type theory, Marc Bezem, Thierry Coquand and Simon Huber.
An equivalent presentation of the Bezem-Coquand-Huber category of cubical sets, Andrew Pitts - This gives a presentation of the cubical set model in nominal sets.
Remark on singleton types, Thierry Coquand.
Note on Kripke model, Marc Bezem and Thierry Coquand.

Authors

Cyril Cohen, Thierry Coquand, Simon Huber, Anders Mörtberg

cubicaltt's People

Contributors

Stargazers

Watchers

Forkers

nad dlicata335 jyp hansbugge np saizan herberteuler simhu dangrayson abooij markfarrell radams78 timrichter gfortaine gullcomb carberg inmathwetrust palladin dreamlinuxer david-christiansen emacsmirror molikto akuklev linuborj weixima rotsor vikraman sobernard ianorton mrkgnao mikeshulman xekoukou paulgustafson formulas-and-numbers anthonybordg jozefg 5ht nponeccop binderdavid silky adept hardentoo soraismus graydon eamon-otuathail thomasdziedzic fpvandoorn marcbezem nau bia10 lemastero 3abc ecavallo cloudysin ekim1919 gancherj andraskovacs lambdaxymox lambda-magic thecapitalistcycle bollu hk-nguyen-math stjordanis tomjack drruisseau dcclogin tjjfvi alissa-tung tridu33 iho

cubicaltt's Issues

Document opaque / transparent

The keywords opaque, transparent, and transparent_all aren't documented anywhere.

Renaming

Rename the following constants

IdP -> PathP
Id -> Path
glue -> Glue
glueElem -> glue
unglueElem -> unglue

in order to better match what is in the paper.

Path completion in :l

:l foo<tab> doesn't complete to foo.ctt as the completion function doesn't have that implemented

Keep names of generated variables and dimensions

It would be nicer to see

\A -> \B -> ...

instead of

\X0 -> \X1 -> ...

Allow opaque/transparent in the command line

It would be nice to be allowed to write
> opaque f
or
> transparent f
at the command line, rather than having to write it in the file and reload all of it.

Finish the proof that \pi_4(S^3)=Z/2Z?

What would be involved in finishing the proof that \pi_4(S^3)=Z/2Z, started in experiments/pi4s3.ctt? Apparently, Brunerie has made progress on a constructive proof of this fact? I wonder if it would be possible to fully formalize it in the current cubical type theory? Thoughts?

Evaluation seems to be too strict

The code below is rejected:

module test where

import prelude
import nat

foo : nat = undefined

fooIsFoo : Id nat foo foo = refl nat foo

Error message:

eval: undefined at test_L6_C13

Why are you evaluating foo?

Incorrect pattern matching in the type checker makes bottom provable

import prelude

data bool = false | true
caseBool (A : U) (f t : A) : bool -> A = split
 false -> f
 true  -> t
falseNeqTrue : neg (Id bool false true) =
  \(h : Id bool false true) -> subst bool (caseBool U bool N0) false true h false

data bool'
  = false'
  | true'
  | p' (bot : N0) <i> [(i=0) -> false' , (i=1) -> true']

g : bool' -> bool = split
  false' -> false
  true'  -> true
  p' bot @ i-> efq (Id bool false true) bot @ i

-- the following line shouldn't type-check, but it does
uhh : Id bool' false' true' = <i> p'{bool'} @ i
blah : Id bool false true = <i> g (uhh @ i)

bot : N0 = falseNeqTrue blah

Nested splits and path constructors

There seems to be an issue with using nested splits with HITs. See the example below:

module broken where

data S1 = base
        | loop <i> [(i=0) -> base, (i=1) -> base]

data Unit = tt

c2t' : S1 -> S1 -> Unit = split
  base -> split@(S1 -> Unit) with
    base -> tt
    loop @ _ -> tt
  loop @ _ -> split@(S1 -> Unit) with
    base -> tt
    loop @ _ -> tt

This produces the following error:

Type checking failed: Faces in branch for "loop" don't match:
got
[ (_ = 0) -> broken_L13_C5 0, (_ = 1) -> broken_L13_C5 1 ]
but expected
[ (_ = 0) -> broken_L10_C5, (_ = 1) -> broken_L10_C5 ]

I think that broken_L13_C5 0 should reduce to tt, and so should broken_L10_C5 and so these systems should in fact be equal.

Wired program type checked.

test1 (t: nat): U = nat

test2 (a: nat): U = 
    (test1 a)
   where
    a: (test2 zero) = zero

An equivalent program doesn't type check in Coq

Learning Guide

Hello,

I am totally new to this area. I would be interested in the following.

High level explanation on the purpose / utility (again for non-experts)
Step by step topic guide to have 'hope' of understanding (maybe just list of expected base knowledge concepts. ex. Compiler theory -> math -> etc. etc.)

Totally not trying to belittle, just really like to try to understand.

Thank you!

Please don't call it the "grad lemma".

Generally there are two ways that theorems and lemmas are named in mathematics: descriptively (giving some information about what the theorem says, e.g. "the intermediate value theorem") and attributively (giving credit to whoever proved it, e.g. "Cauchy's theorem"). Whatever your feelings about the relative merits of the two, the name "grad lemma" achieves neither: it conveys no information about what the lemma says, nor does it give any credit to the people it refers to, instead depersonalizing them as "some nameless graduate students". Moreover it is even factually incorrect, since some of the people in question were actually postdocs at the time.

The HoTT/Coq library calls the analogous theorem adjointify, since it makes a non-adjoint equivalence into a (half-)adjoint one. That may not be so appropriate if your notion of "coherent equivalence" is not the half-adjoint one, but maybe coherentify would work. The HoTT/Agda library calls it is-eq, with a comment that this "is a very, very bad name." But even is-eq is better than "grad lemma".

Issue with HIT path constructors.

This is probably roughly the same bug as #35, but as it does not involve recursive HITs, I am creating a separate issue.

It is possible to create a path p:Path T a b such that p@1 does not reduce to b:

module bug where
import prelude
A:U=undefined
B:U=undefined
f:A->B=undefined
opaque A -- to print #A instead of undefined
opaque B
opaque f

data HIT
  = iA (_:A)
  | iB (_:B)
  | gl (x:A) <i>
    [ (i=0) -> iA x
    , (i=1) -> iB (f x)
    ]

x : A = undefined
opaque x

p1 : HIT = transport (<_> HIT) (gl {HIT} x @ 1)
p : Path HIT
         (transport (<_> HIT) (gl {HIT} x @ 0))
         p1
  = <r> transport (<_> HIT) (gl {HIT} x @ r)

p1 reduces to hComp HIT (iB (comp (<_> B) (f x) [])) [], but p@1 reduces to hComp HIT (iB (f (comp (<_> A) x []))) [].

However, this works:

p : Path HIT
         (transport (<_> HIT) (gl {HIT} x @ 0))
         p1
  = <r> comp (<_> HIT) (gl {HIT} x @ r)
        [(r=0)-><i> fill (<_> HIT) (iA x) [] @ i
        ,(r=1)-><i> fill (<_> HIT) (iB (f x)) [] @ i
        ]

Maybe the definition of composition for a path constructor should depend on its system ?

Origin of type errors

The error message for type checking errors, while correct, is rather unhelpful in bigger proofs. It would be nice if it could at least state a line number where things go haywire.

It looks like this data is not exposed by bnfc, so we'd have to prepend position to every token. Or is there a less invasive solution?

History erased after every reload

You throw away the REPL history every time a file is reloaded, and perhaps you also leak memory:

Just ":r"  -> lift $ initLoop flags f

Composing with refl gives different path

In the context of the interval, I found the following.

fromUnitK' : (a : I) -> Id I (fromUnit (toUnit a)) a = split
  zero -> <i> zero
  one -> <i> seg {I} @ i
  -- the usual case here is:
  -- seg @ i -> <j> (seg {I} @ i /\ j)
  -- but try p (which works) vs. p' (which doesn't):
  seg @ i -> p'
    where
    p : Id I zero (seg {I} @ i) = <j> (seg {I} @ i /\ j)
    p' : Id I zero (seg{I} @ i) =
      compId I zero (seg{I} @ i) (seg{I} @ i)
        p
        (refl I (seg{I} @ i))

Type checking failed: Faces in branch for "seg" don't match:
got
[ (i = 0) -> <!0> hComp I zero [ (!0 = 0) -> <!1> zero, (!0 = 1) -> <!1> zero ], (i = 1) -> <!0> hComp I (seg {I} @ !0) [ (!0 = 0) -> <!1> zero, (!0 = 1) -> <!1> one ] ]
but expected
[ (i = 0) -> <!0> zero, (i = 1) -> <!0> seg {I} @ !0 ]

Synonym for Π not accepted when checking split

The following code is not accepted:

module streamsAsFunctions where

import nat

Stream (A : U) : U = nat -> A

cons (A : U) (x : A) (xs : Stream A) : Stream A =
  split
    zero  -> x
    suc n -> xs n

Error message:

Resolver failed: Pi type expected in cons at (7,1)

The code is accepted if the codomain Stream A is expanded into nat -> A.

A pattern matching for predicate function

Hello @mortberg I have some problem with pattern matching. This is my pretty easy code

filter(A: U) (p: A -> bool): list A -> list A = split
  nil -> nil
  cons x xs -> split@(p x -> bool) with
    true -> cons x (filter A xs)
    false -> filter A xs

Could you please correct it? Or provide more better solution.

Also I think this will be will be helpful, but I got error

if_then_else (A: U): bool -> A -> A -> A = split
  true -> \(x: A) (y: A) -> x
  false -> \(x: A) (y: A) -> y

Checking: if_then_else
Type checking failed: case branches does not match the data type

Thanks

Type-checking performance issues

I am a newcomer to cubicaltt. As part of my experiments, I wrote the following function mapping equivalences to their inverse

import equiv
invEquiv (A B : U) (f : equiv A B) : equiv B A
    = (invEq A B f, gradLemma B A (invEq A B f) f.1 (secEq A B f) (retEq A B f))

together with a proof that this operation is an involution.

invEquiv_invol (A B : U) (f : equiv A B)
    : Id (equiv A B) (invEquiv B A (invEquiv A B f)) f
    = <i> (f.1, propIsEquiv A B f.1 (invEquiv B A (invEquiv A B f)).2 f.2 @ i)

The latter takes a long time (25s on my laptop) to type-check. This is very surprising because type-checking this

invEquiv_invol2 (A B : U) (f : equiv A B)
    : Id (isEquiv A B f.1) (invEquiv B A (invEquiv A B f)).2 f.2
    = propIsEquiv A B f.1  (invEquiv B A (invEquiv A B f)).2 f.2

is very fast, so I would expect the type-checker to be able to extract the endpoints when i = 0 or i = 1.

However (from what I understand of the code), since propIsEquiv is a defined identifier, it expands the invEquiv_invol2 subterm of invEquiv_invol into a path abstraction. Then, it uses substitution of path variables (act) to propagate the value of i, which involves a lot of redundant calls to support (if i is in the support of a value, then act recurses into its subterms and calls support again).

I have a patch that makes path abstraction evaluate to closures (as lambda-abstractions currently do), which fixes this issue. However, it slows down most of the examples (multS1.ctt is the noticeable exception). This is probably because the equality on closure values also compares the environments, including all the previous definitions (which themselves have an environment; although most of it is shared, the derived Eq instances don't know and compare everything).

I have not tried to modify the evaluation strategy so that head variables are not unfolded when applying a path to 0 or 1 (so that Eval.inferType can be used to extract the endpoints) but this seems also doable.
Fixing correctly the issues about pointless comparison of environments seems much more involved, though.

Makefile incorrect?

Hi,

I was trying to build cubicaltt, but ran into a bit of trouble. I installed the require packages with cabal, but then ran into problems with make bnfc && make. Here's what I had to do instead:

bnfc -d --haskell --ghc --alex3 Exp.cf
happy -gca Exp/Par.y
alex -g Exp/Lex.x
ghc --make -O2 Exp/Test.hs -o Exp/Test
ghc --make -O2 -o cubical -rtsopts Main.hs

Should the Makefile be fixed?

Infer type of lambdas

We should be able to infer the type of a lambda.

Definitional equality of lambda is wrong?

Program

pred : nat -> nat = split
  zero -> zero
  suc n -> n


pred_alt : nat -> nat = split
  zero -> zero
  suc n -> n

lamtest_pred_alt: Path (nat -> nat) pred pred_alt = <i> pred_alt

will fail with

Type checking failed: path endpoints don't match for pred_alt, got (pred_alt,pred_alt), but expected (pred,pred_alt)

but in Coq:

Fixpoint add_alt (a b: nat) : nat := match a with 
| O => b
| S p => S (add_alt p b)
end.

Definition add_alt_test: (plus = add_alt) := eq_refl.

Type checks.

Conversion bug with glue systems?

In this example, normalizing a term (transposeInvGlue) results in a term (transposeInvGlueNorm) which doesn't typecheck, due to an apparently spurious incompatible system error.

I noted that the (keys ts == keys ts') check in conv for System is the direct cause, but haven't understood the problem any further.

module convgluebug where

Path (A : U) (x y : A) : U = PathP (<i> A) x y
fiber (A B : U) (f : A -> B) (y : B) : U = (x : A) * Path B y (f x)
isContr (A : U) : U = (x : A) * ((y : A) -> Path A x y)
isEquiv (A B : U) (f : A -> B) : U = (y : B) -> isContr (fiber A B f y)
equiv (A B : U) : U = (f : A -> B) * isEquiv A B f

-- probably there is a simpler way to show the issue, but this is how I found it...
transposeInv (A : U) (x : A) (p : Path (Path A x x) (<_> x) (<_> x))
  : Path (Path (Path A x x) (<_> x) (<_> x)) 
         (<j k> p @ k @ j)
         (<j k> p @ -j @ k)
  = <i j k> comp (<_> A) (p @ ((-j /\ k) \/ (i /\ -j) \/ (-i /\ k))
                            @ ((j /\ k) \/ (-i /\ j) \/ (i /\ k)))
              [ (i=0) -> <_> p @ k @ j
              , (i=1) -> <_> p @ -j @ k
              , (j=0) -> <l> p @ (i \/ k \/ l) @ (i /\ k)
              , (j=1) -> <l> p @ (-i /\ k /\ -l) @ (-i \/ k)
              , (k=0) -> <l> p @ (i /\ -j /\ -l) @ (-i /\ j)
              , (k=1) -> <l> p @ (-i \/ -j \/ l) @ (i \/ j)
              ]

transposeInvGlue (A : U) (e : equiv A A)
  : Path (Path (Path U A A) (<_> A) (<_> A))
         (<i j> Glue A [ (i=0) -> (A, e)
                       , (i=1) -> (A, e)
                       , (j=0) -> (A, e)
                       , (j=1) -> (A, e)
                       ])
         (<i j> Glue A [ (i=0) -> (A, e)
                       , (i=1) -> (A, e)
                       , (j=0) -> (A, e)
                       , (j=1) -> (A, e)
                       ])
  = transposeInv U A
      (<i j> Glue A [ (i=0) -> (A, e)
                    , (i=1) -> (A, e)
                    , (j=0) -> (A, e)
                    , (j=1) -> (A, e)
                    ])

-- transposeInvGlueNorm below is the normal form of transposeInvGlue,
-- prettified, but it gives an incompatible system error:

-- a0 = Glue A [ (j = 0) -> (A,e), (j = 1) -> (A,e), (k = 0) -> (A,e), (k = 1) -> (A,e) ]
-- t0alpha = Glue A [ (j = 0) -> (A,e), (j = 1) -> (A,e), (j = 1)(k = 1) -> (A,e), (k = 0) -> (A,e), (k = 1) -> (A,e) ]

-- those terms _do_ convert if we write them directly, though:

a0 (A : U) (e : equiv A A) 
  : Path (Path (Path U A A) (<_> A) (<_> A))
         (<j k> Glue A [ (j = 0) -> (A,e), (j = 1) -> (A,e), (k = 0) -> (A,e), (k = 1) -> (A,e) ])
         (<j k> Glue A [ (j = 0) -> (A,e), (j = 1) -> (A,e), (k = 0) -> (A,e), (k = 1) -> (A,e) ])
  = <i j k> Glue A [ (j = 0) -> (A,e), (j = 1) -> (A,e), (k = 0) -> (A,e), (k = 1) -> (A,e) ]

t0alpha (A : U) (e : equiv A A)
  : Path (Path (Path U A A) (<_> A) (<_> A))
         (<j k> Glue A [ (j = 0) -> (A,e), (j = 1) -> (A,e), (k = 0) -> (A,e), (k = 1) -> (A,e) ])
         (<j k> Glue A [ (j = 0) -> (A,e), (j = 1) -> (A,e), (k = 0) -> (A,e), (k = 1) -> (A,e) ])
  = <i j k> Glue A [ (j = 0) -> (A,e), (j = 1) -> (A,e), (j = 1)(k = 1) -> (A,e), (k = 0) -> (A,e), (k = 1) -> (A,e) ]

hmm (A : U) (e : equiv A A)
  : Path (Path (Path (Path U A A) (<_> A) (<_> A))
               (<j k> Glue A [ (j = 0) -> (A,e), (j = 1) -> (A,e), (k = 0) -> (A,e), (k = 1) -> (A,e) ])
               (<j k> Glue A [ (j = 0) -> (A,e), (j = 1) -> (A,e), (k = 0) -> (A,e), (k = 1) -> (A,e) ]))
         (a0 A e) (t0alpha A e)
  = <_> a0 A e

transposeInvGlueNorm (A : U) (e : equiv A A)
  : Path (Path (Path U A A) (<_> A) (<_> A))
         (<i j> Glue A [ (i=0) -> (A, e)
                       , (i=1) -> (A, e)
                       , (j=0) -> (A, e)
                       , (j=1) -> (A, e)
                       ])
         (<i j> Glue A [ (i=0) -> (A, e)
                       , (i=1) -> (A, e)
                       , (j=0) -> (A, e)
                       , (j=1) -> (A, e)
                       ])
  = <i j k> comp (<_> U) (Glue A [ (i = 0)(j = 0) -> (A,e)
                                 , (i = 0)(j = 1) -> (A,e)
                                 , (i = 0)(k = 0) -> (A,e)
                                 , (i = 0)(k = 1) -> (A,e)
                                 , (i = 1)(j = 0) -> (A,e)
                                 , (i = 1)(j = 1) -> (A,e)
                                 , (i = 1)(k = 0) -> (A,e)
                                 , (i = 1)(k = 1) -> (A,e)
                                 , (j = 0)(k = 0) -> (A,e)
                                 , (j = 0)(k = 1) -> (A,e)
                                 , (j = 1)(k = 0) -> (A,e)
                                 , (j = 1)(k = 1) -> (A,e)
                                 ])
              [ (i = 0) -> <l> Glue A [ (j = 0) -> (A,e)
                                      , (j = 1) -> (A,e)
                                      , (k = 0) -> (A,e)
                                      , (k = 1) -> (A,e)
                                      ]
              , (i = 1) -> <l> Glue A [ (j = 0) -> (A,e)
                                      , (j = 1) -> (A,e)
                                      , (k = 0) -> (A,e)
                                      , (k = 1) -> (A,e)
                                      ]
              , (j = 0) -> <l> Glue A [ (i = 0) -> (A,e)
                                      , (i = 1) -> (A,e)
                                      , (k = 0) -> (A,e)
                                      , (k = 1) -> (A,e)
                                      , (l = 1) -> (A,e)
                                      ]
              , (j = 1) -> <l> Glue A [ (i = 0) -> (A,e)
                                      , (i = 1) -> (A,e)
                                      , (k = 0) -> (A,e)
                                      , (k = 1) -> (A,e)
                                      , (l = 1) -> (A,e)
                                      ]
              , (k = 0) -> <l> Glue A [ (i = 0) -> (A,e)
                                      , (i = 1) -> (A,e)
                                      , (j = 0) -> (A,e)
                                      , (j = 1) -> (A,e)
                                      , (l = 1) -> (A,e)
                                      ]
              , (k = 1) -> <l> Glue A [ (i = 0) -> (A,e)
                                      , (i = 1) -> (A,e)
                                      , (j = 0) -> (A,e)
                                      , (j = 1) -> (A,e)
                                      , (l = 1) -> (A,e)
                                      ]
              ]

Maintain semantics of type signatures

In many proofs, instead of writing:

propIsProp (A : U) : prop (prop A) = ...

one expands definitions, and instead writes

propIsProp (A : U) (f g : prop A) : Id (prop A) f g = ...

to be able to bind variable names. This cannot be done using lambdas because their scope doesn't reach where clauses (which is often necessary).

However, clearly the former expression is the one we'd like to see in clean, readable code.

Not sure what the best way to solving this is, though. I suppose in agda this is not a problem because the type signature is separate from the implementation, and thus variables can be bound even if their type isn't explicitly written out. So in that sense this could be related to #12?

cubicaltt crashes when replacing an 'undefined' with a 'hole'.

Replacing an undefined with a hole here results in a cubicaltt crash with error :

Hole at (52,46) in lecture4:

A : U
--------------------------------------------------------------------------------
(x : Sigma A (\(x : A) -> (y : A) -> PathP (<!0> A) x y)) -> (y : Sigma A (\(x0 : A) -> (y : A) -> PathP (<!0> A) x0 y)) -> PathP (<!0> Sigma A (\(x0 : A) -> (y0 : A) -> PathP (<!0> A) x0 y0)) x y

Checking: isPropIsEquiv
cubical: inferType: not neutral ? (A = (Sigma A ((\(x : A) -> Path B y (f x)) (A = A, B = B, f = f, y = y))))
CallStack (from HasCallStack):
  error, called at ./Eval.hs:289:8 in main:Eval

Process cubical exited abnormally with code 1

inferType for undefined

If undefined is neutral how should "undefined @@ i" be handled? Maybe decorate undefined by its type?

univalence normalization

Hey Guys,

I've enjoyed playing around with building proofs using funExt, all of which have normalized successfully. When I went to play around with univalence, however, I noticed that none of the proofs of univalence normalize. I let each of the three proofs from examples/univalence.ctt run to about 12GB of memory usage, and none of them terminated.

I haven't carefully read all of the cubicaltt papers, nor carefully reasoned about the proofs of univalence, so I'm wondering if this is a known property of the type theory? It seems worrying from a standard Curry-Howard perspective.

Cheers,
George

Add Identity types

Add identity types as in the paper and prove univalence expressed using Id instead of Path.

@simhu : Didn't you do this at some point?

List reserved names

As a (relative) newcomer to cubicaltt, at times I found the example code somewhat difficult to grasp because it seemed to be using all kinds of previously undefined terms such as "transport" and "glue". I believe it would help accessibility of cubicaltt if the reserved names of the syntax are listed somewhere (e.g. in the readme), so that users do not need to refer to Exp.cf, and will not run into weird bugs when they define a "glue" constructor for their favorite HIT.

Parser too liberal?

Should the following code parse (without comp A)?

  trans (A : U) (a b c : A) (p : Id A a b) (q : Id A b c) : Id A a c =
    <i> (p @ i) [ (i = 1) -> q ]

This construction wasn't mentioned in Simon's presentation today.

Identity Paths Don't Simplify On Left Hand Side

When composing identity paths to the right of some other path p, the composition simplifies to p;

IdPathTest1 (A : U) (a b : A) (p : Id A a b) : Id (Id A a b) p (<i> comp A (p @ i) [(i=1) -> <_> b]) = <_> p
IdPathTest2 (A : U) (a b : A) (p : Id A a b) : Id (Id A a b) p (<i> comp A (p @ i) [(i=1) -> <_> b]) = <_ i> comp A (p @ i) [(i=1) -> <_> b]
IdPathTest3 (A : U) (a b : A) (p : Id A a b) : Id (Id A a b) p (<i> comp A (p @ i) [(i=1) -> <_> b]) = <_ i> comp A (p @ i) [(i=0) -> <_> a]

IdPathTest4 (A : U) (a b : A) (p : Id A a b) : Id (Id A a b) p (<i> comp A (p @ i) [(i=0) -> <_> a]) = <_> p
IdPathTest5 (A : U) (a b : A) (p : Id A a b) : Id (Id A a b) p (<i> comp A (p @ i) [(i=0) -> <_> a]) = <_ i> comp A (p @ i) [(i=0) -> <_> a]
IdPathTest6 (A : U) (a b : A) (p : Id A a b) : Id (Id A a b) p (<i> comp A (p @ i) [(i=0) -> <_> a]) = <_ i> comp A (p @ i) [(i=1) -> <_> b]

However, this doesn't happen when composing an identity path on the left side of p.

--Tests 7, 8, and 10 fail
--IdPathTest7 (A : U) (a b : A) (p : Id A a b) : Id (Id A a b) p (<i> comp A a [(i=1) -> <k> p @ k]) = <_> p
--IdPathTest8 (A : U) (a b : A) (p : Id A a b) : Id (Id A a b) p (<i> comp A b [(i=0) -> <k> p @ -k]) = <_> p
IdPathTest9 (A : U) (a b : A) (p : Id A a b) : Id (Id A a b) p p = <_ i> comp A (p @ i) [(i=0) -> <_> a]
--IdPathTest10 (A : U) (a b : A) (p : Id A a b) : Id (Id A a b) p p = <_ i> comp A a [(i=1) -> <k> p @ k]

Is this behavior correct? If so, why does this happen?

Bracket matching of \(x : A)

In the cubicaltt emacs mode, the brackets in \(x : A) are correctly highlighted only in the source file, not in the *cubical* buffer (the first parenthesis is not considered as a parenthesis), which is annoying when trying to parse a complicated answer given by cubicaltt.

Path from the loop space of the torus to the product of two circles?

In the torus example, why is the construction of the path from the loop space of the torus to the product of two circles commented out? Does something need to be fixed?

"forwardHIT: neutral b" error in hit branch, but not master

Type checking the "alpha" function below with the hit branch of cubicaltt gives a "forwardHIT: neutral b" error. When using the master branch, it type checks without any errors.

module broken where

data Bool =  true | false

data Join (A : U) (B : U) = joinl (a : A)
                          | joinr (b : B)
                          | join (a:A) (b : B) <i> [(i=0) -> joinl a, (i=1) -> joinr b]

Path (A : U) (a0 a1 : A) : U = PathP (<i> A) a0 a1

S1 : U = Join Bool Bool
S2 : U = Join Bool S1

compPath (A : U) (a b c : A) (p : Path A a b) (q : Path A b c) : Path A a c =
  <i> comp (<j>A) (p @ i) [ (i = 1) -> q, (i=0) -> <j> a ]

merid (A : U) (a : A) : (Path (Join Bool A) (joinl true) (joinl false)) =
  <i> compPath (Join Bool A) (joinl true) (joinr a) (joinl false)
                       (<i> join {Join Bool A} true a @ i)
                       (<i> (join {Join Bool A} false a) @-i) 
  		       @ i

-- A modified version of the main map alpha from 8, which is equal to the
-- other one (to be checked) but pointed by reflexivity
alpha : Join S1 S1 -> S2 = split
  joinl x   -> (joinl true)
  joinr y   -> (joinl true)
  join x y @ i -> (compPath S2 (joinl true) (joinl false) (joinl true) (merid S1 x) (<j>merid S1 y@-j))@i

Spurious error with incorrect import

We've noticed that if you import a nonexistent module (import not-real), you will receive a strange error that some identifier cannot be resolved, but this identifier doesn't have anything to do with the module that we failed to import.

We are guessing that the failed import is somehow messing up another import, which causes the identifier resolution error. (It seems to mess up just that imports that come before.)

I think it would be nice if when you import a nonexistent module, you got an error that said something like module 'not-real' cannot be found.

Does indent matter in cubicaltt?

I was looking at lectures/lecture3.ctt and wasn't too careful about indent.

It turns out the parser can only understand the first one of the following two definition (the only difference is the indent of last line):

propPi (A : U) (B : A -> U) (h : (x : A) -> isProp (B x)) :
       isProp ((x : A) -> B x) = rem
       where
       rem (f0 f1 : (x : A) -> B x) :
           Path ((x : A) -> B x) f0 f1 =
           <i> \(x : A) -> h x (f0 x) (f1 x) @ i

propPi (A : U) (B : A -> U) (h : (x : A) -> isProp (B x)) :
       isProp ((x : A) -> B x) = rem
       where
       rem (f0 f1 : (x : A) -> B x) : 
           Path ((x : A) -> B x) f0 f1 =
       <i> \(x : A) -> h x (f0 x) (f1 x) @ i

Since I didn't see anything about indent mentioned, I'm not sure if it's supposed to be like this or a bug.

Layout errors crash REPL

foo.ctt:

-}

> :l foo.ctt
Exception: Parse failed in "foo.ctt"
cubical: Layout error: Found } at (138,2) without an explicit layout block.
CallStack (from HasCallStack):
  error, called at ./Exp/Layout.hs:102:23 in main:Exp.Layout
$

Bound Check Error

> let a : (n: nat) * list nat = (zero,nil) in a.1
Checking: a
EVAL: zero
> let a : (n: nat) * list nat = (zero,nil) in a.2
Checking: a
EVAL: nil
> let a : (n: nat) * list nat = (zero,nil) in a.3
cubical: cannot add token at Err (Pn 46 1 47)
CallStack (from HasCallStack):
  error, called at ./Exp/Layout.hs:201:20 in main:Exp.Layout

Strictness of ap (f o g) = (ap f) o (ap g)

Hi,

is the above equality definitional in cubicaltt? I expected this to work:

testApComp (A B C : U) (f : A -> B) (g : B -> C) (a b : A) (p : Id A a b) :
           Id (Id C (g (f a)) (g (f b)))
           (mapOnPath B C g (f a) (f b) (mapOnPath A B f a b p))
           (mapOnPath A C (\(x : A) -> (g (f x))) a b p) =
           refl (Id C (g (f a)) (g (f b))) (mapOnPath A C (\(x : A) -> (g (f x))) a b p)

But it does not. It seems to boil down to whether terms like comp (<!1> B) (f (p @ !0)) [ (!0 = 0) -> <!1> f a, (!0 = 1) -> <!1> f (q @ !1) ] could get normalized to
f (comp (<!1> A) (p @ !0) [ (!0 = 0) -> <!1> a, (!0 = 1) -> <!1> q @ !1 ] ...

Print a warning when a name is shadowed

It is easy to define something with the same name as something already defined and get very confused. If the system would print a warning it would be easier to figure out what is going wrong.

Constructors as first-class citizen

module test where
import nat
suc' : nat -> nat = suc

yields:

Type checking failed: expected a data type for the constructor suc but got Pi (nat) ((\(_ : nat) -> nat))

The workaround is to lambda-abstract suc:

suc' : nat -> nat = \(n : nat) -> suc n

File loaded.

I tried to end this message in a pun about "pointless" but I can't seem to hit the spot.

The total space of the Hopf fibration, as well as the join of two 1-spheres, is the 3-sphere?

Another idea: prove in experiments/hopf.ctt that the total space of Hopf fibration is the 3-sphere? Also prove that the join of two 1-spheres is the 3-sphere?

Canonicity failure for Z from recursive path constructors

This example is the simplest reproduction I have found so far.

The n-th homotopy group of the n-sphere is the integers?

An idea for an example: prove that the n-th homotopy group of the n-sphere is the integers?

Add support for nested splits

Nested splits don't seem to be supported at the moment, and in the absence of mutual recursion the workarounds can be quite hairy:

module nestedSplits where

import bool
import nat

equalZero : nat -> bool =
  split
    zero  -> true
    suc n -> false

equalSuc
  (equal : nat -> nat -> bool) (m : nat) : nat -> bool =
  split
    zero  -> false
    suc n -> equal m n

equal : nat -> nat -> bool =
  split
    zero  -> equalZero
    suc n -> equalSuc equal n

lessComplicatedButRejected : nat -> nat -> bool =
  split
    zero -> split
      zero  -> true
      suc n -> false
    suc m -> split
      zero  -> false
      suc n -> lessComplicatedButRejected m n

Syntax highlighting for all keywords

It would be probably be good to have syntax highlighting for all of the keywords. It is now easy to incidentally introduce a constant called for example comp and one then ends up getting a parse error. It would be better if comp was colored nicely in the emacs mode so that one see directly that it is a keyword.

Eilenberg-MacLane Spaces?

Another idea for an example: prove that for an Eilenberg-MacLane space with a specified homotopy group at dimension n, the n-th homotopy group of said space is indeed the specified homotopy group? Additionally, prove that the other homotopy groups of said space are trivial otherwise?

Useless(?) hComp’s with empty systems when using higher inductive types

In the code below, the normal form of the term p is

<!0> hComp SuspS1 (merid {SuspS1} (hComp S1 base []) @ !0) [].

It seems strange that we get hComp S1 base [] instead of just base, and it gives us terms full of seemingly useless hComp’s with empty systems.

module bug where

data S1 = base
        | loop <i> [(i = 0) -> base, (i = 1) -> base]

data SuspS1 = north
            | south
            | merid (a : S1) <i> [(i = 0) -> north, (i = 1) -> south]

p : PathP (<_> SuspS1) (comp (<_> SuspS1) north []) (comp (<_> SuspS1) south [])
 = <i> comp (<_> SuspS1) (merid{SuspS1} base @ i) []

Add support for nested mutual blocks again

The PR #44 breaks support for nested mutual blocks.

Solution at "hard" exercise at lecture2.ctt

Hello ,I can't find a way to show the undefined :

-- Another example of a simple composition: compose p with its inverse
compinv (A : U) (a b : A) (p : Path A a b) : Path A a a =
 <i> comp (<_> A) (p @ i) [ (i = 0) -> <j> a, (i = 1) -> <j> p @ -j ]

exlemma (A : U) (a : A) :
  Path (Path A a a) (<j> a) (compinv A a a (<i> a)) = undefined 

-- Exercise (hard): is "compinv A a b p" Path equal to <j> a?
ex (A : U) (a b : A) (p : Path A a b) :
  Path (Path A a a) (<j> a) (compinv A a b p)
    = trans (Path A a a) (<_> a) (compinv A a a (<_> a)) (compinv A a b p) (exlemma A a)(<k> <i> comp (<_> A) (p @ (i /\ k)) [ (i = 0) -> <j> a, (i = 1) -> <j> p @ (k /\ -j) ])

It is from your second lecture here

In algebraic topology, two constant paths are equal by definition.