shorten line length

Author: anshwad10

Cubical/Algebra/Heap/Properties.agda

@@ -33,7 +33,11 @@ module _ (G : Group ℓ) where
   GroupHasHeapStr : HeapStr ⟨ G ⟩
   GroupHasHeapStr .[_,_,_] a b c = a · inv b · c
   GroupHasHeapStr .isHeap .is-set = G-is-set
-  GroupHasHeapStr .isHeap .assoc a b c d e = ·Assoc a (inv b) (c · inv d · e) ∙∙  ·Assoc (a · inv b) c (inv d · e)  ∙∙ congL _·_ (sym (·Assoc a (inv b) c))
+  GroupHasHeapStr .isHeap .assoc a b c d e =
+    a · inv b · c · inv d · e     ≡⟨ ·Assoc a (inv b) (c · inv d · e) ⟩
+    (a · inv b) · c · inv d · e   ≡⟨ ·Assoc (a · inv b) c (inv d · e) ⟩
+    ((a · inv b) · c) · inv d · e ≡⟨ congL _·_ (sym (·Assoc a (inv b) c)) ⟩
+    (a · inv b · c) · inv d · e   ∎
   GroupHasHeapStr .isHeap .idl a b = ·GroupAutomorphismL G a .Iso.rightInv b
   GroupHasHeapStr .isHeap .idr a b = congR _·_ (·InvL b) ∙ ·IdR a
   GroupHasHeapStr .isHeap .inhab = ∣ 1g ∣₁
@@ -56,10 +60,12 @@ module HeapTheory (H : Heap ℓ) where
   -- Wagner's theory of generalized heaps, theorem 8.2.13
   assocl : ∀ a b c d e → [ a , [ d , c , b ] , e ] ≡ [ [ a , b , c ] , d , e ]
   assocl a b c d e =
-    [ a , [ d , c , b ] , e ]                                     ≡⟨ cong [_, [ d , c , b ] , e ] (sym (wriggle a b c d)) ⟩
-    [ [ [ a , b , c ] , d , [ d , c , b ] ] , [ d , c , b ] , e ] ≡⟨ sym (assoc [ a , b , c ] d [ d , c , b ] [ d , c , b ] e) ⟩
-    [ [ a , b , c ] , d , [ [ d , c , b ] , [ d , c , b ] , e ] ] ≡⟨ cong [ [ a , b , c ] , d ,_] (idl [ d , c , b ] e) ⟩
-    [ [ a , b , c ] , d , e ]                                     ∎
+    [ a , [ d , c , b ] , e ] ≡⟨ cong [_, [ d , c , b ] , e ] (sym (wriggle a b c d)) ⟩
+    [ [ [ a , b , c ] , d , [ d , c , b ] ] , [ d , c , b ] , e ]
+                              ≡⟨ sym (assoc [ a , b , c ] d [ d , c , b ] [ d , c , b ] e) ⟩
+    [ [ a , b , c ] , d , [ [ d , c , b ] , [ d , c , b ] , e ] ]
+                              ≡⟨ cong [ [ a , b , c ] , d ,_] (idl [ d , c , b ] e) ⟩
+    [ [ a , b , c ] , d , e ] ∎
 
   assocr : ∀ a b c d e → [ a , [ d , c , b ] , e ] ≡ [ a , b , [ c , d , e ] ]
   assocr a b c d e =
@@ -75,7 +81,8 @@ module HeapTheory (H : Heap ℓ) where
     c                         ∎
 
 StructureGroup : Heap ℓ → Group ℓ
-StructureGroup H = toldYaSo inhab module StructureGroup where
+StructureGroup H = go inhab
+  module StructureGroup where
   open GroupStr hiding (is-set)
   open HeapTheory H
 
@@ -86,7 +93,7 @@ StructureGroup H = toldYaSo inhab module StructureGroup where
   fromPoint e .snd .inv a = [ e , a , e ]
   fromPoint e .snd .isGroup = makeIsGroup is-set
     (λ x y z → assoc x e y e z)
-    (λ x → idr x e) -- is that a maybeJosiah reference
+    (λ x → idr x e)
     (λ x → idl e x)
     (λ x → assoc x e e x e ∙∙ cong [_, x , e ] (idr x e) ∙∙ idl x e)
     (λ x → sym (assoc e x e e x) ∙∙ cong [ e , x ,_] (idl e x) ∙∙ idr e x)
@@ -95,7 +102,7 @@ StructureGroup H = toldYaSo inhab module StructureGroup where
   φ e e' .fst x = [ e' , e , x ]
   φ e e' .snd = makeIsGroupHom λ x y →
     [ e' , e , [ x , e , y ] ]               ≡⟨ assoc e' e x e y ⟩
-    [ [ e' , e , x ] , e , y ]               ≡⟨ cong [ [ e' , e , x ] ,_, y ] (sym (idr e e')) ⟩
+    [ [ e' , e , x ] , e , y ]               ≡⟨ congR [_,_, y ] (sym (idr e e')) ⟩
     [ [ e' , e , x ] , [ e , e' , e' ] , y ] ≡⟨ assocr [ e' , e , x ] e' e' e y ⟩
     [ [ e' , e , x ] , e' , [ e' , e , y ] ] ∎
 
@@ -111,15 +118,24 @@ StructureGroup H = toldYaSo inhab module StructureGroup where
     lemma : ∀ e e' x → φ e e' .fst (φ e' e .fst x) ≡ x
     lemma e e' x = φ-coh e' e e' x ∙ idl e' x
 
-  toldYaSo : ∥ ⟨ H ⟩ ∥₁ → Group _
-  toldYaSo = PropTrunc→Group fromPoint (λ e e' → (φ e e' .fst , φ-eqv e e') , φ e e' .snd) φ-coh
+  go : ∥ ⟨ H ⟩ ∥₁ → Group _
+  go = PropTrunc→Group fromPoint (λ e e' → (φ e e' .fst , φ-eqv e e') , φ e e' .snd) φ-coh
 
 StructureGroupOfGroupHeap : (G : Group ℓ) → GroupEquiv (StructureGroup (GroupHeap G)) G
-StructureGroupOfGroupHeap G = idEquiv _ , makeIsGroupHom λ x y → congR _·_ $ congL _·_ inv1g ∙ ·IdL y
-  where open GroupStr (G .snd); open GroupTheory G
-
-GroupHeapOfStructureGroup : (H : Heap ℓ) → ∥ HeapEquiv (GroupHeap (StructureGroup H)) H ∥₁ -- unnatural isomorphism
-GroupHeapOfStructureGroup H = go inhab module GroupHeapOfStructureGroup where
+StructureGroupOfGroupHeap G = idEquiv _ , makeIsGroupHom λ x y →
+  [ x , 1g , y ] ≡⟨⟩
+  x · inv 1g · y ≡⟨ congR _·_ (congL _·_ inv1g) ⟩
+  x · 1g · y     ≡⟨ congR _·_ (·IdL y) ⟩
+  x · y          ∎
+  where
+    open GroupStr (G .snd)
+    open GroupTheory G
+    open HeapTheory (GroupHeap G)
+
+GroupHeapOfStructureGroup : (H : Heap ℓ)
+                          → ∥ HeapEquiv (GroupHeap (StructureGroup H)) H ∥₁ -- unnatural isomorphism
+GroupHeapOfStructureGroup H = go inhab
+  module GroupHeapOfStructureGroup where
   open HeapTheory H
 
   fromPoint : (e : ⟨ H ⟩) → HeapEquiv (GroupHeap (StructureGroup.fromPoint H e)) H
@@ -130,13 +146,14 @@ GroupHeapOfStructureGroup H = go inhab module GroupHeapOfStructureGroup where
     [ [ a , e , e ] , b , c ]             ≡⟨ cong [_, b , c ] (idr a e) ⟩
     [ a , b , c ]                         ∎
 
-  go : (p : ∥ ⟨ H ⟩ ∥₁) → ∥ HeapEquiv (GroupHeap (StructureGroup.toldYaSo H p)) H ∥₁
+  go : (p : ∥ ⟨ H ⟩ ∥₁) → ∥ HeapEquiv (GroupHeap (StructureGroup.go H p)) H ∥₁
   go = PT.elim (λ _ → isPropPropTrunc) λ e → ∣ fromPoint e ∣₁
 
 PointedHeap : ∀ ℓ → Type (ℓ-suc ℓ)
 PointedHeap ℓ = Σ[ H ∈ Heap ℓ ] ⟨ H ⟩
 
-PointedHeap≡ : {(H , e) (H' , e') : PointedHeap ℓ} (eqv : HeapEquiv H H') (p : eqv .fst .fst e ≡ e') → (H , e) ≡ (H' , e')
+PointedHeap≡ : {(H , e) (H' , e') : PointedHeap ℓ} (eqv : HeapEquiv H H') (p : eqv .fst .fst e ≡ e')
+             → (H , e) ≡ (H' , e')
 PointedHeap≡ eqv p = cong₂ _,_ (uaHeap eqv) (ua-gluePath _ p)
 
 GroupsArePointedHeaps : Group ℓ ≃ PointedHeap ℓ