From fdbb7e290bc489eb46048c688df28146921308cc Mon Sep 17 00:00:00 2001 From: Felix Cherubini Date: Thu, 25 Jan 2024 22:10:42 +0100 Subject: [PATCH] rm LocalizationDefs --- Cubical/Experiments/LocalisationDefs.agda | 146 ---------------------- 1 file changed, 146 deletions(-) delete mode 100644 Cubical/Experiments/LocalisationDefs.agda 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