Path solver

Cubical/Data/List/Properties.agda

@@ -179,3 +179,15 @@ length-map : ∀ {ℓA ℓB} {A : Type ℓA} {B : Type ℓB} → (f : A → B) 
   → length (map f as) ≡ length as
 length-map f [] = refl
 length-map f (a ∷ as) = cong suc (length-map f as)
+
+rot : List A → List A
+rot [] = []
+rot (x ∷ xs) = xs ∷ʳ x
+
+rotN : ℕ → List A → List A
+rotN n = iter n rot
+
+lookupWithDefault : A → List A → ℕ → A
+lookupWithDefault a [] _ = a
+lookupWithDefault _ (x ∷ _) zero = x
+lookupWithDefault a (x ∷ xs) (suc k) = lookupWithDefault a xs k

Cubical/Data/Sigma/Properties.agda

@@ -88,6 +88,14 @@ module _ {A : I → Type ℓ} {B : (i : I) → A i → Type ℓ'}
               ≡ (PathP (λ i → Σ (A i) (B i)) x y)
   ΣPath≡PathΣ = ua ΣPath≃PathΣ
 
+Square× :  {a₀₀ a₀₁ : A × A'} {a₀₋ : a₀₀ ≡ a₀₁}
+           {a₁₀ a₁₁ : A × A'} {a₁₋ : a₁₀ ≡ a₁₁}
+           {a₋₀ : a₀₀ ≡ a₁₀} {a₋₁ : a₀₁ ≡ a₁₁}
+        → Square {A = A} (cong fst a₀₋) (cong fst a₁₋) (cong fst  a₋₀) (cong fst  a₋₁)
+        → Square {A = A' } (cong snd a₀₋) (cong snd a₁₋) (cong snd  a₋₀) (cong snd  a₋₁)
+        → Square {A = A × A'} a₀₋ a₁₋ a₋₀ a₋₁
+Square× s s' i j = s i j , s' i j
+
 ×≡Prop : isProp A' → {u v : A × A'} → u .fst ≡ v .fst → u ≡ v
 ×≡Prop pB {u} {v} p i = (p i) , (pB (u .snd) (v .snd) i)
 

Cubical/Foundations/GroupoidLaws.agda

@@ -78,6 +78,13 @@ rCancel-filler' {x = x} {y} p i j k =
 rCancel' : ∀ {ℓ} {A : Type ℓ} {x y : A} (p : x ≡ y) → p ∙ p ⁻¹ ≡ refl
 rCancel' p j k = rCancel-filler' p i0 j k
 
+midCancel : (p : y ≡ x) (q : z ≡ x) (r : w ≡ x)
+   → (p ∙∙ refl ∙∙ sym q) ∙ (q ∙∙ refl ∙∙ sym r) ≡ (p ∙∙ refl ∙∙ sym r)
+midCancel p q r j =
+     (λ i → p (i ∧ j))
+  ∙∙ doubleCompPath-filler p refl (sym q) (~ j)
+  ∙∙ λ i → hcomp (λ k → λ {(i = i0) → q (~ k ∨ j)  ; (i = i1) → r (~ k) ; (j = i1) → r (~ i ∨ ~ k) }) (r i1)
+
 lCancel : (p : x ≡ y) → p ⁻¹ ∙ p ≡ refl
 lCancel p = rCancel (p ⁻¹)
 

Cubical/Foundations/Path.agda

@@ -437,3 +437,31 @@ Square→compPathΩ² {a = a} sq k i j =
                  ; (j = i1) → a
                  ; (k = i1) → cong (λ x → rUnit x r) (flipSquare sq) i j})
         (sq j i)
+
+module 2-cylinder-from-square
+   {a₀₀ a₀₁ a₁₀ a₁₁ a₀₀' a₀₁' a₁₀' a₁₁' : A }
+   {a₀₋  : a₀₀  ≡ a₀₁ } {a₁₋  : a₁₀  ≡ a₁₁ } {a₋₀  : a₀₀  ≡ a₁₀ } {a₋₁  : a₀₁  ≡ a₁₁ }
+   {a₀₋' : a₀₀' ≡ a₀₁'} {a₁₋' : a₁₀' ≡ a₁₁'} {a₋₀' : a₀₀' ≡ a₁₀'} {a₋₁' : a₀₁' ≡ a₁₁'}
+   (aa'₀₀ : a₀₀ ≡ a₀₀')
+ where
+
+ MissingSquare = (a₁₋ ⁻¹ ∙∙ a₋₀ ⁻¹ ∙∙ aa'₀₀ ∙∙ a₋₀' ∙∙ a₁₋')
+               ≡ (a₋₁ ⁻¹ ∙∙ a₀₋ ⁻¹ ∙∙ aa'₀₀ ∙∙ a₀₋' ∙∙ a₋₁')
+
+ cyl : MissingSquare → ∀ i j → I → Partial (i ∨ ~ i ∨ j ∨ ~ j) A
+
+ cyl c i j k = λ where
+  (i = i0) → doubleCompPath-filler (sym a₀₋) aa'₀₀ a₀₋' j k
+  (i = i1) → doubleCompPath-filler (sym a₁₋) (sym a₋₀ ∙∙ aa'₀₀ ∙∙  a₋₀')  a₁₋' j k
+  (j = i0) → doubleCompPath-filler (sym a₋₀) aa'₀₀ a₋₀' i k
+  (j = i1) → compPathR→PathP∙∙ c (~ i) k
+
+ module _ (s : MissingSquare) where
+  IsoSqSq' : Iso (Square a₀₋ a₁₋ a₋₀ a₋₁) (Square a₀₋' a₁₋' a₋₀' a₋₁')
+  Iso.fun IsoSqSq' x i j = hcomp (cyl s i j) (x i j)
+  Iso.inv IsoSqSq' x i j = hcomp (λ k → cyl s i j (~ k)) (x i j)
+  Iso.rightInv IsoSqSq' x l i j  = hcomp-equivFiller (λ k → cyl s i j (~ k)) (inS (x i j)) (~ l)
+  Iso.leftInv IsoSqSq' x l i j = hcomp-equivFiller (cyl s i j) (inS (x i j)) (~ l)
+
+  Sq≃Sq' : (Square a₀₋ a₁₋ a₋₀ a₋₁) ≃ (Square a₀₋' a₁₋' a₋₀' a₋₁')
+  Sq≃Sq' = isoToEquiv IsoSqSq'

Cubical/Foundations/Prelude.agda

@@ -134,6 +134,15 @@ doubleCompPath-filler : (p : x ≡ y) (q : y ≡ z) (r : z ≡ w)
 doubleCompPath-filler p q r j i =
   hfill (doubleComp-faces p r i) (inS (q i)) j
 
+fill₁₋ : {p : x ≡ y} {q : y ≡ z} {r : z ≡ w} → PathP (λ j → p (~ j) ≡ r j) q (p ∙∙ q ∙∙ r)
+fill₁₋ = doubleCompPath-filler _ _ _
+
+fill₋₁ : {p : x ≡ y} {q : y ≡ z} {r : z ≡ w} → PathP (λ j → q j ≡ (p ∙∙ q ∙∙ r)  j) (sym p) r
+fill₋₁ {p = p} {q} {r} i j =
+  hfill (doubleComp-faces p r i) (inS (q i)) j
+
+
+
 -- any two definitions of double composition are equal
 compPath-unique : (p : x ≡ y) (q : y ≡ z) (r : z ≡ w)
                   → (α β : Σ[ s ∈ x ≡ w ] PathP (λ j → p (~ j) ≡ r j) q s)

Cubical/HITs/S1/Properties.agda

@@ -7,15 +7,24 @@ open import Cubical.Foundations.Equiv
 open import Cubical.Foundations.HLevels
 open import Cubical.Foundations.Isomorphism
 open import Cubical.Foundations.Univalence
+open import Cubical.Foundations.Cubes
+open import Cubical.Foundations.Path
+
+open import Cubical.Data.Sigma
 
 open import Cubical.HITs.S1.Base
 open import Cubical.HITs.PropositionalTruncation as PropTrunc hiding ( rec ; elim )
 
-rec : ∀ {ℓ} {A : Type ℓ} (b : A) (l : b ≡ b) → S¹ → A
+private
+  variable
+    ℓ : Level
+    A : Type ℓ
+
+rec : (b : A) (l : b ≡ b) → S¹ → A
 rec b l base     = b
 rec b l (loop i) = l i
 
-elim : ∀ {ℓ} (C : S¹ → Type ℓ) (b : C base) (l : PathP (λ i → C (loop i)) b b) → (x : S¹) → C x
+elim : (C : S¹ → Type ℓ) (b : C base) (l : PathP (λ i → C (loop i)) b b) → (x : S¹) → C x
 elim _ b l base     = b
 elim _ b l (loop i) = l i
 
@@ -34,9 +43,23 @@ isGroupoidS¹ s t =
           (isConnectedS¹ t)))
     (isConnectedS¹ s)
 
-IsoFunSpaceS¹ : ∀ {ℓ} {A : Type ℓ} → Iso (S¹ → A) (Σ[ x ∈ A ] x ≡ x)
+IsoFunSpaceS¹ : Iso (S¹ → A) (Σ[ x ∈ A ] x ≡ x)
 Iso.fun IsoFunSpaceS¹ f = (f base) , (cong f loop)
 Iso.inv IsoFunSpaceS¹ (x , p) base = x
 Iso.inv IsoFunSpaceS¹ (x , p) (loop i) = p i
 Iso.rightInv IsoFunSpaceS¹ (x , p) = refl
 Iso.leftInv IsoFunSpaceS¹ f = funExt λ {base → refl ; (loop i) → refl}
+
+
+Iso∂Cube2S₁→ : Iso (S¹ → A) (∂Cube 2 A)
+Iso.fun Iso∂Cube2S₁→ x = (_ , cong x loop) , (_ , refl) , refl
+Iso.inv Iso∂Cube2S₁→ ((_ , p) , (_ , q) , r) = rec _
+  (p ∙ (cong snd r ∙' (sym q ∙' sym (cong fst r))))
+Iso.rightInv Iso∂Cube2S₁→ ((_ , p) , (_ , q) , r) =
+ ΣPathP ((ΣPathP (cong₂ _,_ _ _ ,  symP (compPath-filler _ _))) ,
+   ΣPathP (ΣPathP (cong₂ _,_ _ _ , fill₋₁) ,
+    Square× (λ i j → fst (r (i ∧ j))) (congP (λ _ →  symP) fill₋₁)))
+
+Iso.leftInv Iso∂Cube2S₁→ a = funExt (elim _ refl
+  (flipSquare (cong ((cong a loop) ∙_)
+      (λ i → rUnit (lUnit refl (~ i)) (~ i)) ∙ sym (rUnit _))))

Cubical/Tactics/GroupSolver/Example.agda

@@ -0,0 +1,66 @@
+{-# OPTIONS --safe #-}
+
+module Cubical.Tactics.GroupSolver.Example where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.GroupoidLaws
+open import Cubical.Foundations.Path
+open import Cubical.Foundations.Structure
+
+open import Cubical.Tactics.GroupSolver.Groupoid
+
+private
+  variable
+    ℓ ℓ' : Level
+
+module Examples (A : Type ℓ) (x y z w : A) (p p' : x ≡ y) (q : y ≡ z) (q' : z ≡ y) (r : w ≡ z) where
+
+  pA pB pC : x ≡ w
+  pA = (p ∙∙ refl ∙∙ q) ∙ sym r
+  pB = (p ∙ (q ∙ sym (sym r ∙  r) ∙ sym q) ∙∙ q ∙∙ refl) ∙∙ sym r ∙∙ refl
+  pC = refl ∙∙ p' ∙ q ∙ sym q ∙ sym p' ∙∙ p ∙∙ q ∙∙ sym q ∙ q ∙ sym r
+
+  pA=pB : pA ≡ pB
+  pA=pB = solveGroupoidDebug
+
+  pB=pC : pB ≡ pC
+  pB=pC = solveGroupoidDebug
+
+  pA=pC : pA ≡ pC
+  pA=pC = solveGroupoidDebug
+
+  pA=pB∙pB=pC-≡-pA=pC : pA=pB ∙ pB=pC ≡ pA=pC
+  pA=pB∙pB=pC-≡-pA=pC = midCancel _ _ _
+
+
+  sqTest : Square p (sym r ∙ refl) (p ∙ q) (q ∙ sym r)
+  sqTest = solveSquareDebug
+
+module _ {A : Type ℓ} {x y z : A} (p q : x ≡ x) where
+
+ open import Cubical.Foundations.Equiv
+
+ SqCompEquiv : (Square p p q q) ≃ (p ∙ q ≡ q ∙ p)
+ SqCompEquiv = 2-cylinder-from-square.Sq≃Sq' refl solveSquareDebug
+
+
+
+open import Cubical.Algebra.Group
+
+module EM₁-Example (G : Group ℓ) (a b c : fst G) where
+  open GroupStr (snd G)
+
+  data EM₁ : Type ℓ where
+      embase : EM₁
+      emloop : ⟨ G ⟩ → embase ≡ embase
+      emcomp : (g h : ⟨ G ⟩ ) → PathP (λ j → embase ≡ emloop h j) (emloop g) (emloop (g · h))
+
+  double-emcomp :  Square {A = EM₁}
+                    (emloop b) (emloop ((a · b) · c))
+                    (sym (emloop a)) (emloop c)
+
+  double-emcomp =
+    fst (2-cylinder-from-square.Sq≃Sq'
+      (emloop a)
+      solveGroupoidDebug) (emcomp a b ∙v emcomp (a · b) c)
+