diff --git a/.github/workflows/ci-nix.yml b/.github/workflows/ci-nix.yml deleted file mode 100644 index c1962e5390..0000000000 --- a/.github/workflows/ci-nix.yml +++ /dev/null @@ -1,20 +0,0 @@ -name: Nix -on: - push: - branches: - - master - pull_request: - paths: - - '.github/workflows/ci-nix.yml' - - '**.nix' - - 'flake.lock' - workflow_dispatch: - -jobs: - deploy: - runs-on: ubuntu-latest - steps: - - uses: actions/checkout@v3 - - uses: cachix/install-nix-action@v17 - - name: Build - run: nix build -v --print-build-logs diff --git a/.github/workflows/ci-ubuntu.yml b/.github/workflows/ci-ubuntu.yml index 591f1e5bcf..daece42b6b 100644 --- a/.github/workflows/ci-ubuntu.yml +++ b/.github/workflows/ci-ubuntu.yml @@ -42,7 +42,7 @@ on: ######################################################################## env: - AGDA_BRANCH: v2.6.3 + AGDA_BRANCH: v2.6.4 GHC_VERSION: 9.2.5 CABAL_VERSION: 3.6.2.0 CABAL_INSTALL: cabal install --overwrite-policy=always --ghc-options='-O1 +RTS -M6G -RTS' diff --git a/CITATION.cff b/CITATION.cff index 2e2e0124f4..407d6f4eef 100644 --- a/CITATION.cff +++ b/CITATION.cff @@ -3,6 +3,6 @@ message: "If you use this software, please cite it as below." authors: - name: "The Agda Community" title: "Cubical Agda Library" -version: 0.5 -date-released: 2023-07-05 +version: 0.6 +date-released: 2023-10-24 url: "https://github.com/agda/cubical" diff --git a/Cubical/Algebra/DistLattice.agda b/Cubical/Algebra/DistLattice.agda index a0d6e821a5..d5e617f09a 100644 --- a/Cubical/Algebra/DistLattice.agda +++ b/Cubical/Algebra/DistLattice.agda @@ -2,3 +2,4 @@ module Cubical.Algebra.DistLattice where open import Cubical.Algebra.DistLattice.Base public +open import Cubical.Algebra.DistLattice.Properties public diff --git a/Cubical/Algebra/DistLattice/Properties.agda b/Cubical/Algebra/DistLattice/Properties.agda new file mode 100644 index 0000000000..eb5aa171b8 --- /dev/null +++ b/Cubical/Algebra/DistLattice/Properties.agda @@ -0,0 +1,55 @@ +{-# OPTIONS --safe --lossy-unification #-} +module Cubical.Algebra.DistLattice.Properties where + +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.Function +open import Cubical.Foundations.Equiv +open import Cubical.Foundations.Equiv.HalfAdjoint +open import Cubical.Foundations.HLevels +open import Cubical.Foundations.Isomorphism +open import Cubical.Foundations.Univalence +open import Cubical.Foundations.Transport +open import Cubical.Foundations.SIP + +open import Cubical.Data.Sigma + +open import Cubical.Structures.Axioms +open import Cubical.Structures.Auto +open import Cubical.Structures.Macro +open import Cubical.Algebra.Semigroup +open import Cubical.Algebra.Monoid +open import Cubical.Algebra.CommMonoid +open import Cubical.Algebra.Semilattice +open import Cubical.Algebra.Lattice +open import Cubical.Algebra.DistLattice.Base + +open import Cubical.Relation.Binary.Order.Poset + +private + variable + ℓ ℓ' ℓ'' : Level + +module _ where + open LatticeHoms + + compDistLatticeHom : (L : DistLattice ℓ) (M : DistLattice ℓ') (N : DistLattice ℓ'') + → DistLatticeHom L M → DistLatticeHom M N → DistLatticeHom L N + compDistLatticeHom L M N = compLatticeHom {L = DistLattice→Lattice L} {DistLattice→Lattice M} {DistLattice→Lattice N} + + _∘dl_ : {L : DistLattice ℓ} {M : DistLattice ℓ'} {N : DistLattice ℓ''} + → DistLatticeHom M N → DistLatticeHom L M → DistLatticeHom L N + g ∘dl f = compDistLatticeHom _ _ _ f g + + compIdDistLatticeHom : {L M : DistLattice ℓ} (f : DistLatticeHom L M) + → compDistLatticeHom _ _ _ (idDistLatticeHom L) f ≡ f + compIdDistLatticeHom = compIdLatticeHom + + idCompDistLatticeHom : {L M : DistLattice ℓ} (f : DistLatticeHom L M) + → compDistLatticeHom _ _ _ f (idDistLatticeHom M) ≡ f + idCompDistLatticeHom = idCompLatticeHom + + compAssocDistLatticeHom : {L M N U : DistLattice ℓ} + (f : DistLatticeHom L M) (g : DistLatticeHom M N) (h : DistLatticeHom N U) + → compDistLatticeHom _ _ _ (compDistLatticeHom _ _ _ f g) h + ≡ compDistLatticeHom _ _ _ f (compDistLatticeHom _ _ _ g h) + compAssocDistLatticeHom = compAssocLatticeHom diff --git a/Cubical/Algebra/Lattice/Base.agda b/Cubical/Algebra/Lattice/Base.agda index 55889dfa6e..7f411bb793 100644 --- a/Cubical/Algebra/Lattice/Base.agda +++ b/Cubical/Algebra/Lattice/Base.agda @@ -194,6 +194,19 @@ isPropIsLatticeHom R f S = isOfHLevelRetractFromIso 1 IsLatticeHomIsoΣ open LatticeStr S +isSetLatticeHom : (A : Lattice ℓ) (B : Lattice ℓ') → isSet (LatticeHom A B) +isSetLatticeHom A B = isSetΣSndProp (isSetΠ λ _ → is-set) (λ f → isPropIsLatticeHom (snd A) f (snd B)) + where + open LatticeStr (str B) using (is-set) + +isSetLatticeEquiv : (A : Lattice ℓ) (B : Lattice ℓ') → isSet (LatticeEquiv A B) +isSetLatticeEquiv A B = isSetΣSndProp (isOfHLevel≃ 2 A.is-set B.is-set) + (λ e → isPropIsLatticeHom (snd A) (fst e) (snd B)) + where + module A = LatticeStr (str A) + module B = LatticeStr (str B) + + 𝒮ᴰ-Lattice : DUARel (𝒮-Univ ℓ) LatticeStr ℓ 𝒮ᴰ-Lattice = 𝒮ᴰ-Record (𝒮-Univ _) IsLatticeEquiv diff --git a/Cubical/Algebra/Lattice/Properties.agda b/Cubical/Algebra/Lattice/Properties.agda index bd5f3ae8bf..c1622d2fc7 100644 --- a/Cubical/Algebra/Lattice/Properties.agda +++ b/Cubical/Algebra/Lattice/Properties.agda @@ -2,6 +2,7 @@ module Cubical.Algebra.Lattice.Properties where open import Cubical.Foundations.Prelude +open import Cubical.Foundations.Function open import Cubical.Foundations.Equiv open import Cubical.Foundations.Equiv.HalfAdjoint open import Cubical.Foundations.HLevels @@ -25,7 +26,7 @@ open import Cubical.Relation.Binary.Order.Poset private variable - ℓ : Level + ℓ ℓ' ℓ'' ℓ''' : Level module LatticeTheory (L' : Lattice ℓ) where private L = fst L' @@ -81,7 +82,7 @@ module Order (L' : Lattice ℓ) where ∧≤LCancelJoin x y = ≤m→≤j _ _ (∧≤LCancel x y) -module _ {L M : Lattice ℓ} (φ ψ : LatticeHom L M) where +module _ {L : Lattice ℓ} {M : Lattice ℓ'} (φ ψ : LatticeHom L M) where open LatticeStr ⦃...⦄ open IsLatticeHom private @@ -93,3 +94,38 @@ module _ {L M : Lattice ℓ} (φ ψ : LatticeHom L M) where LatticeHom≡f : fst φ ≡ fst ψ → φ ≡ ψ LatticeHom≡f = Σ≡Prop λ f → isPropIsLatticeHom _ f _ + + + +module LatticeHoms where + open IsLatticeHom + + compIsLatticeHom : {A : Lattice ℓ} {B : Lattice ℓ'} {C : Lattice ℓ''} + {g : ⟨ B ⟩ → ⟨ C ⟩} {f : ⟨ A ⟩ → ⟨ B ⟩} + → IsLatticeHom (B .snd) g (C .snd) + → IsLatticeHom (A .snd) f (B .snd) + → IsLatticeHom (A .snd) (g ∘ f) (C .snd) + compIsLatticeHom {g = g} {f} gh fh .pres0 = cong g (fh .pres0) ∙ gh .pres0 + compIsLatticeHom {g = g} {f} gh fh .pres1 = cong g (fh .pres1) ∙ gh .pres1 + compIsLatticeHom {g = g} {f} gh fh .pres∨l x y = cong g (fh .pres∨l x y) ∙ gh .pres∨l (f x) (f y) + compIsLatticeHom {g = g} {f} gh fh .pres∧l x y = cong g (fh .pres∧l x y) ∙ gh .pres∧l (f x) (f y) + + + compLatticeHom : {L : Lattice ℓ} {M : Lattice ℓ'} {N : Lattice ℓ''} + → LatticeHom L M → LatticeHom M N → LatticeHom L N + fst (compLatticeHom f g) x = g .fst (f .fst x) + snd (compLatticeHom f g) = compIsLatticeHom (g .snd) (f .snd) + + _∘l_ : {L : Lattice ℓ} {M : Lattice ℓ'} {N : Lattice ℓ''} → LatticeHom M N → LatticeHom L M → LatticeHom L N + _∘l_ = flip compLatticeHom + + compIdLatticeHom : {L : Lattice ℓ} {M : Lattice ℓ'} (φ : LatticeHom L M) → compLatticeHom (idLatticeHom L) φ ≡ φ + compIdLatticeHom φ = LatticeHom≡f _ _ refl + + idCompLatticeHom : {L : Lattice ℓ} {M : Lattice ℓ'} (φ : LatticeHom L M) → compLatticeHom φ (idLatticeHom M) ≡ φ + idCompLatticeHom φ = LatticeHom≡f _ _ refl + + compAssocLatticeHom : {L : Lattice ℓ} {M : Lattice ℓ'} {N : Lattice ℓ''} {U : Lattice ℓ'''} + → (φ : LatticeHom L M) (ψ : LatticeHom M N) (χ : LatticeHom N U) + → compLatticeHom (compLatticeHom φ ψ) χ ≡ compLatticeHom φ (compLatticeHom ψ χ) + compAssocLatticeHom _ _ _ = LatticeHom≡f _ _ refl diff --git a/Cubical/Algebra/ZariskiLattice/UniversalProperty.agda b/Cubical/Algebra/ZariskiLattice/UniversalProperty.agda index 2216c737b3..351562674d 100644 --- a/Cubical/Algebra/ZariskiLattice/UniversalProperty.agda +++ b/Cubical/Algebra/ZariskiLattice/UniversalProperty.agda @@ -315,3 +315,63 @@ module ZarLatUniversalProp (R' : CommRing ℓ) where open Join ZariskiLattice ⋁D≡ : {n : ℕ} (α : FinVec R n) → ⋁ (D ∘ α) ≡ [ n , α ] ⋁D≡ _ = funExt⁻ (cong fst ZLUniversalPropCorollary) _ + +-- the lattice morphism induced by a ring morphism +module _ {A B : CommRing ℓ} (φ : CommRingHom A B) where + + open ZarLat + open ZarLatUniversalProp + open IsZarMap + open CommRingStr ⦃...⦄ + open DistLatticeStr ⦃...⦄ + open IsRingHom + private + instance + _ = A .snd + _ = B .snd + _ = (ZariskiLattice A) .snd + _ = (ZariskiLattice B) .snd + + Dcomp : A .fst → ZL B + Dcomp f = D B (φ .fst f) + + isZarMapDcomp : IsZarMap A (ZariskiLattice B) Dcomp + pres0 isZarMapDcomp = cong (D B) (φ .snd .pres0) ∙ isZarMapD B .pres0 + pres1 isZarMapDcomp = cong (D B) (φ .snd .pres1) ∙ isZarMapD B .pres1 + ·≡∧ isZarMapDcomp f g = cong (D B) (φ .snd .pres· f g) + ∙ isZarMapD B .·≡∧ (φ .fst f) (φ .fst g) + +≤∨ isZarMapDcomp f g = + let open JoinSemilattice + (Lattice→JoinSemilattice (DistLattice→Lattice (ZariskiLattice B))) + in subst (λ x → x ≤ (Dcomp f) ∨l (Dcomp g)) + (sym (cong (D B) (φ .snd .pres+ f g))) + (isZarMapD B .+≤∨ (φ .fst f) (φ .fst g)) + + inducedZarLatHom : DistLatticeHom (ZariskiLattice A) (ZariskiLattice B) + inducedZarLatHom = ZLHasUniversalProp A (ZariskiLattice B) Dcomp isZarMapDcomp .fst .fst + +-- functoriality +module _ (A : CommRing ℓ) where + open ZarLat + open ZarLatUniversalProp + + inducedZarLatHomId : inducedZarLatHom (idCommRingHom A) + ≡ idDistLatticeHom (ZariskiLattice A) + inducedZarLatHomId = + cong fst + (ZLHasUniversalProp A (ZariskiLattice A) (Dcomp (idCommRingHom A)) + (isZarMapDcomp (idCommRingHom A)) .snd + (idDistLatticeHom (ZariskiLattice A) , refl)) + +module _ {A B C : CommRing ℓ} (φ : CommRingHom A B) (ψ : CommRingHom B C) where + open ZarLat + open ZarLatUniversalProp + + inducedZarLatHomSeq : inducedZarLatHom (ψ ∘cr φ) + ≡ inducedZarLatHom ψ ∘dl inducedZarLatHom φ + inducedZarLatHomSeq = + cong fst + (ZLHasUniversalProp A (ZariskiLattice C) (Dcomp (ψ ∘cr φ)) + (isZarMapDcomp (ψ ∘cr φ)) .snd + (inducedZarLatHom ψ ∘dl inducedZarLatHom φ , funExt (λ _ → ∨lRid _))) + where open DistLatticeStr (ZariskiLattice C .snd) diff --git a/Cubical/Categories/Instances/DistLattices.agda b/Cubical/Categories/Instances/DistLattices.agda new file mode 100644 index 0000000000..15420d3be4 --- /dev/null +++ b/Cubical/Categories/Instances/DistLattices.agda @@ -0,0 +1,23 @@ +{-# OPTIONS --safe #-} +module Cubical.Categories.Instances.DistLattices where + +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.Function + +open import Cubical.Algebra.Lattice +open import Cubical.Algebra.DistLattice + +open import Cubical.Categories.Category + +open Category + + +DistLatticesCategory : ∀ {ℓ} → Category (ℓ-suc ℓ) ℓ +ob DistLatticesCategory = DistLattice _ +Hom[_,_] DistLatticesCategory = DistLatticeHom +id DistLatticesCategory {L} = idDistLatticeHom L +_⋆_ DistLatticesCategory {L} {M} {N} = compDistLatticeHom L M N +⋆IdL DistLatticesCategory {L} {M} = compIdDistLatticeHom {L = L} {M} +⋆IdR DistLatticesCategory {L} {M} = idCompDistLatticeHom {L = L} {M} +⋆Assoc DistLatticesCategory {L} {M} {N} {O} = compAssocDistLatticeHom {L = L} {M} {N} {O} +isSetHom DistLatticesCategory = isSetLatticeHom _ _ diff --git a/Cubical/Categories/Instances/Lattices.agda b/Cubical/Categories/Instances/Lattices.agda new file mode 100644 index 0000000000..1a8b91267a --- /dev/null +++ b/Cubical/Categories/Instances/Lattices.agda @@ -0,0 +1,22 @@ +{-# OPTIONS --safe #-} +module Cubical.Categories.Instances.Lattices where + +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.Function + +open import Cubical.Algebra.Lattice + +open import Cubical.Categories.Category + +open Category +open LatticeHoms + +LatticesCategory : ∀ {ℓ} → Category (ℓ-suc ℓ) ℓ +ob LatticesCategory = Lattice _ +Hom[_,_] LatticesCategory = LatticeHom +id LatticesCategory {L} = idLatticeHom L +_⋆_ LatticesCategory = compLatticeHom +⋆IdL LatticesCategory = compIdLatticeHom +⋆IdR LatticesCategory = idCompLatticeHom +⋆Assoc LatticesCategory = compAssocLatticeHom +isSetHom LatticesCategory = isSetLatticeHom _ _ diff --git a/Cubical/Categories/Instances/ZFunctors.agda b/Cubical/Categories/Instances/ZFunctors.agda new file mode 100644 index 0000000000..701f7c4020 --- /dev/null +++ b/Cubical/Categories/Instances/ZFunctors.agda @@ -0,0 +1,450 @@ +{- + + The impredicative way to define functorial qcqs-schemes (over Spec(ℤ)) + +-} +{-# OPTIONS --safe --lossy-unification #-} +module Cubical.Categories.Instances.ZFunctors where + +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.Equiv +open import Cubical.Foundations.Isomorphism +open import Cubical.Foundations.Function +open import Cubical.Foundations.Powerset +open import Cubical.Foundations.HLevels + + +open import Cubical.Functions.FunExtEquiv + +open import Cubical.Data.Sigma +open import Cubical.Data.Nat using (ℕ) + +open import Cubical.Data.FinData + +open import Cubical.Algebra.Ring +open import Cubical.Algebra.CommRing +open import Cubical.Algebra.Semilattice +open import Cubical.Algebra.Lattice +open import Cubical.Algebra.DistLattice +open import Cubical.Algebra.DistLattice.BigOps +open import Cubical.Algebra.ZariskiLattice.Base +open import Cubical.Algebra.ZariskiLattice.UniversalProperty + +open import Cubical.Categories.Category +open import Cubical.Categories.Functor +open import Cubical.Categories.Instances.Sets +open import Cubical.Categories.Instances.CommRings +open import Cubical.Categories.Instances.DistLattice +open import Cubical.Categories.Instances.DistLattices +open import Cubical.Categories.Instances.Functors +open import Cubical.Categories.NaturalTransformation +open import Cubical.Categories.Yoneda + +open import Cubical.HITs.PropositionalTruncation as PT +open import Cubical.HITs.SetQuotients as SQ + +open import Cubical.Relation.Binary.Order.Poset + +open Category hiding (_∘_) renaming (_⋆_ to _⋆c_) + +private + variable + ℓ ℓ' ℓ'' : Level + + +module _ {ℓ : Level} where + + open Functor + open NatTrans + open CommRingStr ⦃...⦄ + open IsRingHom + + -- using the naming conventions of Nieper-Wisskirchen + ℤFunctor = Functor (CommRingsCategory {ℓ = ℓ}) (SET ℓ) + ℤFUNCTOR = FUNCTOR (CommRingsCategory {ℓ = ℓ}) (SET ℓ) + + -- Yoneda in the notation of Demazure-Gabriel, + -- uses that double op is original category definitionally + Sp : Functor (CommRingsCategory {ℓ = ℓ} ^op) ℤFUNCTOR + Sp = YO {C = (CommRingsCategory {ℓ = ℓ} ^op)} + + -- the forgetful functor + -- aka the affine line + -- (aka the representable of ℤ[x]) + 𝔸¹ : ℤFunctor + 𝔸¹ = ForgetfulCommRing→Set + + -- the global sections functor + Γ : Functor ℤFUNCTOR (CommRingsCategory {ℓ = ℓ-suc ℓ} ^op) + fst (F-ob Γ X) = X ⇒ 𝔸¹ + + -- ring struncture induced by internal ring object 𝔸¹ + N-ob (CommRingStr.0r (snd (F-ob Γ X))) A _ = 0r + where instance _ = A .snd + N-hom (CommRingStr.0r (snd (F-ob Γ X))) φ = funExt λ _ → sym (φ .snd .pres0) + + N-ob (CommRingStr.1r (snd (F-ob Γ X))) A _ = 1r + where instance _ = A .snd + N-hom (CommRingStr.1r (snd (F-ob Γ X))) φ = funExt λ _ → sym (φ .snd .pres1) + + N-ob ((snd (F-ob Γ X) CommRingStr.+ α) β) A x = α .N-ob A x + β .N-ob A x + where instance _ = A .snd + N-hom ((snd (F-ob Γ X) CommRingStr.+ α) β) {x = A} {y = B} φ = funExt path + where + instance + _ = A .snd + _ = B .snd + path : ∀ x → α .N-ob B (X .F-hom φ x) + β .N-ob B (X .F-hom φ x) + ≡ φ .fst (α .N-ob A x + β .N-ob A x) + path x = α .N-ob B (X .F-hom φ x) + β .N-ob B (X .F-hom φ x) + ≡⟨ cong₂ _+_ (funExt⁻ (α .N-hom φ) x) (funExt⁻ (β .N-hom φ) x) ⟩ + φ .fst (α .N-ob A x) + φ .fst (β .N-ob A x) + ≡⟨ sym (φ .snd .pres+ _ _) ⟩ + φ .fst (α .N-ob A x + β .N-ob A x) ∎ + + N-ob ((snd (F-ob Γ X) CommRingStr.· α) β) A x = α .N-ob A x · β .N-ob A x + where instance _ = A .snd + N-hom ((snd (F-ob Γ X) CommRingStr.· α) β) {x = A} {y = B} φ = funExt path + where + instance + _ = A .snd + _ = B .snd + path : ∀ x → α .N-ob B (X .F-hom φ x) · β .N-ob B (X .F-hom φ x) + ≡ φ .fst (α .N-ob A x · β .N-ob A x) + path x = α .N-ob B (X .F-hom φ x) · β .N-ob B (X .F-hom φ x) + ≡⟨ cong₂ _·_ (funExt⁻ (α .N-hom φ) x) (funExt⁻ (β .N-hom φ) x) ⟩ + φ .fst (α .N-ob A x) · φ .fst (β .N-ob A x) + ≡⟨ sym (φ .snd .pres· _ _) ⟩ + φ .fst (α .N-ob A x · β .N-ob A x) ∎ + + N-ob ((CommRingStr.- snd (F-ob Γ X)) α) A x = - α .N-ob A x + where instance _ = A .snd + N-hom ((CommRingStr.- snd (F-ob Γ X)) α) {x = A} {y = B} φ = funExt path + where + instance + _ = A .snd + _ = B .snd + path : ∀ x → - α .N-ob B (X .F-hom φ x) ≡ φ .fst (- α .N-ob A x) + path x = - α .N-ob B (X .F-hom φ x) ≡⟨ cong -_ (funExt⁻ (α .N-hom φ) x) ⟩ + - φ .fst (α .N-ob A x) ≡⟨ sym (φ .snd .pres- _) ⟩ + φ .fst (- α .N-ob A x) ∎ + + CommRingStr.isCommRing (snd (F-ob Γ X)) = makeIsCommRing + isSetNatTrans + (λ _ _ _ → makeNatTransPath (funExt₂ λ A _ → A .snd .CommRingStr.+Assoc _ _ _)) + (λ _ → makeNatTransPath (funExt₂ λ A _ → A .snd .CommRingStr.+IdR _)) + (λ _ → makeNatTransPath (funExt₂ λ A _ → A .snd .CommRingStr.+InvR _)) + (λ _ _ → makeNatTransPath (funExt₂ λ A _ → A .snd .CommRingStr.+Comm _ _)) + (λ _ _ _ → makeNatTransPath (funExt₂ λ A _ → A .snd .CommRingStr.·Assoc _ _ _)) + (λ _ → makeNatTransPath (funExt₂ λ A _ → A .snd .CommRingStr.·IdR _)) + (λ _ _ _ → makeNatTransPath (funExt₂ λ A _ → A .snd .CommRingStr.·DistR+ _ _ _)) + (λ _ _ → makeNatTransPath (funExt₂ λ A _ → A .snd .CommRingStr.·Comm _ _)) + + -- action on natural transformations + fst (F-hom Γ α) = α ●ᵛ_ + pres0 (snd (F-hom Γ α)) = makeNatTransPath (funExt₂ λ _ _ → refl) + pres1 (snd (F-hom Γ α)) = makeNatTransPath (funExt₂ λ _ _ → refl) + pres+ (snd (F-hom Γ α)) _ _ = makeNatTransPath (funExt₂ λ _ _ → refl) + pres· (snd (F-hom Γ α)) _ _ = makeNatTransPath (funExt₂ λ _ _ → refl) + pres- (snd (F-hom Γ α)) _ = makeNatTransPath (funExt₂ λ _ _ → refl) + + -- functoriality of Γ + F-id Γ = RingHom≡ (funExt λ _ → makeNatTransPath (funExt₂ λ _ _ → refl)) + F-seq Γ _ _ = RingHom≡ (funExt λ _ → makeNatTransPath (funExt₂ λ _ _ → refl)) + + +-- we get an adjunction Γ ⊣ Sp modulo size issues +module AdjBij where + + open Functor + open NatTrans + open Iso + open IsRingHom + + private module _ {A : CommRing ℓ} {X : ℤFunctor {ℓ}} where + _♭ : CommRingHom A (Γ .F-ob X) → X ⇒ Sp .F-ob A + fst (N-ob (φ ♭) B x) a = φ .fst a .N-ob B x + + pres0 (snd (N-ob (φ ♭) B x)) = cong (λ y → y .N-ob B x) (φ .snd .pres0) + pres1 (snd (N-ob (φ ♭) B x)) = cong (λ y → y .N-ob B x) (φ .snd .pres1) + pres+ (snd (N-ob (φ ♭) B x)) _ _ = cong (λ y → y .N-ob B x) (φ .snd .pres+ _ _) + pres· (snd (N-ob (φ ♭) B x)) _ _ = cong (λ y → y .N-ob B x) (φ .snd .pres· _ _) + pres- (snd (N-ob (φ ♭) B x)) _ = cong (λ y → y .N-ob B x) (φ .snd .pres- _) + + N-hom (φ ♭) ψ = funExt (λ x → RingHom≡ (funExt λ a → funExt⁻ (φ .fst a .N-hom ψ) x)) + + + -- the other direction is just precomposition modulo Yoneda + _♯ : X ⇒ Sp .F-ob A → CommRingHom A (Γ .F-ob X) + fst (α ♯) a = α ●ᵛ yonedaᴾ 𝔸¹ A .inv a + + pres0 (snd (α ♯)) = makeNatTransPath (funExt₂ λ B x → α .N-ob B x .snd .pres0) + pres1 (snd (α ♯)) = makeNatTransPath (funExt₂ λ B x → α .N-ob B x .snd .pres1) + pres+ (snd (α ♯)) _ _ = makeNatTransPath (funExt₂ λ B x → α .N-ob B x .snd .pres+ _ _) + pres· (snd (α ♯)) _ _ = makeNatTransPath (funExt₂ λ B x → α .N-ob B x .snd .pres· _ _) + pres- (snd (α ♯)) _ = makeNatTransPath (funExt₂ λ B x → α .N-ob B x .snd .pres- _) + + + -- the two maps are inverse to each other + ♭♯Id : ∀ (α : X ⇒ Sp .F-ob A) → ((α ♯) ♭) ≡ α + ♭♯Id _ = makeNatTransPath (funExt₂ λ _ _ → RingHom≡ (funExt (λ _ → refl))) + + ♯♭Id : ∀ (φ : CommRingHom A (Γ .F-ob X)) → ((φ ♭) ♯) ≡ φ + ♯♭Id _ = RingHom≡ (funExt λ _ → makeNatTransPath (funExt₂ λ _ _ → refl)) + + Γ⊣SpIso : {A : CommRing ℓ} {X : ℤFunctor {ℓ}} + → Iso (CommRingHom A (Γ .F-ob X)) (X ⇒ Sp .F-ob A) + fun Γ⊣SpIso = _♭ + inv Γ⊣SpIso = _♯ + rightInv Γ⊣SpIso = ♭♯Id + leftInv Γ⊣SpIso = ♯♭Id + + Γ⊣SpNatℤFunctor : {A : CommRing ℓ} {X Y : ℤFunctor {ℓ}} (α : X ⇒ Sp .F-ob A) (β : Y ⇒ X) + → (β ●ᵛ α) ♯ ≡ (Γ .F-hom β) ∘cr (α ♯) + Γ⊣SpNatℤFunctor _ _ = RingHom≡ (funExt (λ _ → makeNatTransPath (funExt₂ (λ _ _ → refl)))) + + Γ⊣SpNatCommRing : {X : ℤFunctor {ℓ}} {A B : CommRing ℓ} + (φ : CommRingHom A (Γ .F-ob X)) (ψ : CommRingHom B A) + → (φ ∘cr ψ) ♭ ≡ (φ ♭) ●ᵛ Sp .F-hom ψ + Γ⊣SpNatCommRing _ _ = makeNatTransPath (funExt₂ λ _ _ → RingHom≡ (funExt (λ _ → refl))) + + -- the counit is an equivalence + private + ε : (A : CommRing ℓ) → CommRingHom A ((Γ ∘F Sp) .F-ob A) + ε A = (idTrans (Sp .F-ob A)) ♯ + + Γ⊣SpCounitEquiv : (A : CommRing ℓ) → CommRingEquiv A ((Γ ∘F Sp) .F-ob A) + fst (Γ⊣SpCounitEquiv A) = isoToEquiv theIso + where + theIso : Iso (A .fst) ((Γ ∘F Sp) .F-ob A .fst) + fun theIso = ε A .fst + inv theIso = yonedaᴾ 𝔸¹ A .fun + rightInv theIso α = ℤFUNCTOR .⋆IdL _ ∙ yonedaᴾ 𝔸¹ A .leftInv α + leftInv theIso a = path -- I get yellow otherwise + where + path : yonedaᴾ 𝔸¹ A .fun ((idTrans (Sp .F-ob A)) ●ᵛ yonedaᴾ 𝔸¹ A .inv a) ≡ a + path = cong (yonedaᴾ 𝔸¹ A .fun) (ℤFUNCTOR .⋆IdL _) ∙ yonedaᴾ 𝔸¹ A .rightInv a + snd (Γ⊣SpCounitEquiv A) = ε A .snd + + +-- Affine schemes +module _ {ℓ : Level} where + open Functor + + isAffine : (X : ℤFunctor) → Type (ℓ-suc ℓ) + isAffine X = ∃[ A ∈ CommRing ℓ ] NatIso (Sp .F-ob A) X + + -- TODO: 𝔸¹ ≅ Sp ℤ[x] and 𝔾ₘ ≅ Sp ℤ[x,x⁻¹] as first examples of affine schemes + + +-- The unit is an equivalence iff the ℤ-functor is affine. +-- Unfortunately, we can't give a natural transformation +-- X ⇒ Sp (Γ X), because the latter ℤ-functor lives in a higher universe. +-- We can however give terms that look just like the unit, +-- giving us an alternative def. of affine ℤ-functors +private module AffineDefs {ℓ : Level} where + open Functor + open NatTrans + open Iso + open IsRingHom + η : (X : ℤFunctor) (A : CommRing ℓ) → X .F-ob A .fst → CommRingHom (Γ .F-ob X) A + fst (η X A x) α = α .N-ob A x + pres0 (snd (η X A x)) = refl + pres1 (snd (η X A x)) = refl + pres+ (snd (η X A x)) _ _ = refl + pres· (snd (η X A x)) _ _ = refl + pres- (snd (η X A x)) _ = refl + + -- this is basically a natural transformation + ηObHom : (X : ℤFunctor) {A B : CommRing ℓ} (φ : CommRingHom A B) + → η X B ∘ (X .F-hom φ) ≡ (φ ∘cr_) ∘ η X A + ηObHom X φ = funExt (λ x → RingHom≡ (funExt λ α → funExt⁻ (α .N-hom φ) x)) + + -- can only state equality on object part, but that would be enough + ηHom : {X Y : ℤFunctor} (α : X ⇒ Y) (A : CommRing ℓ) (x : X .F-ob A .fst) + → η Y A (α .N-ob A x) ≡ η X A x ∘cr Γ .F-hom α + ηHom _ _ _ = RingHom≡ refl + + isAffine' : (X : ℤFunctor) → Type (ℓ-suc ℓ) + isAffine' X = ∀ (A : CommRing ℓ) → isEquiv (η X A) + -- TODO: isAffine → isAffine' + + +-- compact opens and affine covers +module _ {ℓ : Level} where + + open Iso + open Functor + open NatTrans + open DistLatticeStr ⦃...⦄ + open CommRingStr ⦃...⦄ + open IsRingHom + open IsLatticeHom + open ZarLat + open ZarLatUniversalProp + + -- the Zariski lattice classifying compact open subobjects + 𝓛 : ℤFunctor {ℓ = ℓ} + F-ob 𝓛 A = ZL A , SQ.squash/ + F-hom 𝓛 φ = inducedZarLatHom φ .fst + F-id 𝓛 {A} = cong fst (inducedZarLatHomId A) + F-seq 𝓛 φ ψ = cong fst (inducedZarLatHomSeq φ ψ) + + CompactOpen : ℤFunctor → Type (ℓ-suc ℓ) + CompactOpen X = X ⇒ 𝓛 + + -- the induced subfunctor + ⟦_⟧ᶜᵒ : {X : ℤFunctor} (U : CompactOpen X) → ℤFunctor + F-ob (⟦_⟧ᶜᵒ {X = X} U) A = (Σ[ x ∈ X .F-ob A .fst ] U .N-ob A x ≡ D A 1r) + , isSetΣSndProp (X .F-ob A .snd) λ _ → squash/ _ _ + where instance _ = snd A + F-hom (⟦_⟧ᶜᵒ {X = X} U) {x = A} {y = B} φ (x , Ux≡D1) = (X .F-hom φ x) , path + where + instance + _ = A .snd + _ = B .snd + open IsLatticeHom + path : U .N-ob B (X .F-hom φ x) ≡ D B 1r + path = U .N-ob B (X .F-hom φ x) ≡⟨ funExt⁻ (U .N-hom φ) x ⟩ + 𝓛 .F-hom φ (U .N-ob A x) ≡⟨ cong (𝓛 .F-hom φ) Ux≡D1 ⟩ + 𝓛 .F-hom φ (D A 1r) ≡⟨ inducedZarLatHom φ .snd .pres1 ⟩ + D B 1r ∎ + F-id (⟦_⟧ᶜᵒ {X = X} U) = funExt (λ x → Σ≡Prop (λ _ → squash/ _ _) + (funExt⁻ (X .F-id) (x .fst))) + F-seq (⟦_⟧ᶜᵒ {X = X} U) φ ψ = funExt (λ x → Σ≡Prop (λ _ → squash/ _ _) + (funExt⁻ (X .F-seq φ ψ) (x .fst))) + + + isAffineCompactOpen : {X : ℤFunctor} (U : CompactOpen X) → Type (ℓ-suc ℓ) + isAffineCompactOpen U = isAffine ⟦ U ⟧ᶜᵒ + + -- TODO: define basic opens D(f) ↪ Sp A and prove ⟦ D(f) ⟧ᶜᵒ ≅ Sp A[1/f] + + -- the (big) dist. lattice of compact opens + CompOpenDistLattice : Functor ℤFUNCTOR (DistLatticesCategory {ℓ = ℓ-suc ℓ} ^op) + fst (F-ob CompOpenDistLattice X) = CompactOpen X + + -- lattice structure induce by internal lattice object 𝓛 + N-ob (DistLatticeStr.0l (snd (F-ob CompOpenDistLattice X))) A _ = 0l + where instance _ = ZariskiLattice A .snd + N-hom (DistLatticeStr.0l (snd (F-ob CompOpenDistLattice X))) _ = funExt λ _ → refl + + N-ob (DistLatticeStr.1l (snd (F-ob CompOpenDistLattice X))) A _ = 1l + where instance _ = ZariskiLattice A .snd + N-hom (DistLatticeStr.1l (snd (F-ob CompOpenDistLattice X))) {x = A} {y = B} φ = funExt λ _ → path + where + instance + _ = A .snd + _ = B .snd + _ = ZariskiLattice B .snd + path : D B 1r ≡ D B (φ .fst 1r) ∨l 0l + path = cong (D B) (sym (φ .snd .pres1)) ∙ sym (∨lRid _) + + N-ob ((snd (F-ob CompOpenDistLattice X) DistLatticeStr.∨l U) V) A x = U .N-ob A x ∨l V .N-ob A x + where instance _ = ZariskiLattice A .snd + N-hom ((snd (F-ob CompOpenDistLattice X) DistLatticeStr.∨l U) V) {x = A} {y = B} φ = funExt path + where + instance + _ = ZariskiLattice A .snd + _ = ZariskiLattice B .snd + path : ∀ x → U .N-ob B (X .F-hom φ x) ∨l V .N-ob B (X .F-hom φ x) + ≡ 𝓛 .F-hom φ (U .N-ob A x ∨l V .N-ob A x) + path x = U .N-ob B (X .F-hom φ x) ∨l V .N-ob B (X .F-hom φ x) + ≡⟨ cong₂ _∨l_ (funExt⁻ (U .N-hom φ) x) (funExt⁻ (V .N-hom φ) x) ⟩ + 𝓛 .F-hom φ (U .N-ob A x) ∨l 𝓛 .F-hom φ (V .N-ob A x) + ≡⟨ sym (inducedZarLatHom φ .snd .pres∨l _ _) ⟩ + 𝓛 .F-hom φ (U .N-ob A x ∨l V .N-ob A x) ∎ + + N-ob ((snd (F-ob CompOpenDistLattice X) DistLatticeStr.∧l U) V) A x = U .N-ob A x ∧l V .N-ob A x + where instance _ = ZariskiLattice A .snd + N-hom ((snd (F-ob CompOpenDistLattice X) DistLatticeStr.∧l U) V) {x = A} {y = B} φ = funExt path + where + instance + _ = ZariskiLattice A .snd + _ = ZariskiLattice B .snd + path : ∀ x → U .N-ob B (X .F-hom φ x) ∧l V .N-ob B (X .F-hom φ x) + ≡ 𝓛 .F-hom φ (U .N-ob A x ∧l V .N-ob A x) + path x = U .N-ob B (X .F-hom φ x) ∧l V .N-ob B (X .F-hom φ x) + ≡⟨ cong₂ _∧l_ (funExt⁻ (U .N-hom φ) x) (funExt⁻ (V .N-hom φ) x) ⟩ + 𝓛 .F-hom φ (U .N-ob A x) ∧l 𝓛 .F-hom φ (V .N-ob A x) + ≡⟨ sym (inducedZarLatHom φ .snd .pres∧l _ _) ⟩ + 𝓛 .F-hom φ (U .N-ob A x ∧l V .N-ob A x) ∎ + + DistLatticeStr.isDistLattice (snd (F-ob CompOpenDistLattice X)) = makeIsDistLattice∧lOver∨l + isSetNatTrans + (λ _ _ _ → makeNatTransPath (funExt₂ + (λ A _ → ZariskiLattice A .snd .DistLatticeStr.∨lAssoc _ _ _))) + (λ _ → makeNatTransPath (funExt₂ (λ A _ → ZariskiLattice A .snd .DistLatticeStr.∨lRid _))) + (λ _ _ → makeNatTransPath (funExt₂ (λ A _ → ZariskiLattice A .snd .DistLatticeStr.∨lComm _ _))) + (λ _ _ _ → makeNatTransPath (funExt₂ + (λ A _ → ZariskiLattice A .snd .DistLatticeStr.∧lAssoc _ _ _))) + (λ _ → makeNatTransPath (funExt₂ (λ A _ → ZariskiLattice A .snd .DistLatticeStr.∧lRid _))) + (λ _ _ → makeNatTransPath (funExt₂ (λ A _ → ZariskiLattice A .snd .DistLatticeStr.∧lComm _ _))) + (λ _ _ → makeNatTransPath (funExt₂ -- don't know why ∧lAbsorb∨l doesn't work + (λ A _ → ZariskiLattice A .snd .DistLatticeStr.absorb _ _ .snd))) + (λ _ _ _ → makeNatTransPath (funExt₂ -- same here + (λ A _ → ZariskiLattice A .snd .DistLatticeStr.∧l-dist-∨l _ _ _ .fst))) + + -- (contravariant) action on morphisms + fst (F-hom CompOpenDistLattice α) = α ●ᵛ_ + pres0 (snd (F-hom CompOpenDistLattice α)) = makeNatTransPath (funExt₂ λ _ _ → refl) + pres1 (snd (F-hom CompOpenDistLattice α)) = makeNatTransPath (funExt₂ λ _ _ → refl) + pres∨l (snd (F-hom CompOpenDistLattice α)) _ _ = makeNatTransPath (funExt₂ λ _ _ → refl) + pres∧l (snd (F-hom CompOpenDistLattice α)) _ _ = makeNatTransPath (funExt₂ λ _ _ → refl) + + -- functoriality + F-id CompOpenDistLattice = LatticeHom≡f _ _ + (funExt λ _ → makeNatTransPath (funExt₂ λ _ _ → refl)) + F-seq CompOpenDistLattice _ _ = LatticeHom≡f _ _ + (funExt λ _ → makeNatTransPath (funExt₂ λ _ _ → refl)) + + + module _ (X : ℤFunctor) where + open Join (CompOpenDistLattice .F-ob X) + open JoinSemilattice (Lattice→JoinSemilattice (DistLattice→Lattice (CompOpenDistLattice .F-ob X))) + open PosetStr (IndPoset .snd) hiding (_≤_) + open LatticeTheory ⦃...⦄ -- ((DistLattice→Lattice (CompOpenDistLattice .F-ob X))) + private instance _ = (CompOpenDistLattice .F-ob X) .snd + + record AffineCover : Type (ℓ-suc ℓ) where + field + n : ℕ + U : FinVec (CompactOpen X) n + covers : ⋁ U ≡ 1l -- TODO: equivalent to X ≡ ⟦ ⋁ U ⟧ᶜᵒ + isAffineU : ∀ i → isAffineCompactOpen (U i) + + hasAffineCover : Type (ℓ-suc ℓ) + hasAffineCover = ∥ AffineCover ∥₁ + -- TODO: A ℤ-functor is a qcqs-scheme if it is a Zariski sheaf and has an affine cover + + -- the structure sheaf + private COᵒᵖ = (DistLatticeCategory (CompOpenDistLattice .F-ob X)) ^op + + compOpenIncl : {U V : CompactOpen X} → V ≤ U → ⟦ V ⟧ᶜᵒ ⇒ ⟦ U ⟧ᶜᵒ + N-ob (compOpenIncl {U = U} {V = V} V≤U) A (x , Vx≡D1) = x , path + where + instance + _ = A .snd + _ = ZariskiLattice A .snd + _ = DistLattice→Lattice (ZariskiLattice A) + path : U .N-ob A x ≡ D A 1r + path = U .N-ob A x ≡⟨ funExt⁻ (funExt⁻ (cong N-ob (sym V≤U)) A) x ⟩ + V .N-ob A x ∨l U .N-ob A x ≡⟨ cong (_∨l U .N-ob A x) Vx≡D1 ⟩ + D A 1r ∨l U .N-ob A x ≡⟨ 1lLeftAnnihilates∨l _ ⟩ + D A 1r ∎ + N-hom (compOpenIncl V≤U) φ = funExt λ x → Σ≡Prop (λ _ → squash/ _ _) refl + + compOpenInclId : ∀ {U : CompactOpen X} → compOpenIncl (is-refl U) ≡ idTrans ⟦ U ⟧ᶜᵒ + compOpenInclId = makeNatTransPath (funExt₂ (λ _ _ → Σ≡Prop (λ _ → squash/ _ _) refl)) + + compOpenInclSeq : ∀ {U V W : CompactOpen X} (U≤V : U ≤ V) (V≤W : V ≤ W) + → compOpenIncl (is-trans _ _ _ U≤V V≤W) + ≡ compOpenIncl U≤V ●ᵛ compOpenIncl V≤W + compOpenInclSeq _ _ = makeNatTransPath + (funExt₂ (λ _ _ → Σ≡Prop (λ _ → squash/ _ _) refl)) + + 𝓞 : Functor COᵒᵖ (CommRingsCategory {ℓ = ℓ-suc ℓ}) + F-ob 𝓞 U = Γ .F-ob ⟦ U ⟧ᶜᵒ + F-hom 𝓞 U≥V = Γ .F-hom (compOpenIncl U≥V) + F-id 𝓞 = cong (Γ .F-hom) compOpenInclId ∙ Γ .F-id + F-seq 𝓞 _ _ = cong (Γ .F-hom) (compOpenInclSeq _ _) ∙ Γ .F-seq _ _ diff --git a/Cubical/Cohomology/EilenbergMacLane/Base.agda b/Cubical/Cohomology/EilenbergMacLane/Base.agda index c22bc28635..f0c192a445 100644 --- a/Cubical/Cohomology/EilenbergMacLane/Base.agda +++ b/Cubical/Cohomology/EilenbergMacLane/Base.agda @@ -8,6 +8,7 @@ open import Cubical.Homotopy.EilenbergMacLane.Properties open import Cubical.Homotopy.EilenbergMacLane.Order2 open import Cubical.Foundations.Prelude +open import Cubical.Foundations.Transport open import Cubical.Foundations.HLevels open import Cubical.Foundations.GroupoidLaws open import Cubical.Foundations.Path @@ -308,3 +309,41 @@ fst (coHomHom∙ n f) = coHomFun∙ n f snd (coHomHom∙ n f) = makeIsGroupHom (ST.elim2 (λ _ _ → isSetPathImplicit) λ g h → cong ∣_∣₂ (→∙Homogeneous≡ (isHomogeneousEM n) refl)) + +substℕ-coHom : {A : Type ℓ} {G : AbGroup ℓ'} {n m : ℕ} + → (p : n ≡ m) + → AbGroupEquiv (coHomGr n G A) (coHomGr m G A) +fst (substℕ-coHom {A = A} {G = G} p) = + substEquiv' (λ i → coHom i G A) p +snd (substℕ-coHom {A = A} {G = G} p) = + makeIsGroupHom + λ x y → + J (λ m p → subst (λ i → coHom i G A) p (x +ₕ y) + ≡ (subst (λ i → coHom i G A) p x + +ₕ subst (λ i → coHom i G A) p y)) + (transportRefl _ ∙ cong₂ _+ₕ_ + (sym (transportRefl x)) (sym (transportRefl y))) p + +substℕ-coHomRed : {A : Pointed ℓ} {G : AbGroup ℓ'} {n m : ℕ} + → (p : n ≡ m) + → AbGroupEquiv (coHomRedGr n G A) (coHomRedGr m G A) +fst (substℕ-coHomRed {A = A} {G = G} p) = + substEquiv' (λ i → coHomRed i G A) p +snd (substℕ-coHomRed {A = A} {G = G} p) = + makeIsGroupHom + λ x y → + J (λ m p → subst (λ i → coHomRed i G A) p (x +ₕ∙ y) + ≡ (subst (λ i → coHomRed i G A) p x + +ₕ∙ subst (λ i → coHomRed i G A) p y)) + (transportRefl _ ∙ cong₂ _+ₕ∙_ + (sym (transportRefl x)) (sym (transportRefl y))) p + +subst-EM-0ₖ : ∀{ℓ} {G : AbGroup ℓ} {n m : ℕ} (p : n ≡ m) + → subst (EM G) p (0ₖ n) ≡ 0ₖ m +subst-EM-0ₖ {G = G} {n = n} = + J (λ m p → subst (EM G) p (0ₖ n) ≡ 0ₖ m) (transportRefl _) + +subst-EM∙ : ∀{ℓ} {G : AbGroup ℓ} {n m : ℕ} (p : n ≡ m) + → EM∙ G n →∙ EM∙ G m +fst (subst-EM∙ {G = G} p) = subst (EM G) p +snd (subst-EM∙ p) = subst-EM-0ₖ p diff --git a/Cubical/Cohomology/EilenbergMacLane/Groups/Sn.agda b/Cubical/Cohomology/EilenbergMacLane/Groups/Sn.agda index 0095ff4710..e71c8db909 100644 --- a/Cubical/Cohomology/EilenbergMacLane/Groups/Sn.agda +++ b/Cubical/Cohomology/EilenbergMacLane/Groups/Sn.agda @@ -6,8 +6,11 @@ open import Cubical.Cohomology.EilenbergMacLane.Base open import Cubical.Homotopy.EilenbergMacLane.GroupStructure open import Cubical.Homotopy.EilenbergMacLane.Properties +open import Cubical.Homotopy.EilenbergMacLane.CupProduct open import Cubical.Homotopy.EilenbergMacLane.Base open import Cubical.Homotopy.Connected +open import Cubical.Homotopy.Loopspace +open import Cubical.Homotopy.Group.Base open import Cubical.Foundations.Prelude open import Cubical.Foundations.Function @@ -15,12 +18,17 @@ open import Cubical.Foundations.HLevels open import Cubical.Foundations.Isomorphism open import Cubical.Foundations.Equiv open import Cubical.Foundations.GroupoidLaws +open import Cubical.Foundations.Pointed +open import Cubical.Foundations.Pointed.Homogeneous open import Cubical.Data.Nat renaming (_+_ to _+ℕ_) open import Cubical.Data.Unit +open import Cubical.Data.Bool +open import Cubical.Data.Sigma open import Cubical.Algebra.Group.MorphismProperties open import Cubical.Algebra.AbGroup.Base +open import Cubical.Algebra.Ring open import Cubical.HITs.SetTruncation as ST open import Cubical.HITs.Truncation as TR @@ -30,6 +38,9 @@ open import Cubical.HITs.Susp open import Cubical.HITs.Sn open import Cubical.HITs.S1 renaming (rec to S¹fun) +open RingStr renaming (_+_ to _+r_) +open PlusBis + private variable ℓ ℓ' : Level @@ -84,9 +95,9 @@ S¹-connElim {B = B} conA pr a ind f = (isConnectedPath 1 conA (f base) a .fst)) module _ (G : AbGroup ℓ) where - open AbGroupStr (snd G) + open AbGroupStr (snd G) renaming (is-set to is-setG) H¹S¹→G : coHom 1 G S¹ → fst G - H¹S¹→G = ST.rec is-set λ f → ΩEM+1→EM-gen 0 (f base) (cong f loop) + H¹S¹→G = ST.rec is-setG λ f → ΩEM+1→EM-gen 0 (f base) (cong f loop) G→H¹S¹ : fst G → coHom 1 G S¹ G→H¹S¹ g = ∣ S¹fun (0ₖ 1) (emloop g) ∣₂ @@ -275,3 +286,181 @@ module _ (G : AbGroup ℓ) where (isConnectedEM (suc (suc n))) (0ₖ _) (f north) .fst))) isContrUnit*) snd (Hⁿ[Sᵐ⁺ⁿ,G]≅0 (suc n) m) = makeIsGroupHom λ _ _ → refl + +-- In fact, the above induces an equivalence (S₊∙ n →∙ EM∙ G n) ≃ G +isSet-Sn→∙EM : (G : AbGroup ℓ) (n : ℕ) → isSet (S₊∙ n →∙ EM∙ G n) +isSet-Sn→∙EM G n = + subst isSet (sym (help n) + ∙ isoToPath (invIso (IsoSphereMapΩ n))) + (AbGroupStr.is-set (snd G)) + where + help : (n : ℕ) → fst ((Ω^ n) (EM∙ G n)) ≡ fst G + help zero = refl + help (suc n) = + cong fst (flipΩPath n) + ∙ cong (fst ∘ (Ω^ n)) + (ua∙ (isoToEquiv (invIso (Iso-EM-ΩEM+1 n))) + (ΩEM+1→EM-refl n)) + ∙ help n + +-- The equivalence (Sⁿ →∙ K(G,n)) ≃ G +HⁿSⁿ-raw≃G : (G : AbGroup ℓ) (n : ℕ) + → (S₊∙ n →∙ EM∙ G n) ≃ (fst G) +HⁿSⁿ-raw≃G G zero = + isoToEquiv + (iso (λ f → fst f false) + (λ g → (λ {true → _ ; false → g}) , refl) + (λ g → refl) + λ g → Σ≡Prop (λ _ → AbGroupStr.is-set (snd G) _ _) + (funExt λ { false → refl ; true → sym (snd g)})) +HⁿSⁿ-raw≃G G (suc n) = + compEquiv + (invEquiv + (compEquiv (fst (coHom≅coHomRed n G (S₊∙ (suc n)))) + (isoToEquiv (setTruncIdempotentIso (isSet-Sn→∙EM G (suc n)))))) + (fst (Hⁿ[Sⁿ,G]≅G G n)) + +-- generator of HⁿSⁿ ≃ (Sⁿ →∙ K(G,n)) +gen-HⁿSⁿ-raw : (R : Ring ℓ) (n : ℕ) + → (S₊∙ n →∙ EM∙ (Ring→AbGroup R) n) +fst (gen-HⁿSⁿ-raw R zero) false = 1r (snd R) +fst (gen-HⁿSⁿ-raw R zero) true = 0ₖ {G = Ring→AbGroup R} 0 +snd (gen-HⁿSⁿ-raw R zero) = refl +fst (gen-HⁿSⁿ-raw R (suc zero)) base = 0ₖ 1 +fst (gen-HⁿSⁿ-raw R (suc zero)) (loop i) = emloop (1r (snd R)) i +fst (gen-HⁿSⁿ-raw R (suc (suc n))) north = 0ₖ (2 +ℕ n) +fst (gen-HⁿSⁿ-raw R (suc (suc n))) south = 0ₖ (2 +ℕ n) +fst (gen-HⁿSⁿ-raw R (suc (suc n))) (merid a i) = + EM→ΩEM+1 (suc n) (gen-HⁿSⁿ-raw R (suc n) .fst a) i +snd (gen-HⁿSⁿ-raw R (suc zero)) = refl +snd (gen-HⁿSⁿ-raw R (suc (suc n))) = refl + +-- looping map (Sⁿ⁺¹ →∙ K(G,n+1)) → (Sⁿ →∙ K(G,n)) +desuspHⁿSⁿ : (G : AbGroup ℓ) (n : ℕ) + → (S₊∙ (suc n) →∙ EM∙ G (suc n)) + → (S₊∙ n →∙ EM∙ G n) +fst (desuspHⁿSⁿ G zero f) = + λ {false → ΩEM+1→EM-gen 0 _ (cong (fst f) loop) + ; true → AbGroupStr.0g (snd G)} +fst (desuspHⁿSⁿ G (suc n) f) x = + ΩEM+1→EM-gen (suc n) _ + (cong (fst f) (toSusp (S₊∙ (suc n)) x)) +snd (desuspHⁿSⁿ G zero f) = refl +snd (desuspHⁿSⁿ G (suc n) f) = + cong (ΩEM+1→EM-gen (suc n) _) + (cong (cong (fst f)) (rCancel (merid (ptSn (suc n))))) + ∙ (λ i → ΩEM+1→EM-gen (suc n) _ (refl {x = snd f i})) + ∙ ΩEM+1→EM-refl (suc n) + +-- The equivalence respects desuspHⁿSⁿ +HⁿSⁿ-raw≃G-ind : (G : AbGroup ℓ) (n : ℕ) + → (f : S₊∙ (suc n) →∙ EM∙ G (suc n)) + → HⁿSⁿ-raw≃G G (suc n) .fst f + ≡ HⁿSⁿ-raw≃G G n .fst (desuspHⁿSⁿ G n f) +HⁿSⁿ-raw≃G-ind G zero f = refl +HⁿSⁿ-raw≃G-ind G (suc n) f = refl + +-- The equivalence preserves the unit +gen-HⁿSⁿ-raw↦1 : (R : Ring ℓ) (n : ℕ) + → HⁿSⁿ-raw≃G (Ring→AbGroup R) n .fst (gen-HⁿSⁿ-raw R n) ≡ 1r (snd R) +gen-HⁿSⁿ-raw↦1 R zero = refl +gen-HⁿSⁿ-raw↦1 R (suc zero) = transportRefl _ + ∙ +IdL (snd R) (1r (snd R)) +gen-HⁿSⁿ-raw↦1 R (suc (suc n)) = + cong (fst (Hⁿ[Sⁿ,G]≅G (Ring→AbGroup R) n) .fst) + (cong ∣_∣₂ (funExt λ x + → (cong (ΩEM+1→EM (suc n)) + (cong-∙ (fst (gen-HⁿSⁿ-raw R (suc (suc n)))) + (merid x) (sym (merid (ptSn (suc n))))) + ∙ ΩEM+1→EM-hom (suc n) _ _) + ∙ cong₂ _+ₖ_ + (Iso.leftInv (Iso-EM-ΩEM+1 (suc n)) + (gen-HⁿSⁿ-raw R (suc n) .fst x)) + (((λ i → ΩEM+1→EM-sym (suc n) + (EM→ΩEM+1 (suc n) (snd (gen-HⁿSⁿ-raw R (suc n)) i)) i) + ∙ cong -ₖ_ (Iso.leftInv (Iso-EM-ΩEM+1 (suc n)) (0ₖ (suc n))) + ∙ -0ₖ (suc n))) + ∙ rUnitₖ (suc n) _)) + ∙ gen-HⁿSⁿ-raw↦1 R (suc n) + +-- explicit characterisation of the inverse of the equivalence +-- in terms of ⌣ₖ. +HⁿSⁿ-raw≃G-inv : (R : Ring ℓ) (n : ℕ) + → fst R → (S₊∙ n →∙ EM∙ (Ring→AbGroup R) n) +fst (HⁿSⁿ-raw≃G-inv R n r) x = + subst (EM (Ring→AbGroup R)) (+'-comm n 0) + (_⌣ₖ_ {n = n} {m = 0} (fst (gen-HⁿSⁿ-raw R n) x) r) +snd (HⁿSⁿ-raw≃G-inv R n r) = + cong (subst (EM (Ring→AbGroup R)) (+'-comm n 0)) + (cong (_⌣ₖ r) (snd (gen-HⁿSⁿ-raw R n)) + ∙ 0ₖ-⌣ₖ n 0 r) + ∙ λ j → transp (λ i → EM (Ring→AbGroup R) + (+'-comm n 0 (i ∨ j))) + j (0ₖ (+'-comm n 0 j)) + + +HⁿSⁿ-raw≃G-inv-isInv : (R : Ring ℓ) (n : ℕ) (r : fst R) → + ((fst (HⁿSⁿ-raw≃G (Ring→AbGroup R) n)) + ∘ HⁿSⁿ-raw≃G-inv R n) r + ≡ r +HⁿSⁿ-raw≃G-inv-isInv R zero r = transportRefl _ ∙ ·IdL (snd R) r +HⁿSⁿ-raw≃G-inv-isInv R (suc zero) r = + transportRefl _ + ∙ transportRefl _ + ∙ cong₂ (_+r_ (snd R)) (transportRefl (0r (snd R))) + (transportRefl _ + ∙ ·IdL (snd R) r) + ∙ +IdL (snd R) r +HⁿSⁿ-raw≃G-inv-isInv R (suc (suc n)) r = + HⁿSⁿ-raw≃G-ind (Ring→AbGroup R) (suc n) _ ∙ + (cong (fst (HⁿSⁿ-raw≃G (Ring→AbGroup R) (suc n))) + (→∙Homogeneous≡ + (isHomogeneousEM _) + (funExt λ z → + cong (ΩEM+1→EM (suc n)) (lem z) + ∙ Iso-EM-ΩEM+1 (suc n) .Iso.leftInv (subst (EM (Ring→AbGroup R)) + (+'-comm (suc n) 0) (_⌣ₖ_ {m = 0} + (fst (gen-HⁿSⁿ-raw R (suc n)) z) r))))) + ∙ HⁿSⁿ-raw≃G-inv-isInv R (suc n) r + where + lem : (z : _) + → (λ i → subst (EM (Ring→AbGroup R)) (+'-comm (suc (suc n)) 0) + (fst (gen-HⁿSⁿ-raw R (suc (suc n))) (toSusp (S₊∙ (suc n)) z i) ⌣ₖ r)) + ≡ EM→ΩEM+1 (suc n) (subst (EM (Ring→AbGroup R)) + (+'-comm (suc n) 0) + (_⌣ₖ_ {m = 0} (fst (gen-HⁿSⁿ-raw R (suc n)) z) r)) + lem z = ((λ j → transp (λ i → typ (Ω (EM∙ (Ring→AbGroup R) + (+'-comm (suc (suc n)) 0 (~ j ∨ i))))) (~ j) + λ i → transp (λ i → EM (Ring→AbGroup R) + (+'-comm (suc (suc n)) 0 (~ j ∧ i))) + j + (fst (gen-HⁿSⁿ-raw R (suc (suc n))) + (toSusp (S₊∙ (suc n)) z i) ⌣ₖ r)) + ∙ (λ j → transport (λ i → typ (Ω (EM∙ (Ring→AbGroup R) + (isSetℕ (suc (suc n)) (suc (suc n)) + (+'-comm (suc (suc n)) 0) refl j i)))) + λ i → _⌣ₖ_ {n = suc (suc n)} {m = zero} + (fst (gen-HⁿSⁿ-raw R (suc (suc n))) + (toSusp (S₊∙ (suc n)) z i)) r) + ∙ transportRefl _ + ∙ cong (cong (λ x → _⌣ₖ_ {n = suc (suc n)} {m = zero} x r)) + (cong-∙ (fst (gen-HⁿSⁿ-raw R (suc (suc n)))) + (merid z) (sym (merid (ptSn (suc n)))) + ∙ cong₂ _∙_ refl + (cong sym (cong (EM→ΩEM+1 (suc n)) + (gen-HⁿSⁿ-raw R (suc n) .snd) + ∙ EM→ΩEM+1-0ₖ (suc n))) + ∙ sym (rUnit _)) + ∙ sym (EM→ΩEM+1-distr⌣ₖ0 n (gen-HⁿSⁿ-raw R (suc n) .fst z) r)) + ∙ cong (EM→ΩEM+1 (suc n)) + (sym (transportRefl _) + ∙ λ i → subst (EM (Ring→AbGroup R)) + (isSetℕ (suc n) (suc n) refl (+'-comm (suc n) 0) i) + (_⌣ₖ_ {m = 0} (fst (gen-HⁿSⁿ-raw R (suc n)) z) r)) + +-- Main lemma: HⁿSⁿ-raw≃G-inv (i.e. ⌣ₖ is an equivalence) +isEquiv-HⁿSⁿ-raw≃G-inv : (R : Ring ℓ) (n : ℕ) + → isEquiv (HⁿSⁿ-raw≃G-inv R n) +isEquiv-HⁿSⁿ-raw≃G-inv R n = + composesToId→Equiv _ _ (funExt (HⁿSⁿ-raw≃G-inv-isInv R n)) + (HⁿSⁿ-raw≃G (Ring→AbGroup R) n .snd) diff --git a/Cubical/Cohomology/EilenbergMacLane/Gysin.agda b/Cubical/Cohomology/EilenbergMacLane/Gysin.agda new file mode 100644 index 0000000000..61c95b81e6 --- /dev/null +++ b/Cubical/Cohomology/EilenbergMacLane/Gysin.agda @@ -0,0 +1,1086 @@ +{-# OPTIONS --safe --lossy-unification #-} + +{- +This file contains +1. The Thom isomorphism (various related forms of it) +2. The Gysin sequence +-} + +module Cubical.Cohomology.EilenbergMacLane.Gysin where + +open import Cubical.Cohomology.EilenbergMacLane.Base +open import Cubical.Cohomology.EilenbergMacLane.Groups.Sn +open import Cubical.Cohomology.EilenbergMacLane.CupProduct + +open import Cubical.Homotopy.EilenbergMacLane.CupProduct +open import Cubical.Homotopy.EilenbergMacLane.CupProductTensor + renaming (_⌣ₖ_ to _⌣ₖ⊗_ ; ⌣ₖ-0ₖ to ⌣ₖ-0ₖ⊗ ; 0ₖ-⌣ₖ to 0ₖ-⌣ₖ⊗) +open import Cubical.Homotopy.Connected +open import Cubical.Homotopy.EilenbergMacLane.GradedCommTensor + hiding (⌣ₖ-comm) +open import Cubical.Homotopy.EilenbergMacLane.GroupStructure +open import Cubical.Homotopy.EilenbergMacLane.Base +open import Cubical.Homotopy.EilenbergMacLane.Properties +open import Cubical.Homotopy.Loopspace +open import Cubical.Homotopy.Group.Base + +open import Cubical.Functions.Morphism +open import Cubical.Functions.Embedding +open import Cubical.Functions.Surjection + +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.Transport +open import Cubical.Foundations.HLevels +open import Cubical.Foundations.Function +open import Cubical.Foundations.GroupoidLaws +open import Cubical.Foundations.Path +open import Cubical.Foundations.Equiv +open import Cubical.Foundations.Pointed +open import Cubical.Foundations.Pointed.Homogeneous +open import Cubical.Foundations.Isomorphism + +open import Cubical.HITs.PropositionalTruncation as PT +open import Cubical.HITs.SetTruncation as ST +open import Cubical.HITs.Truncation as TR +open import Cubical.HITs.Sn +open import Cubical.HITs.Pushout +open import Cubical.HITs.EilenbergMacLane1.Base +open import Cubical.HITs.Susp +open import Cubical.HITs.S1 + +open import Cubical.Data.Unit +open import Cubical.Data.Nat +open import Cubical.Data.Nat.Order hiding (eq) +open import Cubical.Data.Sigma +open import Cubical.Data.Bool hiding (_≤_) + +open import Cubical.Algebra.Group.Base +open import Cubical.Algebra.AbGroup.Base +open import Cubical.Algebra.Group.MorphismProperties +open import Cubical.Algebra.Group.Morphisms +open import Cubical.Algebra.Ring +open import Cubical.Algebra.CommRing + +open RingStr renaming (_+_ to _+r_) +open PlusBis + +private + variable + ℓ ℓ' ℓ'' : Level + +-- We show that a specific cup product is an +-- equivalence. This will induce the Thom isomorphism. +module ⌣Eq (R' : CommRing ℓ'') where + R = CommRing→Ring R' + RR = (CommRing→AbGroup R') + EMR = EM (CommRing→AbGroup R') + EMR∙ = EM∙ (CommRing→AbGroup R') + + -- current goal: show that the following map is an equivalence + pre-g : (n i : ℕ) → EMR i → S₊∙ n →∙ EMR∙ (i +' n) + fst (pre-g n i x) y = x ⌣ₖ gen-HⁿSⁿ-raw R n .fst y + snd (pre-g n i x) = + cong (x ⌣ₖ_) (gen-HⁿSⁿ-raw R n .snd) + ∙ ⌣ₖ-0ₖ i n x + + + -- We introduce some alternative versions of the map that + -- may be easier to work with in some situations. + g-comm : (n i : ℕ) → EMR i → S₊∙ n →∙ EMR∙ (n +' i) + fst (g-comm n i x) y = gen-HⁿSⁿ-raw R n .fst y ⌣ₖ x + snd (g-comm n i x) = + cong (_⌣ₖ x) (gen-HⁿSⁿ-raw R n .snd) + ∙ 0ₖ-⌣ₖ n i x + + g-cute : (n i : ℕ) → EMR i → S₊∙ n →∙ EMR∙ (i + n) + g-cute n i x = (subst EMR (+'≡+ i n) + , subst-EM-0ₖ (+'≡+ i n)) ∘∙ pre-g n i x + + indexIso₁ : (n i : ℕ) → EMR∙ (i + n) ≃∙ EMR∙ (n + i) + fst (indexIso₁ n i) = substEquiv EMR (+-comm i n) + snd (indexIso₁ n i) = subst-EM-0ₖ (+-comm i n) + + indexIso₂ : (n i : ℕ) → EMR∙ (n + i) ≃∙ EMR∙ (n +' i) + fst (indexIso₂ n i) = substEquiv EMR (sym (+'≡+ n i)) + snd (indexIso₂ n i) = subst-EM-0ₖ (sym (+'≡+ n i)) + + -ₖ^-iso : ∀ {ℓ} {G : AbGroup ℓ} {k : ℕ} (n m : ℕ) → Iso (EM G k) (EM G k) + Iso.fun (-ₖ^-iso n m) = -ₖ^[ n · m ] + Iso.inv (-ₖ^-iso n m) = -ₖ^[ n · m ] + Iso.rightInv (-ₖ^-iso n m) = -ₖ^< n · m >² _ _ _ + Iso.leftInv (-ₖ^-iso n m) = -ₖ^< n · m >² _ _ _ + + g-cute' : (n i : ℕ) → EMR i → S₊∙ n →∙ EMR∙ (n +' i) + g-cute' n i = + Iso.fun (pre∘∙equiv + (compEquiv∙ (isoToEquiv (-ₖ^-iso i n) , -ₖ^<_·_>∙ i n _ _ _) + (compEquiv∙ (indexIso₁ n i) (indexIso₂ n i)))) + ∘ g-cute n i + + g-cute≡ : (n i : ℕ) → g-cute' n i ≡ g-comm n i + g-cute≡ n i = funExt (λ x → →∙Homogeneous≡ (isHomogeneousEM (n +' i)) + (funExt λ y + → cong (subst EMR (sym (+'≡+ n i))) + (cong (subst EMR (+-comm i n)) + ((cong (-ₖ^[ i · n ]) + (cong (subst EMR (+'≡+ i n)) + (⌣ₖ-comm {G'' = R'} i n x (gen-HⁿSⁿ-raw R n .fst y)))))) + ∙ killTransp EMR -ₖ^[ i · n ] _ + (λ _ x → -ₖ^< i · n >² _ _ _ x) _ + (+'-comm n i) _ _ _ _ _ + (gen-HⁿSⁿ-raw R n .fst y ⌣ₖ x))) + where + killTransp : (A : ℕ → Type ℓ) (-ₖ_ : {n : ℕ} → A n → A n) (a : ℕ) + → ((n : ℕ) → (x : A n) → -ₖ (-ₖ x) ≡ x) + → (b : ℕ) + → (p : a ≡ b) (c : ℕ) (q : b ≡ c) (d : ℕ) (r : c ≡ d) (s : d ≡ a) + → (base : A a) + → subst A s (subst A r (-ₖ subst A q (subst A p (-ₖ base)))) ≡ base + killTransp A f i a = J> (J> (J> λ p b + → cong (subst A p) + (transportRefl _ ∙ cong f (transportRefl _ ∙ transportRefl _) + ∙ a _ b) + ∙ (λ i → subst A (isSetℕ _ _ p refl i) b) + ∙ transportRefl b)) + + isEquivBiImpl : (n i : ℕ) + → (isEquiv (g-comm n i) → isEquiv (g-cute n i)) + × (isEquiv (g-cute n i) → isEquiv (g-comm n i)) + fst (isEquivBiImpl n i) eq = + subst isEquiv + (funExt (λ x → secEq e (g-cute n i x))) + (compEquiv (_ , subst isEquiv (sym (g-cute≡ n i)) eq) e .snd) + where + e = isoToEquiv (invIso (pre∘∙equiv + (compEquiv∙ (isoToEquiv (-ₖ^-iso i n) , -ₖ^<_·_>∙ i n _ _ _) + (compEquiv∙ (indexIso₁ n i) (indexIso₂ n i))))) + snd (isEquivBiImpl n i) eq = + subst isEquiv (g-cute≡ n i) + (compEquiv + (_ , eq) + (isoToEquiv (pre∘∙equiv + (compEquiv∙ (isoToEquiv (-ₖ^-iso i n) , -ₖ^<_·_>∙ i n _ _ _) + (compEquiv∙ (indexIso₁ n i) (indexIso₂ n i))))) .snd) + + isEquiv-lem : (n i : ℕ) + → isEquiv (cong {x = 0ₖ (suc i)} {y = 0ₖ (suc i)} + (g-cute n (suc i))) + → (x y : EMR (suc i)) + → isEquiv (cong {x = x} {y = y} (g-cute n (suc i))) + isEquiv-lem n i p = + EM→Prop (Ring→AbGroup R) i (λ _ → isPropΠ λ _ → isPropIsEquiv _) + (EM→Prop (Ring→AbGroup R) i (λ _ → isPropIsEquiv _) + p) + + ΩFunIso : (n i : ℕ) (f : S₊∙ n →∙ EMR∙ (suc (i + n))) + → Iso (f ≡ f) + (S₊∙ n →∙ EMR∙ (i + n)) + fst (Iso.fun (ΩFunIso n i f) st) x = + ΩEM+1→EM-gen (i + n) _ (funExt⁻ (cong fst st) x) + snd (Iso.fun (ΩFunIso n i f) st) = + (λ j → ΩEM+1→EM-gen (i + n) (snd f j) λ i → snd (st i) j) + ∙ ΩEM+1→EM-gen-refl (i + n) _ + Iso.inv (ΩFunIso n i f) st = + ΣPathP ((funExt (λ x → EM→ΩEM+1-gen _ (fst f x) (fst st x))) + , flipSquare ((λ j → EM→ΩEM+1-gen (i + n) (snd f j) (snd st j)) + ▷ (EM→ΩEM+1-gen-0ₖ (i + n) _ + ∙ EM→ΩEM+1-0ₖ (i + n)))) + Iso.rightInv (ΩFunIso n i f) st = + →∙Homogeneous≡ (isHomogeneousEM _) + (funExt λ x + → Iso.leftInv (Iso-EM-ΩEM+1-gen (i + n) (fst f x)) (st .fst x)) + Iso.leftInv (ΩFunIso n i f) st = + →∙HomogeneousSquare (isHomogeneousEM _) + refl refl (Iso.inv (ΩFunIso n i f) + (Iso.fun (ΩFunIso n i f) st)) st + (cong funExt (funExt + λ x → Iso.rightInv + (Iso-EM-ΩEM+1-gen (i + n) (fst f x)) λ i → st i .fst x)) + + g-cute-ind : (n i : ℕ) + → g-cute n i + ≡ Iso.fun (ΩFunIso n i (g-cute n (suc i) (0ₖ (suc i)))) + ∘ cong {x = 0ₖ (suc i)} {y = 0ₖ (suc i)} (g-cute n (suc i)) + ∘ EM→ΩEM+1 i + g-cute-ind zero zero = + funExt λ x → →∙Homogeneous≡ (isHomogeneousEM {G = Ring→AbGroup R} 0) + (funExt λ y → transportRefl _ + ∙ sym ((λ j → ΩEM+1→EM 0 + (λ i → transportRefl (_⌣ₖ_ {n = 1} {m = 0} + (EM→ΩEM+1 0 x i) + (gen-HⁿSⁿ-raw R zero .fst y)) j)) + ∙ Iso.leftInv (Iso-EM-ΩEM+1 0) + (_⌣ₖ_ {n = 0} {m = 0} x (gen-HⁿSⁿ-raw R zero .fst y)))) + g-cute-ind zero (suc i) = + funExt λ x → →∙Homogeneous≡ (isHomogeneousEM _) + (funExt λ y → + sym (cong (ΩEM+1→EM (suc i + zero)) + (cong (cong (subst EMR (cong suc (+'≡+ (suc i) zero)))) + (sym (EM→ΩEM+1-distr⌣ₖ0 i x (gen-HⁿSⁿ-raw R zero .fst y)))) + ∙∙ (λ j → transp (λ s → EMR (+'≡+ (suc i) zero (s ∨ ~ j))) (~ j) + (ΩEM+1→EM (+'≡+ (suc i) zero (~ j)) + λ k → transp (λ s → EMR (suc (+'≡+ (suc i) zero (s ∧ ~ j)))) + j + (EM→ΩEM+1 (suc i) (_⌣ₖ_ {n = suc i} {m = zero} + x (gen-HⁿSⁿ-raw R zero .fst y)) k))) + ∙∙ cong (subst EMR (λ i₁ → suc (+-zero i (~ i₁)))) + (Iso.leftInv (Iso-EM-ΩEM+1 (suc i)) _))) + g-cute-ind (suc n) zero = funExt λ x → →∙Homogeneous≡ (isHomogeneousEM _) + (funExt λ y + → transportRefl _ + ∙ sym (cong (ΩEM+1→EM (suc n)) + ((λ k j → subst EMR (+'≡+ (suc zero) (suc n)) + (sym (EM→ΩEM+1-distr⌣ₖ0n n x + (gen-HⁿSⁿ-raw R (suc n) .fst y)) k j)) + ∙ (λ j → transp (λ i → Ω (EMR∙ (+'≡+ (suc zero) (suc n) (i ∨ j))) .fst) + (~ j) + λ k → transp (λ i → EMR (+'≡+ (suc zero) (suc n) (i ∨ ~ j))) + j (EM→ΩEM+1 (suc n) + (x ⌣[ R , 0 , (suc n) ]ₖ gen-HⁿSⁿ-raw R (suc n) .fst y) k)) + ∙ (λ j → subst (λ n → Ω (EMR∙ n) .fst) + (isSetℕ (suc (suc n)) (suc (suc n)) + (+'≡+ (suc zero) (suc n)) refl j) + (EM→ΩEM+1 (suc n) + (x ⌣[ R , 0 , (suc n) ]ₖ gen-HⁿSⁿ-raw R (suc n) .fst y))) + ∙ transportRefl _) + ∙ Iso.leftInv (Iso-EM-ΩEM+1 (suc n)) _)) + g-cute-ind (suc n) (suc i) = + funExt λ x → →∙Homogeneous≡ (isHomogeneousEM _) + (funExt λ y + → sym ((cong (ΩEM+1→EM (suc i + suc n))) + (cong (cong (subst EMR (+'≡+ (suc (suc i)) (suc n)))) + (sym (EM→ΩEM+1-distr⌣ₖ i n x (gen-HⁿSⁿ-raw R (suc n) .fst y)))) + ∙ (λ j → transp (λ s → EMR (suc (+-suc i n (j ∧ ~ s)))) (~ j) + ((ΩEM+1→EM (suc (+-suc i n j)) + (λ k → transp (λ s → EMR (suc (suc (+-suc i n (~ s ∨ j))))) + j (EM→ΩEM+1 (suc (suc (i + n))) + (x ⌣ₖ gen-HⁿSⁿ-raw R (suc n) .fst y) k))))) + ∙ cong (subst EMR (λ i₁ → suc (+-suc i n (~ i₁)))) + (Iso.leftInv (Iso-EM-ΩEM+1 (suc i +' suc n)) + (x ⌣ₖ gen-HⁿSⁿ-raw R (suc n) .fst y)))) + + g-ind-main : (n i : ℕ) + → isEquiv (g-cute n i) → isEquiv (g-cute n (suc i)) + g-ind-main n i eq = + isEmbedding×isSurjection→isEquiv + ((λ x y → isEquiv-lem n i + (subst isEquiv (sym help) + (myEq .snd)) + x y) + , λ f → PT.map + (λ p → subst (fiber (g-cute n (suc i))) (sym p) + ((0ₖ (suc i)) , (→∙Homogeneous≡ (isHomogeneousEM _) + (funExt λ x → cong (subst EMR (+'≡+ (suc i) n)) + (0ₖ-⌣ₖ (suc i) n (gen-HⁿSⁿ-raw R n .fst x)) + ∙ subst-EM-0ₖ (+'≡+ (suc i) n))))) + (Iso.fun PathIdTrunc₀Iso + (isContr→isProp (help2 i n) ∣ f ∣₂ (0ₕ∙ _)))) + where + myEq = compEquiv (isoToEquiv (invIso (Iso-EM-ΩEM+1 i))) + (compEquiv (g-cute n i , eq) + (isoToEquiv + (invIso (ΩFunIso n i (g-cute n (suc i) (0ₖ (suc i))))))) + + help : cong (g-cute n (suc i)) + ≡ myEq .fst + help = funExt + (λ p → sym + (Iso.leftInv (ΩFunIso n i (g-cute n (suc i) (0ₖ (suc i)))) _ + ∙ cong (cong (g-cute n (suc i))) + (Iso.rightInv (Iso-EM-ΩEM+1 i) _))) + ∙ sym (cong + (λ f → Iso.inv (ΩFunIso n i (g-cute n (suc i) (0ₖ (suc i)))) + ∘ f ∘ ΩEM+1→EM i) + (g-cute-ind n i)) + + help2 : (i n : ℕ) → isContr (∥ S₊∙ n →∙ EMR∙ (suc (i + n)) ∥₂) + help2 i zero = 0ₕ∙ _ + , ST.elim + (λ _ → isSetPathImplicit) + λ f → TR.rec (isProp→isOfHLevelSuc (i + zero) (squash₂ _ _)) + (λ p → cong ∣_∣₂ (→∙Homogeneous≡ (isHomogeneousEM _) + (funExt λ { false → sym p ; true → sym (snd f)}))) + (Iso.fun (PathIdTruncIso _) + (isContr→isProp (isConnectedEM (suc (i + zero))) + ∣ fst f false ∣ ∣ (0ₖ _) ∣)) + help2 i (suc n) = + isOfHLevelRetractFromIso 0 + (equivToIso (compEquiv + (invEquiv + (coHom≅coHomRed _ (Ring→AbGroup R) (S₊∙ (suc n)) .fst)) + (fst (Hᵐ⁺ⁿ[Sⁿ,G]≅0 (Ring→AbGroup R) n i)))) + isContrUnit* + + g-cute-equiv : (i n : ℕ) → isEquiv (g-cute n i) + g-cute-equiv zero n = isEquivBiImpl n zero .fst + (subst isEquiv (sym pth) + (snd alt-eq)) + where + alt-eq : EMR zero ≃ (S₊∙ n →∙ EMR∙ (n +' zero)) + alt-eq = compEquiv (HⁿSⁿ-raw≃G-inv R n , isEquiv-HⁿSⁿ-raw≃G-inv R n) + (isoToEquiv (pre∘∙equiv + (substEquiv EMR (sym (+'-comm n zero)) , subst-EM-0ₖ _))) + pth : g-comm n zero ≡ alt-eq .fst + pth = funExt (λ r → →∙Homogeneous≡ (isHomogeneousEM _) + (funExt λ x → sym (subst⁻Subst EMR (+'-comm n zero) + (gen-HⁿSⁿ-raw R n .fst x ⌣ₖ r)))) + g-cute-equiv (suc i) n = g-ind-main n i (g-cute-equiv i n) + + -- main lemma + g-equiv : (n i : ℕ) → isEquiv (pre-g n i) + g-equiv n i = subst isEquiv pth (snd help) + where + help : EMR i ≃ (S₊∙ n) →∙ EMR∙ (i +' n) + help = compEquiv (_ , g-cute-equiv i n) + (isoToEquiv + (pre∘∙equiv + (substEquiv EMR (sym (+'≡+ i n)) + , subst-EM-0ₖ (sym (+'≡+ i n))))) + + pth : fst help ≡ pre-g n i + pth = funExt (λ r → →∙Homogeneous≡ (isHomogeneousEM _) + (funExt λ y + → subst⁻Subst EMR (+'≡+ i n) + (r ⌣ₖ gen-HⁿSⁿ-raw R n .fst y))) + +-- We may use the above to construct the (generalised) Thom +-- isomorphism (over a fibration with 0-connected base space) +module preThom + (B : Pointed ℓ) + (Q : fst B → Pointed ℓ') + (conB : isConnected 2 (fst B)) + (R : CommRing ℓ'') + (n : ℕ) + (e : Q (snd B) ≃∙ S₊∙ n) + (c : (b : fst B) → Q b →∙ EM∙ (CommRing→AbGroup R) n) + (r : c (pt B) ≡ (gen-HⁿSⁿ-raw (CommRing→Ring R) n ∘∙ ≃∙map e)) + where + RR = (CommRing→AbGroup R) + EMR = EM RR + EMR∙ = EM∙ RR + + -- Generalisation of previous map g + g : (i : ℕ) (b : fst B) → EMR i → Q b →∙ EMR∙ (i +' n) + fst (g i b x) y = x ⌣ₖ c b .fst y + snd (g i b x) = + cong (x ⌣ₖ_) (c b .snd) + ∙ ⌣ₖ-0ₖ i n x + + isEquiv-g-pt : (i : ℕ) → isEquiv (g i (pt B)) + isEquiv-g-pt i = subst isEquiv (sym help) (eq .snd) + where + eq : EMR i ≃ (Q (pt B) →∙ EMR∙ (i +' n)) + eq = compEquiv (⌣Eq.pre-g R n i , ⌣Eq.g-equiv R n i) + (isoToEquiv (post∘∙equiv (invEquiv∙ e))) -- + + help : g i (pt B) ≡ fst eq + help = funExt λ x → →∙Homogeneous≡ (isHomogeneousEM _) + (funExt λ y → cong (λ y → x ⌣[ R , i , n ]Cₖ y) + (funExt⁻ (cong fst r) y)) + + abstract + isEquiv-g : (i : ℕ) (b : fst B) → isEquiv (g i b) + isEquiv-g i = Iso.inv (elim.isIsoPrecompose + (λ (x : Unit) → pt B) 1 (λ b → isEquiv (g i b) , isPropIsEquiv _) + (isConnectedPoint 1 conB (pt B))) + λ _ → isEquiv-g-pt i + + g-equiv : (i : ℕ) (b : fst B) → EMR i ≃ Q b →∙ EMR∙ (i +' n) + g-equiv i b = g i b , isEquiv-g i b + + g⁻ : (i : ℕ) (b : fst B) → Q b →∙ EMR∙ (i +' n) → EMR i + g⁻ i b = invEq (g-equiv i b) + + private + g-pres+' : (i : ℕ) (b : fst B) (x y : EMR i) (z : _) + → g i b (x +ₖ y) .fst z ≡ (g i b x +ₖ∙ g i b y) .fst z + g-pres+' i b x y z = + distrR⌣ₖ {G'' = CommRing→Ring R} i n x y (c b .fst z) + + g-pres+ : (i : ℕ) (b : fst B) (x y : EMR i) + → g i b (x +ₖ y) ≡ g i b x +ₖ∙ g i b y + g-pres+ i b x y = →∙Homogeneous≡ (isHomogeneousEM (i +' n)) + (funExt (g-pres+' i b x y)) + + g⁻-pres+ : (i : ℕ) (b : fst B) (x y : _) + → g⁻ i b (x +ₖ∙ y) ≡ g⁻ i b x +ₖ g⁻ i b y + g⁻-pres+ i b = + morphLemmas.isMorphInv _+ₖ_ _+ₖ∙_ + (g i b) + (g-pres+ i b) + (g⁻ i b) + (secEq (g-equiv i b)) + (retEq (g-equiv i b)) + + pre-ϕ : (i : ℕ) → (fst B → EMR i) → (b : fst B) → Q b →∙ EMR∙ (i +' n) + fst (pre-ϕ i β b) x = β b ⌣ₖ c b .fst x + snd (pre-ϕ i β b) = cong (β b ⌣ₖ_) (c b .snd) + ∙ ⌣ₖ-0ₖ i n (β b) + + -- main results + pre-ϕIso : (i : ℕ) + → Iso (fst B → EMR i) ((b : fst B) → Q b →∙ EMR∙ (i +' n)) + Iso.fun (pre-ϕIso i) = pre-ϕ i + Iso.inv (pre-ϕIso i) r b = invEq (g-equiv i b) (r b) + Iso.rightInv (pre-ϕIso i) t j b = secEq (g-equiv i b) (t b) j + Iso.leftInv (pre-ϕIso i) t j b = retEq (g-equiv i b) (t b) j + + pre-ϕ-pres+ : (i : ℕ) → (f g : fst B → EMR i) + → pre-ϕ i (λ b → f b +ₖ g b) ≡ λ b → pre-ϕ i f b +ₖ∙ pre-ϕ i g b + pre-ϕ-pres+ i f g = funExt (λ b → →∙Homogeneous≡ (isHomogeneousEM _) + (funExt (g-pres+' i b (f b) (g b)))) + + pre-ϕ⁻-pres+ : (i : ℕ) (f g : (b : fst B) → Q b →∙ EMR∙ (i +' n)) + → Iso.inv (pre-ϕIso i) (λ b → f b +ₖ∙ g b) + ≡ λ b → (Iso.inv (pre-ϕIso i) f b) +ₖ (Iso.inv (pre-ϕIso i) g b) + pre-ϕ⁻-pres+ i f g = funExt (λ b → g⁻-pres+ i b (f b) (g b)) + + isEq-ϕ : (i : ℕ) → isEquiv (pre-ϕ i) + isEq-ϕ i = isoToIsEquiv (pre-ϕIso i) + +-- The (generalised) Thom isomorphism for a fibration with a simply +-- connected base space. +module genThom (B : Pointed ℓ) + (Q : fst B → Pointed ℓ') + (conB : isConnected 3 (fst B)) + (R : CommRing ℓ'') + (n : ℕ) + (e : Q (snd B) ≃∙ S₊∙ n) where + private + RR = (CommRing→AbGroup R) + EMR = EM RR + EMR∙ = EM∙ RR + + Q*→EM : Q (pt B) →∙ EMR∙ n + Q*→EM = gen-HⁿSⁿ-raw (CommRing→Ring R) n ∘∙ ≃∙map e + + private + module hlevcon = + isConnectedPoint 2 conB + (λ a → isProp→isSet ( + isPropIsOfHLevel {A = (Q a →∙ EMR∙ n)} 2)) + (pt B , isOfHLevelRetractFromIso 2 + (post∘∙equiv e) + (isSet-Sn→∙EM RR n)) + + module con = + isConnectedPoint 2 conB + hlevcon.elim ((pt B) , Q*→EM) + + isSetQ→ : (b : fst B) → isSet (Q b →∙ EMR∙ n) + isSetQ→ = hlevcon.elim + + c : (b : fst B) → Q b →∙ EMR∙ n + c = con.elim + + c-id : c (pt B) ≡ Q*→EM + c-id = con.β + + module preThom-inst = + preThom B Q (isConnectedSubtr 2 1 conB) R n e c c-id + + g : (i : ℕ) (b : fst B) → EMR i → Q b →∙ EMR∙ (i +' n) + g = preThom-inst.g + + isEquiv-g : (i : ℕ) (b : fst B) → isEquiv (g i b) + isEquiv-g i b = preThom-inst.g-equiv i b .snd + + ϕ : (i : ℕ) → (fst B → EMR i) → (b : fst B) → Q b →∙ EMR∙ (i +' n) + ϕ = preThom-inst.pre-ϕ + + isEquivϕ : (i : ℕ) → isEquiv (ϕ i) + isEquivϕ = preThom-inst.isEq-ϕ + + ϕIso : (i : ℕ) + → Iso (fst B → EMR i) ((b : fst B) → Q b →∙ EMR∙ (i +' n)) + ϕIso = preThom-inst.pre-ϕIso + +-- Now for the 'true' Thom isomphism: +module Thom (B : Pointed ℓ) + (P : fst B → Type ℓ') + (P* : P (pt B)) + (conB : isConnected 2 (fst B)) + (R : CommRing ℓ'') + where + private + RR = (CommRing→AbGroup R) + EMR = EM RR + EMR∙ = EM∙ RR + * = snd B + + E = Σ[ x ∈ fst B ] (P x) + + E∙ : Pointed _ + fst E∙ = E + snd E∙ = * , P* + + πE : E → fst B + πE = fst + + -- goal: relate cohomology of B to cohomology of + -- the cofibre of πE: + EP : Type _ + EP = Pushout (λ _ → tt) πE + + EP∙ : Pointed _ + fst EP∙ = EP + snd EP∙ = inr (pt B) + + EP-contr : isContr E → Iso EP (fst B) + Iso.fun (EP-contr c) (inl x) = pt B + Iso.fun (EP-contr c) (inr x) = x + Iso.fun (EP-contr c) (push a i) = πE (isContr→isProp c (* , P*) a i) + Iso.inv (EP-contr c) = inr + Iso.rightInv (EP-contr c) = λ _ → refl + Iso.leftInv (EP-contr c) (inl x) = sym (push (* , P*)) + Iso.leftInv (EP-contr c) (inr x) = refl + Iso.leftInv (EP-contr c) (push a i) j = + hcomp (λ k → λ {(i = i0) → push (* , P*) (~ j) + ; (i = i1) → push a (~ j ∨ k) + ; (j = i0) → inr (πE (isContr→isProp c (* , P*) a i)) + ; (j = i1) → push a (i ∧ k)}) + (push (isContr→isProp c (* , P*) a i) (~ j)) + + -- Main goal: establish ((b : fst B) → Q b →∙ EMR∙ k) ≃ (EP∙ →∙ EMR∙ k) + -- Combined with the previous isos, this gives the Thom isomorphism + -- Hⁱ(B,R) ≃ Hⁱ⁺ⁿ(EP∙,R) + Q : fst B → Pointed ℓ' + Q b = Susp (P b) , north + + F = Σ[ x ∈ fst B ] (Q x .fst) + + B→F : fst B → F + B→F b = b , north + + FP : Type _ + FP = Pushout (λ _ → tt) B→F + + FP∙ : Pointed _ + fst FP∙ = FP + snd FP∙ = inr (pt B , north) + + -- step 1: show EP∙ ≃ FP∙, and thus (EP∙ →∙ EMR∙ k) ≃ (FP∙ →∙ EMR∙ k) + EP→FP : EP → FP + EP→FP (inl x) = inl x + EP→FP (inr x) = inr (x , south) + EP→FP (push (e , p) i) = + (push e ∙ λ j → inr (e , merid p j)) i + + FP→EP : FP → EP + FP→EP (inl x) = inl x + FP→EP (inr (x , north)) = inl tt + FP→EP (inr (x , south)) = inr x + FP→EP (inr (x , merid a i)) = push (x , a) i + FP→EP (push a i) = inl tt + + Iso-EP-FP : Iso EP FP + Iso.fun Iso-EP-FP = EP→FP + Iso.inv Iso-EP-FP = FP→EP + Iso.rightInv Iso-EP-FP (inl x) = refl + Iso.rightInv Iso-EP-FP (inr (x , north)) = push x + Iso.rightInv Iso-EP-FP (inr (x , south)) = refl + Iso.rightInv Iso-EP-FP (inr (x , merid a i)) j = + compPath-filler' (push x) (λ j₁ → inr (x , merid a j₁)) (~ j) i + Iso.rightInv Iso-EP-FP (push a i) j = push a (i ∧ j) + Iso.leftInv Iso-EP-FP (inl x) = refl + Iso.leftInv Iso-EP-FP (inr x) = refl + Iso.leftInv Iso-EP-FP (push (b , p) i) j = + (cong-∙ FP→EP (push b) (λ j → inr (b , merid p j)) + ∙ sym (lUnit (push (b , p)))) j i + + EP∙≃FP∙ : EP∙ ≃∙ FP∙ + fst EP∙≃FP∙ = isoToEquiv Iso-EP-FP + snd EP∙≃FP∙ i = inr (pt B , merid P* (~ i)) + + -- step 2: show (FP∙ →∙ A) ≃ ((b : fst B) → Q b →∙ A) for any pointed type A + -- (taken homogeneous for convenience) + mapIso : ∀ {ℓ} {A : Pointed ℓ} + → (isHomogeneous A) + → Iso ((FP , inr ((pt B) , north)) →∙ A) + ((b : fst B) → Q b →∙ A) + fst (Iso.fun (mapIso isHom) r b) y = fst r (inr (b , y)) + snd (Iso.fun (mapIso isHom) r b) = + cong (fst r) (sym (push b) ∙ push (snd B)) ∙ snd r + fst (Iso.inv (mapIso {A = A} isHom) r) (inl x) = pt A + fst (Iso.inv (mapIso isHom) r) (inr (b , p)) = r b .fst p + fst (Iso.inv (mapIso isHom) r) (push a i) = r a .snd (~ i) + snd (Iso.inv (mapIso isHom) r) = r (pt B) .snd + Iso.rightInv (mapIso isHom) r = funExt λ b → →∙Homogeneous≡ isHom refl + Iso.leftInv (mapIso isHom) r = + →∙Homogeneous≡ isHom + (funExt λ { (inl x) → sym (snd r) ∙ cong (fst r) (sym (push (pt B))) + ; (inr x) → refl + ; (push a i) j → h a i j}) + where + h : (a : fst B) + → Square (sym (snd r) ∙ cong (fst r) (sym (push (pt B)))) + refl + (sym (cong (fst r) + (sym (push a) ∙ push (pt B)) ∙ snd r)) + (cong (r .fst) (push a)) + h a = flipSquare + ((symDistr (cong (fst r) (sym (push a) ∙ push (pt B))) + (snd r) + ∙∙ cong (sym (snd r) ∙_) + (cong (cong (fst r)) (symDistr (sym (push a)) (push (pt B))) + ∙ cong-∙ (fst r) (sym (push (pt B))) (push a)) + ∙∙ assoc (sym (snd r)) + (cong (fst r) (sym (push (pt B)))) + (cong (fst r) (push a))) + ◁ flipSquare + λ i j → compPath-filler' (sym (snd r) + ∙ cong (fst r) (sym (push (pt B)))) + (cong (fst r) (push a)) (~ j) i) + + -- We get our first iso + ι : (k : ℕ) → Iso ((b : fst B) → Q b →∙ EMR∙ k) (EP∙ →∙ EMR∙ k) + ι k = + compIso (invIso (mapIso (isHomogeneousEM _))) + (post∘∙equiv (invEquiv∙ EP∙≃FP∙)) + + -- we need it to be structure preserving in the obvious way + ι⁻-pres+ : (k : ℕ) (f g : EP∙ →∙ EMR∙ k) + → Iso.inv (ι k) (f +ₖ∙ g) ≡ + λ b → (Iso.inv (ι k) f b) +ₖ∙ (Iso.inv (ι k) g b) + ι⁻-pres+ k f g = funExt λ b + → →∙Homogeneous≡ + (isHomogeneousEM k) + (funExt λ { north → refl + ; south → refl + ; (merid a i) → refl}) + + ι-pres+ : (k : ℕ) (f g : (b : fst B) → Q b →∙ EMR∙ k) + → Iso.fun (ι k) (λ b → f b +ₖ∙ g b) + ≡ Iso.fun (ι k) f +ₖ∙ Iso.fun (ι k) g + ι-pres+ k = morphLemmas.isMorphInv _+ₖ∙_ (λ f g b → f b +ₖ∙ g b) + (Iso.inv (ι k)) (ι⁻-pres+ k) + (Iso.fun (ι k)) + (Iso.leftInv (ι k)) (Iso.rightInv (ι k)) + + -- We combine it with the generalised thom iso, in order to get the + -- usual Thom isomorphism + + module _ (n : ℕ) (e : (P (pt B) , P*) ≃∙ S₊∙ n) where + Q≃ : Q (pt B) ≃∙ S₊∙ (suc n) + Q≃ = compEquiv∙ + (isoToEquiv + (congSuspIso + (equivToIso (fst e))) , refl) + (isoToEquiv (invIso (IsoSucSphereSusp n)) + , IsoSucSphereSusp∙ n) + + module con (c : (b : fst B) → Q b →∙ EM∙ (CommRing→AbGroup R) (suc n)) + (r : c (pt B) ≡ (gen-HⁿSⁿ-raw (CommRing→Ring R) (suc n) ∘∙ ≃∙map Q≃)) + where + module M = preThom B Q conB R (suc n) Q≃ c r + + -- Finally, the actual Thom ismorphism + ϕ-raw : (i : ℕ) → (fst B → EMR i) ≃ (EP∙ →∙ EMR∙ (i +' suc n)) + ϕ-raw i = isoToEquiv (compIso (M.pre-ϕIso i) (ι (i +' (suc n)))) + + ϕ-equiv : (i : ℕ) → coHom i RR (fst B) ≃ coHomRed (i +' suc n) RR EP∙ + ϕ-equiv i = + isoToEquiv (setTruncIso (compIso (M.pre-ϕIso i) (ι (i +' (suc n))))) + + ϕ-raw-contr : (i : ℕ) → isContr E → (fst B → EMR i) ≃ (B →∙ EMR∙ (i +' suc n)) + ϕ-raw-contr i contr = + compEquiv (ϕ-raw i) + (isoToEquiv (post∘∙equiv (isoToEquiv (EP-contr contr) , refl))) + + ϕ : (i : ℕ) → coHom i RR (fst B) → coHomRed (i +' suc n) RR EP∙ + ϕ i = ϕ-equiv i .fst + + isHomϕ : (i : ℕ) + → (x y : coHom i RR (fst B)) → ϕ i (x +ₕ y) ≡ ϕ i x +ₕ∙ ϕ i y + isHomϕ i = + ST.elim2 (λ _ _ → isSetPathImplicit) + λ f g → cong ∣_∣₂ (cong (Iso.fun (ι (i +' suc n))) + (M.pre-ϕ-pres+ i f g) + ∙ ι-pres+ (i +' suc n) + (λ b → M.g i b (f b)) (λ b → M.g i b (g b)) + ∙ →∙Homogeneous≡ (isHomogeneousEM (i +' suc n)) refl) + + ϕHom : (i : ℕ) → AbGroupHom (coHomGr i RR (fst B)) + (coHomRedGr (i +' suc n) RR EP∙) + fst (ϕHom i) = ϕ i + snd (ϕHom i) = makeIsGroupHom (isHomϕ i) + + ϕGrEquiv : (i : ℕ) → AbGroupEquiv (coHomGr i RR (fst B)) + (coHomRedGr (i +' suc n) RR EP∙) + fst (ϕGrEquiv i) = ϕ-equiv i + snd (ϕGrEquiv i) = ϕHom i .snd + + -- For the Gysin sequence, we will be need the long exact sequence + -- in cohomology related to the cofibre EP∙, i.e. + -- ... → Hⁱ⁻¹(E,R) → H̃ⁱ(EP∙,R) → Hⁱ(B,R) → Hⁱ(E,R) → ... + pre-E↑ : (i : ℕ) → (E → EM RR i) → EP∙ →∙ EM∙ RR (suc i) + fst (pre-E↑ i f) (inl x) = 0ₖ (suc i) + fst (pre-E↑ i f) (inr x) = 0ₖ (suc i) + fst (pre-E↑ i f) (push a i₁) = EM→ΩEM+1 i (f a) i₁ + snd (pre-E↑ i f) = refl + + E↑ : (i : ℕ) → AbGroupHom (coHomGr i RR E) (coHomRedGr (suc i) RR EP∙) + fst (E↑ i) = ST.map (pre-E↑ i) + snd (E↑ i) = + makeIsGroupHom + (ST.elim2 (λ _ _ → isSetPathImplicit) + λ f g → cong ∣_∣₂ + (→∙Homogeneous≡ (isHomogeneousEM (suc i)) + (funExt λ { (inl x) → sym (rUnitₖ (suc i) (0ₖ (suc i))) + ; (inr x) → sym (rUnitₖ (suc i) (0ₖ (suc i))) + ; (push a j) → flipSquare (help i (f a) (g a)) j}))) + where + help : (i : ℕ) (x y : EM RR i) + → PathP (λ j → rUnitₖ {G = RR} (suc i) (0ₖ (suc i)) (~ j) + ≡ rUnitₖ (suc i) (0ₖ (suc i)) (~ j)) + (EM→ΩEM+1 {G = RR} i (x +ₖ y)) + (cong₂ _+ₖ_ (EM→ΩEM+1 i x) (EM→ΩEM+1 i y)) + help zero x y = EM→ΩEM+1-hom zero x y + ∙ sym (cong₂+₁ (EM→ΩEM+1 zero x) (EM→ΩEM+1 zero y)) + help (suc n) x y = EM→ΩEM+1-hom (suc n) x y + ∙ sym (cong₂+₂ n (EM→ΩEM+1 (suc n) x) + (EM→ΩEM+1 (suc n) y)) + + j* : (i : ℕ) → AbGroupHom (coHomRedGr i RR EP∙) (coHomGr i RR (fst B)) + fst (j* i) = ST.map λ f b → fst f (inr b) + snd (j* i) = makeIsGroupHom + (ST.elim2 (λ _ _ → isSetPathImplicit) λ f g → refl) + + p* : (i : ℕ) → AbGroupHom (coHomGr i RR (fst B)) (coHomGr i RR E) + p* i = coHomHom i fst + + Im-j*⊂Ker-p* : (i : ℕ) (x : _) + → isInIm (j* i) x + → isInKer (p* i) x + Im-j*⊂Ker-p* i = + ST.elim + (λ f → isSetΠ λ _ → isSetPathImplicit) + λ f → PT.rec (squash₂ _ _) + (uncurry (ST.elim (λ _ → isSetΠ + λ _ → isSetPathImplicit) + λ g p → PT.rec (squash₂ _ _) + (J (λ f _ → isInKer (p* i) ∣ f ∣₂) + (cong ∣_∣₂ (funExt (λ a + → cong (fst g) (sym (push a) ∙ push (pt B , P*)) + ∙ snd g)))) + (Iso.fun PathIdTrunc₀Iso p))) + + Ker-p*⊂Im-j* : (i : ℕ) (x : _) + → isInKer (p* i) x + → isInIm (j* i) x + Ker-p*⊂Im-j* i = + ST.elim (λ _ → isSetΠ λ _ → isProp→isSet squash₁) + λ f p → PT.map + (λ p → ∣ (λ { (inl x) → 0ₖ i + ; (inr x) → f x + ; (push a i) → p (~ i) a}) + , funExt⁻ p (pt B , P*) ∣₂ + , refl) + (Iso.fun PathIdTrunc₀Iso p) + + Im-p*⊂Ker-E↑ : (i : ℕ) (x : _) + → isInIm (p* i) x + → isInKer (E↑ i) x + Im-p*⊂Ker-E↑ i = ST.elim + (λ f → isSetΠ λ _ → isSetPathImplicit) + λ f → PT.rec (squash₂ _ _) + (uncurry (ST.elim (λ _ → isSetΠ + λ _ → isSetPathImplicit) + λ g p → PT.rec (squash₂ _ _) + (J (λ f _ → isInKer (E↑ i) ∣ f ∣₂) + (cong ∣_∣₂ (→∙Homogeneous≡ (isHomogeneousEM _) + (funExt λ { (inl x) → refl + ; (inr x) → sym (EM→ΩEM+1 i (g x)) + ; (push a j) k + → EM→ΩEM+1 i (g (fst a)) (j ∧ ~ k)})))) + (Iso.fun PathIdTrunc₀Iso p))) + + Ker-E↑⊂Im-p* : (i : ℕ) (x : _) + → isInKer (E↑ i) x + → isInIm (p* i) x + Ker-E↑⊂Im-p* i = + ST.elim (λ _ → isSetΠ λ _ → isProp→isSet squash₁) + λ f p → PT.map (λ r → + ∣ (λ b → ΩEM+1→EM i (sym (funExt⁻ (cong fst r) (inr b))) + +ₖ f (* , P*)) ∣₂ + , cong ∣_∣₂ (funExt λ {(x , p) + → cong (_+ₖ f (* , P*)) + ((cong (ΩEM+1→EM i) + (cong sym (sym (fromPathP (cong (funExt⁻ (cong fst r)) (push (x , p)))) + ∙ (λ j → transp (λ k → EM→ΩEM+1 i (f (x , p)) (j ∨ k) + ≡ 0ₖ (suc i)) + j (compPath-filler' + (sym (EM→ΩEM+1 i (f (x , p)))) + (funExt⁻ (cong fst r) (inl tt)) j))) + ∙ (symDistr (sym (EM→ΩEM+1 i (f (x , p)))) + (funExt⁻ (λ i₂ → fst (r i₂)) (inl tt)))) + ∙ ΩEM+1→EM-hom i + (sym (funExt⁻ (λ i₁ → fst (r i₁)) (inl tt))) + (EM→ΩEM+1 i (f (x , p)))) + ∙ cong₂ _+ₖ_ + (cong (ΩEM+1→EM i) + (cong sym + (rUnit _ ∙∙ sym (Square→compPath + ((cong (funExt⁻ (cong fst r)) (push (* , P*))) + ▷ λ i j → r j .snd i)) ∙∙ sym (rUnit _)))) + (Iso.leftInv (Iso-EM-ΩEM+1 i) (f (x , p)))) + ∙ cong₂ _+ₖ_ (cong₂ _+ₖ_ (cong (ΩEM+1→EM i) + (sym (EM→ΩEM+1-sym i (f (* , P*)))) + ∙ Iso.leftInv (Iso-EM-ΩEM+1 i) (-ₖ (f (* , P*)))) refl + ∙ commₖ i (-ₖ f (* , P*)) (f (x , p))) + refl + ∙ sym (assocₖ i (f (x , p)) (-ₖ (f (* , P*))) (f (* , P*))) + ∙ cong₂ _+ₖ_ refl (lCancelₖ i (f (* , P*))) + ∙ rUnitₖ i (f (x , p))})) + ((Iso.fun PathIdTrunc₀Iso p)) + + Im-E↑⊂Ker-j* : (i : ℕ) (x : _) + → isInIm (E↑ i) x + → isInKer (j* (suc i)) x + Im-E↑⊂Ker-j* i = ST.elim + (λ f → isSetΠ λ _ → isSetPathImplicit) + λ f → PT.rec (squash₂ _ _) + (uncurry (ST.elim (λ _ → isSetΠ + λ _ → isSetPathImplicit) + λ g p → PT.rec (squash₂ _ _) + (J (λ f _ → isInKer (j* (suc i)) ∣ f ∣₂) refl) + (Iso.fun PathIdTrunc₀Iso p))) + + Ker-j*⊂Im-E↑ : (i : ℕ) (x : _) + → isInKer (j* (suc i)) x + → isInIm (E↑ i) x + Ker-j*⊂Im-E↑ i = + ST.elim (λ _ → isSetΠ λ _ → isProp→isSet squash₁) + λ f p → PT.map + (λ p → ∣ (λ b → ΩEM+1→EM i (pth b f (funExt⁻ p))) ∣₂ + , cong ∣_∣₂ (→∙Homogeneous≡ (isHomogeneousEM _) + (funExt λ { (inl x) → sym (snd f) + ∙ cong (fst f) (sym (push (* , P*))) + ; (inr x) → sym (funExt⁻ p x) + ; (push a j) → main a f (funExt⁻ p) j}))) + (Iso.fun PathIdTrunc₀Iso p) + where + pth : (a : E) (f : EP∙ →∙ EM∙ RR (suc i)) + (p : (b : fst B) → fst f (inr b) ≡ 0ₖ (suc i)) + → fst (Ω (EMR∙ (suc i))) + pth a f p = sym (snd f) ∙ cong (fst f) (sym (push (* , P*))) + ∙∙ cong (fst f) (push a) + ∙∙ p (fst a) + + main : (a : E) (f : EP∙ →∙ EM∙ RR (suc i)) + (p : (b : fst B) → fst f (inr b) ≡ 0ₖ (suc i)) + → PathP (λ j → EM→ΩEM+1 i (ΩEM+1→EM i (pth a f p)) j + ≡ f .fst (push a j)) + (sym (snd f) ∙ cong (fst f) (sym (push (* , P*)))) + (sym (p (fst a))) + main a f p = + flipSquare (Iso.rightInv (Iso-EM-ΩEM+1 i) (pth a f p) + ◁ λ j i → doubleCompPath-filler + (sym (snd f) ∙ cong (fst f) (sym (push (* , P*)))) + (cong (fst f) (push a)) + (p (fst a)) (~ j) i) + +module Gysin (B : Pointed ℓ) + (P : fst B → Type ℓ') + (conB : isConnected 2 (fst B)) + (R : CommRing ℓ'') + (n : ℕ) + (eq' : P (pt B) ≃ S₊ n) + (c : (b : fst B) → Susp∙ (P b) →∙ EM∙ (CommRing→AbGroup R) (suc n)) + (c-id : c (pt B) ≡ gen-HⁿSⁿ-raw + (CommRing→Ring R) (suc n) + ∘∙ ≃∙map (Thom.Q≃ B P (invEq eq' (ptSn n)) + conB R n (eq' , (secEq eq' (ptSn n))))) + where + private + RR = (CommRing→AbGroup R) + EMR = EM RR + EMR∙ = EM∙ RR + P* = invEq eq' (ptSn n) + module M = Thom B P P* conB R + open M public + + eq : (P (pt B) , P*) ≃∙ S₊∙ n + fst eq = eq' + snd eq = secEq eq' (ptSn n) + + module _ (c-id : c (pt B) ≡ gen-HⁿSⁿ-raw (CommRing→Ring R) (suc n) ∘∙ ≃∙map (Q≃ n eq)) where + module L = con n eq c c-id + open L + + -- The Euler class + e : coHom (suc n) RR (fst B) + e = ∣ (λ b → c b .fst south) ∣₂ + + minusPath : (i : ℕ) → (suc n ≤ i) → (i ∸ suc n) +' suc n ≡ i + minusPath i p = +'≡+ (i ∸ suc n) (suc n) ∙ ≤-∸-+-cancel p + + -- The main map in the sequence + ⌣-hom : (i : ℕ) → (suc n ≤ i) + → AbGroupHom (coHomGr (i ∸ suc n) RR (fst B)) + (coHomGr i RR (fst B)) + fst (⌣-hom i t) f = + subst (λ i → coHom i RR (fst B)) (minusPath i t) (f ⌣ e) + snd (⌣-hom i t) = + makeIsGroupHom + (λ f g → cong (subst (λ i₁ → coHom i₁ RR (fst B)) (minusPath i t)) + (distrR⌣ (i ∸ suc n) (suc n) f g e) + ∙ IsGroupHom.pres· (snd (substℕ-coHom (minusPath i t))) + (f ⌣ e) (g ⌣ e)) + + private + helpIso : (i : ℕ) → suc n ≤ i + → AbGroupEquiv (coHomRedGr i RR EP∙) + (coHomGr (i ∸ suc n) RR (fst B)) + helpIso i t = + compGroupEquiv (substℕ-coHomRed (sym (minusPath i t))) + (invGroupEquiv (ϕGrEquiv (i ∸ suc n))) + + alt-hom : (i : ℕ) → (suc n ≤ i) + → AbGroupHom (coHomGr (i ∸ suc n) RR (fst B)) + (coHomGr i RR (fst B)) + alt-hom i t = + compGroupHom (ϕHom (i ∸ suc n)) + (compGroupHom (j* _) + (GroupEquiv→GroupHom (substℕ-coHom (minusPath i t)))) + + ⌣≡alt : (i : ℕ) (t : suc n ≤ i) + → ⌣-hom i t ≡ alt-hom i t + ⌣≡alt i t = Σ≡Prop (λ _ → isPropIsGroupHom _ _) + (funExt (ST.elim (λ _ → isSetPathImplicit) λ _ → refl)) + + + -- the other two maps + mapₗ : (i : ℕ) → suc n ≤ suc i + → AbGroupHom (coHomGr i RR E) + (coHomGr (suc i ∸ suc n) RR (fst B)) + mapₗ i t = + compGroupHom (E↑ i) + (GroupEquiv→GroupHom + (helpIso (suc i) t)) + + mapᵣ : (i : ℕ) + → AbGroupHom (coHomGr i RR (fst B)) + (coHomGr i RR E) + mapᵣ i = p* i + + + -- Finally: exactness + Im-mapᵣ⊂Ker-mapₗ : (i : ℕ) (t : suc n ≤ suc i) (x : coHom i RR E) + → isInIm (mapᵣ i) x + → isInKer (mapₗ i t) x + Im-mapᵣ⊂Ker-mapₗ i t x s = + cong (invEq (fst (ϕGrEquiv (suc i ∸ suc n)))) + (cong (subst (λ i → coHomRed i RR EP∙) (sym (minusPath (suc i) t))) + (M.Im-p*⊂Ker-E↑ i x s)) + ∙ IsGroupHom.pres1 (helpIso (suc i) t .snd) + + Ker-mapₗ⊂Im-mapᵣ : (i : ℕ) (t : suc n ≤ suc i) (x : coHom i RR E) + → isInKer (mapₗ i t) x + → isInIm (mapᵣ i) x + Ker-mapₗ⊂Im-mapᵣ i t x p = + Ker-E↑⊂Im-p* i x + (sym (retEq (fst (helpIso (suc i) t)) (E↑ i .fst x)) + ∙ cong (invEq (fst (helpIso (suc i) t))) p + ∙ IsGroupHom.pres1 (invGroupEquiv (helpIso (suc i) t) .snd)) + + private + j*≡ : (i : ℕ) (t : suc n ≤ i) + → (x : _) → j* i .fst x + ≡ fst (alt-hom i t) + (fst (helpIso i t) .fst x) + j*≡ i t f = cong (j* i .fst) + (sym (substSubst⁻ (λ i → coHomRed i RR EP∙) (minusPath i t) f)) + ∙ sym (substCommSlice (λ i → coHomRed i RR EP∙) + (λ i → coHom i RR (fst B)) (λ i → j* i .fst) (minusPath i t) + (subst (λ i → coHomRed i RR EP∙) (sym (minusPath i t)) f)) + ∙ cong (subst (λ i → coHom i RR (fst B)) (minusPath i t)) + (cong (j* ((i ∸ suc n) +' (suc n)) .fst) + (sym (secEq (ϕGrEquiv (i ∸ suc n) .fst) + (subst (λ i → coHomRed i RR EP∙) (sym (minusPath i t)) + f)))) + + Ker-⌣⊂Im-mapₗ : (i : ℕ) (t : suc n ≤ suc i) + (x : coHom (suc i ∸ suc n) RR (fst B)) + → isInKer (⌣-hom (suc i) t) x + → isInIm (mapₗ i t) x + Ker-⌣⊂Im-mapₗ i t x s = + →Im (Ker-j*⊂Im-E↑ i _ + ((j*≡ (suc i) t _ + ∙ cong (fst (alt-hom (suc i) t)) + (secEq (fst (helpIso (suc i) t)) x)) + ∙ funExt⁻ (cong fst (sym (⌣≡alt (suc i) t))) x ∙ s)) + where + →Im : isInIm (E↑ i) (invEq (fst (helpIso (suc i) t)) x) + → isInIm (mapₗ i t) x + →Im = PT.map (uncurry λ f p → f + , cong (fst (fst (helpIso (suc i) t))) p + ∙ secEq (fst (helpIso (suc i) t)) _) + + + Im-mapₗ⊂Ker-⌣ : (i : ℕ) (t : suc n ≤ suc i) + (x : coHom (suc i ∸ suc n) RR (fst B)) + → isInIm (mapₗ i t) x + → isInKer (⌣-hom (suc i) t) x + Im-mapₗ⊂Ker-⌣ i t x p = + (((λ j → ⌣≡alt (suc i) t j .fst x) + ∙ cong (fst (alt-hom (suc i) t)) + (sym (secEq (fst (helpIso (suc i) t)) x))) + ∙ sym (j*≡ (suc i) t (invEq (helpIso (suc i) t .fst) x))) + ∙ Im-E↑⊂Ker-j* i _ (Im-transf x p) + where + Im-transf : (x : _) → isInIm (mapₗ i t) x + → isInIm (E↑ i) (invEq (helpIso (suc i) t .fst) x) + Im-transf f = PT.map (uncurry λ g p → g + , sym (retEq (helpIso (suc i) t .fst) (E↑ i .fst g)) + ∙ cong (invEq (helpIso (suc i) t .fst)) p) + + Im--⌣⊂Ker-mapᵣ : (i : ℕ) (t : suc n ≤ i) (x : coHom i RR (fst B)) + → isInIm (⌣-hom i t) x + → isInKer (mapᵣ i) x + Im--⌣⊂Ker-mapᵣ i t x p = + Im-j*⊂Ker-p* i x + (PT.map + (uncurry (λ f p → invEq (helpIso i t .fst) f + , ((j*≡ i t (invEq (helpIso i t .fst) f) + ∙ cong (alt-hom i t .fst) + (secEq (fst (helpIso i t)) f)) + ∙ ((λ j → ⌣≡alt i t (~ j) .fst f))) + ∙ refl + ∙ p)) p) + + + Ker-mapᵣ⊂Im--⌣ : (i : ℕ) (t : suc n ≤ i) (x : coHom i RR (fst B)) + → isInKer (mapᵣ i) x + → isInIm (⌣-hom i t) x + Ker-mapᵣ⊂Im--⌣ i t x p = + subst (λ f → isInIm f x) (sym (⌣≡alt i t)) + (→Im x (Ker-p*⊂Im-j* i x p)) + where + →Im : (x : _) → isInIm (j* i) x → isInIm (alt-hom i t) x + →Im x = PT.map (uncurry λ f p → (fst (helpIso i t .fst) f) + , sym (j*≡ i t f) + ∙ p) + + + +module GysinCon (B : Pointed ℓ) + (P : fst B → Type ℓ') + (conB : isConnected 3 (fst B)) + (R : CommRing ℓ'') + (n : ℕ) + (eq : P (pt B) ≃ S₊ n) + where + private + module T = Thom B P (invEq eq (ptSn n)) (isConnectedSubtr 2 1 conB) R + module GT = genThom B + (λ b → Susp∙ (P b)) conB R (suc n) (T.Q≃ n (eq , secEq eq (ptSn n))) + + module Inst = Gysin B P (isConnectedSubtr 2 1 conB) + R + n + eq + GT.c + GT.c-id + + open Inst public diff --git a/Cubical/Data/Prod/Properties.agda b/Cubical/Data/Prod/Properties.agda index da8c7eed07..393352c444 100644 --- a/Cubical/Data/Prod/Properties.agda +++ b/Cubical/Data/Prod/Properties.agda @@ -8,6 +8,7 @@ open import Cubical.Data.Sigma renaming (_×_ to _×Σ_) hiding (prodIso ; toPro open import Cubical.Foundations.Prelude open import Cubical.Foundations.Equiv +open import Cubical.Foundations.Function open import Cubical.Foundations.HLevels open import Cubical.Foundations.Isomorphism open import Cubical.Foundations.Univalence @@ -109,3 +110,17 @@ Iso.fun curryIso f a b = f (a , b) Iso.inv curryIso f (a , b) = f a b Iso.rightInv curryIso a = refl Iso.leftInv curryIso f = funExt λ {(a , b) → refl} + +fiber-map-× : ∀ {ℓ ℓ' ℓ''} {A : Type ℓ} {B : Type ℓ'} {C : Type ℓ''} + (f : B → C) (a : A) (c : C) + → Iso (fiber f c) (fiber (map-× (idfun A) f) (a , c)) +fiber-map-× f a c .Iso.fun z .fst .fst = a +fiber-map-× f a c .Iso.fun z .fst .snd = z .fst +fiber-map-× f a c .Iso.fun z .snd = ≡-× refl (z .snd) +fiber-map-× f a c .Iso.inv z .fst = z .fst .snd +fiber-map-× f a c .Iso.inv z .snd = cong snd (z .snd) +fiber-map-× f a c .Iso.rightInv ((az , bz) , e) j .fst .fst = cong fst e (~ j) +fiber-map-× f a c .Iso.rightInv ((az , bz) , e) j .fst .snd = bz +fiber-map-× f a c .Iso.rightInv ((az , bz) , e) j .snd k .fst = cong fst e (k ∨ ~ j) +fiber-map-× f a c .Iso.rightInv ((az , bz) , e) j .snd k .snd = cong snd e k +fiber-map-× f a c .Iso.leftInv z = refl diff --git a/Cubical/Foundations/Equiv/Properties.agda b/Cubical/Foundations/Equiv/Properties.agda index aaa4cbf40f..05d146f08c 100644 --- a/Cubical/Foundations/Equiv/Properties.agda +++ b/Cubical/Foundations/Equiv/Properties.agda @@ -253,3 +253,8 @@ isEquiv[equivFunA≃B∘f]→isEquiv[f] f (g , gIsEquiv) g∘fIsEquiv = w' : isEquiv (equivFun (invEquiv (_ , g∘fIsEquiv)) ∘ g) w' = snd (compEquiv (_ , gIsEquiv) (invEquiv (_ , g∘fIsEquiv))) + +isPointedTarget→isEquiv→isEquiv : {A B : Type ℓ} (f : A → B) + → (B → isEquiv f) → isEquiv f +equiv-proof (isPointedTarget→isEquiv→isEquiv f hf) = + λ y → equiv-proof (hf y) y diff --git a/Cubical/Foundations/Everything.agda b/Cubical/Foundations/Everything.agda index 6f6889b8ff..fb8d41e6d7 100644 --- a/Cubical/Foundations/Everything.agda +++ b/Cubical/Foundations/Everything.agda @@ -13,6 +13,7 @@ open import Cubical.Foundations.Equiv.BiInvertible public open import Cubical.Foundations.Equiv.HalfAdjoint open import Cubical.Foundations.Equiv.Dependent open import Cubical.Foundations.HLevels public +open import Cubical.Foundations.HLevels.Extend open import Cubical.Foundations.Path public open import Cubical.Foundations.Pointed public open import Cubical.Foundations.RelationalStructure public diff --git a/Cubical/Foundations/HLevels/Extend.agda b/Cubical/Foundations/HLevels/Extend.agda new file mode 100644 index 0000000000..ebdae59c6e --- /dev/null +++ b/Cubical/Foundations/HLevels/Extend.agda @@ -0,0 +1,119 @@ +{- + +Kan Operations for n-Truncated Types + +It provides an efficient way to construct cubes in truncated types. + +A draft note on this can be found online at +https://kangrongji.github.io/files/extend-operations.pdf + +-} +{-# OPTIONS --safe #-} +module Cubical.Foundations.HLevels.Extend where + +open import Cubical.Foundations.Prelude +open import Cubical.Foundations.HLevels + +private + variable + ℓ : Level + + +-- For conveniently representing the boundary of cubes +∂ : I → I +∂ i = i ∨ ~ i + + +-- TODO: Write a macro to generate these stuff. + +module _ + {X : Type ℓ} + (h : isContr X) + {ϕ : I} where + + extend₀ : + (x : Partial _ X) + → X [ ϕ ↦ x ] + extend₀ = extend h _ + + +module _ + {X : I → Type ℓ} + (h : (i : I) → isProp (X i)) + {ϕ : I} where + + extend₁ : + (x : (i : I) → Partial _ (X i)) + (i : I) → X i [ ϕ ∨ ∂ i ↦ x i ] + extend₁ x i = inS (hcomp (λ j → λ + { (ϕ = i1) → h i (bottom i) (x i 1=1) j + ; (i = i0) → h i (bottom i) (x i 1=1) j + ; (i = i1) → h i (bottom i) (x i 1=1) j }) + (bottom i)) + where + bottom : (i : I) → X i + bottom i = isProp→PathP h (x i0 1=1) (x i1 1=1) i + + +module _ + {X : I → I → Type} + (h : (i j : I) → isSet (X i j)) + {ϕ : I} where + + extend₂ : + (x : (i j : I) → Partial _ (X i j)) + (i j : I) → X i j [ ϕ ∨ ∂ i ∨ ∂ j ↦ x i j ] + extend₂ x i j = inS (outS (extend₁PathP p i) j) + where + isOfHLevel₁PathP : (i : I) (a : X i i0) (b : X i i1) + → isProp (PathP (λ j → X i j) a b) + isOfHLevel₁PathP i = isOfHLevelPathP' 1 (h i i1) + + extend₁PathP : + (p : (i : I) → Partial _ (PathP _ (x i i0 1=1) (x i i1 1=1))) + (i : I) → PathP _ (x i i0 1=1) (x i i1 1=1) [ ϕ ∨ ∂ i ↦ p i ] + extend₁PathP = extend₁ (λ i → isOfHLevel₁PathP i (x i i0 1=1) (x i i1 1=1)) {ϕ} + + p : (i : I) → Partial _ (PathP _ (x i i0 1=1) (x i i1 1=1)) + p i (i = i0) = λ j → x i j 1=1 + p i (i = i1) = λ j → x i j 1=1 + p i (ϕ = i1) = λ j → x i j 1=1 + + +module _ + (X : I → I → I → Type) + (h : (i j k : I) → isGroupoid (X i j k)) + {ϕ : I} where + + extend₃ : + (x : (i j k : I) → Partial _ (X i j k)) + (i j k : I) → X i j k [ ϕ ∨ ∂ i ∨ ∂ j ∨ ∂ k ↦ x i j k ] + extend₃ x i j k = inS (outS (extend₂PathP p i j) k) + where + isOfHLevel₂PathP : (i j : I) (a : X i j i0) (b : X i j i1) + → isSet (PathP (λ k → X i j k) a b) + isOfHLevel₂PathP i j = isOfHLevelPathP' 2 (h i j i1) + + extend₂PathP : + (p : (i j : I) → Partial _ (PathP _ (x i j i0 1=1) (x i j i1 1=1))) + (i j : I) → PathP _ (x i j i0 1=1) (x i j i1 1=1) [ ϕ ∨ ∂ i ∨ ∂ j ↦ p i j ] + extend₂PathP = extend₂ (λ i j → isOfHLevel₂PathP i j (x i j i0 1=1) (x i j i1 1=1)) {ϕ} + + p : (i j : I) → Partial _ (PathP (λ k → X i j k) (x i j i0 1=1) (x i j i1 1=1)) + p i j (i = i0) = λ k → x i j k 1=1 + p i j (i = i1) = λ k → x i j k 1=1 + p i j (j = i0) = λ k → x i j k 1=1 + p i j (j = i1) = λ k → x i j k 1=1 + p i j (ϕ = i1) = λ k → x i j k 1=1 + + +private + -- An example showing how to directly fill 3-cubes in an h-proposition. + -- It can help when one wants to pattern match certain HITs towards some n-types. + + isProp→Cube : + {X : Type ℓ} (h : isProp X) + (x : (i j k : I) → Partial _ X) + (i j k : I) → X [ ∂ i ∨ ∂ j ∨ ∂ k ↦ x i j k ] + isProp→Cube h x i j = + extend₁ (λ _ → h) {∂ i ∨ ∂ j} (x i j) diff --git a/Cubical/Foundations/Pointed/Properties.agda b/Cubical/Foundations/Pointed/Properties.agda index 9244485d90..014d605213 100644 --- a/Cubical/Foundations/Pointed/Properties.agda +++ b/Cubical/Foundations/Pointed/Properties.agda @@ -7,7 +7,9 @@ open import Cubical.Foundations.Function open import Cubical.Foundations.GroupoidLaws open import Cubical.Foundations.Isomorphism open import Cubical.Foundations.Equiv +open import Cubical.Foundations.Equiv.HalfAdjoint open import Cubical.Foundations.Isomorphism +open import Cubical.Foundations.Path open import Cubical.Data.Sigma @@ -100,73 +102,106 @@ module _ {ℓ ℓ' : Level} {A : Pointed ℓ} {B : Pointed ℓ'} (f : A →∙ B isInKer∙ : (x : fst A) → Type ℓ' isInKer∙ x = fst f x ≡ snd B -pre∘∙equiv : ∀ {ℓ ℓ'} {A : Pointed ℓ} {B C : Pointed ℓ'} +private module _ {ℓA ℓB ℓC : Level} (A : Pointed ℓA) (B : Pointed ℓB) (C : Pointed ℓC) (e : A ≃∙ B) where + toEq : (A →∙ C) → (B →∙ C) + toEq = _∘∙ ≃∙map (invEquiv∙ e) + + fromEq : B →∙ C → (A →∙ C) + fromEq = _∘∙ ≃∙map e + + toEq' : (C →∙ A) → C →∙ B + toEq' = ≃∙map e ∘∙_ + + fromEq' : C →∙ B → (C →∙ A) + fromEq' = ≃∙map (invEquiv∙ e) ∘∙_ + +pre∘∙equiv : ∀ {ℓA ℓB ℓC} {A : Pointed ℓA} {B : Pointed ℓB} {C : Pointed ℓC} → (B ≃∙ C) → Iso (A →∙ B) (A →∙ C) -pre∘∙equiv {A = A} {B = B} {C = C} eq = main +Iso.fun (pre∘∙equiv {A = A} {B = B} {C = C} e) = toEq' B C A e +Iso.inv (pre∘∙equiv {A = A} {B = B} {C = C} e) = fromEq' B C A e +Iso.rightInv (pre∘∙equiv {A = A} {B = B} {C = C} e) = + J (λ ptC p → section (toEq' B (fst C , ptC) A (fst e , p)) + (fromEq' B (fst C , ptC) A (fst e , p))) + (uncurry (λ f p → ΣPathP (funExt (λ x → isHAEquiv.rinv (HAe .snd) (f x)) + , ((sym (rUnit _) + ∙ cong (cong (fst (fst e))) + λ i → cong (invEq (fst e)) p + ∙ (lUnit (retEq (fst e) (pt B)) (~ i))) + ∙ cong-∙ (fst (fst e)) + (cong (invEq (fst e)) p) + (retEq (fst e) (pt B)) + ∙ refl + ◁ flipSquare (((λ _ → isHAEquiv.rinv (HAe .snd) (f (pt A))) + ∙ refl) + ◁ lem _ _ _ _ (cong (isHAEquiv.rinv (HAe .snd)) p + ▷ sym (isHAEquiv.com (HAe .snd) (pt B)))))))) + (snd e) where - module _ {ℓ ℓ' : Level} (A : Pointed ℓ) (B C : Pointed ℓ') - (eq : (B ≃∙ C)) where - to : (A →∙ B) → (A →∙ C) - to = ≃∙map eq ∘∙_ - - from : (A →∙ C) → (A →∙ B) - from = ≃∙map (invEquiv∙ eq) ∘∙_ - - lem : {ℓ : Level} {B : Pointed ℓ} - → ≃∙map (invEquiv∙ {A = B} ((idEquiv (fst B)) , refl)) ≡ id∙ B - lem = ΣPathP (refl , (sym (lUnit _))) - - J-lem : {ℓ ℓ' : Level} {A : Pointed ℓ} {B C : Pointed ℓ'} - → (eq : (B ≃∙ C)) - → retract (to A B C eq) (from _ _ _ eq) - × section (to A B C eq) (from _ _ _ eq) - J-lem {A = A} {B = B} {C = C} = - Equiv∙J (λ B eq → retract (to A B C eq) (from _ _ _ eq) - × section (to A B C eq) (from _ _ _ eq)) - ((λ f → ((λ i → (lem i ∘∙ (id∙ C ∘∙ f))) - ∙ λ i → ∘∙-idʳ (∘∙-idʳ f i) i)) - , λ f → ((λ i → (id∙ C ∘∙ (lem i ∘∙ f))) - ∙ λ i → ∘∙-idʳ (∘∙-idʳ f i) i)) - - main : Iso (A →∙ B) (A →∙ C) - Iso.fun main = to A B C eq - Iso.inv main = from A B C eq - Iso.rightInv main = J-lem eq .snd - Iso.leftInv main = J-lem eq .fst - -post∘∙equiv : ∀ {ℓ ℓC} {A B : Pointed ℓ} {C : Pointed ℓC} + HAe = equiv→HAEquiv (fst e) + lem : ∀ {ℓ} {A : Type ℓ} {x y z w : A} + (p : x ≡ y) (q : y ≡ z) (r : x ≡ w) (l : w ≡ z) + → PathP (λ i → p i ≡ l i) r q + → PathP (λ i → (p ∙ q) i ≡ l i) r refl + lem p q r l P i j = + hcomp (λ k → λ{ (i = i0) → r j + ; (i = i1) → q (j ∨ k) + ; (j = i1) → l i}) + (P i j) +Iso.leftInv (pre∘∙equiv {A = A} {B = B} {C = C} e) = + J (λ pt p → retract (toEq' B (fst C , pt) A (fst e , p)) + (fromEq' B (fst C , pt) A (fst e , p))) + (uncurry (λ f → + J (λ ptB p + → fromEq' (fst B , ptB) + (fst C , fst (fst e) ptB) A (fst e , refl) + (toEq' (fst B , ptB) + (fst C , fst (fst e) ptB) A (fst e , refl) (f , p)) + ≡ (f , p)) + (ΣPathP + (funExt (λ x → retEq (fst e) (f x)) + , ((cong₂ _∙_ ((λ i → cong (invEq (fst e)) (lUnit refl (~ i)))) + (sym (lUnit _) ∙ λ _ → retEq (fst e) (f (pt A))) + ∙ sym (lUnit _)) + ◁ λ i j → retEq (fst e) (f (pt A)) (i ∨ j)))))) + (snd e) + +post∘∙equiv : ∀ {ℓA ℓB ℓC} {A : Pointed ℓA} {B : Pointed ℓB} {C : Pointed ℓC} → (A ≃∙ B) → Iso (A →∙ C) (B →∙ C) -post∘∙equiv {A = A} {B = B} {C = C} eq = main +Iso.fun (post∘∙equiv {A = A} {B = B} {C = C} e) = toEq A B C e +Iso.inv (post∘∙equiv {A = A} {B = B} {C = C} e) = fromEq A B C e +Iso.rightInv (post∘∙equiv {A = A}{B = B , ptB} {C = C} e) = + J (λ pt p → section (toEq A (B , pt) C (fst e , p)) + (fromEq A (B , pt) C (fst e , p))) + (uncurry (λ f → + J (λ ptC p → toEq A (B , fst (fst e) (pt A)) (fst C , ptC) (fst e , refl) + (fromEq A (B , fst (fst e) (pt A)) (fst C , ptC) (fst e , refl) + (f , p)) + ≡ (f , p)) + (ΣPathP (funExt (λ x → cong f (isHAEquiv.rinv (snd HAe) x)) + , (cong₂ _∙_ + (λ i → cong f (cong (fst (fst e)) (lUnit (retEq (fst e) (pt A)) (~ i)))) + (sym (rUnit refl)) + ∙ sym (rUnit _) + ∙ cong (cong f) (isHAEquiv.com (snd HAe) (pt A))) + ◁ λ i j → f (isHAEquiv.rinv (snd HAe) (fst HAe (pt A)) (i ∨ j)))))) + (snd e) where - module _ {ℓ ℓC : Level} (A B : Pointed ℓ) (C : Pointed ℓC) - (eq : (A ≃∙ B)) where - to : (A →∙ C) → (B →∙ C) - to = _∘∙ ≃∙map (invEquiv∙ eq) - - from : (B →∙ C) → (A →∙ C) - from = _∘∙ ≃∙map eq - - lem : {ℓ : Level} {B : Pointed ℓ} - → ≃∙map (invEquiv∙ {A = B} ((idEquiv (fst B)) , refl)) ≡ id∙ B - lem = ΣPathP (refl , (sym (lUnit _))) - - J-lem : {ℓ ℓC : Level} {A B : Pointed ℓ} {C : Pointed ℓC} - → (eq : (A ≃∙ B)) - → retract (to A B C eq) (from _ _ _ eq) - × section (to A B C eq) (from _ _ _ eq) - J-lem {B = B} {C = C} = - Equiv∙J (λ A eq → retract (to A B C eq) (from _ _ _ eq) - × section (to A B C eq) (from _ _ _ eq)) - ((λ f → ((λ i → (f ∘∙ lem i) ∘∙ id∙ B) - ∙ λ i → ∘∙-idˡ (∘∙-idˡ f i) i)) - , λ f → (λ i → (f ∘∙ id∙ B) ∘∙ lem i) - ∙ λ i → ∘∙-idˡ (∘∙-idˡ f i) i) - - main : Iso (A →∙ C) (B →∙ C) - Iso.fun main = to A B C eq - Iso.inv main = from A B C eq - Iso.rightInv main = J-lem eq .snd - Iso.leftInv main = J-lem eq .fst + HAe = equiv→HAEquiv (fst e) +Iso.leftInv (post∘∙equiv {A = A} {B = B , ptB} {C = C} e) = + J (λ pt p → retract (toEq A (B , pt) C (fst e , p)) + (fromEq A (B , pt) C (fst e , p))) + (uncurry (λ f → J (λ ptC y → + fromEq A (B , fst (fst e) (pt A)) (fst C , ptC) (fst e , refl) + (toEq A (B , fst (fst e) (pt A)) (fst C , ptC) (fst e , refl) + (f , y)) + ≡ (f , y)) + (ΣPathP (funExt (λ x → cong f (retEq (fst e) x)) + , (sym (lUnit _) + ∙ sym (rUnit _) + ∙ cong (cong f) (sym (lUnit _)) + ∙ (λ _ → cong f (retEq (fst e) (pt A))) + ◁ λ i j → f (retEq (fst e) (pt A) (i ∨ j))))))) + (snd e) flip→∙∙ : {A : Pointed ℓ} {B : Pointed ℓ'} {C : Pointed ℓA} → (A →∙ (B →∙ C ∙)) → B →∙ (A →∙ C ∙) @@ -190,3 +225,22 @@ Iso.leftInv flip→∙∙Iso _ = refl × (≃∙map f ∘∙ ≃∙map (invEquiv∙ f) ≡ idfun∙ B)) ((ΣPathP (refl , sym (lUnit _) ∙ sym (rUnit refl))) , (ΣPathP (refl , sym (rUnit _) ∙ sym (rUnit refl)))) + +pointedSecIso : ∀ {ℓ''} {A : Pointed ℓ} {B : Pointed ℓ'} (Q : fst A → Pointed ℓ'') + → Iso ((a : fst A) → Q a →∙ B) + (Σ[ F ∈ (Σ (fst A) (fst ∘ Q) → fst B) ] + ((a : fst A) → F (a , pt (Q a)) ≡ pt B)) +Iso.fun (pointedSecIso Q) F = (λ x → F (fst x) .fst (snd x)) , (λ x → F x .snd) +Iso.inv (pointedSecIso Q) F a = (fst F ∘ (a ,_)) , snd F a +Iso.rightInv (pointedSecIso Q) F = refl +Iso.leftInv (pointedSecIso Q) F = refl + +compPathrEquiv∙ : {A : Type ℓ} {a b c : A} {q : a ≡ b} (p : b ≡ c) + → ((a ≡ b) , q) ≃∙ ((a ≡ c) , q ∙ p) +fst (compPathrEquiv∙ p) = compPathrEquiv p +snd (compPathrEquiv∙ p) = refl + +compPathlEquiv∙ : {A : Type ℓ} {a b c : A} {q : b ≡ c} (p : a ≡ b) + → ((b ≡ c) , q) ≃∙ ((a ≡ c) , p ∙ q) +fst (compPathlEquiv∙ p) = compPathlEquiv p +snd (compPathlEquiv∙ p) = refl diff --git a/Cubical/Foundations/Structure.agda b/Cubical/Foundations/Structure.agda index 87b2b5bf62..099bb8a2eb 100644 --- a/Cubical/Foundations/Structure.agda +++ b/Cubical/Foundations/Structure.agda @@ -10,7 +10,7 @@ private S : Type ℓ → Type ℓ' -- A structure is a type-family S : Type ℓ → Type ℓ', i.e. for X : Type ℓ and s : S X, --- the pair (X , s) : TypeWithStr ℓ S means that X is equipped with a S-structure, witnessed by s. +-- the pair (X , s) : TypeWithStr ℓ S means that X is equipped with an S-structure, witnessed by s. TypeWithStr : (ℓ : Level) (S : Type ℓ → Type ℓ') → Type (ℓ-max (ℓ-suc ℓ) ℓ') TypeWithStr ℓ S = Σ[ X ∈ Type ℓ ] S X diff --git a/Cubical/Foundations/Transport.agda b/Cubical/Foundations/Transport.agda index d4b9e156e4..72b084f241 100644 --- a/Cubical/Foundations/Transport.agda +++ b/Cubical/Foundations/Transport.agda @@ -96,6 +96,13 @@ Iso.inv (pathToIso x) = transport⁻ x Iso.rightInv (pathToIso x) = transportTransport⁻ x Iso.leftInv (pathToIso x) = transport⁻Transport x +substIso : ∀ {ℓ ℓ'} {A : Type ℓ} (B : A → Type ℓ') {x y : A} (p : x ≡ y) → Iso (B x) (B y) +substIso B p = pathToIso (cong B p) + +-- Redefining substEquiv in terms of substIso gives an explicit inverse +substEquiv' : ∀ {ℓ ℓ'} {A : Type ℓ} (B : A → Type ℓ') {x y : A} (p : x ≡ y) → B x ≃ B y +substEquiv' B p = isoToEquiv (substIso B p) + isInjectiveTransport : ∀ {ℓ : Level} {A B : Type ℓ} {p q : A ≡ B} → transport p ≡ transport q → p ≡ q isInjectiveTransport {p = p} {q} α i = diff --git a/Cubical/Foundations/Univalence/Dependent.agda b/Cubical/Foundations/Univalence/Dependent.agda index 396f7d078b..c9a39e61cb 100644 --- a/Cubical/Foundations/Univalence/Dependent.agda +++ b/Cubical/Foundations/Univalence/Dependent.agda @@ -21,20 +21,74 @@ private -- Dependent Univalence - --- A quicker proof provided by @ecavallo: uaOver e F equiv = ua→ (λ a → ua (_ , equiv a)) --- Unfortunately it gives a larger term overall. -uaOver : +-- +-- Given families `P` and `Q` over base types `A` and `B` +-- respectively, and given +-- * an equivalence of base types `e : A ≃ B`, +-- * and and a pointwise equivalence of the families, +-- construct a dependent path over `ua e` between the families. +module _ {A B : Type ℓ} {P : A → Type ℓ'} {Q : B → Type ℓ'} (e : A ≃ B) (F : mapOver (e .fst) P Q) (equiv : isEquivOver {P = P} {Q = Q} F) - → PathP (λ i → ua e i → Type ℓ') P Q -uaOver {A = A} {P = P} {Q} e F equiv i x = - hcomp (λ j → λ - { (i = i0) → ua (_ , equiv x) (~ j) - ; (i = i1) → Q x }) - (Q (unglue (i ∨ ~ i) x)) + where + private + -- Bundle `F` and `equiv` into a pointwise equivalence of `P` and `Q`: + Γ : (a : A) → P a ≃ Q (equivFun e a) + Γ a = F a , equiv a + + -- A quick proof provided by @ecavallo. + -- Unfortunately it gives a larger term overall. + _ : PathP (λ i → ua e i → Type ℓ') P Q + _ = ua→ (λ a → ua (Γ a)) + + uaOver : PathP (λ i → ua e i → Type ℓ') P Q + uaOver i x = Glue Base {φ} equiv-boundary where + -- Like `ua`, `uaOver` is obtained from a line of + -- Glue-types, except that they are glued + -- over a line dependent on `ua e : A ≡ B`. + + -- `x` is a point along the path `A ≡ B` obtained + -- from univalence, i.e. glueing over `B`: + -- + -- A = = (ua e) = = B + -- | | + -- (e) (idEquiv B) + -- | | + -- v v + -- B =====(B)====== B + _ : Glue B {φ = i ∨ ~ i} (λ { (i = i0) → A , e ; (i = i1) → B , idEquiv B }) + _ = x + + -- We can therefore `unglue` it to obtain a term in the base line of `ua e`, + -- i.e. term of type `B`: + φ = i ∨ ~ i + b : B + b = unglue φ x + + -- This gives us a line `(i : I) ⊢ Base` in the universe of types, + -- along which we can glue the equivalences `Γ x` and `idEquiv (Q x)`: + -- + -- P (e x) = = = = = = Q x + -- | | + -- (Γ x) (idEquiv (Q x)) + -- | | + -- v v + -- Q x ===(Base)=== Q x + Base : Type ℓ' + Base = Q b + + equiv-boundary : Partial φ (Σ[ T ∈ Type ℓ' ] T ≃ Base) + equiv-boundary (i = i0) = P x , Γ x + equiv-boundary (i = i1) = Q x , idEquiv (Q x) + + -- Note that above `(i = i0) ⊢ x : A` and `(i = i1) ⊢ x : B`, + -- thus `P x` and `Q x` are well-typed. + _ : Partial i B + _ = λ { (i = i1) → x } + _ : Partial (~ i) A + _ = λ { (i = i0) → x } -- Dependent `isoToPath` diff --git a/Cubical/HITs/SetTruncation/Properties.agda b/Cubical/HITs/SetTruncation/Properties.agda index dfbf5c7943..56bd3914ff 100644 --- a/Cubical/HITs/SetTruncation/Properties.agda +++ b/Cubical/HITs/SetTruncation/Properties.agda @@ -333,3 +333,8 @@ Iso.fun (PathIdTrunc₀Iso {b = b}) p = Iso.inv PathIdTrunc₀Iso = pRec (squash₂ _ _) (cong ∣_∣₂) Iso.rightInv PathIdTrunc₀Iso _ = squash₁ _ _ Iso.leftInv PathIdTrunc₀Iso _ = squash₂ _ _ _ _ + +mapFunctorial : {A B C : Type ℓ} (f : A → B) (g : B → C) + → map g ∘ map f ≡ map (g ∘ f) +mapFunctorial f g = + funExt (elim (λ x → isSetPathImplicit) λ a → refl) diff --git a/Cubical/HITs/Susp/Base.agda b/Cubical/HITs/Susp/Base.agda index c9bb99c2e4..98a456bee8 100644 --- a/Cubical/HITs/Susp/Base.agda +++ b/Cubical/HITs/Susp/Base.agda @@ -7,6 +7,7 @@ open import Cubical.Foundations.Univalence open import Cubical.Foundations.Isomorphism open import Cubical.Foundations.Pointed +open import Cubical.Data.Unit open import Cubical.Data.Bool open import Cubical.Data.Empty @@ -35,6 +36,17 @@ suspFun f north = north suspFun f south = south suspFun f (merid a i) = merid (f a) i +UnitIsoSuspUnit : Iso Unit (Susp Unit) +fun UnitIsoSuspUnit _ = north +inv UnitIsoSuspUnit _ = tt +rightInv UnitIsoSuspUnit north = refl +rightInv UnitIsoSuspUnit south = merid tt +rightInv UnitIsoSuspUnit (merid tt j) k = merid tt (j ∧ k) +leftInv UnitIsoSuspUnit _ = refl + +Unit≃SuspUnit : Unit ≃ Susp Unit +Unit≃SuspUnit = isoToEquiv UnitIsoSuspUnit + BoolIsoSusp⊥ : Iso Bool (Susp ⊥) fun BoolIsoSusp⊥ = λ {true → north; false → south} inv BoolIsoSusp⊥ = λ {north → true; south → false} diff --git a/Cubical/HITs/Susp/Properties.agda b/Cubical/HITs/Susp/Properties.agda index f510599c11..4a9358a86d 100644 --- a/Cubical/HITs/Susp/Properties.agda +++ b/Cubical/HITs/Susp/Properties.agda @@ -55,7 +55,7 @@ Susp≃joinBool = isoToEquiv Susp-iso-joinBool Susp≡joinBool : ∀ {ℓ} {A : Type ℓ} → Susp A ≡ join A Bool Susp≡joinBool = isoToPath Susp-iso-joinBool -congSuspIso : ∀ {ℓ} {A B : Type ℓ} → Iso A B → Iso (Susp A) (Susp B) +congSuspIso : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} → Iso A B → Iso (Susp A) (Susp B) fun (congSuspIso is) = suspFun (fun is) inv (congSuspIso is) = suspFun (inv is) rightInv (congSuspIso is) north = refl diff --git a/Cubical/Homotopy/Connected.agda b/Cubical/Homotopy/Connected.agda index 1289e5f00b..5640935b83 100644 --- a/Cubical/Homotopy/Connected.agda +++ b/Cubical/Homotopy/Connected.agda @@ -15,20 +15,25 @@ open import Cubical.Foundations.Univalence open import Cubical.Functions.Fibration open import Cubical.Functions.FunExtEquiv +open import Cubical.Functions.Surjection open import Cubical.Data.Unit -open import Cubical.Data.Bool -open import Cubical.Data.Nat +open import Cubical.Data.Bool hiding (elim; _≤_) +open import Cubical.Data.Nat hiding (elim) +open import Cubical.Data.Nat.Order +open import Cubical.Data.NatMinusOne open import Cubical.Data.Sigma +open import Cubical.Data.Prod.Properties -open import Cubical.HITs.Nullification +open import Cubical.HITs.Nullification hiding (elim) open import Cubical.HITs.Susp open import Cubical.HITs.SmashProduct open import Cubical.HITs.Pushout open import Cubical.HITs.Join open import Cubical.HITs.Sn.Base -open import Cubical.HITs.S1 -open import Cubical.HITs.Truncation as Trunc renaming (rec to trRec) +open import Cubical.HITs.S1 hiding (elim) +open import Cubical.HITs.Truncation as Trunc + renaming (rec to trRec) hiding (elim) open import Cubical.Homotopy.Loopspace @@ -44,6 +49,9 @@ isConnected n A = isContr (hLevelTrunc n A) isConnectedFun : ∀ {ℓ ℓ'} (n : HLevel) {A : Type ℓ} {B : Type ℓ'} (f : A → B) → Type (ℓ-max ℓ ℓ') isConnectedFun n f = ∀ b → isConnected n (fiber f b) +isConnectedZero : ∀ {ℓ} (A : Type ℓ) → isConnected 0 A +isConnectedZero A = isContrUnit* + isConnectedSubtr : ∀ {ℓ} {A : Type ℓ} (n m : HLevel) → isConnected (m + n) A → isConnected n A @@ -59,6 +67,12 @@ isConnectedFunSubtr : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} (n m : HLeve → isConnectedFun n f isConnectedFunSubtr n m f iscon b = isConnectedSubtr n m (iscon b) +isConnectedFun≤ : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} (n m : HLevel) (f : A → B) + → n ≤ m → isConnectedFun m f → isConnectedFun n f +isConnectedFun≤ n m f hnm hf = + isConnectedFunSubtr n (hnm .fst) f + (subst (λ d → isConnectedFun d f) (sym (hnm .snd)) hf) + private typeToFiberIso : ∀ {ℓ} (A : Type ℓ) → Iso A (fiber (λ (x : A) → tt) tt) Iso.fun (typeToFiberIso A) x = x , refl @@ -69,6 +83,15 @@ private typeToFiber : ∀ {ℓ} (A : Type ℓ) → A ≡ fiber (λ (x : A) → tt) tt typeToFiber A = isoToPath (typeToFiberIso A) +isConnectedFun→isConnected : {X : Type ℓ} (n : HLevel) + → isConnectedFun n (λ (_ : X) → tt) → isConnected n X +isConnectedFun→isConnected n h = + subst (isConnected n) (sym (typeToFiber _)) (h tt) + +isConnected→isConnectedFun : {X : Type ℓ} (n : HLevel) + → isConnected n X → isConnectedFun n (λ (_ : X) → tt) +isConnected→isConnectedFun n h = λ { tt → subst (isConnected n) (typeToFiber _) h } + isOfHLevelIsConnectedStable : ∀ {ℓ} {A : Type ℓ} (n : ℕ) → isOfHLevel n (isConnected n A) isOfHLevelIsConnectedStable {A = A} zero = @@ -109,6 +132,16 @@ module elim {ℓ ℓ' : Level} {A : Type ℓ} {B : Type ℓ'} (f : A → B) wher (λ {(a , p) i → transp (λ j → P (p (j ∨ i)) .fst) i (s (p i))}) (fConn b .fst) + isIsoPrecomposeβ : ∀ {ℓ'''} (n : ℕ) (P : B → TypeOfHLevel ℓ''' n) + → (e : isConnectedFun n f) + → (g : ((a : A) → P (f a) .fst)) + → (a : A) + → Iso.inv (isIsoPrecompose n P e) g (f a) ≡ g a + isIsoPrecomposeβ zero P e g a = P (f a) .snd .snd (g a) + isIsoPrecomposeβ (suc n) P e g a = + cong (inv n P g (f a)) (e (f a) .snd ∣ a , refl ∣) + ∙ transportRefl _ + isEquivPrecompose : ∀ {ℓ'''} (n : ℕ) (P : B → TypeOfHLevel ℓ''' n) → isConnectedFun n f → isEquiv (λ(s : (b : B) → P b .fst) → s ∘ f) @@ -273,6 +306,9 @@ isEquiv→isConnected : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} isEquiv→isConnected f iseq n b = isContr→isContr∥ n (equiv-proof iseq b) +isConnectedId : ∀ {ℓ} {A : Type ℓ} {n : HLevel} → isConnectedFun n (idfun A) +isConnectedId = isEquiv→isConnected _ (idIsEquiv _) _ + isConnectedPath : ∀ {ℓ} (n : HLevel) {A : Type ℓ} → isConnected (suc n) A @@ -402,6 +438,23 @@ isConnectedPoint2 n {A = A} a connMap = indMapEquiv→conType _ λ B → isoToIs Iso.rightInv theIso f = funExt λ y → sym (helper f y) Iso.leftInv theIso _ = refl +module isConnectedPoint {ℓ ℓ'} (n : HLevel) {A : Type ℓ} + {B : A → Type ℓ'} + (conA : isConnected (suc n) A) + (hlevB : (a : A) → isOfHLevel n (B a)) + (p : Σ[ a ∈ A ] (B a)) where + private + module m = elim (λ (tt : Unit) → fst p) + P : A → TypeOfHLevel ℓ' n + P a = B a , hlevB a + con* = isConnectedPoint n conA (fst p) + + elim : (a : A) → B a + elim = Iso.inv (m.isIsoPrecompose n P con*) λ _ → snd p + + β : elim (fst p) ≡ snd p + β = m.isIsoPrecomposeβ n P con* (λ _ → snd p) tt + connectedTruncIso : ∀ {ℓ} {A B : Type ℓ} (n : HLevel) (f : A → B) → isConnectedFun n f → Iso (hLevelTrunc n A) (hLevelTrunc n B) @@ -450,6 +503,11 @@ connectedTruncEquiv : ∀ {ℓ} {A B : Type ℓ} (n : HLevel) (f : A → B) → hLevelTrunc n A ≃ hLevelTrunc n B connectedTruncEquiv {A = A} {B = B} n f con = isoToEquiv (connectedTruncIso n f con) +isConnectedSuc→isSurjection : ∀ {ℓ ℓ'} {A : Type ℓ} {B : Type ℓ'} {f : A → B} {n : HLevel} + → isConnectedFun (suc n) f → isSurjection f +isConnectedSuc→isSurjection hf b = + Iso.inv propTruncTrunc1Iso (isConnectedFun≤ 1 _ _ (suc-≤-suc zero-≤) hf b .fst) + isConnectedSuspFun : ∀ {ℓ ℓ'} {X : Type ℓ} {Y : Type ℓ'} (f : X → Y) (n : HLevel) → isConnectedFun n f @@ -491,6 +549,24 @@ isConnectedSuspFun {X = X} {Y = Y} f n con-f = ∙ recₕ n (a , refl) ∙ transportRefl (cong F (merid a)) +isConnectedSusp : ∀ {ℓ} {X : Type ℓ} (n : HLevel) + → isConnected n X + → isConnected (suc n) (Susp X) +isConnectedSusp {X = X} n h = isConnectedFun→isConnected (suc n) $ + isConnectedComp _ (suspFun (λ (x : X) → tt)) (suc n) + (isEquiv→isConnected _ (equivIsEquiv (invEquiv Unit≃SuspUnit)) (suc n)) + (isConnectedSuspFun _ n (isConnected→isConnectedFun n h)) + +-- See also `sphereConnected` for S₊ +isConnectedSphere : ∀ (n : ℕ) → isConnected n (S (-1+ n)) +isConnectedSphere zero = isConnectedZero (S (-1+ 0)) +isConnectedSphere (suc n) = isConnectedSusp n (isConnectedSphere n) + +isConnected-map-× : ∀ {ℓ ℓ' ℓ''} {A : Type ℓ} {B : Type ℓ'} {C : Type ℓ''} (n : HLevel) + (f : B → C) → isConnectedFun n f → isConnectedFun n (map-× (idfun A) f) +isConnected-map-× n f hf z = + isConnectedRetractFromIso _ (invIso $ fiber-map-× f (fst z) (snd z)) (hf (snd z)) + -- TODO : Reorganise the following proofs. inrConnected : ∀ {ℓ ℓ' ℓ''} {A : Type ℓ} {B : Type ℓ'} {C : Type ℓ''} (n : HLevel) diff --git a/Cubical/Homotopy/EilenbergMacLane/CupProduct.agda b/Cubical/Homotopy/EilenbergMacLane/CupProduct.agda index 31aa3fbd45..74733bfdb0 100644 --- a/Cubical/Homotopy/EilenbergMacLane/CupProduct.agda +++ b/Cubical/Homotopy/EilenbergMacLane/CupProduct.agda @@ -143,6 +143,31 @@ module _ {G'' : Ring ℓ} where (fst TensorMultHom b) (fst TensorMultHom c))) λ x y ind ind2 → cong₂ _+G_ ind ind2)) + EM→ΩEM+1-distr⌣ₖ0n : (n : ℕ) + → (x : EM G' zero) (y : EM G' (suc n)) + → EM→ΩEM+1 (suc n) (_⌣ₖ_{n = zero} {m = suc n} x y) + ≡ λ i → _⌣ₖ_ {n = suc zero} {m = suc n} (EM→ΩEM+1 0 x i) y + EM→ΩEM+1-distr⌣ₖ0n n x y = + EMFun-EM→ΩEM+1 (suc n) _ + + EM→ΩEM+1-distr⌣ₖ0 : (n : ℕ) + → (x : EM G' (suc n)) (y : EM G' zero) + → EM→ΩEM+1 (suc n) (_⌣ₖ_{n = (suc n)} {m = zero} x y) + ≡ λ i → _⌣ₖ_ {n = suc (suc n)} {m = zero} (EM→ΩEM+1 (suc n) x i) y + EM→ΩEM+1-distr⌣ₖ0 n x y = + EMFun-EM→ΩEM+1 (suc n) (_⌣ₖ⊗_{n = (suc n)} {m = zero} x y) + ∙ cong (cong (inducedFun-EM TensorMultHom (suc (suc n)))) + (EM→ΩEM+1-distrₙ₀ n y x) + + EM→ΩEM+1-distr⌣ₖ : (n m : ℕ) + → (x : EM G' (suc n)) (y : EM G' (suc m)) + → EM→ΩEM+1 (suc n +' suc m) (_⌣ₖ_{n = (suc n)} {m = suc m} x y) + ≡ λ i → _⌣ₖ_ {n = suc (suc n)} {m = suc m} (EM→ΩEM+1 (suc n) x i) y + EM→ΩEM+1-distr⌣ₖ n m x y = + EMFun-EM→ΩEM+1 _ (_⌣ₖ⊗_{n = (suc n)} {m = suc m} x y) + ∙ cong (cong (inducedFun-EM TensorMultHom (suc (suc n) +' suc m))) + (EM→ΩEM+1-distrₙsuc n m x y) + -- graded commutativity module _ {G'' : CommRing ℓ} where private @@ -198,7 +223,7 @@ module _ {G'' : CommRing ℓ} where → EM (Ring→AbGroup (CommRing→Ring R)) (n +' m) ⌣[,,]Cₖ-syntax n m R x y = x ⌣ₖ y -syntax ⌣[]ₖ-syntax R x y = x ⌣[ R ]ₖ y -syntax ⌣[]Cₖ-syntax R x y = x ⌣[ R ]Cₖ y +syntax ⌣[]ₖ-syntax R x y = x ⌣[ R R]ₖ y +syntax ⌣[]Cₖ-syntax R x y = x ⌣[ R R]Cₖ y syntax ⌣[,,]ₖ-syntax n m R x y = x ⌣[ R , n , m ]ₖ y syntax ⌣[,,]Cₖ-syntax n m R x y = x ⌣[ R , n , m ]Cₖ y diff --git a/Cubical/Homotopy/EilenbergMacLane/GroupStructure.agda b/Cubical/Homotopy/EilenbergMacLane/GroupStructure.agda index ee7ea93e32..3b75b6afe8 100644 --- a/Cubical/Homotopy/EilenbergMacLane/GroupStructure.agda +++ b/Cubical/Homotopy/EilenbergMacLane/GroupStructure.agda @@ -446,6 +446,16 @@ module _ {G : AbGroup ℓ} where ∙ sym (lUnit _) ◁ λ i j → ∣ compPath-filler (merid a) (sym (merid ptEM-raw)) (~ i) j ∣ₕ) +_+ₖ∙_ : ∀ {ℓ ℓ'} {A : Pointed ℓ} {G : AbGroup ℓ'} {n : ℕ} + → (A →∙ EM∙ G n) → (A →∙ EM∙ G n) + → A →∙ EM∙ G n +fst (f +ₖ∙ g) x = fst f x +ₖ fst g x +snd (_+ₖ∙_ {A = A} {n = n} f g) = s + where + abstract + s : fst f (pt A) +ₖ fst g (pt A) ≡ 0ₖ n + s = cong₂ _+ₖ_ (snd f) (snd g) ∙ rUnitₖ _ (0ₖ _) + -distrₖ : {G : AbGroup ℓ} (n : ℕ) (x y : EM G n) → -[ n ]ₖ (x +[ n ]ₖ y) ≡ (-[ n ]ₖ x) +[ n ]ₖ (-[ n ]ₖ y) -distrₖ {G = G} zero x y = diff --git a/Cubical/Homotopy/EilenbergMacLane/Order2.agda b/Cubical/Homotopy/EilenbergMacLane/Order2.agda index f482decae5..bd09f17d52 100644 --- a/Cubical/Homotopy/EilenbergMacLane/Order2.agda +++ b/Cubical/Homotopy/EilenbergMacLane/Order2.agda @@ -247,7 +247,7 @@ symConst-ℤ/2-refl = EMZ/2.symConstEM-refl (evenOrOdd n) ⌣ₖ-commℤ/2 : (n m : ℕ) (x : EM ℤ/2 n) (y : EM ℤ/2 m) - → (x ⌣[ ℤ/2Ring ]ₖ y) ≡ subst (EM ℤ/2) (+'-comm m n) (y ⌣[ ℤ/2Ring ]ₖ x) + → (x ⌣[ ℤ/2Ring R]ₖ y) ≡ subst (EM ℤ/2) (+'-comm m n) (y ⌣[ ℤ/2Ring R]ₖ x) ⌣ₖ-commℤ/2 n m x y = ⌣ₖ-comm {G'' = ℤ/2CommRing} n m x y ∙ cong (subst (EM ℤ/2) (+'-comm m n)) (-ₖ^[ n · m ]-const _) diff --git a/Cubical/Homotopy/EilenbergMacLane/Properties.agda b/Cubical/Homotopy/EilenbergMacLane/Properties.agda index c002976c3b..76a5092bec 100644 --- a/Cubical/Homotopy/EilenbergMacLane/Properties.agda +++ b/Cubical/Homotopy/EilenbergMacLane/Properties.agda @@ -438,6 +438,79 @@ module _ {G : AbGroup ℓ} where EM→ΩEM+1∘EM-raw→EM zero x = refl EM→ΩEM+1∘EM-raw→EM (suc n) x = refl + EM→ΩEM+1-gen : (n : ℕ) (x : EM G (suc n)) + → EM G n → x ≡ x + EM→ΩEM+1-gen n x p = + sym (rUnitₖ (suc n) x) + ∙∙ cong (x +ₖ_) (EM→ΩEM+1 n p) + ∙∙ rUnitₖ (suc n) x + + ΩEM+1-gen→EM-0ₖ : (n : ℕ) (x : _) + → ΩEM+1→EM-gen n (0ₖ (suc n)) x + ≡ ΩEM+1→EM n x + ΩEM+1-gen→EM-0ₖ zero p = refl + ΩEM+1-gen→EM-0ₖ (suc n) p = refl + + EM→ΩEM+1-gen-0ₖ : (n : ℕ) (x : _) + → EM→ΩEM+1-gen n (0ₖ (suc n)) x + ≡ EM→ΩEM+1 n x + EM→ΩEM+1-gen-0ₖ zero x = sym (rUnit _) + ∙ λ j i → lUnitₖ 1 (EM→ΩEM+1 zero x i) j + EM→ΩEM+1-gen-0ₖ (suc n) x = sym (rUnit _) + ∙ λ j i → lUnitₖ (suc (suc n)) (EM→ΩEM+1 (suc n) x i) j + + EM→ΩEM+1→EM-gen : (n : ℕ) (x : EM G (suc n)) + → (y : EM G n) → ΩEM+1→EM-gen n x (EM→ΩEM+1-gen n x y) ≡ y + EM→ΩEM+1→EM-gen n = + EM-raw'-elim _ _ + (λ _ → isOfHLevelΠ (suc (suc n)) + (λ _ → isOfHLevelPath (suc (suc n)) + (hLevelEM _ n) _ _)) + (EM-raw'-trivElim _ n + (λ _ → isOfHLevelΠ (suc n) λ _ → hLevelEM _ n _ _) + λ y → cong (λ p → ΩEM+1→EM-gen n p + (EM→ΩEM+1-gen n p y)) + (EM-raw'→EM∙ G (suc n)) + ∙ (λ i → ΩEM+1-gen→EM-0ₖ n (EM→ΩEM+1-gen-0ₖ n y i) i) + ∙ Iso.leftInv (Iso-EM-ΩEM+1 n) y) + + ΩEM+1→EM→ΩEM+1-gen : (n : ℕ) (x : EM G (suc n)) + → (y : x ≡ x) → EM→ΩEM+1-gen n x (ΩEM+1→EM-gen n x y) ≡ y + ΩEM+1→EM→ΩEM+1-gen n = + EM-raw'-elim _ _ + (λ _ → isOfHLevelΠ (suc (suc n)) + (λ _ → isOfHLevelPath (suc (suc n)) + (hLevelEM _ (suc n) _ _) _ _)) + (EM-raw'-trivElim _ n + (λ _ → isOfHLevelΠ (suc n) + λ _ → hLevelEM _ (suc n) _ _ _ _) + (subst (λ p → (y : p ≡ p) + → EM→ΩEM+1-gen n p (ΩEM+1→EM-gen n p y) ≡ y) + (sym (EM-raw'→EM∙ _ (suc n))) + λ p → (λ i → EM→ΩEM+1-gen-0ₖ n (ΩEM+1-gen→EM-0ₖ n p i) i) + ∙ Iso.rightInv (Iso-EM-ΩEM+1 n) p)) + + Iso-EM-ΩEM+1-gen : (n : ℕ) (x : EM G (suc n)) + → Iso (EM G n) (x ≡ x) + Iso.fun (Iso-EM-ΩEM+1-gen n x) = EM→ΩEM+1-gen n x + Iso.inv (Iso-EM-ΩEM+1-gen n x) = ΩEM+1→EM-gen n x + Iso.rightInv (Iso-EM-ΩEM+1-gen n x) = ΩEM+1→EM→ΩEM+1-gen n x + Iso.leftInv (Iso-EM-ΩEM+1-gen n x) = EM→ΩEM+1→EM-gen n x + + ΩEM+1→EM-gen-refl : (n : ℕ) (x : EM G (suc n)) + → ΩEM+1→EM-gen n x refl ≡ 0ₖ n + ΩEM+1→EM-gen-refl n = + EM-raw'-elim _ (suc n) + (λ _ → isOfHLevelPath (suc (suc n)) (hLevelEM _ n) _ _) + (EM-raw'-trivElim _ n + (λ _ → hLevelEM _ n _ _) + (lem n)) + where + lem : (n : ℕ) → ΩEM+1→EM-gen n + (EM-raw'→EM G (suc n) (snd (EM-raw'∙ G (suc n)))) refl + ≡ 0ₖ n + lem zero = ΩEM+1→EM-refl 0 + lem (suc n) = ΩEM+1→EM-refl (suc n) -- Some HLevel lemmas about function spaces (EM∙ G n →∙ EM∙ H m), mainly used for -- the cup product diff --git a/Cubical/Homotopy/Loopspace.agda b/Cubical/Homotopy/Loopspace.agda index 05f722d1e4..b5b2d5aecd 100644 --- a/Cubical/Homotopy/Loopspace.agda +++ b/Cubical/Homotopy/Loopspace.agda @@ -209,6 +209,19 @@ snd (inv (ΩfunExtIso A B) (f , p) i) j = p j i rightInv (ΩfunExtIso A B) _ = refl leftInv (ΩfunExtIso A B) _ = refl +relax→∙Ω-Iso : ∀ {ℓ ℓ'} {A : Pointed ℓ} {B : Pointed ℓ'} + → Iso (Σ[ b ∈ fst B ] (fst A → b ≡ pt B)) + (A →∙ (Ω B)) +Iso.fun (relax→∙Ω-Iso {A = A}) (b , p) = (λ a → sym (p (pt A)) ∙ p a) , lCancel (p (snd A)) +Iso.inv (relax→∙Ω-Iso {B = B}) a = (pt B) , (fst a) +Iso.rightInv (relax→∙Ω-Iso) a = + →∙Homogeneous≡ (isHomogeneousPath _ _) + (funExt λ x → cong (_∙ fst a x) (cong sym (snd a)) ∙ sym (lUnit (fst a x))) +Iso.leftInv (relax→∙Ω-Iso {A = A}) (b , p) = + ΣPathP (sym (p (pt A)) + , λ i a j → compPath-filler' (sym (p (pt A))) (p a) (~ i) j) + + {- Commutativity of loop spaces -} isComm∙ : ∀ {ℓ} (A : Pointed ℓ) → Type ℓ isComm∙ A = (p q : typ (Ω A)) → p ∙ q ≡ q ∙ p diff --git a/Cubical/Homotopy/WhiteheadsLemma.agda b/Cubical/Homotopy/WhiteheadsLemma.agda new file mode 100644 index 0000000000..70533091bd --- /dev/null +++ b/Cubical/Homotopy/WhiteheadsLemma.agda @@ -0,0 +1,373 @@ +{- + +Whitehead's lemma for truncated spaces. + +-} +{-# OPTIONS --safe #-} +module Cubical.Homotopy.WhiteheadsLemma where + +open import Cubical.Foundations.Prelude + +open import Cubical.Foundations.Equiv +open import Cubical.Foundations.Equiv.Properties +open import Cubical.Foundations.Function +open import Cubical.Foundations.GroupoidLaws +open import Cubical.Foundations.HLevels +open import Cubical.Foundations.Isomorphism +open import Cubical.Foundations.Path +open import Cubical.Foundations.Pointed +open import Cubical.Foundations.Transport + +open import Cubical.Data.Nat +open import Cubical.Data.Sigma +open import Cubical.HITs.PropositionalTruncation hiding (map) +open import Cubical.HITs.SetTruncation renaming (rec to sRec ; elim to sElim) +open import Cubical.Homotopy.Group.Base +open import Cubical.Homotopy.Loopspace + +private + variable + ℓ : Level + +-- lots of easy helper lemmas, hopefully no duplicates +private + SetTrunc→PropTrunc : {A : Type ℓ} → ∥ A ∥₂ → ∥ A ∥₁ + SetTrunc→PropTrunc = sRec (isProp→isSet isPropPropTrunc) ∣_∣₁ + + module _ (F : Pointed ℓ → Pointed ℓ) + (F' : {A B : Pointed ℓ} → (A →∙ B) → (F A →∙ F B)) where + + specialCong∙ : {A B C D : Pointed ℓ} (p : A ≡ C) (q : B ≡ D) + (f : A →∙ B) (g : C →∙ D) + (r : PathP (λ i → (p i) →∙ (q i)) f g) + → PathP (λ i → (cong F p) i →∙ (cong F q) i) (F' f) (F' g) + specialCong∙ {A = A} {B = B} {C = C} {D = D} = + J ( λ C' p → + (q : B ≡ D) (f : A →∙ B) (g : C' →∙ D) + (r : PathP (λ i → (p i) →∙ (q i)) f g) + → PathP (λ i → (cong F p) i →∙ (cong F q) i) (F' f) (F' g)) + ( J ( λ D' q → + (f : A →∙ B) (g : A →∙ D') + (r : PathP (λ i → A →∙ (q i)) f g) + → PathP (λ i → F A →∙ (cong F q) i) (F' f) (F' g)) + ( λ f g r → cong F' r)) + + ∙PathP→Square : {A B C D : Pointed ℓ} (p : A ≡ C) (q : B ≡ D) + (f : A →∙ B) (g : C →∙ D) + → PathP (λ i → (p i) →∙ (q i)) f g + → (Iso.inv (pathToIso (λ i → fst (q i)))) + ∘ (fst g) + ∘ (Iso.fun (pathToIso (λ i → fst (p i)))) + ≡ (fst f) + ∙PathP→Square {A = A} {B = B} {C = C} {D = D} = + J ( λ C' p → + (q : B ≡ D) (f : A →∙ B) (g : C' →∙ D) + → PathP (λ i → (p i) →∙ (q i)) f g + → (Iso.inv (pathToIso (λ i → fst (q i)))) + ∘ (fst g) + ∘ (Iso.fun (pathToIso (λ i → fst (p i)))) + ≡ (fst f)) + ( J ( λ D' q → + (f : A →∙ B) (g : A →∙ D') + → PathP (λ i → A →∙ (q i)) f g + → (Iso.inv (pathToIso (λ i → fst (q i)))) + ∘ (fst g) + ∘ (Iso.fun (pathToIso (λ i → (fst A)))) + ≡ (fst f)) + ( λ f g r → + funExt ( λ a → transportRefl (fst g (transport refl a)) + ∙ cong (fst g) (transportRefl a) + ∙ λ i → (fst (r (~ i))) a))) + + squareWithEquivs→Equiv : {A B C D : Type ℓ} + (f : A → B) (e1 : C → D) (e2 : A → C) (e3 : D → B) + → isEquiv e1 → isEquiv e2 → isEquiv e3 → e3 ∘ e1 ∘ e2 ≡ f + → isEquiv f + squareWithEquivs→Equiv f e1 e2 e3 e1Eq e2Eq e3Eq p = + transport + ( λ i → isEquiv (p i)) + ( snd (compEquiv + ( e2 , e2Eq) + ( (e3 ∘ e1) , (snd (compEquiv (e1 , e1Eq) (e3 , e3Eq)))))) +-- end of the long private block of helper lemmas + +-- some useful paths between different maps + +{- + +a ≡ b ------> f a ≡ f b + | ^ + | | + | | + v | +a ≡ a ------> f a ≡ f a + +-} +ΩCongSquare : {A B : Type ℓ} {a b : A} (f : A → B) (p : a ≡ b) + → (λ q → q ∙ (cong f p)) + ∘ fst (Ω→ (f , refl)) + ∘ (λ q → q ∙ sym p) + ≡ cong f +ΩCongSquare f = + J ( λ b p → (λ q → q ∙ (cong f p)) + ∘ fst (Ω→ (f , refl)) + ∘ (λ q → q ∙ sym p) + ≡ cong f) + ( funExt (λ x → sym (rUnit _) + ∙ sym (rUnit _) + ∙ cong (cong f) (sym (rUnit _)))) + +private + πHomπHomCongSquareAux : {A B : Type ℓ} {a : A} {n : ℕ} (f : A → B) + → Iso.inv (Iso-πΩ-π (1 + n)) + ∘ (fst (πHom {A = (A , a)} {B = (B , f a)} (1 + n) (f , refl))) + ∘ (Iso.fun (Iso-πΩ-π (1 + n))) + ≡ map (Iso.inv (invIso (flipΩIso (1 + n))) + ∘ fst ((Ω^→ (2 + n)) (f , refl)) + ∘ Iso.fun (invIso (flipΩIso (1 + n)))) + πHomπHomCongSquareAux {n = n} f = + cong + ( λ g → g ∘ (Iso.fun (Iso-πΩ-π (1 + n)))) + ( mapFunctorial + ( fst ((Ω^→ (2 + n)) (f , refl))) + ( Iso.fun (flipΩIso (1 + n)))) + ∙ mapFunctorial + ( Iso.inv (flipΩIso (1 + n))) + ( Iso.fun (flipΩIso (1 + n)) ∘ fst ((Ω^→ (2 + n)) (f , refl))) + +-- Ω (Ω→ f) ≡ Ω→ (Ω f) +PathPΩ^→Ω : {A B : Pointed ℓ} (n : ℕ) (f : A →∙ B) + → PathP (λ i → (flipΩPath {A = A} n) i + →∙ (flipΩPath {A = B} n) i) + ((Ω^→ (1 + n)) f) ((Ω^→ n) (Ω→ f)) +PathPΩ^→Ω zero f = refl +PathPΩ^→Ω (suc n) f = + specialCong∙ Ω Ω→ + ( flipΩPath n) + ( flipΩPath n) + ( Ω^→ (1 + n) f) + ( (Ω^→ n) (Ω→ f)) + ( PathPΩ^→Ω n f) + +private + flipIsoSquare : {A B C D : Type ℓ} (f : A → B) (g : C → D) + (H : Iso A C) (J : Iso B D) + → Iso.inv J ∘ g ∘ (Iso.fun H) ≡ f + → Iso.inv (invIso J) ∘ f ∘ Iso.fun (invIso H) ≡ g + flipIsoSquare f g H J p = + sym + ( funExt + ( λ x → + sym ((Iso.rightInv J) (g x)) + ∙ cong (λ y → Iso.fun J (Iso.inv J (g y))) + (sym ((Iso.rightInv H) x)) + ∙ cong (λ h → (Iso.fun J ∘ h ∘ Iso.inv H) x) p)) + +{- + +Ωⁿ⁺¹ (Ω (A, a)) -------> Ωⁿ⁺¹ (Ω (B, f a)) + | ^ + | | + | | + v | +Ω (Ωⁿ⁺¹ (A, a)) -------> Ω (Ωⁿ⁺¹ (B, f a)) + +-} +Ω+1ΩCongSquare : {A B : Type ℓ} {a : A} {n : ℕ} (f : A → B) + → Iso.inv (invIso (flipΩIso (1 + n))) + ∘ fst ((Ω^→ {A = (A , a)} (2 + n)) (f , refl)) + ∘ Iso.fun (invIso (flipΩIso (1 + n))) + ≡ fst ((Ω^→ (1 + n)) (Ω→ (f , refl))) +Ω+1ΩCongSquare {A = A} {a = a} {n = n} f = + flipIsoSquare + ( fst ((Ω^→ {A = (A , a)} (2 + n)) (f , refl))) + ( fst ((Ω^→ (1 + n)) (Ω→ (f , refl)))) + ( flipΩIso (1 + n)) + ( flipΩIso (1 + n)) + ( ∙PathP→Square + ( flipΩPath (1 + n)) + ( flipΩPath (1 + n)) + ( (Ω^→ {A = (A , a)} (2 + n)) (f , refl)) + ( (Ω^→ (1 + n)) (Ω→ (f , refl))) + ( PathPΩ^→Ω (1 + n) (f , refl))) + +{- + +πₙ (Ω (A, a)) ------> πₙ (Ω (B, f a)) + | ^ + | | + | | + v | +πₙ₊₁ (A, a) ---------> πₙ₊₁ (B, f a) + +-} +πHomπHomCongSquare : {A B : Type ℓ} {a : A} {n : ℕ} (f : A → B) + → Iso.inv (Iso-πΩ-π (1 + n)) + ∘ (fst (πHom {A = (A , a)} {B = (B , f a)} (1 + n) (f , refl))) + ∘ (Iso.fun (Iso-πΩ-π (1 + n))) + ≡ (fst (πHom n (cong f , refl))) +πHomπHomCongSquare {A = A} {B = B} {a = a} {n = n} f = + πHomπHomCongSquareAux {A = A} {B = B} {a = a} {n = n} f + ∙ cong map (Ω+1ΩCongSquare {A = A} {B = B} {a = a} {n = n} f) + ∙ cong map (cong (fst ∘ (Ω^→ (1 + n))) + ( funExt∙ ( (λ a → sym (rUnit (cong f a))) + , rUnit (∙∙lCancel refl)))) + +πHomEquiv→πHomCongEquiv : {A B : Type ℓ} {a : A} {n : ℕ} (f : A → B) + → isEquiv (fst (πHom {A = (A , a)} {B = (B , f a)} (1 + n) (f , refl))) + → isEquiv (fst (πHom {A = Ω (A , a)} n (cong f , refl))) +πHomEquiv→πHomCongEquiv {A = A} {a = a} {n = n} f hf = + squareWithEquivs→Equiv + ( fst (πHom n (cong f , refl))) + ( fst (πHom {A = (A , a)} (1 + n) (f , refl))) + ( Iso.fun (Iso-πΩ-π (1 + n))) + ( Iso.inv (Iso-πΩ-π (1 + n))) + ( hf) + ( snd (isoToEquiv (Iso-πΩ-π (1 + n)))) + ( snd (isoToEquiv (invIso (Iso-πΩ-π (1 + n))))) + ( πHomπHomCongSquare {A = A} {a = a} {n = n} f) + +-- helper lemmas for stronger statement: +-- (map f) is equiv and (cong f) is equiv together imply f is equiv +private + congEquiv→EquivAux : {A B : Type ℓ} + (f : A → B) + (hf0 : isEquiv (map f)) + (b : B) → Σ[ a ∈ ∥ A ∥₂ ] ((map f) a ≡ ∣ b ∣₂) + congEquiv→EquivAux f hf0 b = fst (equiv-proof hf0 ∣ b ∣₂) + + congEquiv→EquivAux''' : {A B : Type ℓ} + (f : A → B) + (b : B) + → Σ[ a ∈ ∥ A ∥₂ ] ((map f) a ≡ ∣ b ∣₂) + → ∥ Σ[ a ∈ A ] (f a ≡ b) ∥₁ + congEquiv→EquivAux''' {A = A} f b (a , p) = + ( sElim + { B = λ a → ((map f) a ≡ ∣ b ∣₂) → ∥ Σ[ a ∈ A ] (f a ≡ b) ∥₁} + ( λ a → isSet→ (isProp→isSet isPropPropTrunc)) + ( λ a p → rec isPropPropTrunc ( λ p' → ∣ a , p' ∣₁) + ( Iso.fun PathIdTrunc₀Iso p)) + ( a)) + ( p) + + congEquiv→EquivAux'' : {A B : Type ℓ} + (f : A → B) + (hf : (a b : A) → isEquiv {A = (a ≡ b)} (cong f)) + (b : B) + → (x y : Σ[ a ∈ A ] (f a ≡ b)) + → Σ[ r ∈ ((fst x) ≡ (fst y)) ] ((cong f) r ≡ (snd x) ∙ (sym (snd y))) + congEquiv→EquivAux'' f hf b x y = + fst (equiv-proof (hf (fst x) (fst y)) (snd x ∙ (sym (snd y)))) + + congEquiv→EquivAux' : {A B : Type ℓ} + (f : A → B) + (hf : (a b : A) → isEquiv {A = (a ≡ b)} (cong f)) + (b : B) → Σ[ a ∈ A ] (f a ≡ b) → isContr (Σ[ a ∈ A ] (f a ≡ b)) + congEquiv→EquivAux' f hf b (a , p) = + ( a , p) + , (λ y → ΣPathP ( fst (congEquiv→EquivAux'' f hf b (a , p) y) + , compPathR→PathP ( sym (assoc _ _ _ + ∙ sym (rUnit _) + ∙ cong (_∙ (snd y)) + ( snd ( congEquiv→EquivAux'' + f hf b (a , p) y)) + ∙ assoc _ _ _ ⁻¹ + ∙ cong (p ∙_) (lCancel (snd y)) + ∙ rUnit p ⁻¹)))) + + +-- Stronger statement +congEquiv→Equiv : {A B : Type ℓ} + (f : A → B) + (hf0 : isEquiv (map f)) + (hf : (a b : A) → isEquiv {A = (a ≡ b)} (cong f)) + → isEquiv f +equiv-proof (congEquiv→Equiv f hf0 hf) b = + rec isPropIsContr + ( congEquiv→EquivAux' f hf b) + ( congEquiv→EquivAux''' f b (congEquiv→EquivAux f hf0 b)) + +mapEquiv→imId→Id₋₁ : {A B : Type ℓ} {a b : A} (f : A → B) + (hf0 : isEquiv (map f)) + → (f a ≡ f b) → ∥ a ≡ b ∥₁ +mapEquiv→imId→Id₋₁ {a = a} {b = b} f hf0 p = + Iso.fun PathIdTrunc₀Iso + ( sym (fst (PathPΣ (snd (equiv-proof hf0 ∣ f b ∣₂) (∣ a ∣₂ , cong ∣_∣₂ p)))) + ∙ fst (PathPΣ (snd (equiv-proof hf0 ∣ f b ∣₂) (∣ b ∣₂ , refl)))) + +-- Stronger statement for Ω→ instead of cong +ΩEquiv→Equiv : {A B : Type ℓ} + (f : A → B) + (hf0 : isEquiv (map f)) + (hf : (a : A) + → isEquiv + ( fst (Ω→ {A = (A , a)} {B = (B , f a)} (f , refl)))) + → isEquiv f +ΩEquiv→Equiv {A = A} f hf0 hf = + congEquiv→Equiv f hf0 + (λ a b → isPointedTarget→isEquiv→isEquiv + ( cong f) + ( λ q → rec + ( isPropIsEquiv _) + ( λ p → squareWithEquivs→Equiv + ( cong f) + ( fst (Ω→ {A = (A , a)} (f , refl))) + ( λ r → r ∙ sym p) + ( λ r → r ∙ (cong f p)) + ( hf a) + ( snd (compPathrEquiv (sym p))) + ( snd (compPathrEquiv (cong f p))) + ( ΩCongSquare f p)) + ( mapEquiv→imId→Id₋₁ f hf0 q))) + +-- Appears as Theorem 8.8.3 in the HoTT Book +-- Proof similar to one there +WhiteheadsLemma : {A B : Type ℓ} {n : ℕ} + (hA : isOfHLevel n A) (hB : isOfHLevel n B) (f : A → B) + (hf0 : isEquiv (map f)) + (hf : (a : A) (k : ℕ) + → isEquiv (fst (πHom {A = (A , a)} {B = (B , f a)} k (f , refl)))) + → isEquiv f +WhiteheadsLemma {n = zero} hA hB f hf0 hf = isEquivFromIsContr f hA hB +WhiteheadsLemma {A = A} {B = B} {n = suc n} hA hB f hf0 hf = + ΩEquiv→Equiv + ( f) + ( hf0) + ( λ a → WhiteheadsLemma + ( isOfHLevelPath' n hA a a) + ( isOfHLevelPath' n hB (f a) (f a)) + ( fst (Ω→ {A = (A , a)} {B = (B , f a)} (f , refl))) + ( hf a 0) + ( ΩWhiteheadHyp a)) + where + congWhiteheadHyp : (a a' : A) (p : a ≡ a') (k : ℕ) + → isEquiv + ( fst (πHom + { A = ((a ≡ a') , p)} + { B = (((f a) ≡ (f a')) , cong f p)} + ( k) + ( cong f , refl))) + congWhiteheadHyp a a' = + J ( λ b p → (k : ℕ) + → isEquiv + ( fst (πHom + { A = ((a ≡ b) , p)} + { B = (((f a) ≡ (f b)) , cong f p)} + ( k) + ( cong f , refl)))) + ( λ k → πHomEquiv→πHomCongEquiv + { A = A} + { B = B} + { n = k} + ( f) + ( hf a (1 + k))) + + ΩWhiteheadHyp : (a : A) (p : fst (Ω (A , a))) (k : ℕ) + → isEquiv (fst (πHom k (fst (Ω→ (f , refl)) , refl))) + ΩWhiteheadHyp a p k = transport + ( λ i → isEquiv + ( fst (πHom {A = (typ (Ω (A , a)) , p)} k + ( (λ p → (rUnit + ( cong f p)) i) + , refl)))) + ( congWhiteheadHyp a a p k) diff --git a/Cubical/Tactics/Reflection.agda b/Cubical/Tactics/Reflection.agda index 9db131d08c..ba1d3b1a82 100644 --- a/Cubical/Tactics/Reflection.agda +++ b/Cubical/Tactics/Reflection.agda @@ -89,7 +89,7 @@ get-boundary tm = unapply-path tm >>= λ where equation-solver : List Name → (Term -> Term -> TC Term) → Bool → Term → TC Unit equation-solver don't-Reduce mk-call debug hole = withNormalisation false ( - dontReduceDefs don't-Reduce ( + withReduceDefs (false , don't-Reduce) ( do -- | First we normalize the goal goal ← inferType hole >>= reduce diff --git a/README.md b/README.md index 92faa73a1d..9ce7431e45 100644 --- a/README.md +++ b/README.md @@ -12,17 +12,18 @@ For detailed install instructions see the [INSTALL](https://github.com/agda/cubical/blob/master/INSTALL.md) file. If you want to use some specific release of Agda, -the following table lists which release of Agda you can use with which release of this library. +the following table lists which releases of Agda you can use with which release of this library. Agda versions as written below, correspond to tags. -| cubical library version | Agda version | -|-------------------------|----------------| -| `current master` | `v2.6.3` | -| `v0.5` | `v2.6.3` | -| `v0.4` | `v2.6.2.2` | -| `v0.3` | `v2.6.2` | -| `v0.2` | `v2.6.1.3` | -| `v0.1` | `v2.6.0.1` | +| cubical library version | Agda versions | +|-------------------------|-------------------| +| `current master` | `v2.6.4` | +| `v0.6` | `v2.6.4` | +| `v0.5` | `v2.6.3` `v2.6.4` | +| `v0.4` | `v2.6.2.2` | +| `v0.3` | `v2.6.2` | +| `v0.2` | `v2.6.1.3` | +| `v0.1` | `v2.6.0.1` | For example, if you have Agda 2.6.2.2, you can switch to version 0.4 of the cubical library with ``` diff --git a/cubical.agda-lib b/cubical.agda-lib index b9fcbdb627..6565f1c369 100644 --- a/cubical.agda-lib +++ b/cubical.agda-lib @@ -1,4 +1,4 @@ -name: cubical-0.5 +name: cubical-0.6 include: . depend: flags: --cubical --no-import-sorts -WnoUnsupportedIndexedMatch diff --git a/flake.lock b/flake.lock index 2be7b50878..b8510c40ce 100644 --- a/flake.lock +++ b/flake.lock @@ -10,16 +10,16 @@ ] }, "locked": { - "lastModified": 1669235596, - "narHash": "sha256-u4yZPqadMfTnE98c5FKV7yMY3cTehXqjNVZmXPXfkYo=", + "lastModified": 1696540558, + "narHash": "sha256-fqYyjgOFQrU4ryGcLyz5gMYMdPk1P24ra7kQiUrbilg=", "owner": "agda", "repo": "agda", - "rev": "19960e93da5bd775a795a4a3f7c301aceeca645d", + "rev": "f42acb696e43d382639f04f869e9a99ab36a91c6", "type": "github" }, "original": { "owner": "agda", - "ref": "release-2.6.3", + "ref": "v2.6.4", "repo": "agda", "type": "github" } @@ -27,11 +27,11 @@ "flake-compat": { "flake": false, "locked": { - "lastModified": 1668681692, - "narHash": "sha256-Ht91NGdewz8IQLtWZ9LCeNXMSXHUss+9COoqu6JLmXU=", + "lastModified": 1696426674, + "narHash": "sha256-kvjfFW7WAETZlt09AgDn1MrtKzP7t90Vf7vypd3OL1U=", "owner": "edolstra", "repo": "flake-compat", - "rev": "009399224d5e398d03b22badca40a37ac85412a1", + "rev": "0f9255e01c2351cc7d116c072cb317785dd33b33", "type": "github" }, "original": { @@ -41,12 +41,15 @@ } }, "flake-utils": { + "inputs": { + "systems": "systems" + }, "locked": { - "lastModified": 1667395993, - "narHash": "sha256-nuEHfE/LcWyuSWnS8t12N1wc105Qtau+/OdUAjtQ0rA=", + "lastModified": 1694529238, + "narHash": "sha256-zsNZZGTGnMOf9YpHKJqMSsa0dXbfmxeoJ7xHlrt+xmY=", "owner": "numtide", "repo": "flake-utils", - "rev": "5aed5285a952e0b949eb3ba02c12fa4fcfef535f", + "rev": "ff7b65b44d01cf9ba6a71320833626af21126384", "type": "github" }, "original": { @@ -57,11 +60,11 @@ }, "nixpkgs": { "locked": { - "lastModified": 1669165918, - "narHash": "sha256-hIVruk2+0wmw/Kfzy11rG3q7ev3VTi/IKVODeHcVjFo=", + "lastModified": 1696757521, + "narHash": "sha256-cfgtLNCBLFx2qOzRLI6DHfqTdfWI+UbvsKYa3b3fvaA=", "owner": "NixOS", "repo": "nixpkgs", - "rev": "3b400a525d92e4085e46141ff48cbf89fd89739e", + "rev": "2646b294a146df2781b1ca49092450e8a32814e1", "type": "github" }, "original": { @@ -77,6 +80,21 @@ "flake-utils": "flake-utils", "nixpkgs": "nixpkgs" } + }, + "systems": { + "locked": { + "lastModified": 1681028828, + "narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=", + "owner": "nix-systems", + "repo": "default", + "rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e", + "type": "github" + }, + "original": { + "owner": "nix-systems", + "repo": "default", + "type": "github" + } } }, "root": "root", diff --git a/flake.nix b/flake.nix index cec52b0c13..2d5fcb7c3d 100644 --- a/flake.nix +++ b/flake.nix @@ -8,7 +8,7 @@ flake = false; }; inputs.agda = { - url = "github:agda/agda/v2.6.3"; + url = "github:agda/agda/v2.6.4"; inputs = { nixpkgs.follows = "nixpkgs"; flake-utils.follows = "flake-utils"; @@ -21,7 +21,7 @@ overlay = final: prev: { cubical = final.agdaPackages.mkDerivation rec { pname = "cubical"; - version = "0.5"; + version = "0.6"; src = cleanSourceWith { filter = name: type: