lean2/hott/hit/colimit.hlean

163 lines
5.9 KiB
Text
Raw Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

/-
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