diff --git a/Cubical.Cohomology.EilenbergMacLane.CupProduct.html b/Cubical.Cohomology.EilenbergMacLane.CupProduct.html index 1ddb5dd9df..eb11192a3c 100644 --- a/Cubical.Cohomology.EilenbergMacLane.CupProduct.html +++ b/Cubical.Cohomology.EilenbergMacLane.CupProduct.html @@ -193,13 +193,13 @@ ⌣-1ₕDep : (n : ℕ) (x : coHom n G' A) → PathP (λ i → coHom (+'-comm zero n (~ i)) G' A) (x ⌣ 1ₕ) x ⌣-1ₕDep n x = toPathP {A = λ i → coHom (+'-comm zero n (~ i)) G' A} - (flipTransport (⌣-1ₕ n x)) + (flipTransport (⌣-1ₕ n x)) assoc⌣Dep : (n m l : ℕ) (x : coHom n G' A) (y : coHom m G' A) (z : coHom l G' A) → PathP (λ i → coHom (+'-assoc n m l (~ i)) G' A) ((x ⌣ y) ⌣ z) (x ⌣ (y ⌣ z)) assoc⌣Dep n m l x y z = toPathP {A = λ i → coHom (+'-assoc n m l (~ i)) G' A} - (flipTransport (assoc⌣ n m l x y z)) + (flipTransport (assoc⌣ n m l x y z)) module _ {G'' : CommRing ℓ} {A : Type ℓ'} where private @@ -209,5 +209,5 @@ (x ⌣ y) (-ₕ^[ n · m ] (y ⌣ x)) comm⌣Dep n m x y = toPathP {A = λ i → coHom (+'-comm m n (~ i)) G' A} - (flipTransport (comm⌣ n m x y)) + (flipTransport (comm⌣ n m x y)) \ No newline at end of file diff --git a/Cubical.Cohomology.EilenbergMacLane.RingStructure.html b/Cubical.Cohomology.EilenbergMacLane.RingStructure.html index 80caf41919..039694ba1a 100644 --- a/Cubical.Cohomology.EilenbergMacLane.RingStructure.html +++ b/Cubical.Cohomology.EilenbergMacLane.RingStructure.html @@ -54,7 +54,7 @@ _⌣_ (λ {k} {l} → 0ₕ-⌣ k l) (λ {k} {l} → ⌣-0ₕ k l) - (λ _ _ _ → sym (ΣPathTransport→PathΣ _ _ (sym (+'-assoc _ _ _) , flipTransport (assoc⌣ _ _ _ _ _ _)))) + (λ _ _ _ → sym (ΣPathTransport→PathΣ _ _ (sym (+'-assoc _ _ _) , flipTransport (assoc⌣ _ _ _ _ _ _)))) (λ {n} a → sym (ΣPathTransport→PathΣ _ _ (sym (+'-rid _) , sym (⌣-1ₕ _ _ ∙ cong (λ p → subst (λ p → coHom p R-ab A) p a) (isSetℕ _ _ _ _))))) diff --git a/Cubical.Foundations.Transport.html b/Cubical.Foundations.Transport.html index 1390ea0eed..2fb1b773be 100644 --- a/Cubical.Foundations.Transport.html +++ b/Cubical.Foundations.Transport.html @@ -175,40 +175,40 @@ -- substition over families of paths -- theorem 2.11.3 in The Book -substInPaths : ∀ {ℓ} {A B : Type ℓ} {a a' : A} - → (f g : A → B) → (p : a ≡ a') (q : f a ≡ g a) - → subst (λ x → f x ≡ g x) p q ≡ sym (cong f p) ∙ q ∙ cong g p -substInPaths {a = a} f g p q = - J (λ x p' → (subst (λ y → f y ≡ g y) p' q) ≡ (sym (cong f p') ∙ q ∙ cong g p')) - p=refl p - where - p=refl : subst (λ y → f y ≡ g y) refl q - ≡ refl ∙ q ∙ refl - p=refl = subst (λ y → f y ≡ g y) refl q - ≡⟨ substRefl {B = (λ y → f y ≡ g y)} q ⟩ q - ≡⟨ (rUnit q) ∙ lUnit (q ∙ refl) ⟩ refl ∙ q ∙ refl ∎ - -flipTransport : ∀ {ℓ} {A : I → Type ℓ} {x : A i0} {y : A i1} - → x ≡ transport⁻ (λ i → A i) y - → transport (λ i → A i) x ≡ y -flipTransport {A = A} {y = y} p = - cong (transport (λ i → A i)) p ∙ transportTransport⁻ (λ i → A i) y - --- special cases of substInPaths from lemma 2.11.2 in The Book -module _ {ℓ : Level} {A : Type ℓ} {a x1 x2 : A} (p : x1 ≡ x2) where - substInPathsL : (q : a ≡ x1) → subst (λ x → a ≡ x) p q ≡ q ∙ p - substInPathsL q = subst (λ x → a ≡ x) p q - ≡⟨ substInPaths (λ _ → a) (λ x → x) p q ⟩ - sym (cong (λ _ → a) p) ∙ q ∙ cong (λ x → x) p - ≡⟨ assoc (λ _ → a) q p ⟩ - (refl ∙ q) ∙ p - ≡⟨ cong (_∙ p) (sym (lUnit q)) ⟩ q ∙ p ∎ - - substInPathsR : (q : x1 ≡ a) → subst (λ x → x ≡ a) p q ≡ sym p ∙ q - substInPathsR q = subst (λ x → x ≡ a) p q - ≡⟨ substInPaths (λ x → x) (λ _ → a) p q ⟩ - sym (cong (λ x → x) p) ∙ q ∙ cong (λ _ → a) p - ≡⟨ assoc (sym p) q refl ⟩ - (sym p ∙ q) ∙ refl - ≡⟨ sym (rUnit (sym p ∙ q))⟩ sym p ∙ q ∎ +substInPaths : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} {a a' : A} + → (f g : A → B) → (p : a ≡ a') (q : f a ≡ g a) + → subst (λ x → f x ≡ g x) p q ≡ sym (cong f p) ∙ q ∙ cong g p +substInPaths {a = a} f g p q = + J (λ x p' → (subst (λ y → f y ≡ g y) p' q) ≡ (sym (cong f p') ∙ q ∙ cong g p')) + p=refl p + where + p=refl : subst (λ y → f y ≡ g y) refl q + ≡ refl ∙ q ∙ refl + p=refl = subst (λ y → f y ≡ g y) refl q + ≡⟨ substRefl {B = (λ y → f y ≡ g y)} q ⟩ q + ≡⟨ (rUnit q) ∙ lUnit (q ∙ refl) ⟩ refl ∙ q ∙ refl ∎ + +flipTransport : ∀ {ℓ} {A : I → Type ℓ} {x : A i0} {y : A i1} + → x ≡ transport⁻ (λ i → A i) y + → transport (λ i → A i) x ≡ y +flipTransport {A = A} {y = y} p = + cong (transport (λ i → A i)) p ∙ transportTransport⁻ (λ i → A i) y + +-- special cases of substInPaths from lemma 2.11.2 in The Book +module _ {ℓ : Level} {A : Type ℓ} {a x1 x2 : A} (p : x1 ≡ x2) where + substInPathsL : (q : a ≡ x1) → subst (λ x → a ≡ x) p q ≡ q ∙ p + substInPathsL q = subst (λ x → a ≡ x) p q + ≡⟨ substInPaths (λ _ → a) (λ x → x) p q ⟩ + sym (cong (λ _ → a) p) ∙ q ∙ cong (λ x → x) p + ≡⟨ assoc (λ _ → a) q p ⟩ + (refl ∙ q) ∙ p + ≡⟨ cong (_∙ p) (sym (lUnit q)) ⟩ q ∙ p ∎ + + substInPathsR : (q : x1 ≡ a) → subst (λ x → x ≡ a) p q ≡ sym p ∙ q + substInPathsR q = subst (λ x → x ≡ a) p q + ≡⟨ substInPaths (λ x → x) (λ _ → a) p q ⟩ + sym (cong (λ x → x) p) ∙ q ∙ cong (λ _ → a) p + ≡⟨ assoc (sym p) q refl ⟩ + (sym p ∙ q) ∙ refl + ≡⟨ sym (rUnit (sym p ∙ q))⟩ sym p ∙ q ∎ \ No newline at end of file diff --git a/Cubical.Homotopy.EilenbergMacLane.Order2.html b/Cubical.Homotopy.EilenbergMacLane.Order2.html index 311d5850a9..f0a28a87a8 100644 --- a/Cubical.Homotopy.EilenbergMacLane.Order2.html +++ b/Cubical.Homotopy.EilenbergMacLane.Order2.html @@ -133,7 +133,7 @@ λ p → (p ∙ cong ∣_∣ₕ (sym (merid ptEM-raw)) ≡ cong ∣_∣ₕ (merid ptEM-raw) ∙ sym p) h a = - toPathP (flipTransport + toPathP (flipTransport {A = λ i → Path K2 ∣ north ∣ ∣ merid a i ∣ → Type ℓ} (funExt (λ p → (((p₃ p diff --git a/Cubical.Homotopy.EilenbergMacLane.Properties.html b/Cubical.Homotopy.EilenbergMacLane.Properties.html index c5fe805c53..0839af30e3 100644 --- a/Cubical.Homotopy.EilenbergMacLane.Properties.html +++ b/Cubical.Homotopy.EilenbergMacLane.Properties.html @@ -416,7 +416,7 @@ (transport (λ i → Path (EM G (suc (suc n))) ∣ merid a (~ i) ∣ ∣ merid a (~ i) ∣) p)) ∙ cong (ΩEM+1→EM (suc n)) - (flipTransport + (flipTransport (((rUnit p ∙ cong (p ∙_) (sym (lCancel _))) ∙ isCommΩEM-base (suc n) ∣ south ∣ p _)