lean2/hott/hit/colimit.hlean

164 lines
5.9 KiB
Text
Raw Normal View History

/-
Copyright (c) 2015 Floris van Doorn. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Module: hit.colimit
Authors: Floris van Doorn
Definition of general colimits and sequential colimits.
-/
/- definition of a general colimit -/
open eq nat type_quotient sigma equiv
namespace colimit
section
parameters {I J : Type} (A : I → Type) (dom cod : J → I)
(f : Π(j : J), A (dom j) → A (cod j))
variables {i : I} (a : A i) (j : J) (b : A (dom j))
local abbreviation B := Σ(i : I), A i
inductive colim_rel : B → B → Type :=
| Rmk : Π{j : J} (a : A (dom j)), colim_rel ⟨cod j, f j a⟩ ⟨dom j, a⟩
open colim_rel
local abbreviation R := colim_rel
-- TODO: define this in root namespace
definition colimit : Type :=
type_quotient colim_rel
definition incl : colimit :=
class_of R ⟨i, a⟩
abbreviation ι := @incl
definition cglue : ι (f j b) = ι b :=
eq_of_rel (Rmk f b)
protected definition rec {P : colimit → Type}
(Pincl : Π⦃i : I⦄ (x : A i), P (ι x))
(Pglue : Π(j : J) (x : A (dom j)), cglue j x ▹ Pincl (f j x) = Pincl x)
(y : colimit) : P y :=
begin
fapply (type_quotient.rec_on y),
{ intro a, cases a, apply Pincl},
{ intros [a, a', H], cases H, apply Pglue}
end
protected definition rec_on [reducible] {P : colimit → Type} (y : colimit)
(Pincl : Π⦃i : I⦄ (x : A i), P (ι x))
(Pglue : Π(j : J) (x : A (dom j)), cglue j x ▹ Pincl (f j x) = Pincl x) : P y :=
rec Pincl Pglue y
definition rec_cglue [reducible] {P : colimit → Type}
(Pincl : Π⦃i : I⦄ (x : A i), P (ι x))
(Pglue : Π(j : J) (x : A (dom j)), cglue j x ▹ Pincl (f j x) = Pincl x)
{j : J} (x : A (dom j)) : apD (rec Pincl Pglue) (cglue j x) = Pglue j x :=
sorry
protected definition elim {P : Type} (Pincl : Π⦃i : I⦄ (x : A i), P)
(Pglue : Π(j : J) (x : A (dom j)), Pincl (f j x) = Pincl x) (y : colimit) : P :=
rec Pincl (λj a, !tr_constant ⬝ Pglue j a) y
protected definition elim_on [reducible] {P : Type} (y : colimit)
(Pincl : Π⦃i : I⦄ (x : A i), P)
(Pglue : Π(j : J) (x : A (dom j)), Pincl (f j x) = Pincl x) : P :=
elim Pincl Pglue y
definition elim_cglue [reducible] {P : Type}
(Pincl : Π⦃i : I⦄ (x : A i), P)
(Pglue : Π(j : J) (x : A (dom j)), Pincl (f j x) = Pincl x)
{j : J} (x : A (dom j)) : ap (elim Pincl Pglue) (cglue j x) = Pglue j x :=
sorry
protected definition elim_type (Pincl : Π⦃i : I⦄ (x : A i), Type)
(Pglue : Π(j : J) (x : A (dom j)), Pincl (f j x) ≃ Pincl x) (y : colimit) : Type :=
elim Pincl (λj a, ua (Pglue j a)) y
protected definition elim_type_on [reducible] (y : colimit)
(Pincl : Π⦃i : I⦄ (x : A i), Type)
(Pglue : Π(j : J) (x : A (dom j)), Pincl (f j x) ≃ Pincl x) : Type :=
elim_type Pincl Pglue y
definition elim_type_cglue [reducible] (Pincl : Π⦃i : I⦄ (x : A i), Type)
(Pglue : Π(j : J) (x : A (dom j)), Pincl (f j x) ≃ Pincl x)
{j : J} (x : A (dom j)) : transport (elim_type Pincl Pglue) (cglue j x) = sorry /-Pglue j x-/ :=
sorry
end
end colimit
/- definition of a sequential colimit -/
namespace seq_colim
section
parameters {A : → Type} (f : Π⦃n⦄, A n → A (succ n))
variables {n : } (a : A n)
local abbreviation B := Σ(n : ), A n
inductive seq_rel : B → B → Type :=
| Rmk : Π{n : } (a : A n), seq_rel ⟨succ n, f a⟩ ⟨n, a⟩
open seq_rel
local abbreviation R := seq_rel
-- TODO: define this in root namespace
definition seq_colim : Type :=
type_quotient seq_rel
definition inclusion : seq_colim :=
class_of R ⟨n, a⟩
abbreviation sι := @inclusion
definition glue : sι (f a) = sι a :=
eq_of_rel (Rmk f a)
protected definition rec [reducible] {P : seq_colim → Type}
(Pincl : Π⦃n : ℕ⦄ (a : A n), P (sι a))
(Pglue : Π(n : ) (a : A n), glue a ▹ Pincl (f a) = Pincl a) (aa : seq_colim) : P aa :=
begin
fapply (type_quotient.rec_on aa),
{ intro a, cases a, apply Pincl},
{ intros [a, a', H], cases H, apply Pglue}
end
protected definition rec_on [reducible] {P : seq_colim → Type} (aa : seq_colim)
(Pincl : Π⦃n : ℕ⦄ (a : A n), P (sι a))
(Pglue : Π⦃n : ℕ⦄ (a : A n), glue a ▹ Pincl (f a) = Pincl a)
: P aa :=
rec Pincl Pglue aa
protected definition elim {P : Type} (Pincl : Π⦃n : ℕ⦄ (a : A n), P)
(Pglue : Π⦃n : ℕ⦄ (a : A n), Pincl (f a) = Pincl a) : seq_colim → P :=
rec Pincl (λn a, !tr_constant ⬝ Pglue a)
protected definition elim_on [reducible] {P : Type} (aa : seq_colim)
(Pincl : Π⦃n : ℕ⦄ (a : A n), P)
(Pglue : Π⦃n : ℕ⦄ (a : A n), Pincl (f a) = Pincl a) : P :=
elim Pincl Pglue aa
definition rec_glue {P : seq_colim → Type} (Pincl : Π⦃n : ℕ⦄ (a : A n), P (sι a))
(Pglue : Π⦃n : ℕ⦄ (a : A n), glue a ▹ Pincl (f a) = Pincl a) {n : } (a : A n)
: apD (rec Pincl Pglue) (glue a) = sorry ⬝ Pglue a ⬝ sorry :=
sorry
definition elim_glue {P : Type} (Pincl : Π⦃n : ℕ⦄ (a : A n), P)
(Pglue : Π⦃n : ℕ⦄ (a : A n), Pincl (f a) = Pincl a) {n : } (a : A n)
: ap (elim Pincl Pglue) (glue a) = sorry ⬝ Pglue a ⬝ sorry :=
sorry
protected definition elim_type (Pincl : Π⦃n : ℕ⦄ (a : A n), Type)
(Pglue : Π⦃n : ℕ⦄ (a : A n), Pincl (f a) ≃ Pincl a) : seq_colim → Type :=
elim Pincl (λn a, ua (Pglue a))
protected definition elim_type_on [reducible] (aa : seq_colim)
(Pincl : Π⦃n : ℕ⦄ (a : A n), Type)
(Pglue : Π⦃n : ℕ⦄ (a : A n), Pincl (f a) ≃ Pincl a) : Type :=
elim_type Pincl Pglue aa
definition elim_type_glue (Pincl : Π⦃n : ℕ⦄ (a : A n), Type)
(Pglue : Π⦃n : ℕ⦄ (a : A n), Pincl (f a) ≃ Pincl a) {n : } (a : A n)
: transport (elim_type Pincl Pglue) (glue a) = sorry /-Pglue a-/ :=
sorry
end
end seq_colim