83 lines
2.6 KiB
Text
83 lines
2.6 KiB
Text
/-
|
||
Copyright (c) 2016 Floris van Doorn. All rights reserved.
|
||
Released under Apache 2.0 license as described in the file LICENSE.
|
||
Authors: Floris van Doorn, Egbert Rijke
|
||
-/
|
||
|
||
import hit.two_quotient .seq_colim
|
||
|
||
open eq prod sum two_quotient sigma function relation e_closure nat seq_colim
|
||
|
||
namespace localization
|
||
section quasi_local_extension
|
||
|
||
universe variables u v w
|
||
parameters {A : Type.{u}} {P : A → Type.{v}} {Q : A → Type.{w}} (F : Πa, P a → Q a)
|
||
definition is_local [class] (Y : Type) : Type :=
|
||
Π(a : A), is_equiv (λg, g ∘ F a : (Q a → Y) → (P a → Y))
|
||
|
||
|
||
|
||
section
|
||
parameter (X : Type.{max u v w})
|
||
local abbreviation Y := X + Σa, (P a → X) × Q a
|
||
|
||
-- do we want to remove the contractible pairs?
|
||
inductive qleR : Y → Y → Type :=
|
||
| J : Π{a : A} (f : P a → X) (p : P a), qleR (inr ⟨a, (f, F a p)⟩) (inl (f p))
|
||
| k : Π{a : A} (g : Q a → X) (q : Q a), qleR (inl (g q)) (inr ⟨a, (g ∘ F a, q)⟩)
|
||
|
||
inductive qleQ : Π⦃y₁ y₂ : Y⦄, e_closure qleR y₁ y₂ → e_closure qleR y₁ y₂ → Type :=
|
||
| K : Π{a : A} (g : Q a → X) (p : P a), qleQ [qleR.k g (F a p)] [qleR.J (g ∘ F a) p]⁻¹ʳ
|
||
|
||
definition one_step_localization : Type := two_quotient qleR qleQ
|
||
definition incl : X → one_step_localization := incl0 _ _ ∘ inl
|
||
|
||
end
|
||
variables (X : Type.{max u v w}) {Z : Type}
|
||
|
||
definition n_step_localization : ℕ → Type :=
|
||
nat.rec X (λn Y, localization.one_step_localization F Y)
|
||
|
||
definition incln (n : ℕ) :
|
||
n_step_localization X n → n_step_localization X (succ n) :=
|
||
localization.incl F (n_step_localization X n)
|
||
|
||
-- localization if P and Q consist of ω-compact types
|
||
definition localization : Type := seq_colim (incln X)
|
||
definition incll : X → localization X := ι' _ 0
|
||
|
||
protected definition rec {P : localization X → Type} [Πz, is_local (P z)]
|
||
(H : Πx, P (incll X x)) (z : localization X) : P z :=
|
||
begin
|
||
exact sorry
|
||
end
|
||
|
||
definition extend {Y Z : Type} (f : Y → Z) [is_local Z] (x : one_step_localization Y) : Z :=
|
||
begin
|
||
induction x,
|
||
{ induction a,
|
||
{ exact f a},
|
||
{ induction a with a v, induction v with f q, exact sorry}},
|
||
{ exact sorry},
|
||
{ exact sorry}
|
||
end
|
||
|
||
protected definition elim {Y : Type} [is_local Y]
|
||
(H : X → Y) (z : localization X) : Y :=
|
||
begin
|
||
induction z with n x n x,
|
||
{ induction n with n IH,
|
||
{ exact H x},
|
||
induction x,
|
||
{ induction a,
|
||
{ exact IH a},
|
||
{ induction a with a v, induction v with f q, exact sorry}},
|
||
{ exact sorry},
|
||
exact sorry},
|
||
exact sorry
|
||
end
|
||
|
||
|
||
end quasi_local_extension
|
||
end localization
|