SCT.VolumeI.Chapter03.Section03.Localizations

Complete compiler-highlighted source. Follow a symbol to its declaration.

# Localizations and the localization axiom

`def:Localization` asks that the restriction functor constructed above
be an equivalence for every target. The record retains the witness that
the given functor inverts the collection. `axiom:M_Localization_Axiom`
then supplies such a localization for every collection; no closure
condition on that collection is imposed.

```agda
{-# OPTIONS --safe --without-K #-}
open import Agda.Primitive using (Level; _⊔_)
open import SCT.VolumeI.Chapter01.Theory using (Theory)
import SCT.VolumeI.Chapter01.Section04.MappingAnimae as Mapping
import SCT.VolumeI.Chapter01.Section07.FunctorCategories as Categories
import SCT.VolumeI.Chapter01.Section06.PullbackLaws as Pullbacks
import SCT.VolumeI.Chapter02.Section01.WalkingMorphism as Walking
import SCT.VolumeI.Chapter02.Section01.IntervalEndpoints as Endpoints
import SCT.VolumeI.Chapter02.Section02.SegalAxiom as Segal
import SCT.VolumeI.Chapter02.Section01.CommutativeSquareAxiom as Squares
import SCT.VolumeI.Chapter02.Section03.RezkAxiom as Rezk

module SCT.VolumeI.Chapter03.Section03.Localizations
  {c m a : Level} (𝒯 : Theory c m a) (M : Mapping.MappingAnimae 𝒯)
  (ℱ : Categories.FunctorCategories 𝒯 M) (P : Pullbacks.PullbackStructure 𝒯)
  (I : Walking.WalkingMorphism 𝒯) (E : Endpoints.IntervalEndpoints 𝒯 M ℱ P I)
  (S : Segal.SegalAxiom 𝒯 M ℱ P I E)
  (Q : Squares.CommutativeSquareAxiom 𝒯 M ℱ P I E)
  (R : Rezk.RezkAxiom 𝒯 M ℱ P I E) where

open import SCT.VolumeI.Chapter01.Section05.Setup 𝒯 M
open import SCT.VolumeI.Chapter03.Section01.MorphismCollections 𝒯 M P I using (MorphismCollection)
open import SCT.VolumeI.Chapter03.Section01.SubcategoryAxiom 𝒯 M ℱ P I E S using (SubcategoryAxiom)
open import SCT.VolumeI.Chapter03.Section03.InvertingFunctors 𝒯 M ℱ P I E S Q using (Inverts)
open import SCT.VolumeI.Chapter03.Section03.MappingCalculus.LocalizationRestriction 𝒯 M ℱ P I E S Q R using (module RestrictionAlong)

module WithSubcategories (L : SubcategoryAxiom) where
  record IsLocalization {C T : CAT} (W : MorphismCollection C) (l : MAP C T) : Set (c ⊔ m) where
    field
      inverts : Inverts l W
      universal : (D : CAT) → IsEquiv (RestrictionAlong.functor L W l inverts D)

  record Localization {C : CAT} (W : MorphismCollection C) : Set (c ⊔ m) where
    field
      category : CAT
      functor : MAP C category
      isLocalization : IsLocalization W functor

  record LocalizationAxiom : Set (c ⊔ m ⊔ a) where
    field
      localized : {C : CAT} (W : MorphismCollection C) → Localization W
```