From c6a96eeefc6f5f1ce346512d3130de45e4b9a065 Mon Sep 17 00:00:00 2001 From: Felix Cherubini Date: Fri, 2 Feb 2024 10:41:02 +0100 Subject: [PATCH] Check all agda files (#1058) * remove stuff with broken dependencies * Revert "remove stuff with broken dependencies" This reverts commit 6a0ded95bb8c51d07b25125319e1faa1ec850bb3. * fix * rm LocalizationDefs * fixes/commented out lots of things * no automatic Experiments/Everything.agda * deleted the two files --- .gitignore | 1 - Cubical/Experiments/CohomologyGroups.agda | 3 +- Cubical/Experiments/Combinatorics.agda | 3 +- Cubical/Experiments/Everything.agda | 16 - Cubical/Experiments/HInt.agda | 9 +- Cubical/Experiments/IntegerMatrix.agda | 3 +- Cubical/Experiments/LocalisationDefs.agda | 146 ------- .../Experiments/ZCohomologyExperiments.agda | 79 ---- .../MayerVietorisUnreduced.agda | 384 ------------------ .../Experiments/ZariskiLatticeBasicOpens.agda | 13 +- GNUmakefile | 4 +- 11 files changed, 21 insertions(+), 640 deletions(-) delete mode 100644 Cubical/Experiments/Everything.agda delete mode 100644 Cubical/Experiments/LocalisationDefs.agda delete mode 100644 Cubical/Experiments/ZCohomologyExperiments.agda delete mode 100644 Cubical/Experiments/ZCohomologyOld/MayerVietorisUnreduced.agda diff --git a/.gitignore b/.gitignore index 19f6faa6d4..7d344f2d84 100644 --- a/.gitignore +++ b/.gitignore @@ -6,4 +6,3 @@ Cubical/*/Everything.agda !Cubical/Core/Everything.agda !Cubical/Foundations/Everything.agda !Cubical/Codata/Everything.agda -!Cubical/Experiments/Everything.agda diff --git a/Cubical/Experiments/CohomologyGroups.agda b/Cubical/Experiments/CohomologyGroups.agda index 1f2403aac3..2887870e89 100644 --- a/Cubical/Experiments/CohomologyGroups.agda +++ b/Cubical/Experiments/CohomologyGroups.agda @@ -1,6 +1,6 @@ {-# OPTIONS --safe #-} module Cubical.Experiments.CohomologyGroups where - +{- open import Cubical.Experiments.ZCohomologyOld.Base open import Cubical.Experiments.ZCohomologyOld.Properties open import Cubical.Experiments.ZCohomologyOld.MayerVietorisUnreduced @@ -138,3 +138,4 @@ H¹-S¹≅ℤ = → Σ[ x ∈ Int ] (inv H⁰-S⁰≅ℤ×ℤ (x , x)) ≡ GroupHom.fun (K.Δ 0) (∣ f ∣₂ , ∣ g ∣₂) helper2 f g = (f _ -[ 0 ]ₖ g _) , cong ∣_∣₂ (funExt λ {true → refl ; false → refl}) +-} diff --git a/Cubical/Experiments/Combinatorics.agda b/Cubical/Experiments/Combinatorics.agda index ecf9ab7646..b49b1daf4b 100644 --- a/Cubical/Experiments/Combinatorics.agda +++ b/Cubical/Experiments/Combinatorics.agda @@ -78,10 +78,11 @@ s = refl p : prod (Fin _) f ≡ 6480 p = refl +{- -- the maximal value m : maxValue (Fin _) f ∣ fzero ∣ ≡ 9 m = refl - +-} -- the number of numeral 1 n1 : card (_ , isFinSetFiberDisc (Fin _) ℕ discreteℕ f 1) ≡ 2 n1 = refl diff --git a/Cubical/Experiments/Everything.agda b/Cubical/Experiments/Everything.agda deleted file mode 100644 index 3ba96c099c..0000000000 --- a/Cubical/Experiments/Everything.agda +++ /dev/null @@ -1,16 +0,0 @@ --- Export only the experiments that are expected to compile (without --- any holes) -module Cubical.Experiments.Everything where - -open import Cubical.Experiments.EscardoSIP public -open import Cubical.Experiments.Generic public -open import Cubical.Experiments.NatMinusTwo -open import Cubical.Experiments.IsoInt -open import Cubical.Experiments.HAEquivInt -open import Cubical.Experiments.Poset -open import Cubical.Experiments.Problem -open import Cubical.Experiments.FunExtFromUA public -open import Cubical.Experiments.HoTT-UF -open import Cubical.Experiments.ZCohomologyOld.Base -open import Cubical.Experiments.ZCohomologyOld.KcompPrelims -open import Cubical.Experiments.ZCohomologyOld.Properties diff --git a/Cubical/Experiments/HInt.agda b/Cubical/Experiments/HInt.agda index 7532ab79f8..73acec41c8 100644 --- a/Cubical/Experiments/HInt.agda +++ b/Cubical/Experiments/HInt.agda @@ -1,3 +1,4 @@ +{-# OPTIONS --safe #-} {- Definition of the integers as a HIT inspired by slide 10 of (original @@ -22,7 +23,8 @@ module Cubical.Experiments.HInt where open import Cubical.Foundations.Prelude open import Cubical.Foundations.Equiv open import Cubical.Foundations.Isomorphism -open import Cubical.Data.Int + +open import Cubical.Data.Int renaming (ℤ to Int; sucℤ to sucInt; predℤ to predInt; isSetℤ to isSetInt) open import Cubical.Data.Nat data ℤ : Type₀ where @@ -77,6 +79,7 @@ lem2 (pos (suc n)) = sym (predsuc (ℕ→ℤ n)) lem2 (negsuc n) = refl -- I don't see how to fill these holes, especially the last one +{- ℤ→Int→ℤ : ∀ (n : ℤ) → Int→ℤ (ℤ→Int n) ≡ n ℤ→Int→ℤ zero = refl ℤ→Int→ℤ (suc n) = (lem1 (ℤ→Int n)) ∙ (cong suc (ℤ→Int→ℤ n)) @@ -84,15 +87,17 @@ lem2 (negsuc n) = refl ℤ→Int→ℤ (sucpred n i) = {!!} ℤ→Int→ℤ (predsuc n i) = {!!} ℤ→Int→ℤ (coh n i j) = {!!} +-} Int→ℤ→Int : ∀ n → ℤ→Int (Int→ℤ n) ≡ n Int→ℤ→Int (pos zero) = refl Int→ℤ→Int (pos (suc n)) = cong sucInt (Int→ℤ→Int (pos n)) Int→ℤ→Int (negsuc zero) = refl Int→ℤ→Int (negsuc (suc n)) = cong predInt (Int→ℤ→Int (negsuc n)) - +{- Int≡ℤ : Int ≡ ℤ Int≡ℤ = isoToPath (iso Int→ℤ ℤ→Int ℤ→Int→ℤ Int→ℤ→Int) isSetℤ : isSet ℤ isSetℤ = subst isSet Int≡ℤ isSetInt +-} diff --git a/Cubical/Experiments/IntegerMatrix.agda b/Cubical/Experiments/IntegerMatrix.agda index 2331b6e545..ad70360209 100644 --- a/Cubical/Experiments/IntegerMatrix.agda +++ b/Cubical/Experiments/IntegerMatrix.agda @@ -16,7 +16,6 @@ open import Cubical.Data.List open import Cubical.Algebra.CommRing open import Cubical.Algebra.CommRing.Instances.Int - renaming (ℤ to ℤRing) open import Cubical.Algebra.Matrix open import Cubical.Algebra.Matrix.CommRingCoefficient @@ -27,7 +26,7 @@ private variable m n : ℕ -open Coefficient ℤRing +open Coefficient ℤCommRing -- Get divisors directly diff --git a/Cubical/Experiments/LocalisationDefs.agda b/Cubical/Experiments/LocalisationDefs.agda deleted file mode 100644 index f0e2da1c09..0000000000 --- a/Cubical/Experiments/LocalisationDefs.agda +++ /dev/null @@ -1,146 +0,0 @@ --- This file contains several ways to define localisation --- and proves them all to be equivalent - -{-# OPTIONS --safe #-} -module Cubical.Experiments.LocalisationDefs where - -open import Cubical.Foundations.Prelude -open import Cubical.Foundations.Function -open import Cubical.Foundations.Equiv -open import Cubical.Foundations.Isomorphism -open import Cubical.Foundations.Univalence -open import Cubical.Foundations.HLevels -open import Cubical.Foundations.Powerset -open import Cubical.Foundations.Transport -open import Cubical.Functions.FunExtEquiv - -import Cubical.Data.Empty as ⊥ -open import Cubical.Data.Bool -open import Cubical.Data.Vec -open import Cubical.Data.Sigma.Base -open import Cubical.Data.Sigma.Properties -open import Cubical.Data.FinData -open import Cubical.Relation.Nullary -open import Cubical.Relation.Binary - -open import Cubical.Algebra.Group -open import Cubical.Algebra.AbGroup -open import Cubical.Algebra.Monoid -open import Cubical.Algebra.Ring -open import Cubical.Algebra.CommRing - -open import Cubical.HITs.SetQuotients as SQ -open import Cubical.HITs.PropositionalTruncation as PT - -open Iso - -private - variable - ℓ ℓ' : Level - A : Type ℓ - -record isMultClosedSubset (R' : CommRing {ℓ}) (S' : ℙ (R' .fst)) : Type ℓ where - constructor - multclosedsubset - field - containsOne : (R' .snd .CommRingStr.1r) ∈ S' - multClosed : ∀ {s t} → s ∈ S' → t ∈ S' → (R' .snd .CommRingStr._·_ s t) ∈ S' - -module _ (R' : CommRing {ℓ}) (S' : ℙ (R' .fst)) (SMultClosedSubset : isMultClosedSubset R' S') where - open isMultClosedSubset - private R = R' .fst - open CommRingStr (R' .snd) - open Theory (CommRing→Ring R') - - S = Σ[ s ∈ R ] (s ∈ S') - - -- HIT definition - data S⁻¹R : Type ℓ where - _/ₗ_ : R → S → S⁻¹R - zd : (r₁ r₂ : R) (s s₁ s₂ : S) - → fst s · r₁ · fst s₂ ≡ fst s · r₂ · fst s₁ - → r₁ /ₗ s₁ ≡ r₂ /ₗ s₂ - trunc : isSet S⁻¹R - - infixr 5 _/ₗ_ - - - module Elim {ℓ'} {B : S⁻¹R → Type ℓ'} - (_/*_ : (r : R) (s : S) → B (r /ₗ s)) - (zd* : (r₁ r₂ : R) (s s₁ s₂ : S) - → (p : fst s · r₁ · fst s₂ ≡ fst s · r₂ · fst s₁) - → PathP (λ i → B (zd r₁ r₂ s s₁ s₂ p i)) (r₁ /* s₁) (r₂ /* s₂)) - (trunc* : (q : S⁻¹R) → isSet (B q)) where - - - f : (q : S⁻¹R) → B q - f (r /ₗ s) = r /* s - f (zd r₁ r₂ s s₁ s₂ p i) = zd* r₁ r₂ s s₁ s₂ p i - f (trunc q₁ q₂ x y i j) = isOfHLevel→isOfHLevelDep 2 trunc* (f q₁) (f q₂) (cong f x) (cong f y) - (trunc q₁ q₂ x y) i j - - - module ElimProp {ℓ'} {B : S⁻¹R → Type ℓ'} (Bprop : {q : S⁻¹R} → isProp (B q)) - (_/*_ : (r : R) → (s : S) → B (r /ₗ s)) where - - - f : (q : S⁻¹R) → B q - f = Elim.f _/*_ (λ r₁ r₂ s s₁ s₂ p - → toPathP (Bprop (transp (λ i → B (zd r₁ r₂ s s₁ s₂ p i)) i0 (r₁ /* s₁)) - (r₂ /* s₂))) - λ q → isProp→isSet Bprop - - - module Rec {ℓ'} {B : Type ℓ'} (BType : isSet B) - (_/*_ : R → S → B) - (zd* : (r₁ r₂ : R) (s s₁ s₂ : S) - → (p : fst s · r₁ · fst s₂ ≡ fst s · r₂ · fst s₁) - → r₁ /* s₁ ≡ r₂ /* s₂) - where - - f : S⁻¹R → B - f = Elim.f _/*_ zd* (λ _ → BType) - - - -- approach using set quotients - _≈_ : R × S → R × S → Type ℓ - (r₁ , s₁) ≈ (r₂ , s₂) = ∃[ s ∈ S ] (fst s · r₁ · fst s₂ ≡ fst s · r₂ · fst s₁) - - S⁻¹R/ = (R × S) / _≈_ - - -- proving equivalence of the two types - φ : S⁻¹R/ → S⁻¹R - φ = SQ.rec trunc (λ (r , s) → r /ₗ s) β - where - α : ((r₁ , s₁) (r₂ , s₂) : R × S) → Σ[ s ∈ S ] (fst s · r₁ · fst s₂ ≡ fst s · r₂ · fst s₁) - → r₁ /ₗ s₁ ≡ r₂ /ₗ s₂ - α _ _ (s , p) = zd _ _ s _ _ p - - β : ((r₁ , s₁) (r₂ , s₂) : R × S) → ∃[ s ∈ S ] (fst s · r₁ · fst s₂ ≡ fst s · r₂ · fst s₁) - → r₁ /ₗ s₁ ≡ r₂ /ₗ s₂ - β _ _ = PT.rec (trunc _ _) (α _ _) - - ψ : S⁻¹R → S⁻¹R/ - ψ (r /ₗ s) = [ r , s ] - ψ (zd r₁ r₂ s s₁ s₂ p i) = eq/ (r₁ , s₁) (r₂ , s₂) ∣ s , p ∣ i - ψ (trunc x y p q i j) = squash/ (ψ x) (ψ y) (cong ψ p) (cong ψ q) i j - - η : section φ ψ - η = ElimProp.f (trunc _ _) λ _ _ → refl - - ε : retract φ ψ - ε = elimProp (λ _ → squash/ _ _) λ _ → refl - - S⁻¹R/≃S⁻¹R : S⁻¹R/ ≃ S⁻¹R - S⁻¹R/≃S⁻¹R = isoToEquiv (iso φ ψ η ε) - - - -- Set quotients but with Σ, this is the type used in Algebra.Localisation.Base - -- as this is easiest to use - _≈'_ : R × S → R × S → Type ℓ - (r₁ , s₁) ≈' (r₂ , s₂) = Σ[ s ∈ S ] (fst s · r₁ · fst s₂ ≡ fst s · r₂ · fst s₁) - - S⁻¹R/' = (R × S) / _≈'_ - - S⁻¹R/'≃S⁻¹R/ : S⁻¹R/' ≃ S⁻¹R/ - S⁻¹R/'≃S⁻¹R/ = SQ.truncRelEquiv diff --git a/Cubical/Experiments/ZCohomologyExperiments.agda b/Cubical/Experiments/ZCohomologyExperiments.agda deleted file mode 100644 index fec50806b9..0000000000 --- a/Cubical/Experiments/ZCohomologyExperiments.agda +++ /dev/null @@ -1,79 +0,0 @@ -{-# OPTIONS --safe #-} -module Cubical.Experiments.ZCohomologyExperiments where -open import Cubical.ZCohomology.Base -open import Cubical.ZCohomology.Properties -open import Cubical.ZCohomology.GroupStructure -open import Cubical.ZCohomology.Groups.Sn -open import Cubical.ZCohomology.Groups.S2wedgeS1wedgeS1 -open import Cubical.Foundations.Prelude - -open import Cubical.HITs.Truncation -open import Cubical.HITs.SetTruncation -open import Cubical.HITs.Pushout -open import Cubical.HITs.S1 -open import Cubical.HITs.Sn -open import Cubical.HITs.Susp -open import Cubical.Data.Int -open import Cubical.Foundations.Equiv -open import Cubical.Data.Sigma -open import Cubical.Foundations.Isomorphism -open import Cubical.Algebra.Group hiding (Int) - -private - - ⋁-to : coHom 2 S²⋁S¹⋁S¹ → Int - ⋁-to = Iso.fun (GroupIso.isom H²-S²⋁S¹⋁S¹) - ⋁-from : Int → coHom 2 S²⋁S¹⋁S¹ - ⋁-from = Iso.inv (GroupIso.isom H²-S²⋁S¹⋁S¹) - - g : S²⋁S¹⋁S¹ → ∥ S₊ 2 ∥ 4 - g (inl x) = ∣ x ∣ - g (inr x) = 0ₖ 2 - g (push a i) = 0ₖ 2 - - G = ∣ g ∣₂ - -{- -This computes: -⋁-to (⋁-from 1 +ₕ ⋁-from 1) ≡ 2 -⋁-to = refl - -We have ⋁-from 1 ≡ G and G is much simpler - -But this does not compute: -test₀ : ⋁-to (G +ₕ G) ≡ 2 -test₀ = refl - -With the strange addition it does: -test₁ : ⋁-to (G +'ₕ G) ≡ 2 -test₁ = refl --} - --- Similar stuff happens with Sⁿ. -private - S²-to : coHom 2 (S₊ 2) → Int - S²-to = Iso.fun (GroupIso.isom (Hⁿ-Sⁿ≅ℤ 1)) - - S²-from : Int → coHom 2 (S₊ 2) - S²-from = Iso.inv (GroupIso.isom (Hⁿ-Sⁿ≅ℤ 1)) - - one : coHom 2 (S₊ 2) - one = ∣ ∣_∣ ∣₂ - -{- -Does not compute -test₂ : S²-to (S²-from 1 +ₕ S²-from 1) ≡ 2 -test₂ = refl - -But this does -test₂ : S²-to (S²-from 1 +'ₕ S²-from 1) ≡ 2 -test₂ = refl - -This doesn't -test₃ : S²-to (one +ₕ one) ≡ 2 -test₃ = refl - -But this does -test₃ : S²-to (one +'ₕ one) ≡ 2 -test₃ = refl --} diff --git a/Cubical/Experiments/ZCohomologyOld/MayerVietorisUnreduced.agda b/Cubical/Experiments/ZCohomologyOld/MayerVietorisUnreduced.agda deleted file mode 100644 index 8ad1449b2e..0000000000 --- a/Cubical/Experiments/ZCohomologyOld/MayerVietorisUnreduced.agda +++ /dev/null @@ -1,384 +0,0 @@ -{-# OPTIONS --safe #-} -module Cubical.Experiments.ZCohomologyOld.MayerVietorisUnreduced where - -open import Cubical.ZCohomology.Base -open import Cubical.Experiments.ZCohomologyOld.Properties -open import Cubical.Experiments.ZCohomologyOld.KcompPrelims hiding (ϕ) - -open import Cubical.Foundations.HLevels -open import Cubical.Foundations.Function -open import Cubical.Foundations.Prelude -open import Cubical.Foundations.Structure -open import Cubical.Foundations.Isomorphism -open import Cubical.Foundations.GroupoidLaws -open import Cubical.Data.Sigma -open import Cubical.HITs.Pushout -open import Cubical.HITs.Sn -open import Cubical.HITs.S1 -open import Cubical.HITs.Susp -open import Cubical.HITs.SetTruncation renaming (rec to sRec ; rec2 to sRec2 ; elim to sElim ; elim2 to sElim2) -open import Cubical.HITs.PropositionalTruncation renaming (rec to pRec ; elim to pElim ; elim2 to pElim2 ; ∥_∥ to ∥_∥₁ ; ∣_∣ to ∣_∣₁) -open import Cubical.Data.Nat -open import Cubical.Data.Prod hiding (_×_) -open import Cubical.Algebra.Group -open import Cubical.HITs.Truncation renaming (elim to trElim ; map to trMap ; rec to trRec ; elim3 to trElim3) - -open GroupHom - --- "Very" short exact sequences --- i.e. an exact sequence A → B → C → D where A and D are trivial -record vSES {ℓ ℓ' ℓ'' ℓ'''} (A : Group {ℓ}) (B : Group {ℓ'}) (leftGr : Group {ℓ''}) (rightGr : Group {ℓ'''}) - : Type (ℓ-suc (ℓ-max ℓ (ℓ-max ℓ' (ℓ-max ℓ'' ℓ''')))) where - constructor vses - - field - isTrivialLeft : isProp ⟨ leftGr ⟩ - isTrivialRight : isProp ⟨ rightGr ⟩ - - left : GroupHom leftGr A - right : GroupHom B rightGr - ϕ : GroupHom A B - - Ker-ϕ⊂Im-left : (x : ⟨ A ⟩) - → isInKer ϕ x - → isInIm left x - Ker-right⊂Im-ϕ : (x : ⟨ B ⟩) - → isInKer right x - → isInIm ϕ x - -open BijectionIso -open vSES - -vSES→GroupIso : ∀ {ℓ ℓ' ℓ'' ℓ'''} {A : Group {ℓ}} {B : Group {ℓ'}} (leftGr : Group {ℓ''}) (rightGr : Group {ℓ'''}) - → vSES A B leftGr rightGr - → GroupIso A B -vSES→GroupIso {A = A} lGr rGr isvses = BijectionIsoToGroupIso theIso - where - theIso : BijectionIso _ _ - fun theIso = vSES.ϕ isvses - inj theIso a inker = pRec (isSetCarrier A _ _) - (λ (a , p) → sym p - ∙∙ cong (fun (left isvses)) (isTrivialLeft isvses a _) - ∙∙ morph1g→1g lGr A (left isvses)) - (Ker-ϕ⊂Im-left isvses a inker) - surj theIso a = Ker-right⊂Im-ϕ isvses a (isTrivialRight isvses _ _) - -vSES→GroupEquiv : {ℓ ℓ₁ ℓ₂ ℓ₃ : Level} {A : Group {ℓ}} {B : Group {ℓ₁}} (leftGr : Group {ℓ₂}) (rightGr : Group {ℓ₃}) - → vSES A B leftGr rightGr - → GroupEquiv A B -vSES→GroupEquiv lGr rGr isvses = GrIsoToGrEquiv (vSES→GroupIso lGr rGr isvses) - -module MV {ℓ ℓ' ℓ''} (A : Type ℓ) (B : Type ℓ') (C : Type ℓ'') (f : C → A) (g : C → B) where - -- Proof from Brunerie 2016. - -- We first define the three morphisms involved: i, Δ and d. - - private - i* : (n : ℕ) → coHom n (Pushout f g) → coHom n A × coHom n B - i* _ = sRec (isSet× isSetSetTrunc isSetSetTrunc) λ δ → ∣ (λ x → δ (inl x)) ∣₂ , ∣ (λ x → δ (inr x)) ∣₂ - - iIsHom : (n : ℕ) → isGroupHom (coHomGr n (Pushout f g)) (×coHomGr n A B) (i* n) - iIsHom _ = sElim2 (λ _ _ → isOfHLevelPath 2 (isSet× isSetSetTrunc isSetSetTrunc) _ _) λ _ _ → refl - - i : (n : ℕ) → GroupHom (coHomGr n (Pushout f g)) (×coHomGr n A B) - GroupHom.fun (i n) = i* n - GroupHom.isHom (i n) = iIsHom n - - - private - distrLem : (n : ℕ) (x y z w : coHomK n) → (x +[ n ]ₖ y) -[ n ]ₖ (z +[ n ]ₖ w) ≡ (x -[ n ]ₖ z) +[ n ]ₖ (y -[ n ]ₖ w) - distrLem n x y z w = - cong (ΩKn+1→Kn n) (cong₂ (λ q p → q ∙ sym p) (+ₖ→∙ n x y) (+ₖ→∙ n z w) - ∙∙ cong ((Kn→ΩKn+1 n x ∙ Kn→ΩKn+1 n y) ∙_) (symDistr (Kn→ΩKn+1 n z) (Kn→ΩKn+1 n w)) - ∙∙ ((sym (assoc (Kn→ΩKn+1 n x) (Kn→ΩKn+1 n y) _)) - ∙∙ cong (Kn→ΩKn+1 n x ∙_) (assoc (Kn→ΩKn+1 n y) (sym (Kn→ΩKn+1 n w)) (sym (Kn→ΩKn+1 n z))) - ∙∙ (cong (Kn→ΩKn+1 n x ∙_) (isCommΩK (suc n) _ _) - ∙∙ assoc _ _ _ - ∙∙ cong₂ _∙_ (sym (Iso.rightInv (Iso-Kn-ΩKn+1 n) (Kn→ΩKn+1 n x ∙ sym (Kn→ΩKn+1 n z)))) - (sym (Iso.rightInv (Iso-Kn-ΩKn+1 n) (Kn→ΩKn+1 n y ∙ sym (Kn→ΩKn+1 n w))))))) - - - Δ' : (n : ℕ) → ⟨ ×coHomGr n A B ⟩ → ⟨ coHomGr n C ⟩ - Δ' n (α , β) = coHomFun n f α -[ n ]ₕ coHomFun n g β - - Δ'-isMorph : (n : ℕ) → isGroupHom (×coHomGr n A B) (coHomGr n C) (Δ' n) - Δ'-isMorph n = - prodElim2 (λ _ _ → isOfHLevelPath 2 isSetSetTrunc _ _ ) - λ f' x1 g' x2 i → ∣ (λ x → distrLem n (f' (f x)) (g' (f x)) (x1 (g x)) (x2 (g x)) i) ∣₂ - - Δ : (n : ℕ) → GroupHom (×coHomGr n A B) (coHomGr n C) - GroupHom.fun (Δ n) = Δ' n - GroupHom.isHom (Δ n) = Δ'-isMorph n - - d-pre : (n : ℕ) → (C → coHomK n) → Pushout f g → coHomK (suc n) - d-pre n γ (inl x) = 0ₖ (suc n) - d-pre n γ (inr x) = 0ₖ (suc n) - d-pre zero γ (push a i) = Kn→ΩKn+1 zero (γ a) i - d-pre (suc n) γ (push a i) = Kn→ΩKn+1 (suc n) (γ a) i - - dHomHelperPath : (n : ℕ) (h l : C → coHomK n) (a : C) → I → I → coHomK (suc n) - dHomHelperPath zero h l a i j = - hcomp (λ k → λ { (i = i0) → lUnitₖ 1 (0ₖ 1) (~ j) - ; (i = i1) → lUnitₖ 1 (0ₖ 1) (~ j) - ; (j = i0) → +ₖ→∙ 0 (h a) (l a) (~ k) i - ; (j = i1) → cong₂Funct (λ x y → x +[ 1 ]ₖ y) - (Kn→ΩKn+1 0 (h a)) (Kn→ΩKn+1 0 (l a)) (~ k) i}) - (bottom i j) - where - bottom : I → I → coHomK 1 - bottom i j = hcomp (λ k → λ { (i = i0) → lUnitₖ 1 (0ₖ 1) (~ j) - ; (i = i1) → lUnitₖ 1 (Kn→ΩKn+1 0 (l a) k) (~ j) }) - (anotherbottom i j) - - where - anotherbottom : I → I → coHomK 1 - anotherbottom i j = hcomp (λ k → λ { (i = i0) → rUnitlUnit0 1 k (~ j) - ; (i = i1) → rUnitlUnit0 1 k (~ j) - ; (j = i0) → Kn→ΩKn+1 0 (h a) i - ; (j = i1) → Kn→ΩKn+1 0 (h a) i +[ 1 ]ₖ 0ₖ 1 }) - (rUnitₖ 1 (Kn→ΩKn+1 0 (h a) i) (~ j)) - dHomHelperPath (suc n) h l a i j = - hcomp (λ k → λ { (i = i0) → lUnitₖ (2 + n) (0ₖ (2 + n)) (~ j) - ; (i = i1) → lUnitₖ (2 + n) (0ₖ (2 + n)) (~ j) - ; (j = i0) → +ₖ→∙ (suc n) (h a) (l a) (~ k) i - ; (j = i1) → cong₂Funct (λ x y → x +[ 2 + n ]ₖ y) - (Kn→ΩKn+1 (suc n) (h a)) (Kn→ΩKn+1 (suc n) (l a)) (~ k) i}) - (bottom i j) - where - bottom : I → I → coHomK (2 + n) - bottom i j = hcomp (λ k → λ { (i = i0) → lUnitₖ (2 + n) (0ₖ (2 + n)) (~ j) - ; (i = i1) → lUnitₖ (2 + n) (Kn→ΩKn+1 (suc n) (l a) k) (~ j) }) - (anotherbottom i j) - - where - anotherbottom : I → I → coHomK (2 + n) - anotherbottom i j = hcomp (λ k → λ { (i = i0) → rUnitlUnit0 (2 + n) k (~ j) - ; (i = i1) → rUnitlUnit0 (2 + n) k (~ j) - ; (j = i0) → Kn→ΩKn+1 (suc n) (h a) i - ; (j = i1) → Kn→ΩKn+1 (suc n) (h a) i +[ 2 + n ]ₖ (0ₖ (2 + n)) }) - (rUnitₖ (2 + n) (Kn→ΩKn+1 (suc n) (h a) i) (~ j)) - - dHomHelper : (n : ℕ) (h l : C → coHomK n) (x : Pushout f g) - → d-pre n (λ x → h x +[ n ]ₖ l x) x ≡ d-pre n h x +[ suc n ]ₖ d-pre n l x - dHomHelper n h l (inl x) = sym (lUnitₖ (suc n) (0ₖ (suc n))) - dHomHelper n h l (inr x) = sym (lUnitₖ (suc n) (0ₖ (suc n))) - dHomHelper zero h l (push a i) j = dHomHelperPath zero h l a i j - dHomHelper (suc n) h l (push a i) j = dHomHelperPath (suc n) h l a i j - - dIsHom : (n : ℕ) → isGroupHom (coHomGr n C) (coHomGr (suc n) (Pushout f g)) (sRec isSetSetTrunc λ a → ∣ d-pre n a ∣₂) - dIsHom zero = sElim2 (λ _ _ → isOfHLevelPath 2 isSetSetTrunc _ _) - λ f g i → ∣ funExt (λ x → dHomHelper zero f g x) i ∣₂ - dIsHom (suc n) = sElim2 (λ _ _ → isOfHLevelPath 2 isSetSetTrunc _ _) - λ f g i → ∣ funExt (λ x → dHomHelper (suc n) f g x) i ∣₂ - - d : (n : ℕ) → GroupHom (coHomGr n C) (coHomGr (suc n) (Pushout f g)) - GroupHom.fun (d n) = sRec isSetSetTrunc λ a → ∣ d-pre n a ∣₂ - GroupHom.isHom (d n) = dIsHom n - - -- The long exact sequence - Im-d⊂Ker-i : (n : ℕ) (x : ⟨ (coHomGr (suc n) (Pushout f g)) ⟩) - → isInIm (d n) x - → isInKer (i (suc n)) x - Im-d⊂Ker-i n = sElim (λ _ → isSetΠ λ _ → isOfHLevelPath 2 (isSet× isSetSetTrunc isSetSetTrunc) _ _) - λ a → pRec (isOfHLevelPath' 1 (isSet× isSetSetTrunc isSetSetTrunc) _ _) - (sigmaElim (λ _ → isOfHLevelPath 2 (isSet× isSetSetTrunc isSetSetTrunc) _ _) - λ δ b i → sRec (isSet× isSetSetTrunc isSetSetTrunc) - (λ δ → ∣ (λ x → δ (inl x)) ∣₂ , ∣ (λ x → δ (inr x)) ∣₂ ) (b (~ i))) - - - Ker-i⊂Im-d : (n : ℕ) (x : ⟨ coHomGr (suc n) (Pushout f g) ⟩) - → isInKer (i (suc n)) x - → isInIm (d n) x - Ker-i⊂Im-d zero = - sElim (λ _ → isSetΠ λ _ → isProp→isSet isPropPropTrunc) - λ a p → pRec {A = (λ x → a (inl x)) ≡ λ _ → 0ₖ 1} - (isProp→ isPropPropTrunc) - (λ p1 → pRec isPropPropTrunc λ p2 → ∣ ∣ (λ c → ΩKn+1→Kn 0 (sym (cong (λ F → F (f c)) p1) - ∙∙ cong a (push c) - ∙∙ cong (λ F → F (g c)) p2)) ∣₂ - , cong ∣_∣₂ (funExt (λ δ → helper a p1 p2 δ)) ∣₁) - (Iso.fun PathIdTrunc₀Iso (cong fst p)) - (Iso.fun PathIdTrunc₀Iso (cong snd p)) - - where - helper : (F : (Pushout f g) → hLevelTrunc 3 (S₊ 1)) - (p1 : Path (_ → hLevelTrunc 3 (S₊ 1)) (λ a₁ → F (inl a₁)) (λ _ → ∣ base ∣)) - (p2 : Path (_ → hLevelTrunc 3 (S₊ 1)) (λ a₁ → F (inr a₁)) (λ _ → ∣ base ∣)) - → (δ : Pushout f g) - → d-pre 0 (λ c → ΩKn+1→Kn 0 ((λ i₁ → p1 (~ i₁) (f c)) - ∙∙ cong F (push c) - ∙∙ cong (λ F → F (g c)) p2)) δ - ≡ F δ - helper F p1 p2 (inl x) = sym (cong (λ f → f x) p1) - helper F p1 p2 (inr x) = sym (cong (λ f → f x) p2) - helper F p1 p2 (push a i) j = - hcomp (λ k → λ { (i = i0) → p1 (~ j) (f a) - ; (i = i1) → p2 (~ j) (g a) - ; (j = i0) → Iso.rightInv (Iso-Kn-ΩKn+1 0) ((λ i₁ → p1 (~ i₁) (f a)) - ∙∙ cong F (push a) - ∙∙ cong (λ F₁ → F₁ (g a)) p2) (~ k) i - ; (j = i1) → F (push a i)}) - (doubleCompPath-filler (sym (cong (λ F → F (f a)) p1)) (cong F (push a)) (cong (λ F → F (g a)) p2) (~ j) i) - Ker-i⊂Im-d (suc n) = - sElim (λ _ → isSetΠ λ _ → isProp→isSet isPropPropTrunc) - λ a p → pRec {A = (λ x → a (inl x)) ≡ λ _ → 0ₖ (2 + n)} (isProp→ isPropPropTrunc) - (λ p1 → pRec isPropPropTrunc λ p2 → ∣ ∣ (λ c → ΩKn+1→Kn (suc n) (sym (cong (λ F → F (f c)) p1) - ∙∙ cong a (push c) - ∙∙ cong (λ F → F (g c)) p2)) ∣₂ - , cong ∣_∣₂ (funExt (λ δ → helper a p1 p2 δ)) ∣₁) - (Iso.fun PathIdTrunc₀Iso (cong fst p)) - (Iso.fun PathIdTrunc₀Iso (cong snd p)) - - where - helper : (F : (Pushout f g) → hLevelTrunc (4 + n) (S₊ (2 + n))) - (p1 : Path (_ → hLevelTrunc (4 + n) (S₊ (2 + n))) (λ a₁ → F (inl a₁)) (λ _ → ∣ north ∣)) - (p2 : Path (_ → hLevelTrunc (4 + n) (S₊ (2 + n))) (λ a₁ → F (inr a₁)) (λ _ → ∣ north ∣)) - → (δ : (Pushout f g)) - → d-pre (suc n) (λ c → ΩKn+1→Kn (suc n) ((λ i₁ → p1 (~ i₁) (f c)) - ∙∙ cong F (push c) - ∙∙ cong (λ F → F (g c)) p2)) δ - ≡ F δ - helper F p1 p2 (inl x) = sym (cong (λ f → f x) p1) - helper F p1 p2 (inr x) = sym (cong (λ f → f x) p2) - helper F p1 p2 (push a i) j = - hcomp (λ k → λ { (i = i0) → p1 (~ j) (f a) - ; (i = i1) → p2 (~ j) (g a) - ; (j = i0) → Iso.rightInv (Iso-Kn-ΩKn+1 (suc n)) ((λ i₁ → p1 (~ i₁) (f a)) - ∙∙ cong F (push a) - ∙∙ cong (λ F₁ → F₁ (g a)) p2) (~ k) i - ; (j = i1) → F (push a i)}) - (doubleCompPath-filler (sym (cong (λ F → F (f a)) p1)) (cong F (push a)) (cong (λ F → F (g a)) p2) (~ j) i) - - open GroupHom - - Im-i⊂Ker-Δ : (n : ℕ) (x : ⟨ ×coHomGr n A B ⟩) - → isInIm (i n) x - → isInKer (Δ n) x - Im-i⊂Ker-Δ n (Fa , Fb) = - sElim {B = λ Fa → (Fb : _) → isInIm (i n) (Fa , Fb) - → isInKer (Δ n) (Fa , Fb)} - (λ _ → isSetΠ2 λ _ _ → isOfHLevelPath 2 isSetSetTrunc _ _) - (λ Fa → sElim (λ _ → isSetΠ λ _ → isOfHLevelPath 2 isSetSetTrunc _ _) - λ Fb → pRec (isSetSetTrunc _ _) - (sigmaElim (λ x → isProp→isSet (isSetSetTrunc _ _)) - λ Fd p → helper n Fa Fb Fd p)) - Fa - Fb - where - helper : (n : ℕ) (Fa : A → coHomK n) (Fb : B → coHomK n) (Fd : (Pushout f g) → coHomK n) - → (fun (i n) ∣ Fd ∣₂ ≡ (∣ Fa ∣₂ , ∣ Fb ∣₂)) - → (fun (Δ n)) (∣ Fa ∣₂ , ∣ Fb ∣₂) ≡ 0ₕ n - helper zero Fa Fb Fd p = cong (fun (Δ zero)) (sym p) - ∙∙ (λ i → ∣ (λ x → Fd (inl (f x))) ∣₂ -[ 0 ]ₕ ∣ (λ x → Fd (push x (~ i))) ∣₂ ) - ∙∙ cancelₕ 0 ∣ (λ x → Fd (inl (f x))) ∣₂ - helper (suc n) Fa Fb Fd p = cong (fun (Δ (suc n))) (sym p) - ∙∙ (λ i → ∣ (λ x → Fd (inl (f x))) ∣₂ -[ (suc n) ]ₕ ∣ (λ x → Fd (push x (~ i))) ∣₂) - ∙∙ cancelₕ (suc n) ∣ (λ x → Fd (inl (f x))) ∣₂ - - Ker-Δ⊂Im-i : (n : ℕ) (a : ⟨ ×coHomGr n A B ⟩) - → isInKer (Δ n) a - → isInIm (i n) a - Ker-Δ⊂Im-i n = prodElim (λ _ → isSetΠ (λ _ → isProp→isSet isPropPropTrunc)) - (λ Fa Fb p → pRec isPropPropTrunc - (λ q → ∣ ∣ helpFun Fa Fb q ∣₂ , refl ∣₁) - (helper Fa Fb p)) - where - helper : (Fa : A → coHomK n) (Fb : B → coHomK n) - → fun (Δ n) (∣ Fa ∣₂ , ∣ Fb ∣₂) ≡ 0ₕ n - → ∥ Path (_ → _) (λ c → Fa (f c)) (λ c → Fb (g c)) ∥₁ - helper Fa Fb p = Iso.fun PathIdTrunc₀Iso - (sym (-+cancelₕ n ∣ (λ c → Fa (f c)) ∣₂ ∣ (λ c → Fb (g c)) ∣₂) - ∙∙ cong (λ x → x +[ n ]ₕ ∣ (λ c → Fb (g c)) ∣₂) p - ∙∙ lUnitₕ n _) - - helpFun : (Fa : A → coHomK n) (Fb : B → coHomK n) - → ((λ c → Fa (f c)) ≡ (λ c → Fb (g c))) - → Pushout f g → coHomK n - helpFun Fa Fb p (inl x) = Fa x - helpFun Fa Fb p (inr x) = Fb x - helpFun Fa Fb p (push a i) = p i a - - - private - distrHelper : (n : ℕ) (p q : _) - → ΩKn+1→Kn n p +[ n ]ₖ (-[ n ]ₖ ΩKn+1→Kn n q) ≡ ΩKn+1→Kn n (p ∙ sym q) - distrHelper n p q i = - ΩKn+1→Kn n (Iso.rightInv (Iso-Kn-ΩKn+1 n) p i - ∙ Iso.rightInv (Iso-Kn-ΩKn+1 n) (sym (Iso.rightInv (Iso-Kn-ΩKn+1 n) q i)) i) - - Ker-d⊂Im-Δ : (n : ℕ) (a : coHom n C) - → isInKer (d n) a - → isInIm (Δ n) a - Ker-d⊂Im-Δ zero = - sElim (λ _ → isOfHLevelΠ 2 λ _ → isOfHLevelSuc 1 isPropPropTrunc) - λ Fc p → pRec isPropPropTrunc (λ p → ∣ (∣ (λ a → ΩKn+1→Kn 0 (cong (λ f → f (inl a)) p)) ∣₂ , - ∣ (λ b → ΩKn+1→Kn 0 (cong (λ f → f (inr b)) p)) ∣₂) , - Iso.inv (PathIdTrunc₀Iso) ∣ funExt (λ c → helper2 Fc p c) ∣₁ ∣₁) - (Iso.fun (PathIdTrunc₀Iso) p) - - where - - helper2 : (Fc : C → coHomK 0) - (p : d-pre 0 Fc ≡ (λ _ → ∣ base ∣)) (c : C) - → ΩKn+1→Kn 0 (λ i₁ → p i₁ (inl (f c))) -[ 0 ]ₖ (ΩKn+1→Kn 0 (λ i₁ → p i₁ (inr (g c)))) ≡ Fc c - helper2 Fc p c = cong₂ (λ x y → ΩKn+1→Kn 0 (x ∙ sym y)) (Iso.rightInv (Iso-Kn-ΩKn+1 0) (λ i₁ → p i₁ (inl (f c)))) - (Iso.rightInv (Iso-Kn-ΩKn+1 0) (λ i₁ → p i₁ (inr (g c)))) - ∙∙ cong (ΩKn+1→Kn 0) (sym ((PathP→compPathR (cong (λ f → cong f (push c)) p)) - ∙ (λ i → (λ i₁ → p i₁ (inl (f c))) - ∙ (lUnit (sym (λ i₁ → p i₁ (inr (g c)))) (~ i))))) - ∙∙ Iso.leftInv (Iso-Kn-ΩKn+1 zero) (Fc c) - Ker-d⊂Im-Δ (suc n) = - sElim (λ _ → isOfHLevelΠ 2 λ _ → isOfHLevelSuc 1 isPropPropTrunc) - λ Fc p → pRec isPropPropTrunc (λ p → ∣ (∣ (λ a → ΩKn+1→Kn (suc n) (cong (λ f → f (inl a)) p)) ∣₂ , - ∣ (λ b → ΩKn+1→Kn (suc n) (cong (λ f → f (inr b)) p)) ∣₂) , - Iso.inv (PathIdTrunc₀Iso) ∣ funExt (λ c → helper2 Fc p c) ∣₁ ∣₁) - (Iso.fun (PathIdTrunc₀Iso) p) - - where - - helper2 : (Fc : C → coHomK (suc n)) - (p : d-pre (suc n) Fc ≡ (λ _ → ∣ north ∣)) (c : C) - → ΩKn+1→Kn (suc n) (λ i₁ → p i₁ (inl (f c))) -[ (suc n) ]ₖ (ΩKn+1→Kn (suc n) (λ i₁ → p i₁ (inr (g c)))) ≡ Fc c - helper2 Fc p c = cong₂ (λ x y → ΩKn+1→Kn (suc n) (x ∙ sym y)) (Iso.rightInv (Iso-Kn-ΩKn+1 (suc n)) (λ i₁ → p i₁ (inl (f c)))) - (Iso.rightInv (Iso-Kn-ΩKn+1 (suc n)) (λ i₁ → p i₁ (inr (g c)))) - ∙∙ cong (ΩKn+1→Kn (suc n)) (sym ((PathP→compPathR (cong (λ f → cong f (push c)) p)) - ∙ (λ i → (λ i₁ → p i₁ (inl (f c))) - ∙ (lUnit (sym (λ i₁ → p i₁ (inr (g c)))) (~ i))))) - ∙∙ Iso.leftInv (Iso-Kn-ΩKn+1 (suc n)) (Fc c) - - Im-Δ⊂Ker-d : (n : ℕ) (a : coHom n C) - → isInIm (Δ n) a - → isInKer (d n) a - Im-Δ⊂Ker-d n = - sElim (λ _ → isOfHLevelΠ 2 λ _ → isOfHLevelPath 2 isSetSetTrunc _ _) - λ Fc → pRec (isOfHLevelPath' 1 isSetSetTrunc _ _) - (sigmaProdElim (λ _ → isOfHLevelPath 2 isSetSetTrunc _ _) - λ Fa Fb p → pRec (isOfHLevelPath' 1 isSetSetTrunc _ _) - (λ q → ((λ i → fun (d n) ∣ (q (~ i)) ∣₂) ∙ dΔ-Id n Fa Fb)) - (Iso.fun (PathIdTrunc₀Iso) p)) - - where - d-preLeftId : (n : ℕ) (Fa : A → coHomK n)(d : (Pushout f g)) - → d-pre n (Fa ∘ f) d ≡ 0ₖ (suc n) - d-preLeftId zero Fa (inl x) = Kn→ΩKn+1 0 (Fa x) - d-preLeftId (suc n) Fa (inl x) = Kn→ΩKn+1 (suc n) (Fa x) - d-preLeftId zero Fa (inr x) = refl - d-preLeftId (suc n) Fa (inr x) = refl - d-preLeftId zero Fa (push a i) j = Kn→ΩKn+1 zero (Fa (f a)) (j ∨ i) - d-preLeftId (suc n) Fa (push a i) j = Kn→ΩKn+1 (suc n) (Fa (f a)) (j ∨ i) - - d-preRightId : (n : ℕ) (Fb : B → coHomK n) (d : (Pushout f g)) - → d-pre n (Fb ∘ g) d ≡ 0ₖ (suc n) - d-preRightId n Fb (inl x) = refl - d-preRightId zero Fb (inr x) = sym (Kn→ΩKn+1 0 (Fb x)) - d-preRightId (suc n) Fb (inr x) = sym (Kn→ΩKn+1 (suc n) (Fb x)) - d-preRightId zero Fb (push a i) j = Kn→ΩKn+1 zero (Fb (g a)) (~ j ∧ i) - d-preRightId (suc n) Fb (push a i) j = Kn→ΩKn+1 (suc n) (Fb (g a)) (~ j ∧ i) - - dΔ-Id : (n : ℕ) (Fa : A → coHomK n) (Fb : B → coHomK n) - → fun (d n) (fun (Δ n) (∣ Fa ∣₂ , ∣ Fb ∣₂)) ≡ 0ₕ (suc n) - dΔ-Id zero Fa Fb = -distrLemma 0 1 (d zero) ∣ Fa ∘ f ∣₂ ∣ Fb ∘ g ∣₂ - ∙∙ (λ i → ∣ (λ x → d-preLeftId zero Fa x i) ∣₂ -[ 1 ]ₕ ∣ (λ x → d-preRightId zero Fb x i) ∣₂) - ∙∙ cancelₕ 1 (0ₕ 1) - dΔ-Id (suc n) Fa Fb = -distrLemma (suc n) (2 + n) (d (suc n)) ∣ Fa ∘ f ∣₂ ∣ Fb ∘ g ∣₂ - ∙∙ (λ i → ∣ (λ x → d-preLeftId (suc n) Fa x i) ∣₂ -[ (2 + n) ]ₕ ∣ (λ x → d-preRightId (suc n) Fb x i) ∣₂) - ∙∙ cancelₕ (2 + n) (0ₕ (2 + n)) diff --git a/Cubical/Experiments/ZariskiLatticeBasicOpens.agda b/Cubical/Experiments/ZariskiLatticeBasicOpens.agda index 1e522b0296..79ec647016 100644 --- a/Cubical/Experiments/ZariskiLatticeBasicOpens.agda +++ b/Cubical/Experiments/ZariskiLatticeBasicOpens.agda @@ -23,7 +23,7 @@ open import Cubical.Data.Sigma.Properties open import Cubical.Data.FinData open import Cubical.Relation.Nullary open import Cubical.Relation.Binary -open import Cubical.Relation.Binary.Poset +-- open import Cubical.Relation.Binary.Poset open import Cubical.Algebra.Ring open import Cubical.Algebra.Algebra @@ -51,7 +51,7 @@ private module Presheaf (A' : CommRing ℓ) where open CommRingStr (snd A') renaming (_·_ to _·r_ ; ·Comm to ·r-comm ; ·Assoc to ·rAssoc - ; ·Lid to ·rLid ; ·Rid to ·rRid) + ; ·IdL to ·rLid ; ·IdR to ·rRid) open Exponentiation A' open CommRingTheory A' open InvertingElementsBase A' @@ -72,7 +72,7 @@ module Presheaf (A' : CommRing ℓ) where -- ≼ is a pre-order: Refl≼ : isRefl _≼_ - Refl≼ x = PT.∣ 1 , 1r , ·r-comm _ _ ∣ + Refl≼ x = PT.∣ 1 , 1r , ·r-comm _ _ ∣₁ Trans≼ : isTrans _≼_ Trans≼ x y z = map2 Trans≼Σ @@ -123,7 +123,7 @@ module Presheaf (A' : CommRing ℓ) where path2 = solve A' lemmaΣ : Σ[ n ∈ ℕ ] Σ[ a ∈ A ] x ^ n ≡ a ·r y → y ⋆ 1a ∈ A[1/ x ]ˣ - lemmaΣ (n , z , p) = [ z , (x ^ n) , PT.∣ n , refl ∣ ] -- xⁿ≡zy → y⁻¹ ≡ z/xⁿ + lemmaΣ (n , z , p) = [ z , (x ^ n) , PT.∣ n , refl ∣₁ ] -- xⁿ≡zy → y⁻¹ ≡ z/xⁿ , eq/ _ _ ((1r , powersFormMultClosedSubset _ .containsOne) , (path1 _ _ ∙∙ sym p ∙∙ path2 _)) @@ -175,7 +175,7 @@ module Presheaf (A' : CommRing ℓ) where ·r-lcoh : (x y z : A) → R x y → R (x ·r z) (y ·r z) ·r-lcoh x y z Rxy = ·r-lcoh-≼ x y z (Rxy .fst) , ·r-lcoh-≼ y x z (Rxy .snd) - +{- BasicOpens : Semilattice ℓ BasicOpens = makeSemilattice [ 1r ] _∧/_ squash/ (elimProp3 (λ _ _ _ → squash/ _ _) λ _ _ _ → cong [_] (·rAssoc _ _ _)) @@ -210,7 +210,7 @@ module Presheaf (A' : CommRing ℓ) where x≼y→x≼xyΣ (n , z , p) = suc n , z , cong (x ·r_) p ∙ ·CommAssocl _ _ _ ≼To· : x ≼ y → R x ( x ·r y) - ≼To· x≼y = PT.map x≼y→x≼xyΣ x≼y , PT.∣ 1 , y , ·rRid _ ∙ ·r-comm _ _ ∣ + ≼To· x≼y = PT.map x≼y→x≼xyΣ x≼y , PT.∣ 1 , y , ·rRid _ ∙ ·r-comm _ _ ∣₁ open IsPoset open PosetStr @@ -247,3 +247,4 @@ module Presheaf (A' : CommRing ℓ) where → ρᴰ x z (Trans≼/ _ _ _ l m) ≡ ρᴰ x y l ∘a ρᴰ y z m ρᴰComp = SQ.elimProp3 (λ _ _ _ → isPropΠ2 (λ _ _ → isSetAlgebraHom _ _ _ _)) λ a b c _ _ → sym (ρᴰᴬ a c _ .snd _) ∙ ρᴰᴬComp a b c _ _ +-} diff --git a/GNUmakefile b/GNUmakefile index 6e58efd832..9ff39ba0d1 100644 --- a/GNUmakefile +++ b/GNUmakefile @@ -35,11 +35,11 @@ check-everythings: .PHONY : gen-everythings gen-everythings: - $(EVERYTHINGS) gen-except Core Foundations Codata Experiments + $(EVERYTHINGS) gen-except Core Foundations Codata .PHONY : gen-and-check-everythings gen-and-check-everythings: - $(EVERYTHINGS) gen-except Core Foundations Codata Experiments + $(EVERYTHINGS) gen-except Core Foundations Codata $(EVERYTHINGS) check Core Foundations Codata .PHONY : check-README