mortberg cubicaltt issues

mortberg / cubicaltt

Experimental implementation of Cubical Type Theory

https://arxiv.org/abs/1611.02108

MIT License

571 stars 76 forks source link

issues

Newest

Newest Most commented Recently updated Oldest Least commented Least recently updated

Solution at "hard" exercise at lecture2.ctt

#73 xekoukou closed 7 years ago
2
Please don't call it the "grad lemma".

#72 mikeshulman closed 7 years ago
6
Added a primitive composition for Id types which reduces with refl on…

#71 IanOrton opened 7 years ago
1
Constant cubes in 2D, 3D and 4D

#70 Sobernard closed 7 years ago
1
"forwardHIT: neutral b" error in hit branch, but not master

#69 PaulGustafson opened 7 years ago
1
Add more keywords for syntax highlighting

#68 vikraman closed 7 years ago
2
Useless(?) hComp’s with empty systems when using higher inductive types

#67 guillaumebrunerie opened 7 years ago
10
Check if some names were shadowed while loading a file

#66 mortberg closed 7 years ago
6
Proper error handling when importing files

#65 mortberg closed 7 years ago
5
Spurious error with incorrect import

#64 jonsterling closed 7 years ago
2
Nested splits and path constructors

#63 IanOrton opened 7 years ago
2
No support for recursive HITs, but forward instead of squeeze and transp

#62 mortberg closed 7 years ago
3
Syntax highlighting for all keywords

#61 mortberg closed 7 years ago
1
More parentheses when printing values

#60 Rotsor closed 7 years ago
3
better error message from checkPLam

#59 Rotsor closed 7 years ago
1
Emacs mode: ignore backslash character

#58 Rotsor closed 7 years ago
1
Learning Guide

#57 ronaldpetty closed 7 years ago
2
Added a formalisation of the Grothendieck group and a proof that a family of universal arrows gives rise to an adjunction.

#56 linuborj closed 7 years ago
2
Added a formalisation of the Grothendieck group and a proof that a family of universal arrows gives rise to and adjunction.

#55 linuborj closed 7 years ago
3
Algebraic structures, the Grothendieck group, and universal properties

#54 linuborj closed 7 years ago
1
Definitional equality of lambda is wrong?

#53 molikto closed 8 years ago
2
Conversion bug with glue systems?

#52 tomjack closed 8 years ago
1
Wired program type checked.

#51 molikto opened 8 years ago
1
Emacs mode updates

#50 david-christiansen closed 8 years ago
1
Add Id types

#49 mortberg closed 8 years ago
0
Add support for nested mutual blocks again

#48 mortberg opened 8 years ago
6
Issue with HIT path constructors.

#47 RafaelBocquet opened 8 years ago
3
Emacs mode: completion, imenu, and friendlier Customize

#46 david-christiansen closed 8 years ago
0
Add subprocess to Emacs mode

#45 david-christiansen closed 8 years ago
12
Speed up comparison of environments

#44 gullcomb closed 8 years ago
2
Print a warning when a name is shadowed

#43 mortberg closed 7 years ago
3
Add Identity types

#42 mortberg closed 8 years ago
4
Renaming

#41 mortberg closed 8 years ago
1
Implement girard's paradox to show impredicativity of cubicaltt

#40 abooij closed 7 years ago
2
implement propositional truncation

#39 abooij closed 8 years ago
7
Type-checking performance issues

#38 gullcomb closed 8 years ago
3
List reserved names

#37 abooij closed 8 years ago
1
added imports and changed examples/collection.ctt (corrUniv B A)

#36 georgydunaev closed 8 years ago
1
Canonicity failure for Z from recursive path constructors

#35 tomjack opened 8 years ago
6
The total space of the Hopf fibration, as well as the join of two 1-spheres, is the 3-sphere?

#34 markfarrell closed 8 years ago
0
Finish the proof that \pi_4(S^3)=Z/2Z?

#33 markfarrell closed 8 years ago
0
Eilenberg-MacLane Spaces?

#32 markfarrell closed 8 years ago
0
The n-th homotopy group of the n-sphere is the integers?

#31 markfarrell closed 8 years ago
0
Path from the loop space of the torus to the product of two circles?

#30 markfarrell closed 8 years ago
0
Soften version constraints

#29 abooij closed 8 years ago
1
Composing with refl gives different path

#28 abooij closed 8 years ago
2
Incorrect pattern matching in the type checker makes bottom provable

#27 abooij closed 8 years ago
2
univalence normalization

#26 stelleg closed 8 years ago
21
Maintain semantics of type signatures

#25 abooij closed 8 years ago
2
Add a few proofs to what currently goes for the "standard library"

#24 abooij closed 7 years ago
6

Previous Next