A shorter definition of isHAEquiv.com-op

Cubical/Foundations/Equiv/HalfAdjoint.agda

@@ -31,40 +31,29 @@ record isHAEquiv {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} (f : A → B) : Type
     rinv : ∀ b → f (g b) ≡ b
     com : ∀ a → cong f (linv a) ≡ rinv (f a)
 
-  -- from redtt's ha-equiv/symm
   com-op : ∀ b → cong g (rinv b) ≡ linv (g b)
-  com-op b j i = hcomp (λ k → λ { (i = i0) → linv (g b) (j ∧ (~ k))
-                                ; (j = i0) → g (rinv b i)
-                                ; (j = i1) → linv (g b) (i ∨ (~ k))
-                                ; (i = i1) → g b })
-                       (cap1 j i)
-
-    where cap0 : Square {- (j = i0) -} (λ i → f (g (rinv b i)))
-                        {- (j = i1) -} (λ i → rinv b i)
-                        {- (i = i0) -} (λ j → f (linv (g b) j))
-                        {- (i = i1) -} (λ j → rinv b j)
-
-          cap0 j i = hcomp (λ k → λ { (i = i0) → com (g b) (~ k) j
-                                    ; (j = i0) → f (g (rinv b i))
-                                    ; (j = i1) → rinv b i
-                                    ; (i = i1) → rinv b j })
-                           (rinv (rinv b i) j)
-
-          filler : I → I → A
-          filler j i = hfill (λ k → λ { (i = i0) → g (rinv b k)
-                                      ; (i = i1) → g b })
-                             (inS (linv (g b) i)) j
-
-          cap1 : Square {- (j = i0) -} (λ i → g (rinv b i))
-                        {- (j = i1) -} (λ i → g b)
-                        {- (i = i0) -} (λ j → linv (g b) j)
-                        {- (i = i1) -} (λ j → g b)
-
-          cap1 j i = hcomp (λ k → λ { (i = i0) → linv (linv (g b) j) k
-                                    ; (j = i0) → linv (g (rinv b i)) k
-                                    ; (j = i1) → filler i k
-                                    ; (i = i1) → filler j k })
-                           (g (cap0 j i))
+  com-op b i j = hcomp (λ k → λ { (i = i0) → g (rinv (rinv b k) j)
+                                ; (i = i1) → cap j k
+                                ; (j = i0) → g (f (g (rinv b k)))
+                                ; (j = i1) → g (rinv b k) })
+                       (g (com (g b) (~ i) j))
+
+    where
+    filler : I → I → A
+    filler j k = hfill (λ i → λ { (k = i0) → linv (g b) i
+                                ; (k = i1) → g b })
+                       (inS (g (rinv b k))) j
+
+    cap : Square {- (j = i0) -} (λ k → g (f (g (rinv b k))))
+                 {- (j = i1) -} (λ k → g (rinv b k))
+                 {- (k = i0) -} (λ j → g (f (linv (g b) j)))
+                 {- (k = i1) -} (λ j → linv (g b) j)
+
+    cap j k = hcomp (λ i → λ { (j = i0) → linv (g (rinv b k)) (~ i)
+                             ; (j = i1) → filler (~ i) k
+                             ; (k = i0) → linv (linv (g b) j) (~ i)
+                             ; (k = i1) → linv (g b) (j ∨ ~ i) })
+                    (filler j k)
 
   isHAEquiv→Iso : Iso A B
   Iso.fun isHAEquiv→Iso = f