Clean up Cohomology Ring

Cubical/Algebra/DirectSum/DirectSumHIT/Properties.agda

@@ -71,15 +71,20 @@ module SubstLemma
 
   open AbGroupStr
 
-  subst0g : {l k : Idx} → (p : l ≡ k) → subst G p (0g (Gstr l)) ≡ 0g (Gstr k)
-  subst0g {l} {k} p = J (λ k p → subst G p (0g (Gstr l)) ≡ 0g (Gstr k)) (transportRefl _) p
+  substG : {k l : Idx} → (x : k ≡ l) → (a : G k) → G l
+  substG x a = subst G x a
 
-  subst+ : {l : Idx} → (a b : G l) → {k : Idx} →  (p : l ≡ k) →
-           Gstr k ._+_ (subst G p a) (subst G p b) ≡ subst G p (Gstr l ._+_ a b)
-  subst+ {l} a b {k} p = J (λ k p → Gstr k ._+_ (subst G p a) (subst G p b) ≡ subst G p (Gstr l ._+_ a b))
-                         (cong₂ (Gstr l ._+_) (transportRefl _) (transportRefl _) ∙ sym (transportRefl _))
+  substG0 : {k l : Idx} → (p : k ≡ l) → subst G p (0g (Gstr k)) ≡ 0g (Gstr l)
+  substG0 {k} {l} p = J (λ l p → subst G p (0g (Gstr k)) ≡ 0g (Gstr l)) (transportRefl _) p
+
+  substG+ : {k : Idx} → (a b : G k) → {l : Idx} →  (p : k ≡ l) →
+           Gstr l ._+_ (subst G p a) (subst G p b) ≡ subst G p (Gstr k ._+_ a b)
+  substG+ {k} a b {l} p = J (λ l p → Gstr l ._+_ (subst G p a) (subst G p b) ≡ subst G p (Gstr k ._+_ a b))
+                         (cong₂ (Gstr k ._+_) (transportRefl _) (transportRefl _) ∙ sym (transportRefl _))
                          p
 
+
+
 module DecIndec-BaseProperties
   (Idx  : Type ℓ)
   (decIdx : Discrete Idx)
@@ -108,12 +113,12 @@ module DecIndec-BaseProperties
 
      base-neutral-eq : _
      base-neutral-eq l with decIdx l k
-     ... | yes p = subst0g p
+     ... | yes p = substG0 p
      ... | no ¬p = refl
 
      base-add-eq : _
      base-add-eq l a b with decIdx l k
-     ... | yes p = subst+ a b p
+     ... | yes p = substG+ a b p
      ... | no ¬p = +IdR (Gstr k) _
 
   πₖ-id : {k : Idx} → (a : G k) → πₖ k (base k a) ≡ a

Cubical/Algebra/DirectSum/Equiv-DSHIT-DSFun.agda

@@ -99,8 +99,8 @@ module Equiv-Properties
 
   open SubstLemma ℕ G Gstr
 
-  substG : (g : (n : ℕ) → G n) → {k n : ℕ} → (p : k ≡ n) → subst G p (g k) ≡ g n
-  substG g {k} {n} p = J (λ n p → subst G p (g k) ≡ g n) (transportRefl _) p
+  substG-fct : (g : (n : ℕ) → G n) → {k n : ℕ} → (p : k ≡ n) → subst G p (g k) ≡ g n
+  substG-fct g {k} {n} p = J (λ n p → subst G p (g k) ≡ g n) (transportRefl _) p
 
 
 -----------------------------------------------------------------------------
@@ -140,14 +140,14 @@ module Equiv-Properties
            where
            base0-eq : (k : ℕ) → (n : ℕ) → fun-trad k (0g (Gstr k)) n ≡ 0g (Gstr n)
            base0-eq k n with (discreteℕ k n)
-           ... | yes p = subst0g _
+           ... | yes p = substG0 _
            ... | no ¬p = refl
 
            base-add-eq : (k : ℕ) → (a b : G k) → (n : ℕ) →
                          PathP (λ _ → G n) (Gstr n ._+_ (fun-trad k a n) (fun-trad k b n))
                                                          (fun-trad k ((Gstr k + a) b) n)
            base-add-eq k a b n with (discreteℕ k n)
-           ... | yes p = subst+ _ _ _
+           ... | yes p = substG+ _ _ _
            ... | no ¬p = +IdR (Gstr n)_
 
   ⊕HIT→Fun-pres0 : ⊕HIT→Fun 0⊕HIT ≡ 0Fun
@@ -239,8 +239,6 @@ module Equiv-Properties
   sumFunTail {m} a b dva dvb x n with discreteℕ m n
   ... | yes p = sumFun dva n                   ≡⟨ sym (substSumFun dva n p) ⟩
                 subst G p (sumFun dva m)       ≡⟨ cong (subst G p) (sumFun< dva m ≤-refl) ⟩
-                subst G p (0g (Gstr m))        ≡⟨ subst0g p ⟩
-                0g (Gstr n)                    ≡⟨ sym (subst0g p) ⟩
                 subst G p (0g (Gstr m))        ≡⟨ sym (cong (subst G p) (sumFun< dvb m ≤-refl)) ⟩
                 subst G p (sumFun dvb m)       ≡⟨ substSumFun dvb n p ⟩
                 sumFun dvb n ∎
@@ -321,10 +319,10 @@ module Equiv-Properties
                   if n ≢ suc m, then it is in the rest of the sum => recursive call -}
   Strad-n≤m : (g : (n : ℕ) → G n) → (m : ℕ) → (n : ℕ) → (r : n ≤ m) → ⊕HIT→Fun (Strad g m) n ≡ g n
   Strad-n≤m g zero n r with discreteℕ 0 n
-  ... | yes p = substG g p
+  ... | yes p = substG-fct g p
   ... | no ¬p = ⊥.rec (¬p (sym (≤0→≡0 r)))
   Strad-n≤m g (suc m) n r with discreteℕ (suc m) n
-  ... | yes p = cong₂ ((Gstr n)._+_) (substG g p) (Strad-m<n g m n (0 , p)) ∙ +IdR (Gstr n) _
+  ... | yes p = cong₂ ((Gstr n)._+_) (substG-fct g p) (Strad-m<n g m n (0 , p)) ∙ +IdR (Gstr n) _
   ... | no ¬p = +IdL (Gstr n) _ ∙ Strad-n≤m g m n (≤-suc-≢ r λ x → ¬p (sym x))
 
 

Cubical/Algebra/GradedRing/DirectSumFun.agda

@@ -104,8 +104,7 @@ module _
 
     -- import for pres
     open Equiv-Properties G Gstr using
-      ( substG
-      ; fun-trad
+      ( fun-trad
       ; fun-trad-eq
       ; fun-trad-neq
       ; ⊕HIT→Fun
@@ -152,7 +151,7 @@ module _
       where
       sumF0 : (i n : ℕ) → (pp : k +ℕ l < n) → (r : i ≤ n) → sumFun i n r f g ≡ 0g (Gstr n)
       sumF0 zero n pp r = cong (subst G (sameFiber r))
-                               (cong (λ X → f 0 ⋆ X) (ng (n -ℕ zero) (<-k+-trans pp)) ∙ ⋆-0 _) ∙ subst0g _
+                               (cong (λ X → f 0 ⋆ X) (ng (n -ℕ zero) (<-k+-trans pp)) ∙ ⋆-0 _) ∙ substG0 _
       sumF0 (suc i) n pp r with splitℕ-≤ (suc i) k
       ... | inl x = cong₂ (Gstr n ._+_)
                         (cong (subst G (sameFiber r))
@@ -165,15 +164,15 @@ module _
                               ∙ ⋆-0 (f (suc i))))
                         (sumF0 i n pp (≤-trans ≤-sucℕ r))
                   ∙ +IdR (Gstr n) _
-                  ∙ subst0g _
+                  ∙ substG0 _
 
       ... | inr x = cong₂ (Gstr n ._+_)
                           (cong (subst G (sameFiber r))
                                 (cong (λ X → X ⋆ g (n -ℕ (suc i))) (nf (suc i) x)
                                 ∙ 0-⋆ _))
                           (sumF0 i n pp (≤-trans ≤-sucℕ r))
                     ∙ +IdR (Gstr n) _
-                    ∙ subst0g _
+                    ∙ substG0 _
 
     _prodF_ : ⊕Fun G Gstr → ⊕Fun G Gstr → ⊕Fun G Gstr
     _prodF_(f , Anf) (g , Ang) = (f prodFun g) , helper Anf Ang
@@ -190,33 +189,33 @@ module _
     prodFunAnnihilL f = funExt (λ n → sumF0 n n ≤-refl)
       where
       sumF0 : (i n : ℕ) → (r : i ≤ n) → sumFun i n r 0Fun f ≡ 0g (Gstr n)
-      sumF0 zero n r = cong (subst G (sameFiber r)) (0-⋆ _) ∙ subst0g _
+      sumF0 zero n r = cong (subst G (sameFiber r)) (0-⋆ _) ∙ substG0 _
       sumF0 (suc i) n r = cong₂ (Gstr n ._+_)
                                 (cong (subst G (sameFiber r)) (0-⋆ _))
                                 (sumF0 i n (≤-trans ≤-sucℕ r))
                           ∙ +IdR (Gstr n) _
-                          ∙ subst0g _
+                          ∙ substG0 _
 
 
     prodFunAnnihilR : (f : (n : ℕ) → (G n)) → f prodFun 0Fun ≡ 0Fun
     prodFunAnnihilR f = funExt (λ n → sumF0 n n ≤-refl)
       where
       sumF0 : (i n : ℕ) → (r : i ≤ n) → sumFun i n r f 0Fun ≡ 0g (Gstr n)
-      sumF0 zero n r = cong (subst G (sameFiber r)) (⋆-0 _) ∙ subst0g _
+      sumF0 zero n r = cong (subst G (sameFiber r)) (⋆-0 _) ∙ substG0 _
       sumF0 (suc i) n r = cong₂ (Gstr n ._+_)
                                 (cong (subst G (sameFiber r)) (⋆-0 _))
                                 (sumF0 i n (≤-trans ≤-sucℕ r))
                           ∙ +IdR (Gstr n) _
-                          ∙ subst0g _
+                          ∙ substG0 _
 
     prodFunDistR : (f g h : (n : ℕ) → G n) → f prodFun (g +Fun h) ≡ (f prodFun g) +Fun (f prodFun h)
     prodFunDistR f g h = funExt (λ n → sumFAssoc n n ≤-refl)
      where
      sumFAssoc : (i n : ℕ) → (r : i ≤ n) → sumFun i n r f (g +Fun h) ≡ (Gstr n) ._+_ (sumFun i n r f g) (sumFun i n r f h)
      sumFAssoc zero n r = cong (subst G (sameFiber r)) (⋆DistR+ _ _ _)
-                          ∙ sym (subst+ _ _ _)
+                          ∙ sym (substG+ _ _ _)
      sumFAssoc (suc i) n r = cong₂ (Gstr n ._+_)
-                                   (cong (subst G (sameFiber r)) (⋆DistR+ _ _ _) ∙ sym (subst+ _ _ _))
+                                   (cong (subst G (sameFiber r)) (⋆DistR+ _ _ _) ∙ sym (substG+ _ _ _))
                                    (sumFAssoc i n (≤-trans ≤-sucℕ r))
                              ∙ comm-4 ((G n) , (Gstr n)) _ _ _ _
 
@@ -225,9 +224,9 @@ module _
      where
      sumFAssoc : (i n : ℕ) → (r : i ≤ n) → sumFun i n r (f +Fun g) h ≡ (Gstr n) ._+_ (sumFun i n r f h) (sumFun i n r g h)
      sumFAssoc zero n r = cong (subst G (sameFiber r)) (⋆DistL+ _ _ _)
-                          ∙ sym (subst+ _ _ _)
+                          ∙ sym (substG+ _ _ _)
      sumFAssoc (suc i) n r = cong₂ (Gstr n ._+_)
-                                   (cong (subst G (sameFiber r)) (⋆DistL+ _ _ _) ∙ sym (subst+ _ _ _))
+                                   (cong (subst G (sameFiber r)) (⋆DistL+ _ _ _) ∙ sym (substG+ _ _ _))
                                    (sumFAssoc i n (≤-trans ≤-sucℕ r))
                              ∙ comm-4 ((G n) , (Gstr n)) _ _ _ _
 
@@ -254,26 +253,26 @@ module _
               sumFun i n r (fun-trad k a) (fun-trad l b) ≡ 0g (Gstr n)
     sumFun≠ k a l b zero n r ¬pp with discreteℕ k 0 | discreteℕ l n
     ... | yes p | yes q = ⊥.rec (¬pp ((k +≡ l) ∙ cong₂ _+ℕ_ p q) )
-    ... | yes p | no ¬q = cong (subst G (sameFiber r)) (⋆-0 _) ∙ subst0g _
-    ... | no ¬p | yes q = cong (subst G (sameFiber r)) (0-⋆ _) ∙ subst0g _
-    ... | no ¬p | no ¬q = cong (subst G (sameFiber r)) (0-⋆ _) ∙ subst0g _
+    ... | yes p | no ¬q = cong (subst G (sameFiber r)) (⋆-0 _) ∙ substG0 _
+    ... | no ¬p | yes q = cong (subst G (sameFiber r)) (0-⋆ _) ∙ substG0 _
+    ... | no ¬p | no ¬q = cong (subst G (sameFiber r)) (0-⋆ _) ∙ substG0 _
     sumFun≠ k a l b (suc i) n r ¬pp with discreteℕ k (suc i) | discreteℕ l (n -ℕ (suc i))
     ... | yes p | yes q = ⊥.rec (¬pp (cong₂ _+n_ p q ∙ sameFiber r))
     ... | yes p | no ¬q = cong₂ (Gstr n ._+_)
                                 (cong (subst G (sameFiber r)) (⋆-0 _))
                                 (sumFun≠ k a l b i n (≤-trans ≤-sucℕ r) ¬pp)
                           ∙ +IdR (Gstr n) _
-                          ∙ subst0g _
+                          ∙ substG0 _
     ... | no ¬p | yes q = cong₂ (Gstr n ._+_)
                                 (cong (subst G (sameFiber r)) (0-⋆ _))
                                 (sumFun≠ k a l b i n (≤-trans ≤-sucℕ r) ¬pp)
                           ∙ +IdR (Gstr n) _
-                          ∙ subst0g _
+                          ∙ substG0 _
     ... | no ¬p | no ¬q = cong₂ (Gstr n ._+_)
                                 (cong (subst G (sameFiber r)) (0-⋆ _))
                                 (sumFun≠ k a l b i n (≤-trans ≤-sucℕ r) ¬pp)
                           ∙ +IdR (Gstr n) _
-                          ∙ subst0g _
+                          ∙ substG0 _
 
 
     -- If k +n l ≡ n then, we unwrap the sum until we reach k.
@@ -283,14 +282,14 @@ module _
               sumFun i n r (fun-trad k a) (fun-trad l b) ≡ 0g (Gstr n)
     sumFun< k a l b zero n r pp with discreteℕ k 0
     ... | yes p = ⊥.rec (<→≢ pp (sym p))
-    ... | no ¬p = cong (subst G (sameFiber r)) (0-⋆ _) ∙ subst0g _
+    ... | no ¬p = cong (subst G (sameFiber r)) (0-⋆ _) ∙ substG0 _
     sumFun< k a l b (suc i) n r pp with discreteℕ k (suc i)
     ... | yes p = ⊥.rec (<→≢ pp (sym p))
     ... | no ¬p = cong₂ (Gstr n ._+_)
                         (cong (subst G (sameFiber r)) (0-⋆ _))
                         (sumFun< k a l b i n (≤-trans ≤-sucℕ r) (<-trans ≤-refl pp))
                   ∙ +IdR (Gstr n) _
-                  ∙ subst0g _
+                  ∙ substG0 _
 
     sumFun≤ : (k : ℕ) → (a : G k) → (l : ℕ) →  (b : G l ) →
               (i n : ℕ) → (r : i ≤ n) → (pp : k +n l ≡ n) → (k ≤ i) →
@@ -321,7 +320,7 @@ module _
                                               ∙ sym (sameFiber r)
                                               ∙ ((suc i) +≡ (n -ℕ suc i)))))
     ... | no ¬p | no ¬q = cong₂ (Gstr n ._+_)
-                                (cong (subst G (sameFiber r)) (0-⋆ _) ∙ subst0g _)
+                                (cong (subst G (sameFiber r)) (0-⋆ _) ∙ substG0 _)
                                 (sumFun≤ k a l b i n (≤-trans ≤-sucℕ r) pp (≤-suc-≢ rr ¬p))
                           ∙ +IdL (Gstr n) _
 

Cubical/Foundations/Transport.agda

@@ -59,6 +59,14 @@ transportTransport⁻ : ∀ {ℓ} {A B : Type ℓ} → (p : A ≡ B) → (b : B)
                         transport p (transport⁻ p b) ≡ b
 transportTransport⁻ p b j = transport-fillerExt⁻ p j (transport⁻-fillerExt⁻ p j b)
 
+subst⁻Subst : ∀ {ℓ ℓ'} {A : Type ℓ} {x y : A} (B : A → Type ℓ') (p : x ≡ y)
+              → (u : B x) → subst⁻ B p (subst B p u) ≡ u
+subst⁻Subst {x = x} {y = y} B p u = transport⁻Transport {A = B x} {B = B y} (cong B p) u
+
+substSubst⁻ : ∀ {ℓ ℓ'} {A : Type ℓ} {x y : A} (B : A → Type ℓ') (p : x ≡ y)
+              → (v : B y) → subst B p (subst⁻ B p v) ≡ v
+substSubst⁻ {x = x} {y = y} B p v = transportTransport⁻ {A = B x} {B = B y} (cong B p) v
+
 substEquiv : ∀ {ℓ ℓ'} {A : Type ℓ} {a a' : A} (P : A → Type ℓ') (p : a ≡ a') → P a ≃ P a'
 substEquiv P p = (subst P p , isEquivTransport (λ i → P (p i)))