Skip to content
Browse files

gcube

  • Loading branch information...
1 parent cb379f0 commit 99b056a6a6e263813ea754c65f27e41b291a4626 @dlicata335 committed
Showing with 1 addition and 1 deletion.
  1. +1 −1 computational-interp/GCube.agda
View
2 computational-interp/GCube.agda
@@ -31,7 +31,7 @@ module computational-interp.GCube where
BoundaryPath (S n) (c1 , c1' , p11') (c2 , c2' , p22') =
Σ (λ (p12 : CubePath n c1 c2)
Σ (λ (p1'2' : CubePath n c1' c2')
- Inside (S n) {!!}))
+ {!"p11' = p22' over p12 , p1'2'"? !}))
CubePath n c1 c2 =
Σ (λ (p : BoundaryPath n (d n c1) (d n c2)) Inside (S n) (c1 , c2 , p))

0 comments on commit 99b056a

Please sign in to comment.
Something went wrong with that request. Please try again.