gcube

computational-interp/Cube.agda

@@ -156,3 +156,48 @@ module computational-interp.Cube where
   pair' : {A : Type} {B : A → Type} (n : Nat) → (Σ \ (a : Cube n A) →  CubeOver' B n a) → Cube n (Σ B)
   pair' Z p = p
   pair' (S n) ((a1 , a2 , α) , (b1 , b2 , β)) = pair' n (a1 , b1) , pair' n (a2 , b2) , ap (pair' n) (pair= α β)
+
+
+
+  module Foo (A : Type) where
+
+    Cube' : Nat → Type 
+    Boundary : Nat → Type
+    d : (n : Nat) → Cube' n → Boundary n
+    Inside : (n : Nat) → Boundary (S n) → Type
+
+    Boundary 0 = Unit
+    Boundary (S n) = Σ λ (c1 : Cube' n) → Σ \ (c2 : Cube' n) → d n c1 == d n c2
+
+    Cube' 0 = A
+    Cube' (S n) = Σ \ (b : Boundary (S n)) → Inside n b
+
+    d Z c = <>
+    d (S n) c = fst c
+
+    -- theorem
+    Inside Z (c1 , c2 , b) = c1 == c2
+    Inside (S n) ((.b2 , α1) , (b2 , α2) , id) = α1 == α2
+
+    mutual
+      expand : (n : Nat) → A → Cube' n 
+      expand Z x = x
+      expand (S n) x = (expand n x , expand n x , id) , expand-in n x
+
+      expand-in : (n : Nat) → (x : A) → Inside n (expand n x , expand n x , id)
+      expand-in Z x = id
+      expand-in (S n) x = id
+
+    pt : (n : Nat) → Cube' n → A
+    pt Z c = c
+    pt (S n) c = pt n (fst (fst c))
+
+    pt-expand : (n : Nat) (c : Cube' n) → expand n (pt n c) == c
+    pt-expand Z c = id
+    pt-expand (S Z) ((.c2 , c2 , b) , id) = {!UIP for Unit!}
+    pt-expand (S (S n)) (((.b2 , .i2) , (b2 , i2) , id) , id) = pair= (pair= (pt-expand (S n) (b2 , i2)) {!!}) {!!}  --grungy but should work 
+
+    test' : _
+    test' = {!Cube' 2!}
+
+

computational-interp/GCube.agda

@@ -0,0 +1,56 @@
+{-# OPTIONS --type-in-type --without-K #-}
+
+open import lib.Prelude
+open import lib.PathOver
+
+module computational-interp.GCube where
+
+  module Cube (A : Type) where
+
+    Cube : Nat → Type 
+    Boundary : Nat → Type
+    d : (n : Nat) → Cube n → Boundary n
+    Inside : (n : Nat) → Boundary n → Type
+    CubePath : (n : Nat) → Cube n → Cube n → Type
+    BoundaryPath : (n : Nat) -> Boundary n -> Boundary n -> Type
+
+    Boundary 0 = Unit
+    Boundary (S n) = Σ λ (c1 : Cube n) → Σ \ (c2 : Cube n) → BoundaryPath n (d n c1) (d n c2) -- d n c1 == d n c2
+
+    Cube n = Σ \ (B : Boundary n) → Inside n B
+
+    d n (B , _) = B
+
+    postulate 
+      InsideS : (n : Nat) → (c1 : Cube n) → (c2 : Cube n) → BoundaryPath n (d n c1) (d n c2) → Type
+
+    Inside Z <> = A
+    Inside (S n) (c1 , c2 , p) = InsideS n c1 c2 p
+
+    BoundaryPath Z B1 B2 = Unit
+    BoundaryPath (S n) (c1 , c1' , p11') (c2 , c2' , p22') = 
+      Σ (λ (p12 : CubePath n c1 c2) → 
+      Σ (λ (p1'2' : CubePath n c1' c2') → 
+        Inside (S n) {!!}))
+
+    CubePath n c1 c2 = 
+      Σ (λ (p : BoundaryPath n (d n c1) (d n c2)) → Inside (S n) (c1 , c2 , p))
+
+    test1 : Cube 1 → _
+    test1 (((<> , a) , (<> , b) , <>) , pab) = {!!}
+
+    test2 : Cube 2 → _
+    test2 (((((<> , a) , (<> , b) , <>) , pab) , (((<> , c) , (<> , d) , <>) , pcd) , (<> , pac) , (<> , pbd) , XXX) , sq) 
+      = {!snd₁!} -- XXX should be unit
+
+    test3 : Cube 3 → _
+    test3 (((((((<> , a) , (<> , b) , <>) , pab) , 
+              (((<> , c) , (<> , d) , <>) , pcd) , 
+              (<> , pac) , (<> , pbd) , trivabcd) , sqabcd) , 
+           (((((<> , a') , (<> , b') , <>) , pab') , 
+             (((<> , c') , (<> , d') , <>) , pcd') , 
+              (<> , pac') , (<> , pbd') , triva'b'c'd') , sqa'b'c'd') , 
+           (((<> , paa') , (<> , pbb') , trivaba'b') , sqaba'b') , 
+           (((<> , pcc') , (<> , pdd') , trivcdc'd') , sqcdc'd') , 
+           x) , 
+          cub) = {!x!}

homotopy/Pi2HSusp.agda

@@ -73,7 +73,7 @@ module homotopy.Pi2HSusp (A : Type)
               Path{Trunc (tl 1) (Path {(Susp A)} No So) }
                    [ mer (a ⊙ a') ] [ (mer a ∘ ! (mer a0) ∘ mer a') ]
     homomorphism = ConnectedProduct.wedge-elim {A = A} {B = A} A-Connected A-Connected
-                      (λ a a' → _ , use-level (Trunc-level{tl 1}) _ _)
+                      (λ a a' → _ , use-level (Trunc-level {tl 1}) _ _)
                       (Inr id) {a0} {a0}
                       (λ a → [ (mer (a0 ⊙ a)) ] ≃〈 ap ([_]) (ap mer (unitl a)) 〉
                              [ (mer a) ] ≃〈 ap ([_]) (! (!-inv-r-front (mer a0) (mer a))) 〉