cubicaltt
cubicaltt copied to clipboard
mortberg
Experimental implementation of Cubical Type Theory
I used a lemma called `g2TruncFib` similar to `setTruncFib`. Just one remark, for `g2TruncFib` (and similarly `setTruncFib`) to work we don't need that `gP x` is a 2-groupoid for all...
This will simplify the batch job description a lot!
Should I be able to do the circles to torus map with nested splits? module torustest where data S1 = base | loop [ (i=0) -> base , (i=1) ->...
When there is an error message showing a system (e.g. incompatible system, and maybe others), it would be nice if the system is printed with one component per line: ```...
The PR https://github.com/mortberg/cubicaltt/pull/44 breaks support for nested mutual blocks.
At his talk in San Diego yesterday, @guillaumebrunerie showed that making certain functions opaque can help with evaluating nasty terms. The problem is that sometimes the opaque functions have to...
`:l foo` doesn't complete to `foo.ctt` as the completion function doesn't have that implemented
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...
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...