diff --git a/homotopy/TS1S1.agda b/homotopy/TS1S1.agda
index 80ad82b..6632d83 100644
--- a/homotopy/TS1S1.agda
+++ b/homotopy/TS1S1.agda
@@ -76,7 +76,8 @@ module homotopy.TS1S1 where
                                (ap (λ z → z , x₁) S¹.loop)
                                (S¹-elimo (λ x₂ → t2c (c2t' S¹.base x₂) == (S¹.base , x₂)) id (PathOver=.in-PathOver-= square1) x₁))
                 square2
-                (coe (! (PathOver-square/= S¹.loop square2 square2)) 
+                (PathOver-Square.in-PathOver-Square 
+                  S¹.loop square2 square2
                   (transport (λ x₁ → Cube square2 square2 
                                           x₁ (PathOver=.out-PathOver-= (apdo (λ x₂ → ap (λ z → t2c (c2t' z x₂)) S¹.loop) S¹.loop))
                                           (PathOver=.out-PathOver-= (apdo (λ x₂ → ap (λ z → z , x₂) S¹.loop) S¹.loop)) x₁)
diff --git a/lib/cubical/Cube.agda b/lib/cubical/Cube.agda
index 1efd94d..2edc63d 100644
--- a/lib/cubical/Cube.agda
+++ b/lib/cubical/Cube.agda
@@ -71,6 +71,39 @@ module lib.cubical.Cube where
     → Type where
     id : CubeOver B id id id id id id id
 
+  whisker-cube :  {A : Type} {a000 : A}  
+    {a010 a100 a110 a001 a011 a101 a111 : A}
+    {p0-0 : a000 == a010}
+    {p-00 : a000 == a100}
+    {p-10 : a010 == a110}
+    {p1-0 : a100 == a110}
+    {f--0 f--0' : Square p0-0 p-00 p-10 p1-0} -- left
+    → f--0 == f--0'
+    → 
+    {p0-1 : a001 == a011}
+    {p-01 : a001 == a101}
+    {p-11 : a011 == a111}
+    {p1-1 : a101 == a111}
+    {f--1 f--1' : Square p0-1 p-01 p-11 p1-1} -- right
+    → f--1 == f--1'
+    → 
+    {p00- : a000 == a001}
+    {p01- : a010 == a011}
+    {p10- : a100 == a101}
+    {p11- : a110 == a111}
+    {f0-- f0--' : Square p0-0 p00- p01- p0-1} -- back
+    → f0-- == f0--'
+    →
+    {f-0- f-0-' : Square p-00 p00- p10- p-01} -- top
+    → f-0- == f-0-'
+    → {f-1- f-1-' : Square p-10 p01- p11- p-11} -- bot
+    → f-1- == f-1-'
+    → {f1-- f1--' : Square p1-0 p10- p11- p1-1} -- front
+    → f1-- == f1--'
+    -> Cube f--0 f--1 f0-- f-0- f-1- f1--
+    -> Cube f--0' f--1' f0--' f-0-' f-1-' f1--'
+  whisker-cube id id id id id id c = c
+
   -- old left and right are new top and bottom
   -- old top and bottom are new front and back
   -- old back and front are new left and right
@@ -298,32 +331,103 @@ module lib.cubical.Cube where
                                 q1-
     SquareOver-= f q1 q2 q3 q4 c = SquareOver-=' f _ q1 _ q2 _ q3 q4 c
 
+  module CubePath where
+    cube-to-path :
+      {A : Type}
+      {a000 a010 a100 a110 a001 a011 a101 a111 : A}
+      {p0-0 : a000 == a010}
+      {p-00 : a000 == a100}
+      {p-10 : a010 == a110}
+      {p1-0 : a100 == a110}
+      {f--0 : Square p0-0 p-00 p-10 p1-0}
+      {p0-1 : a001 == a011}
+      {p-01 : a001 == a101}
+      {p-11 : a011 == a111}
+      {p1-1 : a101 == a111}
+      {f--1 : Square p0-1 p-01 p-11 p1-1}
+      {p00- : a000 == a001}
+      {p01- : a010 == a011}
+      {p10- : a100 == a101}
+      {p11- : a110 == a111}
+      {f0-- : Square p0-0 p00- p01- p0-1}
+      {f-0- : Square p-00 p00- p10- p-01}
+      {f-1- : Square p-10 p01- p11- p-11}
+      {f1-- : Square p1-0 p10- p11- p1-1}
+      → Cube f--0 f--1 f0-- f-0- f-1- f1--
+      → Path (whisker-square id (square-to-disc' f-0-) (square-to-disc' f-1-) id
+                ((!-square-h f0-- ∘-square-h f--0) ∘-square-h f1--)) f--1
+    cube-to-path id = id
+{-
+  module CubeSquare where
+    cube-to-square : {A : Type} {a000 : A}  
+      {a010 X : A}
+      {p0-0 : a000 == a010}
+      {p1-0 : a000 == a010}
+      (f--0 : Square p0-0 id id p1-0) -- left
+      {p0-1 : a000 == a010}
+      {p1-1 : a000 == a010}
+      (f--1 : Square p0-1 id id p1-1) -- right
+      (f0-- : Square p0-0 id id p0-1) -- back
+      (f1-- : Square p1-0 id id p1-1) -- front
+      → Cube f--0 f--1 f0-- id id f1--
+      → Square (horiz-degen-square-to-path f--0) (horiz-degen-square-to-path f0--) (horiz-degen-square-to-path f1--) (horiz-degen-square-to-path f--1)
+    cube-to-square {a000 = a000} {p0-0 = id} = horiz-degen-square-induction1 
+      (\ {p1-0} f--0 → 
+       {p0-1 : a000 == a000}
+       {p1-1 : a000 == a000}
+       (f--1 : Square p0-1 id id p1-1) -- right
+       (f0-- : Square id id id p0-1) -- back
+       (f1-- : Square p1-0 id id p1-1) -- front
+       → Cube f--0 f--1 f0-- id id f1--
+       → Square (horiz-degen-square-to-path f--0) (horiz-degen-square-to-path f0--) (horiz-degen-square-to-path f1--) (horiz-degen-square-to-path f--1))
+      {!!}
+-}
   
   module SquareOver=ND where
 
     open PathOver=
 
-    postulate
-      in-SquareOver-= : {A B : Type} {f g : A → B} 
-                     {a00 : A} {a01 a10 a11 : A} 
-                     {p0- : a00 == a01}
-                     {p-0 : a00 == a10}
-                     {p-1 : a01 == a11}
-                     {p1- : a10 == a11}
-                     {fa   : Square p0- p-0 p-1 p1- }
-                     {b00 : f a00 == g a00} {b01 : f a01 == g a01} {b10 : f a10 == g a10} {b11 : f a11 == g a11}
-                     {q0- : PathOver (\ x -> f x == g x) p0- b00 b01}
-                     {q-0 : PathOver (\ x -> f x == g x) p-0 b00 b10}
-                     {q-1 : PathOver (\ x -> f x == g x) p-1 b01 b11}
-                     {q1- : PathOver (\ x -> f x == g x) p1- b10 b11}
-                     → Cube (out-PathOver-= q0-) (out-PathOver-= q1-) (out-PathOver-= q-0) (ap-square f fa) (ap-square g fa) (out-PathOver-= q-1)
-                     → SquareOver (\ x -> f x == g x) fa
-                                  q0-
-                                  q-0
-                                  q-1
-                                  q1-
-
-      out-SquareOver-= : {A B : Type} {f g : A → B} 
+    in-SquareOver-= : {A B : Type} {f g : A → B} 
+                       {a00 : A} {a01 a10 a11 : A} 
+                       {p0- : a00 == a01}
+                       {p-0 : a00 == a10}
+                       {p-1 : a01 == a11}
+                       {p1- : a10 == a11}
+                       {fa   : Square p0- p-0 p-1 p1- }
+                       {b00 : f a00 == g a00} {b01 : f a01 == g a01} {b10 : f a10 == g a10} {b11 : f a11 == g a11}
+                       {q0- : PathOver (\ x -> f x == g x) p0- b00 b01}
+                       {q-0 : PathOver (\ x -> f x == g x) p-0 b00 b10}
+                       {q-1 : PathOver (\ x -> f x == g x) p-1 b01 b11}
+                       {q1- : PathOver (\ x -> f x == g x) p1- b10 b11}
+                       → Cube (out-PathOver-= q0-) (out-PathOver-= q1-) (out-PathOver-= q-0) (ap-square f fa) (ap-square g fa) (out-PathOver-= q-1)
+                       → SquareOver (\ x -> f x == g x) fa
+                                    q0-
+                                    q-0
+                                    q-1
+                                    q1-
+    in-SquareOver-= {f = f} {g} {fa = fa} {b00 = b00} {q0- = id} {q-0 = id} {q-1 = id} c = 
+      horiz-degen-square-induction1
+        (λ {p1- } fa →
+           {q1- : PathOver (λ x → f x == g x) p1- b00 b00}
+           (c₁
+            : Cube hrefl-square (out-PathOver-= q1-) hrefl-square
+              (ap-square f fa) (ap-square g fa) hrefl-square) →
+           SquareOver (λ x → f x == g x) fa id id id q1-)
+        (λ {q1- } c → transport
+         (λ x → SquareOver (λ x₁ → Id (f x₁) (g x₁)) id id id id x) (IsEquiv.β (snd hom-to-over/left-eqv) q1-)
+                        (square-to-over-id
+                         (coh {q1- = over-to-hom q1- }
+                          (whisker-cube id (! (coh2 _ q1-)) id id id id c))) ) fa c where -- need square over id is a square
+      coh : ∀ {A} {a b : A} {b00 : a == b} {q1- : b00 == b00} →
+         Cube hrefl-square (horiz-degen-square q1-) hrefl-square id id hrefl-square → Square id id id q1-
+      coh {b00 = id} {q1- } c = transport (λ x → Square id id id x) (IsEquiv.β (snd horiz-degen-square-eqv) q1- ∘ ap horiz-degen-square-to-path (CubePath.cube-to-path c)) id
+
+      coh2 : (b00' : _) (q1- : PathOver (λ x → f x == g x) id b00 b00') → (horiz-degen-square (over-to-hom q1-)) == (out-PathOver-= q1-) 
+      coh2 = path-induction-homo-e _ (coh2a b00) where
+        coh2a : ∀ {A} {a b : A} (p : a == b) → horiz-degen-square id == hrefl-square {p = p}
+        coh2a id = id
+
+    out-SquareOver-= : {A B : Type} {f g : A → B} 
                      {a00 : A} {a01 a10 a11 : A} 
                      {p0- : a00 == a01}
                      {p-0 : a00 == a10}
@@ -341,19 +445,33 @@ module lib.cubical.Cube where
                                   q-1
                                   q1-
                      → Cube (out-PathOver-= q0-) (out-PathOver-= q1-) (out-PathOver-= q-0) (ap-square f fa) (ap-square g fa) (out-PathOver-= q-1)
+    out-SquareOver-= {b00 = b00} id = coh b00 where 
+      coh : ∀ {a b} (p : a == b) → Cube (hrefl-square {p = p}) (hrefl-square {p = p}) (hrefl-square {p = p}) id id (hrefl-square {p = p})
+      coh id = id
 
-  postulate
-    PathOver-square/= : {Γ A : Type} {x1 x2 : Γ} (δ : x1 == x2) {a00 a01 a10 a11 : Γ → A} 
+  module PathOver-Square where
+
+    in-PathOver-Square : {Γ A : Type} {x1 x2 : Γ} (δ : x1 == x2) {a00 a01 a10 a11 : Γ → A} 
                           {p0- : (x : Γ) → a00 x == a01 x}
                           {p-0 : (x : Γ) → a00 x == a10 x }
                           {p-1 : (x : Γ) → a01 x == a11 x }
                           {p1- : (x : Γ) → a10 x == a11 x }
                           (f1 : Square (p0- x1) (p-0 x1) (p-1 x1) (p1- x1))
                        → (f2 : Square (p0- x2) (p-0 x2) (p-1 x2) (p1- x2))
-                       →     (PathOver (\ x -> Square (p0- x) (p-0 x) (p-1 x) (p1- x)) δ f1 f2)
-                           == (Cube f1 f2 (PathOver=.out-PathOver-= (apdo p0- δ)) (PathOver=.out-PathOver-= (apdo p-0 δ)) (PathOver=.out-PathOver-= (apdo p-1 δ)) (PathOver=.out-PathOver-= (apdo p1- δ)))
+                       → (Cube f1 f2 (PathOver=.out-PathOver-= (apdo p0- δ)) (PathOver=.out-PathOver-= (apdo p-0 δ)) (PathOver=.out-PathOver-= (apdo p-1 δ)) (PathOver=.out-PathOver-= (apdo p1- δ)))
+                       → (PathOver (\ x -> Square (p0- x) (p-0 x) (p-1 x) (p1- x)) δ f1 f2)
+    in-PathOver-Square id f1 f2 c = hom-to-over (coh _ _ c) where
+      coh : {A : Type}
+            {a00 a01 a10 a11 : A} 
+            {p0- : a00 == a01}
+            {p-0 : a00 == a10}
+            {p-1 : a01 == a11}
+            {p1- : a10 == a11}
+          → (f1 f2 : (Square p0- p-0 p-1 p1-))
+          → Cube f1 f2 hrefl-square hrefl-square hrefl-square hrefl-square
+          → f1 == f2
+      coh id f2 c = CubePath.cube-to-path c
 
-  -- FIXME: match with cubical sets terminology?
   degen-cube-h :{A : Type} {a000 : A} 
     {a010 a100 a110 : A}
     {p0-0 : a000 == a010}
@@ -365,49 +483,6 @@ module lib.cubical.Cube where
     → Cube f--0 f--1 hrefl-square hrefl-square hrefl-square hrefl-square
   degen-cube-h {f--0 = id} id = id
 
-{- annoying to prove and not used
-  postulate
-   ∘-cube-horiz/degen : 
-    {A : Type}
-    {a000 a010 a100 a110 : A}
-
-    {p0-0 : a000 == a010}
-    {p-00 : a000 == a100}
-    {p-10 : a010 == a110}
-    {p1-0 : a100 == a110}
-    {f--0 : Square p0-0 p-00 p-10 p1-0}
-
-    {p0-1 : a000 == a010}
-    {p-01 : a000 == a100}
-    {p-11 : a010 == a110}
-    {p1-1 : a100 == a110}
-    {f--1 : Square p0-1 p-01 p-11 p1-1}
-
-    {f0-- : p0-0 == p0-1}
-    {f-0- : p-00 == p-01}
-    {f-1- : p-10 == p-11}
-    {f1-- : p1-0 == p1-1}
-
-    {p0-2 : a000 == a010}
-    {p-02 : a000 == a100}
-    {p-12 : a010 == a110}
-    {p1-2 : a100 == a110}
-    {f--2 : Square p0-2 p-02 p-12 p1-2}
-
-    {f0--' : p0-1 == p0-2}
-    {f-0-' : p-01 == p-02}
-    {f-1-' : p-11 == p-12}
-    {f1--' : p1-1 == p1-2}
-
-    → Cube f--0 f--1 (horiz-degen-square f0--) (horiz-degen-square f-0-) (horiz-degen-square f-1-) (horiz-degen-square f1--)
-    → Cube f--1 f--2 (horiz-degen-square f0--') (horiz-degen-square f-0-') (horiz-degen-square f-1-') (horiz-degen-square f1--')
-    → Cube f--0 f--2 (horiz-degen-square (f0--' ∘ f0--)) (horiz-degen-square (f-0-' ∘ f-0-)) (horiz-degen-square (f-1-' ∘ f-1-)) (horiz-degen-square (f1--' ∘ f1--))
---  ∘-cube-horiz/degen = {!!} 
-
-  _∘-cube-h/degen_ = ∘-cube-horiz/degen
-  infixr 10 _∘-cube-h/degen_
--}
-
   -- ap to inner argument first
   -- could do it in the other order, too
   bifunctor-square1 : {A B C : Type} (f : A → B → C) {a a' : A} {b b' : B}
@@ -482,7 +557,106 @@ module lib.cubical.Cube where
                             (bifunctor-square2d f p-1 pb) 
   bifunctor-on-cube f s pb = SquareOver=ND.out-SquareOver-= (apdo-square (λ x → ap (λ y → f x (y x)) pb) s)
 
-{-
+  fill-cube-left : 
+      {A : Type} 
+      {a000 a010 a100 a110 a001 a011 a101 a111 : A}
+      {p0-0 : a000 == a010}
+      {p-00 : a000 == a100}
+      {p-10 : a010 == a110}
+      {p1-0 : a100 == a110}
+  
+      {p0-1 : a001 == a011}
+      {p-01 : a001 == a101}
+      {p-11 : a011 == a111}
+      {p1-1 : a101 == a111}
+      (f--1 : Square p0-1 p-01 p-11 p1-1) -- right
+  
+      {p00- : a000 == a001}
+      {p01- : a010 == a011}
+      {p10- : a100 == a101}
+      {p11- : a110 == a111}
+      (f0-- : Square p0-0 p00- p01- p0-1) -- back
+      (f-0- : Square p-00 p00- p10- p-01) -- top
+      (f-1- : Square p-10 p01- p11- p-11) -- bot
+      (f1-- : Square p1-0 p10- p11- p1-1) -- front
+      → Σ \ (f--0 : Square p0-0 p-00 p-10 p1-0) → 
+            Cube f--0 f--1 f0-- f-0- f-1- f1--
+  fill-cube-left {p-00 = id}  {p-10 = p-10} {p-01 = p-01} f--1 id f-0- f-1- id = 
+    horiz-degen-square-induction1
+      (λ {p-11} f-1- →
+         (f-0-₁ : Square id id id p-01) (f--2 : Square id p-01 p-11 id) →
+         Σ (λ f--0 → Cube f--0 f--2 id f-0-₁ f-1- id))
+      (λ f-0- f--1 → horiz-degen-square-induction1
+                       (λ {p-1} f-0- →
+                          (f--1 : Square id p-1 p-10 id) →
+                          Σ (λ f--0 → Cube f--0 f--1 id f-0- hrefl-square id))
+                       (λ f--1 → f--1 , (degen-cube-h id)) f-0- f--1) f-1- f-0- f--1 
+
+
+  ap-square-id! : {A : Type} {a00 a01 a10 a11 : A} 
+              {p0- : a00 == a01}
+              {p-0 : a00 == a10}
+              {p-1 : a01 == a11}
+              {p1- : a10 == a11}
+              (f   : Square p0- p-0 p-1 p1-)
+              → Cube f (ap-square (\ x -> x) f)
+                        (horiz-degen-square (! (ap-id p0-)))
+                        (horiz-degen-square (! (ap-id p-0)))
+                        (horiz-degen-square (! (ap-id p-1)))
+                        (horiz-degen-square (! (ap-id p1-))) 
+  ap-square-id! id = id
+
+  ap-square-o : {A B C : Type} (g : B → C) (f : A → B) 
+              {a00 a01 a10 a11 : A} 
+              {p0- : a00 == a01}
+              {p-0 : a00 == a10}
+              {p-1 : a01 == a11}
+              {p1- : a10 == a11}
+              (s   : Square p0- p-0 p-1 p1-)
+              → Cube (ap-square (g o f) s) (ap-square g (ap-square f s)) (horiz-degen-square (ap-o g f p0-)) (horiz-degen-square (ap-o g f p-0)) (horiz-degen-square (ap-o g f p-1)) (horiz-degen-square (ap-o g f p1-))
+  ap-square-o g f id = id
+
+{- annoying to prove and not used
+   ∘-cube-horiz/degen : 
+    {A : Type}
+    {a000 a010 a100 a110 : A}
+
+    {p0-0 : a000 == a010}
+    {p-00 : a000 == a100}
+    {p-10 : a010 == a110}
+    {p1-0 : a100 == a110}
+    {f--0 : Square p0-0 p-00 p-10 p1-0}
+
+    {p0-1 : a000 == a010}
+    {p-01 : a000 == a100}
+    {p-11 : a010 == a110}
+    {p1-1 : a100 == a110}
+    {f--1 : Square p0-1 p-01 p-11 p1-1}
+
+    {f0-- : p0-0 == p0-1}
+    {f-0- : p-00 == p-01}
+    {f-1- : p-10 == p-11}
+    {f1-- : p1-0 == p1-1}
+
+    {p0-2 : a000 == a010}
+    {p-02 : a000 == a100}
+    {p-12 : a010 == a110}
+    {p1-2 : a100 == a110}
+    {f--2 : Square p0-2 p-02 p-12 p1-2}
+
+    {f0--' : p0-1 == p0-2}
+    {f-0-' : p-01 == p-02}
+    {f-1-' : p-11 == p-12}
+    {f1--' : p1-1 == p1-2}
+
+    → Cube f--0 f--1 (horiz-degen-square f0--) (horiz-degen-square f-0-) (horiz-degen-square f-1-) (horiz-degen-square f1--)
+    → Cube f--1 f--2 (horiz-degen-square f0--') (horiz-degen-square f-0-') (horiz-degen-square f-1-') (horiz-degen-square f1--')
+    → Cube f--0 f--2 (horiz-degen-square (f0--' ∘ f0--)) (horiz-degen-square (f-0-' ∘ f-0-)) (horiz-degen-square (f-1-' ∘ f-1-)) (horiz-degen-square (f1--' ∘ f1--))
+--  ∘-cube-horiz/degen = {!!} 
+
+  _∘-cube-h/degen_ = ∘-cube-horiz/degen
+  infixr 10 _∘-cube-h/degen_
+
   cross-square-path-Σ : {A : Type} {B : A → Type} 
               {a00 a01 a10 a11 : A} 
               {p0- : a00 == a01}
@@ -502,11 +676,8 @@ module lib.cubical.Cube where
                           (PathOver=.out-PathOver-= (apdo (λ b → pair= p-0 (apdo b p-0)) pb))
                           (PathOver=.out-PathOver-= (apdo (λ b → pair= p-1 (apdo b p-1)) pb))
                           (PathOver=.out-PathOver-= (apdo (λ b → pair= p1- (apdo b p1-)) pb))
-  cross-square-path-Σ id id = FIXME where
-    postulate FIXME : {A : Type} → A
--}
+  cross-square-path-Σ id id = ?
 
-{-
   cross-square-path-Σ-compute : {A : Type} {B : A → Type} {C : Type}
             (f : (x : A) → B x → C)
             {a00 a01 a10 a11 : A} 
@@ -524,7 +695,6 @@ module lib.cubical.Cube where
          (PathOver=.out-PathOver-=
           (apdo (λ b → pair= p0- (apdo b p0-)) pb)))) !} (bifunctor-on-cube f s pb)
   cross-square-path-Σ-compute = {!!}
--}
 
 -- Square (ap (λ y → f a00 (y a00)) pb)
 --       (ap (λ z → f z (b0 z)) p0-) (ap (λ z → f z (b1 z)) p0-)
@@ -536,92 +706,9 @@ module lib.cubical.Cube where
 --    (ap (λ xy → f (fst xy) (snd xy)) (pair= p0- (apdo b1 p0-)))
 --    (ap (λ xy → f (fst xy) (snd xy)) (ap (λ z → a01 , z a01) pb))
 
-  ap-square-id! : {A : Type} {a00 a01 a10 a11 : A} 
-              {p0- : a00 == a01}
-              {p-0 : a00 == a10}
-              {p-1 : a01 == a11}
-              {p1- : a10 == a11}
-              (f   : Square p0- p-0 p-1 p1-)
-              → Cube f (ap-square (\ x -> x) f)
-                        (horiz-degen-square (! (ap-id p0-)))
-                        (horiz-degen-square (! (ap-id p-0)))
-                        (horiz-degen-square (! (ap-id p-1)))
-                        (horiz-degen-square (! (ap-id p1-))) 
-  ap-square-id! id = id
-
-  ap-square-o : {A B C : Type} (g : B → C) (f : A → B) 
-              {a00 a01 a10 a11 : A} 
-              {p0- : a00 == a01}
-              {p-0 : a00 == a10}
-              {p-1 : a01 == a11}
-              {p1- : a10 == a11}
-              (s   : Square p0- p-0 p-1 p1-)
-              → Cube (ap-square (g o f) s) (ap-square g (ap-square f s)) (horiz-degen-square (ap-o g f p0-)) (horiz-degen-square (ap-o g f p-0)) (horiz-degen-square (ap-o g f p-1)) (horiz-degen-square (ap-o g f p1-))
-  ap-square-o g f id = id
-
   -- FIXME how do you get this from composition?
-  whisker-cube :  {A : Type} {a000 : A}  
-    {a010 a100 a110 a001 a011 a101 a111 : A}
-    {p0-0 : a000 == a010}
-    {p-00 : a000 == a100}
-    {p-10 : a010 == a110}
-    {p1-0 : a100 == a110}
-    {f--0 f--0' : Square p0-0 p-00 p-10 p1-0} -- left
-    → f--0 == f--0'
-    → 
-    {p0-1 : a001 == a011}
-    {p-01 : a001 == a101}
-    {p-11 : a011 == a111}
-    {p1-1 : a101 == a111}
-    {f--1 f--1' : Square p0-1 p-01 p-11 p1-1} -- right
-    → f--1 == f--1'
-    → 
-    {p00- : a000 == a001}
-    {p01- : a010 == a011}
-    {p10- : a100 == a101}
-    {p11- : a110 == a111}
-    {f0-- f0--' : Square p0-0 p00- p01- p0-1} -- back
-    → f0-- == f0--'
-    →
-    {f-0- f-0-' : Square p-00 p00- p10- p-01} -- top
-    → f-0- == f-0-'
-    → {f-1- f-1-' : Square p-10 p01- p11- p-11} -- bot
-    → f-1- == f-1-'
-    → {f1-- f1--' : Square p1-0 p10- p11- p1-1} -- front
-    → f1-- == f1--'
-    -> Cube f--0 f--1 f0-- f-0- f-1- f1--
-    -> Cube f--0' f--1' f0--' f-0-' f-1-' f1--'
-  whisker-cube id id id id id id c = c
 
-  postulate
-    fill-cube-left : 
-      {A : Type} 
-      {a000 a010 a100 a110 a001 a011 a101 a111 : A}
-      {p0-0 : a000 == a010}
-      {p-00 : a000 == a100}
-      {p-10 : a010 == a110}
-      {p1-0 : a100 == a110}
-  
-      {p0-1 : a001 == a011}
-      {p-01 : a001 == a101}
-      {p-11 : a011 == a111}
-      {p1-1 : a101 == a111}
-      (f--1 : Square p0-1 p-01 p-11 p1-1) -- right
-  
-      {p00- : a000 == a001}
-      {p01- : a010 == a011}
-      {p10- : a100 == a101}
-      {p11- : a110 == a111}
-      (f0-- : Square p0-0 p00- p01- p0-1) -- back
-      (f-0- : Square p-00 p00- p10- p-01) -- top
-      (f-1- : Square p-10 p01- p11- p-11) -- bot
-      (f1-- : Square p1-0 p10- p11- p1-1) -- front
-      → Σ \ (f--0 : Square p0-0 p-00 p-10 p1-0) → 
-            Cube f--0 f--1 f0-- f-0- f-1- f1--
-  -- fill-cube-left f--1 id f-0- f-1- id = {!!} -- need induction on degen square
-
-{-
-    fill-cube-top : 
+  fill-cube-top : 
       {A : Type} 
       {a000 a010 a100 a110 a001 a011 a101 a111 : A}
       {p0-0 : a000 == a010}
@@ -646,7 +733,7 @@ module lib.cubical.Cube where
       → Σ \ (f-0- : Square p-00 p00- p10- p-01) -- top
           → Cube f--0 f--1 f0-- f-0- f-1- f1--
 
-    fill-cube-back : 
+  fill-cube-back : 
       {A : Type} 
       {a000 a010 a100 a110 a001 a011 a101 a111 : A}
       {p0-0 : a000 == a010}
@@ -670,10 +757,8 @@ module lib.cubical.Cube where
       (f1-- : Square p1-0 p10- p11- p1-1) -- front
       → Σ \       (f0-- : Square p0-0 p00- p01- p0-1) -- back
           → Cube f--0 f--1 f0-- f-0- f-1- f1--
-  
 
-  postulate
-    CubeΣ-eqv : {A : Type} {B : A → Type} {a000 : Σ B}  
+  CubeΣ-eqv : {A : Type} {B : A → Type} {a000 : Σ B}  
               {a010 a100 a110 a001 a011 a101 a111 : Σ B}
               {p0-0 : a000 == a010}
               {p-00 : a000 == a100}
@@ -697,8 +782,7 @@ module lib.cubical.Cube where
                       (Σ \ (c : Cube (fst (oute SquareΣ-eqv f--0)) (fst (oute SquareΣ-eqv f--1)) (fst (oute SquareΣ-eqv f0--)) (fst (oute SquareΣ-eqv f-0-)) (fst (oute SquareΣ-eqv f-1-)) (fst (oute SquareΣ-eqv f1--))) → 
                            CubeOver B c (snd (oute SquareΣ-eqv f--0)) (snd (oute SquareΣ-eqv f--1)) (snd (oute SquareΣ-eqv f0--)) (snd (oute SquareΣ-eqv f-0-)) (snd (oute SquareΣ-eqv f-1-)) (snd (oute SquareΣ-eqv f1--)))
 
-  postulate
-    ap-bifunctor-square : {A C : Type} {B : A → Type} (f : (x : A) → B x → C) → 
+  ap-bifunctor-square : {A C : Type} {B : A → Type} (f : (x : A) → B x → C) → 
                 {a00 a01 a10 a11 : A} 
                 {la : a00 == a01}
                 {ta : a00 == a10}
@@ -715,5 +799,5 @@ module lib.cubical.Cube where
                         (oute SquareOver-constant-eqv
                            (oute SquareOver-Π-eqv (apdo-square f fa) _ _ _ _ _ _ _ _ fb))
                         (horiz-degen-square (ap-bifunctor-pair= f _ lb)) (horiz-degen-square (ap-bifunctor-pair= f _ tb)) (horiz-degen-square (ap-bifunctor-pair= f _ bb)) (horiz-degen-square (ap-bifunctor-pair= f _ rb))
-  -- ap-bifunctor-square f .id id = {!!}
+  ap-bifunctor-square f .id id = {!!}
 -}
diff --git a/lib/cubical/Square.agda b/lib/cubical/Square.agda
index 53c4b9c..3323d79 100644
--- a/lib/cubical/Square.agda
+++ b/lib/cubical/Square.agda
@@ -6,6 +6,30 @@ open import lib.cubical.PathOver
 
 module lib.cubical.Square where
 
+  module Derivable where
+     Square' : {A : Type} {a00 : A} {a01 a10 a11 : A} → a00 == a01 -> a00 == a10 -> a01 == a11 -> a10 == a11 -> Type 
+     Square' p q r s = r ∘ p == s ∘ q
+   
+     idSquare' : {A : Type} {a00 : A} → Square' {a00 = a00} id id id id
+     idSquare' = id
+   
+     Square'-induction : {A : Type} {a00 : A} 
+                         (C : {a01 a10 a11 : A} → {p : a00 == a01} {q : a00 == a10} {r : a01 == a11} {s :  a10 == a11} -> Square' p q r s → Type)
+                       → C {p = id} {q = id} {r = id} {s = id} (idSquare' {_}{a00})
+                       → {a01 a10 a11 : A} → {p : a00 == a01} {q : a00 == a10} {r : a01 == a11} {s :  a10 == a11} 
+                          (sq : Square' p q r s) → C {p = p} {q = q} {r = r} {s = s} sq
+     Square'-induction C b {p = id} {q = id} {r = id} {.id} id = b
+   
+     Square'-induction-β : {A : Type} {a00 : A} 
+                         (C : {a01 a10 a11 : A} → {p : a00 == a01} {q : a00 == a10} {r : a01 == a11} {s :  a10 == a11} -> Square' p q r s → Type)
+                       → (b : C {p = id} {q = id} {r = id} {s = id} (idSquare' {_}{a00}))
+                       → Square'-induction {a00 = a00} 
+                                           (\ {a01} {a10} {a11}{p}{q}{r}{s} sq → C {a01}{a10}{a11}{p}{q}{r}{s} sq)
+                                           b {a00} {a00} {a00} {p = id} {q = id} {r = id} {s = id} (idSquare' {A}{a00}) 
+                          == b
+     Square'-induction-β C b = id
+                     
+
   data Square {A : Type} {a00 : A} : 
               {a01 a10 a11 : A} → a00 == a01 -> a00 == a10 -> a01 == a11 -> a10 == a11 -> Type where 
     id : Square id id id id
@@ -65,6 +89,16 @@ module lib.cubical.Square where
               → p-1 ∘ p0- == p1- ∘ p-0
   square-to-disc id = id
 
+  square-to-disc' : {A : Type}
+              {a00 a01 a10 a11 : A} 
+              {p0- : a00 == a01}
+              {p-0 : a00 == a10}
+              {p-1 : a01 == a11}
+              {p1- : a10 == a11}
+              (f   : Square p0- p-0 p-1 p1-)
+              → p-1 ∘ p0- ∘ ! p-0 == p1-
+  square-to-disc' id = id
+
   disc-to-square : {A : Type}
               {a00 a01 a10 a11 : A} 
               {p0- : a00 == a01}
@@ -104,6 +138,49 @@ module lib.cubical.Square where
               → Equiv (Square p0- p-0 p-1 p1-) (p-1 ∘ p0- == p1- ∘ p-0) 
   square-disc-eqv = (improve (hequiv square-to-disc disc-to-square square-disc-square disc-square-disc))
 
+  horiz-degen-square : {A : Type} {a a' : A} {p q : a == a'} (r : p == q)
+                     → Square p id id q
+  horiz-degen-square {p = id}{q = .id} id = id
+  -- disc-to-square {p0- = p} {id} {id} {q}
+
+  horiz-degen-square-to-path : {A : Type} {a a' : A} {p q : a == a'} 
+                     → Square p id id q → p == q
+  horiz-degen-square-to-path {p = p} s = square-to-disc s ∘ ! (∘-unit-l p)
+
+  vertical-degen-square : {A : Type} {a a' : A} {p q : a == a'} (r : p == q)
+                     → Square id p q id
+  vertical-degen-square {p = id}{q = .id} id = id
+
+
+  horiz-degen-square-induction : {A : Type} {a : A}
+                               → (C : {a' : A} {p : a == a'} {q : a == a'} (s : Square p id id q) → Type)
+                               → C id 
+                               → {a' : A} {p q : a == a'} (s : Square p id id q) → C s
+  horiz-degen-square-induction {A}{a} C b {a'}{p}{q} s = transport (λ s₁ → C s₁) (IsEquiv.α (snd square-disc-eqv) s) (coh (square-to-disc s)) where
+    coh : ∀ {a'} {p : a == a'} {q : a == a'} → (d : id ∘ p == q) → C (disc-to-square {p0- = p}{id}{id}{q} d)
+    coh {p = id} {.id} id = b
+
+  horiz-degen-square-induction1 : {A : Type} {a a' : A} {p : a == a'}
+                               → (C : {q : a == a'} (s : Square p id id q) → Type)
+                               → C {p} (hrefl-square) 
+                               → {q : a == a'} (s : Square p id id q) → C s
+  horiz-degen-square-induction1 {A}{a}{.a} {id} C b {q} s = transport (λ s₁ → C s₁) (IsEquiv.α (snd square-disc-eqv) s) (coh (square-to-disc s)) where
+     coh : ∀ {q : a == a} → (d : id == q) → C (disc-to-square {p0- = id}{id}{id}{q} d)
+     coh id = b
+
+  horiz-degen-square-induction1-β : {A : Type} {a a' : A} {p : a == a'}
+                                  → (C : {q : a == a'} (s : Square p id id q) → Type)
+                                  → (b : C {p} (hrefl-square))
+                                  → horiz-degen-square-induction1 C b (hrefl-square) == b
+  horiz-degen-square-induction1-β {p = id} C b = id
+
+  horiz-degen-square-eqv : {A : Type} {a a' : A} {p q : a == a'} 
+                         → Equiv (Square p id id q) (p == q)
+  horiz-degen-square-eqv {p = id} = improve (hequiv horiz-degen-square-to-path horiz-degen-square
+                                           (λ s →
+                                                horiz-degen-square-induction
+                                                (λ x → Path (horiz-degen-square (horiz-degen-square-to-path x)) x)
+                                                id s) (λ y → path-induction (\ _ y → Path (horiz-degen-square-to-path (horiz-degen-square y)) y) id y))
 
   square-∘-topright-right' : {A : Type}
               {a00 a01 a10 a11 : A} 
@@ -214,13 +291,32 @@ module lib.cubical.Square where
                → Square pa (ap f p) (ap g p) pa'
     out-PathOver-= id = hrefl-square
 
-    postulate 
-      in-PathOver-= : {A B : Type} {f g : A → B}
+    in-PathOver-= : {A B : Type} {f g : A → B}
                 {a a' : A} {p : a == a'}
                 {pa : f a == g a}
                 {pa' : f a' == g a'}
                → Square pa (ap f p) (ap g p) pa'
                → PathOver (\ x -> f x == g x) p pa pa'
+    in-PathOver-= {f = f} {g} {p = id} {pa} s = horiz-degen-square-induction1
+                                                  (λ {pa'} s₁ → PathOver (λ x → f x == g x) id pa pa') id s
+
+    in-out : {A B : Type} {f g : A → B}
+                {a a' : A} {p : a == a'}
+                {pa : f a == g a}
+                {pa' : f a' == g a'}
+               → (s : Square pa (ap f p) (ap g p) pa')
+               → out-PathOver-= (in-PathOver-= s) == s
+    in-out {f = f}{g} {p = id} {pa} s = horiz-degen-square-induction1 (λ s₁ → out-PathOver-= (in-PathOver-= s₁) == s₁) (ap out-PathOver-=
+                                                                                                                          (horiz-degen-square-induction1-β
+                                                                                                                           (λ {pa'} s₁ → PathOver (λ x → f x == g x) id pa pa') id)) s
+
+    out-in : {A B : Type} {f g : A → B}
+                {a a' : A} {p : a == a'}
+                {pa : f a == g a}
+                {pa' : f a' == g a'}
+               → (p : PathOver (\ x -> f x == g x) p pa pa')
+               → in-PathOver-= (out-PathOver-= p) == p
+    out-in {f = f} {g} {p = .id} {pa} id = horiz-degen-square-induction1-β (λ {pa'} s₁ → PathOver (λ x → f x == g x) id pa pa') id
       
     out-PathOver-=-eqv : {A B : Type} {f g : A → B}
                 {a a' : A} {p : a == a'}
@@ -228,13 +324,11 @@ module lib.cubical.Square where
                 {pa' : f a' == g a'}
                → Equiv (PathOver (\ x -> f x == g x) p pa pa')
                         (Square pa (ap f p) (ap g p) pa')
-    out-PathOver-=-eqv = improve (hequiv out-PathOver-= in-PathOver-= FIXME1 FIXME2) where
-      postulate FIXME1 : _
-                FIXME2 : _
+    out-PathOver-=-eqv = improve (hequiv out-PathOver-= in-PathOver-= out-in in-out) 
 
+{-
   module PathOver=D where
 
-    postulate 
       in-PathOver-= : {A : Type} {B : A → Type} {f g : (x : A) → B x}
                 {a a' : A} {p : a == a'}
                 {pa : f a == g a}
@@ -242,6 +336,8 @@ module lib.cubical.Square where
                → SquareOver B (vrefl-square {p = p}) (hom-to-over/left id pa) (apdo f p) (apdo g p) (hom-to-over/left id pa')
                -- Square pa (ap f p) (ap g p) pa'
                → PathOver (\ x -> f x == g x) p pa pa'
+      in-PathOver-= = ?
+-}
       
   extend-triangle : {A : Type} {a00 a01 a11 : A}
               {p0- : a00 == a01}
@@ -370,18 +466,8 @@ module lib.cubical.Square where
               → Square (ap g l) (ap g t) (ap g b) (ap g r)
   ap-square f id = id
 
-  horiz-degen-square : {A : Type} {a a' : A} {p q : a == a'} (r : p == q)
-                     → Square p id id q
-  horiz-degen-square {p = id}{q = .id} id = id
-  -- disc-to-square {p0- = p} {id} {id} {q}
-
-  horiz-degen-square-to-path : {A : Type} {a a' : A} {p q : a == a'} 
-                     → Square p id id q → p == q
-  horiz-degen-square-to-path {p = p} s = square-to-disc s ∘ ! (∘-unit-l p)
+                                 
 
-  vertical-degen-square : {A : Type} {a a' : A} {p q : a == a'} (r : p == q)
-                     → Square id p q id
-  vertical-degen-square {p = id}{q = .id} id = id
 
 
   pair-square : {A B : Type} 
@@ -481,6 +567,24 @@ module lib.cubical.Square where
   sides-same-square : {A : Type} {a : A} (p : a == a) → Square p p p p 
   sides-same-square p = disc-to-square {p0- = p} {p} {p} {p} id
 
+  whisker-square : {A : Type} {a00 : A} 
+                   {a01 a10 a11 : A} → {p p' : a00 == a01} -> {q q' : a00 == a10} -> {r r' : a01 == a11} -> {s s' : a10 == a11}
+                   → p == p' → q == q' → r == r' -> s == s'
+                   → Square p q r s → Square p' q' r' s'
+  whisker-square id id id id id = id
+
+  square-to-over-id : {A : Type} {a00 : A} {B : A → Type}
+                      {b00 b01 b10 b11 : B a00} 
+                      {p0- : b00 == b01}
+                      {p-0 : b00 == b10}
+                      {p-1 : b01 == b11}
+                      {p1- : b10 == b11}
+                      (f   : Square p0- p-0 p-1 p1-)
+                   → SquareOver B id (hom-to-over p0-) (hom-to-over p-0) (hom-to-over p-1) (hom-to-over p1-)
+  square-to-over-id id = id
+
+
+{-
   out-SquareΣ : {A : Type} {B : A → Type}
                   {p00 p01 p10 p11 : Σ B}
                   {l : p00 == p01}
@@ -510,11 +614,10 @@ module lib.cubical.Square where
                                        (over-o-ap B (apdo snd t))
                                        (over-o-ap B (apdo snd b))
                                        (over-o-ap B (apdo snd r))))
-  SquareΣ-eqv = (out-SquareΣ , FIXME) where postulate FIXME : ∀ {A : Type} → A
+  SquareΣ-eqv = (out-SquareΣ , ?) 
 
   -- derive from above
-  postulate
-    SquareΣ-eqv-intro : {A : Type} {B : A → Type}
+  SquareΣ-eqv-intro : {A : Type} {B : A → Type}
                   {p00 p01 p10 p11 : A}
                   {l : p00 == p01}
                   {t : p00 == p10}
@@ -528,9 +631,9 @@ module lib.cubical.Square where
                 → Equiv (Square (pair= l lb) (pair= t tb) (pair= b bb) (pair= r rb))
                          (Σ (λ (s1 : Square l t b r) → 
                             SquareOver B s1 lb tb bb rb))
-  
-  postulate
-    out-SquareOver-Π-eqv : {A : Type} {B1 : A → Type} {B2 : Σ B1 → Type}
+  SquareΣ-eqv-intro = ?
+
+  out-SquareOver-Π-eqv : {A : Type} {B1 : A → Type} {B2 : Σ B1 → Type}
               {a00 : A} {b00 : (x : B1 a00) → B2 (a00 , x)} 
               {a01 a10 a11 : A} 
               {p0- : a00 == a01}
@@ -551,7 +654,7 @@ module lib.cubical.Square where
                          (q11- : PathOver B1 p1- b110 b111) →
                          (f1 : SquareOver B1 f q10- q1-0 q1-1 q11-) → 
                          SquareOver B2 (ine SquareΣ-eqv-intro (f , f1)) (oute PathOverΠ-eqv q0- _ _ q10-) (oute PathOverΠ-eqv q-0 _ _ q1-0) (oute PathOverΠ-eqv q-1 _ _ q1-1) (oute PathOverΠ-eqv q1- _ _ q11-))
-  -- out-SquareOver-Π-eqv id _ _ _ _ _ _ _ _ f1 = {!!}
+  out-SquareOver-Π-eqv id _ _ _ _ _ _ _ _ f1 = {!!}
 
   SquareOver-Π-eqv : {A : Type} {B1 : A → Type} {B2 : Σ B1 → Type}
               {a00 : A} {b00 : (x : B1 a00) → B2 (a00 , x)} 
@@ -574,14 +677,13 @@ module lib.cubical.Square where
                          (q11- : PathOver B1 p1- b110 b111) →
                          (f1 : SquareOver B1 f q10- q1-0 q1-1 q11-) → 
                          SquareOver B2 (ine SquareΣ-eqv-intro (f , f1)) (oute PathOverΠ-eqv q0- _ _ q10-) (oute PathOverΠ-eqv q-0 _ _ q1-0) (oute PathOverΠ-eqv q-1 _ _ q1-1) (oute PathOverΠ-eqv q1- _ _ q11-))
-  SquareOver-Π-eqv = out-SquareOver-Π-eqv , FIXME where
-    postulate FIXME : {A : Type} → A
+  SquareOver-Π-eqv = out-SquareOver-Π-eqv , ?
 
-{-
-  postulate
-    in-square-Type : ∀ {A B C D} {l : A == B} {t : A == C} {b : B == D} {r : C == D}
+
+  in-square-Type : ∀ {A B C D} {l : A == B} {t : A == C} {b : B == D} {r : C == D}
                   → ((x : A) → coe (b ∘ l) x == coe (r ∘ t) x)
                   → (Square {Type} l t b r)
+  in-square-Type = ?
 
   out-square-Type : ∀ {A B C D} {l : A == B} {t : A == C} {b : B == D} {r : C == D}
                 → (Square {Type} l t b r)
@@ -591,12 +693,8 @@ module lib.cubical.Square where
   square-Type-eqv : ∀ {A B C D} {l : A == B} {t : A == C} {b : B == D} {r : C == D}
                 → Equiv (Square {Type} l t b r)
                         ((x : A) → coe (b ∘ l) x == coe (r ∘ t) x)
-  square-Type-eqv = improve (hequiv out-square-Type in-square-Type FIXME FIXME) where
-    postulate
-      FIXME : {A : Type} → A
--}
+  square-Type-eqv = improve (hequiv out-square-Type in-square-Type ? ?) 
 
-{-
   out-squareover-El : ∀ {A B C D} {l : A == B} {t : A == C} {b : B == D} {r : C == D} {s : (Square {Type} l t b r)}
                           {b1 : A} {b2 : B} {b3 : C} {b4 : D}
                           {lo : PathOver (\ X -> X) l b1 b2}
@@ -610,8 +708,7 @@ module lib.cubical.Square where
                                       (over-to-hom/left (ro ∘o to)))
   out-squareover-El id = id
 
-  postulate
-    in-squareover-El : ∀ {A B C D} {l : A == B} {t : A == C} {b : B == D} {r : C == D} (s : (Square {Type} l t b r))
+  in-squareover-El : ∀ {A B C D} {l : A == B} {t : A == C} {b : B == D} {r : C == D} (s : (Square {Type} l t b r))
                           {b1 : A}
                           (b2 : B) 
                           (lo : PathOver (\ X -> X) l b1 b2)
@@ -625,7 +722,7 @@ module lib.cubical.Square where
                                   id
                                   (over-to-hom/left (ro ∘o to)))
                        → (SquareOver (\ X -> X) s lo to bo ro)
-  --in-squareover-El id = path-induction-homo-e _ (path-induction-homo-e _ (path-induction-homo-e _ {!!})) 
+  in-squareover-El id = path-induction-homo-e _ (path-induction-homo-e _ (path-induction-homo-e _ {!!})) 
 
   squareover-El-eqv : ∀ {A B C D} {l : A == B} {t : A == C} {b : B == D} {r : C == D} {s : (Square {Type} l t b r)}
                           {b1 : A} {b2 : B} {b3 : C} {b4 : D}
@@ -638,8 +735,7 @@ module lib.cubical.Square where
                                        (out-square-Type s b1) 
                                        id
                                        (over-to-hom/left (ro ∘o to)))
-  squareover-El-eqv = improve (hequiv out-squareover-El (in-squareover-El _ _ _ _ _ _ _ _) FIXME FIXME) where
-    postulate FIXME : {A : Type} → A
+  squareover-El-eqv = improve (hequiv out-squareover-El (in-squareover-El _ _ _ _ _ _ _ _) ? ? ) 
 
   out-SquareOver-constant : {A : Type} {B : Type} {a00 : A} {b00 : B }  
               {a01 a10 a11 : A} 
@@ -671,13 +767,6 @@ module lib.cubical.Square where
               {q1- : PathOver (\ _ -> B) p1- b10 b11}
               → Equiv (SquareOver (\ _ -> B) f q0- q-0 q-1 q1-)
                       (Square (out-PathOver-constant q0-) (out-PathOver-constant q-0) (out-PathOver-constant q-1) (out-PathOver-constant q1-))
-  SquareOver-constant-eqv = (out-SquareOver-constant , FIXME) where
-    postulate FIXME : {A : Type} → A
-
-  postulate
-    whisker-square : {A : Type} {a00 : A} 
-                   {a01 a10 a11 : A} → {p p' : a00 == a01} -> {q q' : a00 == a10} -> {r r' : a01 == a11} -> {s s' : a10 == a11}
-                   → p == p' → q == q' → r == r' -> s == s'
-                   → Square p q r s → Square p' q' r' s'
-  whisker-square = ?
+  SquareOver-constant-eqv = (out-SquareOver-constant , ?) 
 -}
+
diff --git a/programming/Patch.agda b/programming/Patch.agda
index 74203cd..b965094 100644
--- a/programming/Patch.agda
+++ b/programming/Patch.agda
@@ -104,7 +104,7 @@ module programming.Patch where
       ...            | Inl _ = b
       ...            | Inr _ = c
 
-      postulate
+      postulate {- HoTT Axiom -}
         R    : Type
         mkr  : Spec → R
         edit : (c d : Char) (i : Fin n) {φ : Spec} →
@@ -119,10 +119,12 @@ module programming.Patch where
  
     patch = ('a' ↔ 'b' at Z) ∘ ('x' ↔ 'y' at (S Z)) ∘ ('s' ↔ 'b' at (S (S Z)))
 
+{-
     open Infer
     test : Path (mkr (apply-at (λ _ → Some 'd') (S Z) (None :: None :: None :: [])))
                 (mkr (apply-at (λ _ → Some 'b') Z _))
     test = edit 'a' 'b' Z ∘p edit 'c' 'd' (S Z)
+-}
 
   open Test
 
diff --git a/programming/PatchWithHistories.agda b/programming/PatchWithHistories.agda
index c786e33..54d959b 100644
--- a/programming/PatchWithHistories.agda
+++ b/programming/PatchWithHistories.agda
@@ -18,7 +18,7 @@ module programming.PatchWithHistories where
     []ms = []ms'
     _::ms_ = _::ms'_
 
-    postulate 
+    postulate  {- HoTT Axiom -}
       Ex : (x y : Bool) (xs : MS) → (x ::ms (y ::ms xs)) == (y ::ms (x ::ms xs))
 
     MS-ind : (C : MS → Type) 
@@ -39,7 +39,7 @@ module programming.PatchWithHistories where
 
   open HistoryHIT 
 
-  postulate
+  postulate {- HoTT Axiom -}
     R : Type
     doc : MS → R
     add : (x : Bool) (xs : MS) → doc xs == doc (x ::ms xs)
diff --git a/programming/PatchWithHistories2.agda b/programming/PatchWithHistories2.agda
index 2896918..78f9f25 100644
--- a/programming/PatchWithHistories2.agda
+++ b/programming/PatchWithHistories2.agda
@@ -24,7 +24,7 @@ module programming.PatchWithHistories2
     _::ms_ : ∀ {n n1} → (x : A n1 n) → MS' n1 → MS' n
     _::ms_ = _::ms'_
 
-    postulate 
+    postulate  {- HoTT Axiom -}
       Ex : {n1 n2 n2' n3 : I} {x : A n1 n2} {x' : A n1 n2'}
            {y : A n2 n3}
            {y' : A n2' n3}
@@ -48,7 +48,7 @@ module programming.PatchWithHistories2
     MS-ind C c0 c1 c2 []ms' = c0
     MS-ind C c0 c1 c2 (x ::ms' xs) = c1 x xs (MS-ind C c0 c1 c2 xs)
 
-    postulate 
+    postulate  {- HoTT Axiom -}
       MS-ind/βEx : (C : {n : I} → MS n → Type) 
            → (c0 : C []ms)
            → (c1 : {n1 n2 : I} (x : A n1 n2) (xs : _) → C xs → C (x ::ms xs))
@@ -70,7 +70,7 @@ module programming.PatchWithHistories2
 
   open HistoryHIT 
 
-  postulate
+  postulate  {- HoTT Axiom -}
     R : Type
     doc : {n : I} → MS n → R
     add : ∀ {n1 n2} → (x : A n1 n2) (xs : MS n1) → doc xs == doc (x ::ms xs)
diff --git a/programming/PatchWithHistories3.agda b/programming/PatchWithHistories3.agda
index 67ac012..af78711 100644
--- a/programming/PatchWithHistories3.agda
+++ b/programming/PatchWithHistories3.agda
@@ -18,7 +18,7 @@ module programming.PatchWithHistories3 (A : Type) (CanExchange : A → A → Typ
     []ms = []ms'
     _::ms_ = _::ms'_
 
-    postulate 
+    postulate {- HoTT Axiom -}
       Ex : (x y : A) (ce : CanExchange x y) (xs : MS) → (x ::ms (y ::ms xs)) == (y ::ms (x ::ms xs))
 
     MS-ind : (C : MS → Type) 
@@ -29,7 +29,7 @@ module programming.PatchWithHistories3 (A : Type) (CanExchange : A → A → Typ
     MS-ind C c0 c1 c2 []ms' = c0
     MS-ind C c0 c1 c2 (x ::ms' xs) = c1 x xs (MS-ind C c0 c1 c2 xs)
 
-    postulate 
+    postulate  {- HoTT Axiom -}
       MS-ind/βEx : (C : MS → Type) 
                  → (c0 : C []ms)
                  → (c1 : (x : _) (xs : _) → C xs → C (x ::ms xs))
@@ -39,7 +39,7 @@ module programming.PatchWithHistories3 (A : Type) (CanExchange : A → A → Typ
 
   open HistoryHIT 
 
-  postulate
+  postulate  {- HoTT Axiom -}
     R : Type
     doc : MS → R
     add : (x : A) (xs : MS) → doc xs == doc (x ::ms xs)