mortberg / cubicaltt Goto Github PK
View Code? Open in Web Editor NEWExperimental implementation of Cubical Type Theory
Home Page: https://arxiv.org/abs/1611.02108
License: MIT License
Experimental implementation of Cubical Type Theory
Home Page: https://arxiv.org/abs/1611.02108
License: MIT License
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".
The keywords opaque
, transparent
, and transparent_all
aren't documented anywhere.
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?
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.
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 ]
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.
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 ?
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
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.
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?
It would be nicer to see
\A -> \B -> ...
instead of
\X0 -> \X1 -> ...
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?
Hello,
I am totally new to this area. I would be interested in the following.
Totally not trying to belittle, just really like to try to understand.
Thank you!
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?
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?
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
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
> 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
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?
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
You throw away the REPL history every time a file is reloaded, and perhaps you also leak memory:
Just ":r" -> lift $ initLoop flags f
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.
An idea for an example: prove that the n-th homotopy group of the n-sphere is the integers?
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
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
.
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
$
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.
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.
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.
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
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.
This example is the simplest reproduction I have found so far.
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) []
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?
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?
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
?
We should be able to infer the type of a lambda.
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.
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
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)
]
]
If undefined is neutral how should "undefined @@ i" be handled? Maybe decorate undefined by its type?
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
.
The PR #44 breaks support for nested mutual blocks.
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.
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?
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.
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 ]
...
:l foo<tab>
doesn't complete to foo.ctt
as the completion function doesn't have that implemented
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.
Rename the following constants
IdP -> PathP
Id -> Path
glue -> Glue
glueElem -> glue
unglueElem -> unglue
in order to better match what is in the paper.
A declarative, efficient, and flexible JavaScript library for building user interfaces.
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google ❤️ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.