hoq
hoq copied to clipboard
A language based on homotopy type theory with an interval
Results
2
hoq issues
Sort by
recently updated
recently updated
newest added
``` hlevel.hoq:42:25: Expected type: x = y Actual type: x.proj1 , x.proj2 = y.proj1 , y.proj2 Term: path (\i -> p @ i , path-over (\i' -> B (p @...