Normal form of FreeGroup (#1099)

* nomral form of freegroup and Group solver tactic

* some cleanup

* group solver specialised to paths (aware of double-path-composition)

* fixed name conflict

* start with boilerplate

* functor notation

* free cats

* write down a candidate def for free wild cat

* notes

* wip on grupoidSolver

* removed solvers

* removed solvers

* added brief description of module

* tweaking comments

---------

Co-authored-by: Felix Cherubini <felix.cherubini@posteo.de>

Cubical/Data/List/Base.agda

@@ -3,8 +3,8 @@ module Cubical.Data.List.Base where
 
 open import Agda.Builtin.List public
 open import Cubical.Core.Everything
-open import Cubical.Data.Maybe.Base as Maybe
-open import Cubical.Data.Nat.Base
+open import Cubical.Data.Maybe.Base as Maybe hiding (rec ; elim)
+open import Cubical.Data.Nat.Base hiding (elim)
 
 module _ {ℓ} {A : Type ℓ} where
 
@@ -50,3 +50,27 @@ module _ {ℓ} {A : Type ℓ} where
   foldl : ∀ {ℓ'} {B : Type ℓ'} → (B → A → B) → B → List A → B
   foldl f b [] = b
   foldl f b (x ∷ xs) = foldl f (f b x) xs
+
+  drop : ℕ → List A → List A
+  drop zero xs = xs
+  drop (suc n) [] = []
+  drop (suc n) (x ∷ xs) = drop n xs
+
+  take : ℕ → List A → List A
+  take zero xs = []
+  take (suc n) [] = []
+  take (suc n) (x ∷ xs) = x ∷ take n xs
+
+  elim : ∀ {ℓ'} {B : List A → Type ℓ'}
+           → B []
+           → (∀ {a l} → B l → B (a ∷ l))
+           → ∀ l → B l
+  elim b _ [] = b
+  elim {B = B} b[] b (a ∷ l) = b (elim {B = B} b[] b l )
+
+  rec : ∀ {ℓ'} {B : Type ℓ'}
+           → B
+           → (A → B → B)
+           → List A → B
+  rec b _ [] = b
+  rec b f (x ∷ xs) = f x (rec b f xs)

Cubical/Data/List/Properties.agda

@@ -6,13 +6,16 @@ open import Cubical.Core.Everything
 open import Cubical.Foundations.GroupoidLaws
 open import Cubical.Foundations.HLevels
 open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Function
+open import Cubical.Foundations.Isomorphism
 open import Cubical.Data.Empty as ⊥
 open import Cubical.Data.Nat
 open import Cubical.Data.Sigma
+open import Cubical.Data.Sum as ⊎ hiding (map)
 open import Cubical.Data.Unit
 open import Cubical.Relation.Nullary
 
-open import Cubical.Data.List.Base
+open import Cubical.Data.List.Base as List
 
 module _ {ℓ} {A : Type ℓ} where
 
@@ -117,8 +120,11 @@ isOfHLevelList n ofLevel xs ys =
 
 private
   variable
-    ℓ : Level
+    ℓ ℓ' : Level
     A : Type ℓ
+    B : Type ℓ'
+    x y : A
+    xs ys : List A
 
   caseList : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} → (n c : B) → List A → B
   caseList n _ []      = n
@@ -132,23 +138,32 @@ private
   safe-tail []       = []
   safe-tail (_ ∷ xs) = xs
 
-cons-inj₁ : ∀ {x y : A} {xs ys} → x ∷ xs ≡ y ∷ ys → x ≡ y
+cons-inj₁ : x ∷ xs ≡ y ∷ ys → x ≡ y
 cons-inj₁ {x = x} p = cong (safe-head x) p
 
-cons-inj₂ : ∀ {x y : A} {xs ys} → x ∷ xs ≡ y ∷ ys → xs ≡ ys
+cons-inj₂ : x ∷ xs ≡ y ∷ ys → xs ≡ ys
 cons-inj₂ = cong safe-tail
 
-¬cons≡nil : ∀ {x : A} {xs} → ¬ (x ∷ xs ≡ [])
-¬cons≡nil {A = A} p = lower (subst (caseList (Lift ⊥) (List A)) p [])
+snoc-inj₂ : xs ∷ʳ x ≡ ys ∷ʳ y → x ≡ y
+snoc-inj₂ {xs = xs} {ys = ys} p =
+ cons-inj₁ ((sym (rev-++ xs _)) ∙∙ cong rev p ∙∙ (rev-++ ys _))
 
-¬nil≡cons : ∀ {x : A} {xs} → ¬ ([] ≡ x ∷ xs)
-¬nil≡cons {A = A} p = lower (subst (caseList (List A) (Lift ⊥)) p [])
+snoc-inj₁ : xs ∷ʳ x ≡ ys ∷ʳ y → xs ≡ ys
+snoc-inj₁ {xs = xs} {ys = ys} p =
+   sym (rev-rev _) ∙∙ cong rev (cons-inj₂ ((sym (rev-++ xs _)) ∙∙ cong rev p ∙∙ (rev-++ ys _)))
+        ∙∙ rev-rev _
 
-¬snoc≡nil : ∀ {x : A} {xs} → ¬ (xs ∷ʳ x ≡ [])
+¬cons≡nil : ¬ (x ∷ xs ≡ [])
+¬cons≡nil {_} {A} p = lower (subst (caseList (Lift ⊥) (List A)) p [])
+
+¬nil≡cons : ¬ ([] ≡ x ∷ xs)
+¬nil≡cons {_} {A} p = lower (subst (caseList (List A) (Lift ⊥)) p [])
+
+¬snoc≡nil : ¬ (xs ∷ʳ x ≡ [])
 ¬snoc≡nil {xs = []} contra = ¬cons≡nil contra
 ¬snoc≡nil {xs = x ∷ xs} contra = ¬cons≡nil contra
 
-¬nil≡snoc : ∀ {x : A} {xs} → ¬ ([] ≡ xs ∷ʳ x)
+¬nil≡snoc : ¬ ([] ≡ xs ∷ʳ x)
 ¬nil≡snoc contra = ¬snoc≡nil (sym contra)
 
 cons≡rev-snoc : (x : A) → (xs : List A) → x ∷ rev xs ≡ rev (xs ∷ʳ x)
@@ -158,7 +173,7 @@ cons≡rev-snoc x (y ∷ ys) = λ i → cons≡rev-snoc x ys i ++ y ∷ []
 isContr[]≡[] : isContr (Path (List A) [] [])
 isContr[]≡[] = refl , ListPath.decodeEncode [] []
 
-isPropXs≡[] : {xs : List A} → isProp (xs ≡ [])
+isPropXs≡[] : isProp (xs ≡ [])
 isPropXs≡[] {xs = []} = isOfHLevelSuc 0 isContr[]≡[]
 isPropXs≡[] {xs = x ∷ xs} = λ p _ → ⊥.rec (¬cons≡nil p)
 
@@ -175,7 +190,161 @@ foldrCons : (xs : List A) → foldr _∷_ [] xs ≡ xs
 foldrCons [] = refl
 foldrCons (x ∷ xs) = cong (x ∷_) (foldrCons xs)
 
-length-map : ∀ {ℓA ℓB} {A : Type ℓA} {B : Type ℓB} → (f : A → B) → (as : List A)
+length-map : (f : A → B) → (as : List A)
   → length (map f as) ≡ length as
 length-map f [] = refl
 length-map f (a ∷ as) = cong suc (length-map f as)
+
+map++ : (f : A → B) → (as bs : List A)
+   → map f as ++ map f bs ≡ map f (as ++ bs)
+map++ f [] bs = refl
+map++ f (x ∷ as) bs = cong (f x ∷_) (map++ f as bs)
+
+rev-map-comm : (f : A → B) → (as : List A)
+  → map f (rev as) ≡ rev (map f as)
+rev-map-comm f [] = refl
+rev-map-comm f (x ∷ as) =
+ sym (map++ f (rev as) _) ∙ cong (_++ [ f x ]) (rev-map-comm f as)
+
+length++ : (xs ys : List A) → length (xs ++ ys) ≡ length xs + length ys
+length++ [] ys = refl
+length++ (x ∷ xs) ys = cong suc (length++ xs ys)
+
+drop++ : ∀ (xs ys : List A) k →
+   drop (length xs + k) (xs ++ ys) ≡ drop k ys
+drop++ [] ys k = refl
+drop++ (x ∷ xs) ys k = drop++ xs ys k
+
+dropLength++ : (xs : List A) → drop (length xs) (xs ++ ys) ≡ ys
+dropLength++ {ys = ys} xs =
+  cong (flip drop (xs ++ ys)) (sym (+-zero (length xs))) ∙ drop++ xs ys 0
+
+
+dropLength : (xs : List A) → drop (length xs) xs ≡ []
+dropLength xs =
+    cong (drop (length xs)) (sym (++-unit-r xs))
+  ∙ dropLength++ xs
+
+
+take++ : ∀ (xs ys : List A) k → take (length xs + k) (xs ++ ys) ≡ xs ++ take k ys
+take++ [] ys k = refl
+take++ (x ∷ xs) ys k = cong (_ ∷_) (take++ _ _ k)
+
+
+takeLength++ : ∀ ys → take (length xs) (xs ++ ys) ≡ xs
+takeLength++ {xs = xs} ys =
+      cong (flip take (xs ++ ys)) (sym (+-zero (length xs)))
+   ∙∙ take++ xs ys 0
+   ∙∙ ++-unit-r xs
+
+takeLength : take (length xs) xs ≡ xs
+takeLength = cong (take _) (sym (++-unit-r _)) ∙ takeLength++ []
+
+map-∘ : ∀ {ℓA ℓB ℓC} {A : Type ℓA} {B : Type ℓB} {C : Type ℓC}
+        (g : B → C) (f : A → B) (as : List A)
+        → map g (map f as) ≡ map (λ x → g (f x)) as
+map-∘ g f [] = refl
+map-∘ g f (x ∷ as) = cong (_ ∷_) (map-∘ g f as)
+
+map-id : (as : List A) → map (λ x → x) as ≡ as
+map-id [] = refl
+map-id (x ∷ as) = cong (_ ∷_) (map-id as)
+
+length≡0→≡[] : ∀ (xs : List A) → length xs ≡ 0 → xs ≡ []
+length≡0→≡[] [] x = refl
+length≡0→≡[] (x₁ ∷ xs) x = ⊥.rec (snotz x)
+
+init : List A → List A
+init [] = []
+init (x ∷ []) = []
+init (x ∷ xs@(_ ∷ _)) = x ∷ init xs
+
+tail : List A → List A
+tail [] = []
+tail (x ∷ xs) = xs
+
+init-red-lem : ∀ (x : A) xs → ¬ (xs ≡ []) → (x ∷ init xs) ≡ (init (x ∷ xs))
+init-red-lem x [] x₁ = ⊥.rec (x₁ refl)
+init-red-lem x (x₂ ∷ xs) x₁ = refl
+
+init∷ʳ : init (xs ∷ʳ x) ≡ xs
+init∷ʳ {xs = []} = refl
+init∷ʳ {xs = _ ∷ []} = refl
+init∷ʳ {xs = _ ∷ _ ∷ _} = cong (_ ∷_) init∷ʳ
+
+tail∷ʳ : tail (xs ∷ʳ y) ∷ʳ x ≡ tail (xs ∷ʳ y ∷ʳ x)
+tail∷ʳ {xs = []} = refl
+tail∷ʳ {xs = x ∷ xs} = refl
+
+init-rev-tail : rev (init xs) ≡ tail (rev xs)
+init-rev-tail {xs = []} = refl
+init-rev-tail {xs = x ∷ []} = refl
+init-rev-tail {xs = x ∷ y ∷ xs} =
+   cong (_∷ʳ x) (init-rev-tail {xs = y ∷ xs})
+ ∙ tail∷ʳ {xs = rev xs}
+
+init++ : ∀ xs → xs ++ init (x ∷ ys) ≡ init (xs ++ x ∷ ys)
+init++ [] = refl
+init++ (_ ∷ []) = refl
+init++ (_ ∷ _ ∷ _) = cong (_ ∷_) (init++ (_ ∷ _))
+
+Split++ : (xs ys xs' ys' zs : List A) → Type _
+Split++ xs ys xs' ys' zs = ((xs ++ zs ≡ xs') × (ys ≡ zs ++ ys'))
+
+split++ : ∀ (xs' ys' xs ys : List A) → xs' ++ ys' ≡ xs ++ ys →
+              Σ _ λ zs →
+                ((Split++ xs' ys' xs ys zs)
+                ⊎ (Split++ xs ys xs' ys' zs))
+split++ [] ys' xs ys x = xs , inl (refl , x)
+split++ xs'@(_ ∷ _) ys' [] ys x = xs' , inr (refl , sym x)
+split++ (x₁ ∷ xs') ys' (x₂ ∷ xs) ys x =
+ let (zs , q) = split++ xs' ys' xs ys (cons-inj₂ x)
+     p = cons-inj₁ x
+ in zs , ⊎.map (map-fst (λ q i → p    i  ∷ q i))
+               (map-fst (λ q i → p (~ i) ∷ q i)) q
+
+rot : List A → List A
+rot [] = []
+rot (x ∷ xs) = xs ∷ʳ x
+
+take[] : ∀ n → take {A = A} n [] ≡ []
+take[] zero = refl
+take[] (suc n) = refl
+
+drop[] : ∀ n → drop {A = A} n [] ≡ []
+drop[] zero = refl
+drop[] (suc n) = refl
+
+lookupAlways : A → List A → ℕ → A
+lookupAlways a [] _ = a
+lookupAlways _ (x ∷ _) zero = x
+lookupAlways a (x ∷ xs) (suc k) = lookupAlways a xs k
+
+module List₂ where
+ open import Cubical.HITs.SetTruncation renaming
+   (rec to rec₂ ; map to map₂ ; elim to elim₂ )
+
+ ∥List∥₂→List∥∥₂ : ∥ List A ∥₂ → List ∥ A ∥₂
+ ∥List∥₂→List∥∥₂ = rec₂ (isOfHLevelList 0 squash₂) (map ∣_∣₂)
+
+ List∥∥₂→∥List∥₂ : List ∥ A ∥₂ → ∥ List A ∥₂
+ List∥∥₂→∥List∥₂ [] = ∣ [] ∣₂
+ List∥∥₂→∥List∥₂ (x ∷ xs) =
+   rec2 squash₂ (λ x xs → ∣ x ∷ xs ∣₂) x (List∥∥₂→∥List∥₂ xs)
+
+ Iso∥List∥₂List∥∥₂ : Iso (List ∥ A ∥₂) ∥ List A ∥₂
+ Iso.fun Iso∥List∥₂List∥∥₂ = List∥∥₂→∥List∥₂
+ Iso.inv Iso∥List∥₂List∥∥₂ = ∥List∥₂→List∥∥₂
+ Iso.rightInv Iso∥List∥₂List∥∥₂ =
+   elim₂ (isProp→isSet ∘ λ _ → squash₂ _ _)
+     (List.elim refl (cong (rec2 squash₂ (λ x₁ xs → ∣ x₁ ∷ xs ∣₂) ∣ _ ∣₂)))
+ Iso.leftInv Iso∥List∥₂List∥∥₂ = List.elim refl ((lem _ _ ∙_) ∘S cong (_ ∷_))
+  where
+  lem = elim2 {C = λ a l' → ∥List∥₂→List∥∥₂
+      (rec2 squash₂ (λ x₁ xs → ∣ x₁ ∷ xs ∣₂) a l')
+      ≡ a ∷ ∥List∥₂→List∥∥₂ l'}
+       (λ _ _ → isProp→isSet (isOfHLevelList 0 squash₂ _ _))
+        λ _ _ → refl
+
+ List-comm-∥∥₂ : ∀ {ℓ} → List {ℓ} ∘ ∥_∥₂ ≡ ∥_∥₂ ∘ List
+ List-comm-∥∥₂ = funExt λ A → isoToPath (Iso∥List∥₂List∥∥₂ {A = A})

Cubical/Data/Nat/Properties.agda

@@ -173,6 +173,12 @@ m+n≡0→m≡0×n≡0 : m + n ≡ 0 → (m ≡ 0) × (n ≡ 0)
 m+n≡0→m≡0×n≡0 {zero} = refl ,_
 m+n≡0→m≡0×n≡0 {suc m} p = ⊥.rec (snotz p)
 
+m+n≡1→m≡0×n≡1⊎m≡1n≡0 : m + n ≡ 1 → ((m ≡ 0) × (n ≡ 1)) ⊎ ((m ≡ 1) × (n ≡ 0))
+m+n≡1→m≡0×n≡1⊎m≡1n≡0 {zero} x = inl (refl , x)
+m+n≡1→m≡0×n≡1⊎m≡1n≡0 {suc m} {n} x =
+ let (m≡0 , n≡0) = m+n≡0→m≡0×n≡0 (injSuc x)
+ in inr (cong suc m≡0 , n≡0 )
+
 -- Arithmetic facts about ·
 
 0≡m·0 : ∀ m → 0 ≡ m · 0

Cubical/Data/Sigma/Properties.agda

@@ -378,6 +378,10 @@ snd (ΣPathPProp {B = B} {u = u} {v = v} pB p i) = lem i
   lem : PathP (λ i → B i (p i)) (snd u) (snd v)
   lem = toPathP (pB _ _ _)
 
+discreteΣProp : Discrete A → ((x : A) → isProp (B x)) → Discrete (Σ A B)
+discreteΣProp _≟_ isPropA _ _ =
+  EquivPresDec (Σ≡PropEquiv isPropA) (_ ≟ _)
+
 ≃-× : ∀ {ℓ'' ℓ'''} {A : Type ℓ} {B : Type ℓ'} {C : Type ℓ''} {D : Type ℓ'''} → A ≃ C → B ≃ D → A × B ≃ C × D
 ≃-× eq1 eq2 =
     map-× (fst eq1) (fst eq2)

Cubical/Foundations/Function.agda

@@ -9,7 +9,7 @@ open import Cubical.Foundations.Prelude
 private
   variable
     ℓ ℓ' ℓ'' : Level
-    A : Type ℓ
+    A A' A'' : Type ℓ
     B : A → Type ℓ
     C : (a : A) → B a → Type ℓ
     D : (a : A) (b : B a) → C a b → Type ℓ
@@ -26,12 +26,16 @@ _$_ : ∀ {ℓ ℓ'} {A : Type ℓ} {B : A → Type ℓ'} → ((a : A) → B a)
 f $ a = f a
 {-# INLINE _$_ #-}
 
-infixr 9 _∘_
+infixr 9 _∘_ _∘S_
 
 _∘_ : (g : {a : A} → (b : B a) → C a b) → (f : (a : A) → B a) → (a : A) → C a (f a)
 g ∘ f = λ x → g (f x)
 {-# INLINE _∘_ #-}
 
+_∘S_ : (A' → A'') → (A → A') → A → A''
+g ∘S f = λ x → g (f x)
+{-# INLINE _∘S_ #-}
+
 ∘-assoc : (h : {a : A} {b : B a} → (c : C a b) → D a b c)
           (g : {a : A} → (b : B a) → C a b)
           (f : (a : A) → B a)

Cubical/Foundations/Univalence.agda

@@ -69,6 +69,13 @@ module _ {A B : Type ℓ} (e : A ≃ B) {x : A} {y : B} where
   unquoteDef ua-ungluePath-Equiv =
     defStrictEquiv ua-ungluePath-Equiv ua-ungluePath ua-gluePath
 
+ua-ungluePathExt : {A B : Type ℓ} (e : A ≃ B) → PathP (λ i → ua e i → B) (fst e) (idfun B)
+ua-ungluePathExt e i = ua-unglue e i
+
+ua-gluePathExt : {A B : Type ℓ} (e : A ≃ B) → PathP (λ i → A → ua e i) (idfun _) (fst e)
+ua-gluePathExt e i x =
+  ua-glue e i (λ { (i = i0) → x }) (inS (fst e x))
+
 -- ua-unglue and ua-glue are also definitional inverses, in a way
 -- strengthening the types of ua-unglue and ua-glue gives a nicer formulation of this, see below
 
@@ -137,6 +144,14 @@ unglueEquiv : ∀ (A : Type ℓ) (φ : I)
               (Glue A f) ≃ A
 unglueEquiv A φ f = ( unglue φ , unglueIsEquiv A φ f )
 
+ua-unglueEquiv : ∀ {A B : Type ℓ} (e : A ≃ B) →
+                    PathP (λ i → ua e i ≃ B)
+                       e
+                       (idEquiv _)
+fst (ua-unglueEquiv e i) = ua-unglue e i
+snd (ua-unglueEquiv e i) =
+  isProp→PathP (λ i → isPropIsEquiv (ua-unglue e i))
+   (snd e) (idIsEquiv _) i
 
 -- The following is a formulation of univalence proposed by Martín Escardó:
 -- https://groups.google.com/forum/#!msg/homotopytypetheory/HfCB_b-PNEU/Ibb48LvUMeUJ
@@ -194,6 +209,9 @@ pathToEquivRefl {A = A} = equivEq (λ i x → transp (λ _ → A) i x)
 uaβ : {A B : Type ℓ} (e : A ≃ B) (x : A) → transport (ua e) x ≡ equivFun e x
 uaβ e x = transportRefl (equivFun e x)
 
+~uaβ : {A B : Type ℓ} (e : A ≃ B) (x : B) → transport (sym (ua e)) x ≡ invEq e x
+~uaβ e x = cong (invEq e) (transportRefl x)
+
 uaη : ∀ {A B : Type ℓ} → (P : A ≡ B) → ua (pathToEquiv P) ≡ P
 uaη {A = A} {B = B} P i j = Glue B {φ = φ} sides where
   -- Adapted from a proof by @dolio, cf. commit e42a6fa1