feat(hit): For all hits, add the elimination to the universe (using ua)
This commit is contained in:
Floris van Doorn
Leonardo de Moura
parent
f41d92199a
commit
591a563be3
11 changed files with 171 additions and 166 deletions
|
|
@ -10,7 +10,7 @@ Declaration of the circle
|
|||
|
||||
import .sphere
|
||||
|
||||
open eq suspension bool sphere_index
|
||||
open eq suspension bool sphere_index equiv
|
||||
|
||||
definition circle [reducible] := suspension bool --redefine this as sphere 1
|
||||
|
||||
|
|
@ -76,22 +76,34 @@ namespace circle
|
|||
|
||||
protected definition rec_on [reducible] {P : circle → Type} (x : circle) (Pbase : P base)
|
||||
(Ploop : loop ▹ Pbase = Pbase) : P x :=
|
||||
circle.rec Pbase Ploop x
|
||||
rec Pbase Ploop x
|
||||
|
||||
definition rec_loop {P : circle → Type} (Pbase : P base) (Ploop : loop ▹ Pbase = Pbase) :
|
||||
ap (rec Pbase Ploop) loop = sorry ⬝ Ploop ⬝ sorry :=
|
||||
sorry
|
||||
|
||||
protected definition elim {P : Type} (Pbase : P) (Ploop : Pbase = Pbase)
|
||||
(x : circle) : P :=
|
||||
circle.rec Pbase (tr_constant loop Pbase ⬝ Ploop) x
|
||||
rec Pbase (tr_constant loop Pbase ⬝ Ploop) x
|
||||
|
||||
protected definition elim_on [reducible] {P : Type} (x : circle) (Pbase : P)
|
||||
(Ploop : Pbase = Pbase) : P :=
|
||||
elim Pbase Ploop x
|
||||
|
||||
definition rec_loop {P : circle → Type} (Pbase : P base) (Ploop : loop ▹ Pbase = Pbase) :
|
||||
ap (circle.rec Pbase Ploop) loop = sorry ⬝ Ploop ⬝ sorry :=
|
||||
definition elim_loop {P : Type} (Pbase : P) (Ploop : Pbase = Pbase) :
|
||||
ap (elim Pbase Ploop) loop = sorry ⬝ Ploop ⬝ sorry :=
|
||||
sorry
|
||||
|
||||
definition elim_loop {P : Type} (Pbase : P) (Ploop : Pbase = Pbase) :
|
||||
ap (circle.elim Pbase Ploop) loop = sorry ⬝ Ploop ⬝ sorry :=
|
||||
protected definition elim_type (Pbase : Type) (Ploop : Pbase ≃ Pbase)
|
||||
(x : circle) : Type :=
|
||||
elim Pbase (ua Ploop) x
|
||||
|
||||
protected definition elim_type_on [reducible] (x : circle) (Pbase : Type)
|
||||
(Ploop : Pbase ≃ Pbase) : Type :=
|
||||
elim_type Pbase Ploop x
|
||||
|
||||
definition elim_type_loop (Pbase : Type) (Ploop : Pbase ≃ Pbase) :
|
||||
transport (elim_type Pbase Ploop) loop = sorry /-Ploop-/ :=
|
||||
sorry
|
||||
|
||||
end circle
|
||||
|
|
|
|||
|
|
@ -10,7 +10,7 @@ Declaration of the coequalizer
|
|||
|
||||
import .type_quotient
|
||||
|
||||
open type_quotient eq
|
||||
open type_quotient eq equiv
|
||||
|
||||
namespace coeq
|
||||
context
|
||||
|
|
@ -44,6 +44,11 @@ parameters {A B : Type.{u}} (f g : A → B)
|
|||
(P_i : Π(x : B), P (coeq_i x)) (Pcp : Π(x : A), cp x ▹ P_i (f x) = P_i (g x)) : P y :=
|
||||
rec P_i Pcp y
|
||||
|
||||
definition rec_cp {P : coeq → Type} (P_i : Π(x : B), P (coeq_i x))
|
||||
(Pcp : Π(x : A), cp x ▹ P_i (f x) = P_i (g x))
|
||||
(x : A) : apD (rec P_i Pcp) (cp x) = sorry ⬝ Pcp x ⬝ sorry :=
|
||||
sorry
|
||||
|
||||
protected definition elim {P : Type} (P_i : B → P)
|
||||
(Pcp : Π(x : A), P_i (f x) = P_i (g x)) (y : coeq) : P :=
|
||||
rec P_i (λx, !tr_constant ⬝ Pcp x) y
|
||||
|
|
@ -52,15 +57,23 @@ parameters {A B : Type.{u}} (f g : A → B)
|
|||
(Pcp : Π(x : A), P_i (f x) = P_i (g x)) : P :=
|
||||
elim P_i Pcp y
|
||||
|
||||
definition rec_cp {P : coeq → Type} (P_i : Π(x : B), P (coeq_i x))
|
||||
(Pcp : Π(x : A), cp x ▹ P_i (f x) = P_i (g x))
|
||||
(x : A) : apD (rec P_i Pcp) (cp x) = sorry ⬝ Pcp x ⬝ sorry :=
|
||||
sorry
|
||||
|
||||
definition elim_cp {P : Type} (P_i : B → P) (Pcp : Π(x : A), P_i (f x) = P_i (g x))
|
||||
(x : A) : ap (elim P_i Pcp) (cp x) = sorry ⬝ Pcp x ⬝ sorry :=
|
||||
sorry
|
||||
|
||||
protected definition elim_type (P_i : B → Type)
|
||||
(Pcp : Π(x : A), P_i (f x) ≃ P_i (g x)) (y : coeq) : Type :=
|
||||
elim P_i (λx, ua (Pcp x)) y
|
||||
|
||||
protected definition elim_type_on [reducible] (y : coeq) (P_i : B → Type)
|
||||
(Pcp : Π(x : A), P_i (f x) ≃ P_i (g x)) : Type :=
|
||||
elim_type P_i Pcp y
|
||||
|
||||
definition elim_type_cp (P_i : B → Type) (Pcp : Π(x : A), P_i (f x) ≃ P_i (g x))
|
||||
(x : A) : transport (elim_type P_i Pcp) (cp x) = sorry /-Pcp x-/ :=
|
||||
sorry
|
||||
|
||||
|
||||
end
|
||||
|
||||
end coeq
|
||||
|
|
|
|||
|
|
@ -9,7 +9,7 @@ Definition of general colimits and sequential colimits.
|
|||
-/
|
||||
|
||||
/- definition of a general colimit -/
|
||||
open eq nat type_quotient sigma
|
||||
open eq nat type_quotient sigma equiv
|
||||
|
||||
namespace colimit
|
||||
context
|
||||
|
|
@ -49,6 +49,12 @@ context
|
|||
(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) = sorry ⬝ Pglue j x ⬝ sorry :=
|
||||
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
|
||||
|
|
@ -58,18 +64,26 @@ context
|
|||
(Pglue : Π(j : J) (x : A (dom j)), Pincl (f j x) = Pincl x) : P :=
|
||||
elim 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) = sorry ⬝ Pglue j x ⬝ sorry :=
|
||||
sorry
|
||||
|
||||
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) = sorry ⬝ Pglue j x ⬝ sorry :=
|
||||
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
|
||||
|
||||
|
|
@ -131,5 +145,19 @@ context
|
|||
: 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
|
||||
|
|
|
|||
|
|
@ -10,7 +10,7 @@ Declaration of mapping cylinders
|
|||
|
||||
import .type_quotient
|
||||
|
||||
open type_quotient eq sum
|
||||
open type_quotient eq sum equiv
|
||||
|
||||
namespace cylinder
|
||||
context
|
||||
|
|
@ -51,6 +51,12 @@ parameters {A B : Type.{u}} (f : A → B)
|
|||
(Pseg : Π(a : A), seg a ▹ Pbase (f a) = Ptop a) : P x :=
|
||||
rec Pbase Ptop Pseg x
|
||||
|
||||
definition rec_seg {P : cylinder → Type}
|
||||
(Pbase : Π(b : B), P (base b)) (Ptop : Π(a : A), P (top a))
|
||||
(Pseg : Π(a : A), seg a ▹ Pbase (f a) = Ptop a)
|
||||
(a : A) : apD (rec Pbase Ptop Pseg) (seg a) = sorry ⬝ Pseg a ⬝ sorry :=
|
||||
sorry
|
||||
|
||||
protected definition elim {P : Type} (Pbase : B → P) (Ptop : A → P)
|
||||
(Pseg : Π(a : A), Pbase (f a) = Ptop a) (x : cylinder) : P :=
|
||||
rec Pbase Ptop (λa, !tr_constant ⬝ Pseg a) x
|
||||
|
|
@ -59,17 +65,24 @@ parameters {A B : Type.{u}} (f : A → B)
|
|||
(Pseg : Π(a : A), Pbase (f a) = Ptop a) : P :=
|
||||
elim Pbase Ptop Pseg x
|
||||
|
||||
definition rec_seg {P : cylinder → Type}
|
||||
(Pbase : Π(b : B), P (base b)) (Ptop : Π(a : A), P (top a))
|
||||
(Pseg : Π(a : A), seg a ▹ Pbase (f a) = Ptop a)
|
||||
(a : A) : apD (rec Pbase Ptop Pseg) (seg a) = sorry ⬝ Pseg a ⬝ sorry :=
|
||||
sorry
|
||||
|
||||
definition elim_seg {P : Type} (Pbase : B → P) (Ptop : A → P)
|
||||
(Pseg : Π(a : A), Pbase (f a) = Ptop a)
|
||||
(a : A) : ap (elim Pbase Ptop Pseg) (seg a) = sorry ⬝ Pseg a ⬝ sorry :=
|
||||
sorry
|
||||
|
||||
protected definition elim_type (Pbase : B → Type) (Ptop : A → Type)
|
||||
(Pseg : Π(a : A), Pbase (f a) ≃ Ptop a) (x : cylinder) : Type :=
|
||||
elim Pbase Ptop (λa, ua (Pseg a)) x
|
||||
|
||||
protected definition elim_type_on [reducible] (x : cylinder) (Pbase : B → Type) (Ptop : A → Type)
|
||||
(Pseg : Π(a : A), Pbase (f a) ≃ Ptop a) : Type :=
|
||||
elim_type Pbase Ptop Pseg x
|
||||
|
||||
definition elim_type_seg (Pbase : B → Type) (Ptop : A → Type)
|
||||
(Pseg : Π(a : A), Pbase (f a) ≃ Ptop a)
|
||||
(a : A) : transport (elim_type Pbase Ptop Pseg) (seg a) = sorry /-Pseg a-/ :=
|
||||
sorry
|
||||
|
||||
end
|
||||
|
||||
end cylinder
|
||||
|
|
|
|||
|
|
@ -10,7 +10,7 @@ Declaration of the pushout
|
|||
|
||||
import .type_quotient
|
||||
|
||||
open type_quotient eq sum
|
||||
open type_quotient eq sum equiv
|
||||
|
||||
namespace pushout
|
||||
context
|
||||
|
|
@ -61,24 +61,36 @@ parameters {TL BL TR : Type} (f : TL → BL) (g : TL → TR)
|
|||
(x : TR) : rec Pinl Pinr Pglue (inr x) = Pinr x :=
|
||||
rec_class_of _ _ _ --idp
|
||||
|
||||
protected definition elim {P : Type} (Pinl : BL → P) (Pinr : TR → P)
|
||||
(Pglue : Π(x : TL), Pinl (f x) = Pinr (g x)) (y : pushout) : P :=
|
||||
rec Pinl Pinr (λx, !tr_constant ⬝ Pglue x) y
|
||||
|
||||
protected definition elim_on [reducible] {P : Type} (Pinl : BL → P) (y : pushout)
|
||||
(Pinr : TR → P) (Pglue : Π(x : TL), Pinl (f x) = Pinr (g x)) : P :=
|
||||
elim Pinl Pinr Pglue y
|
||||
|
||||
definition rec_glue {P : pushout → Type} (Pinl : Π(x : BL), P (inl x))
|
||||
(Pinr : Π(x : TR), P (inr x)) (Pglue : Π(x : TL), glue x ▹ Pinl (f x) = Pinr (g x))
|
||||
(x : TL) : apD (rec Pinl Pinr Pglue) (glue x) = sorry ⬝ Pglue x ⬝ sorry :=
|
||||
sorry
|
||||
|
||||
protected definition elim {P : Type} (Pinl : BL → P) (Pinr : TR → P)
|
||||
(Pglue : Π(x : TL), Pinl (f x) = Pinr (g x)) (y : pushout) : P :=
|
||||
rec Pinl Pinr (λx, !tr_constant ⬝ Pglue x) y
|
||||
|
||||
protected definition elim_on [reducible] {P : Type} (y : pushout) (Pinl : BL → P)
|
||||
(Pinr : TR → P) (Pglue : Π(x : TL), Pinl (f x) = Pinr (g x)) : P :=
|
||||
elim Pinl Pinr Pglue y
|
||||
|
||||
definition elim_glue {P : Type} (Pinl : BL → P) (Pinr : TR → P)
|
||||
(Pglue : Π(x : TL), Pinl (f x) = Pinr (g x)) (y : pushout) (x : TL)
|
||||
: ap (elim Pinl Pinr Pglue) (glue x) = sorry ⬝ Pglue x ⬝ sorry :=
|
||||
sorry
|
||||
|
||||
protected definition elim_type (Pinl : BL → Type) (Pinr : TR → Type)
|
||||
(Pglue : Π(x : TL), Pinl (f x) ≃ Pinr (g x)) (y : pushout) : Type :=
|
||||
elim Pinl Pinr (λx, ua (Pglue x)) y
|
||||
|
||||
protected definition elim_type_on [reducible] (y : pushout) (Pinl : BL → Type)
|
||||
(Pinr : TR → Type) (Pglue : Π(x : TL), Pinl (f x) ≃ Pinr (g x)) : Type :=
|
||||
elim_type Pinl Pinr Pglue y
|
||||
|
||||
definition elim_type_glue (Pinl : BL → Type) (Pinr : TR → Type)
|
||||
(Pglue : Π(x : TL), Pinl (f x) ≃ Pinr (g x)) (y : pushout) (x : TL)
|
||||
: transport (elim_type Pinl Pinr Pglue) (glue x) = sorry /-Pglue x-/ :=
|
||||
sorry
|
||||
|
||||
end
|
||||
|
||||
|
|
|
|||
|
|
@ -27,7 +27,7 @@ parameters {A : Type} (R : A → A → hprop)
|
|||
theorem is_hset_quotient : is_hset quotient :=
|
||||
by unfold quotient; exact _
|
||||
|
||||
protected definition rec {P : quotient → Type} [Pt : Πaa, is_trunc 0 (P aa)]
|
||||
protected definition rec {P : quotient → Type} [Pt : Πaa, is_hset (P aa)]
|
||||
(Pc : Π(a : A), P (class_of a)) (Pp : Π⦃a a' : A⦄ (H : R a a'), eq_of_rel H ▹ Pc a = Pc a')
|
||||
(x : quotient) : P x :=
|
||||
begin
|
||||
|
|
@ -40,24 +40,24 @@ parameters {A : Type} (R : A → A → hprop)
|
|||
end
|
||||
|
||||
protected definition rec_on [reducible] {P : quotient → Type} (x : quotient)
|
||||
[Pt : Πaa, is_trunc 0 (P aa)] (Pc : Π(a : A), P (class_of a))
|
||||
[Pt : Πaa, is_hset (P aa)] (Pc : Π(a : A), P (class_of a))
|
||||
(Pp : Π⦃a a' : A⦄ (H : R a a'), eq_of_rel H ▹ Pc a = Pc a') : P x :=
|
||||
rec Pc Pp x
|
||||
|
||||
definition rec_eq_of_rel {P : quotient → Type} [Pt : Πaa, is_trunc 0 (P aa)]
|
||||
definition rec_eq_of_rel {P : quotient → Type} [Pt : Πaa, is_hset (P aa)]
|
||||
(Pc : Π(a : A), P (class_of a)) (Pp : Π⦃a a' : A⦄ (H : R a a'), eq_of_rel H ▹ Pc a = Pc a')
|
||||
{a a' : A} (H : R a a') : apD (rec Pc Pp) (eq_of_rel H) = sorry ⬝ Pp H ⬝ sorry :=
|
||||
sorry
|
||||
|
||||
protected definition elim {P : Type} [Pt : is_trunc 0 P] (Pc : A → P)
|
||||
protected definition elim {P : Type} [Pt : is_hset P] (Pc : A → P)
|
||||
(Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a = Pc a') (x : quotient) : P :=
|
||||
rec Pc (λa a' H, !tr_constant ⬝ Pp H) x
|
||||
|
||||
protected definition elim_on [reducible] {P : Type} (x : quotient) [Pt : is_trunc 0 P]
|
||||
protected definition elim_on [reducible] {P : Type} (x : quotient) [Pt : is_hset P]
|
||||
(Pc : A → P) (Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a = Pc a') : P :=
|
||||
elim Pc Pp x
|
||||
|
||||
protected definition elim_eq_of_rel {P : Type} [Pt : is_trunc 0 P] (Pc : A → P)
|
||||
protected definition elim_eq_of_rel {P : Type} [Pt : is_hset P] (Pc : A → P)
|
||||
(Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a = Pc a') {a a' : A} (H : R a a')
|
||||
: ap (elim Pc Pp) (eq_of_rel H) = sorry ⬝ Pp H ⬝ sorry :=
|
||||
sorry
|
||||
|
|
|
|||
|
|
@ -12,11 +12,13 @@ import .suspension
|
|||
|
||||
open eq nat suspension bool is_trunc unit
|
||||
|
||||
/- We can define spheres with the following possible indices:
|
||||
- trunc_index
|
||||
- nat
|
||||
- nat, but counting wrong (S^0 = empty, S^1 = bool, ...)
|
||||
- some new type "integers >= 1"
|
||||
/-
|
||||
We can define spheres with the following possible indices:
|
||||
- trunc_index (defining S^-2 = S^-1 = empty)
|
||||
- nat (forgetting that S^1 = empty)
|
||||
- nat, but counting wrong (S^0 = empty, S^1 = bool, ...)
|
||||
- some new type "integers >= -1"
|
||||
We choose the last option here.
|
||||
-/
|
||||
|
||||
/- Sphere levels -/
|
||||
|
|
@ -56,6 +58,7 @@ namespace sphere_index
|
|||
|
||||
definition trunc_index_of_sphere_index [coercion] [reducible] (n : sphere_index) : trunc_index :=
|
||||
sphere_index.rec_on n -1 (λ n k, k.+1)
|
||||
|
||||
end sphere_index
|
||||
|
||||
open sphere_index equiv
|
||||
|
|
|
|||
|
|
@ -10,11 +10,12 @@ Declaration of suspension
|
|||
|
||||
import .pushout
|
||||
|
||||
open pushout unit eq
|
||||
open pushout unit eq equiv
|
||||
|
||||
definition suspension (A : Type) : Type := pushout (λ(a : A), star.{0}) (λ(a : A), star.{0})
|
||||
|
||||
namespace suspension
|
||||
variable {A : Type}
|
||||
|
||||
definition north (A : Type) : suspension A :=
|
||||
inl _ _ star
|
||||
|
|
@ -22,10 +23,10 @@ namespace suspension
|
|||
definition south (A : Type) : suspension A :=
|
||||
inr _ _ star
|
||||
|
||||
definition merid {A : Type} (a : A) : north A = south A :=
|
||||
definition merid (a : A) : north A = south A :=
|
||||
glue _ _ a
|
||||
|
||||
protected definition rec {A : Type} {P : suspension A → Type} (PN : P !north) (PS : P !south)
|
||||
protected definition rec {P : suspension A → Type} (PN : P !north) (PS : P !south)
|
||||
(Pm : Π(a : A), merid a ▹ PN = PS) (x : suspension A) : P x :=
|
||||
begin
|
||||
fapply (pushout.rec_on _ _ x),
|
||||
|
|
@ -34,25 +35,38 @@ namespace suspension
|
|||
{ exact Pm},
|
||||
end
|
||||
|
||||
protected definition rec_on [reducible] {A : Type} {P : suspension A → Type} (y : suspension A)
|
||||
protected definition rec_on [reducible] {P : suspension A → Type} (y : suspension A)
|
||||
(PN : P !north) (PS : P !south) (Pm : Π(a : A), merid a ▹ PN = PS) : P y :=
|
||||
rec PN PS Pm y
|
||||
|
||||
definition rec_merid {A : Type} {P : suspension A → Type} (PN : P !north) (PS : P !south)
|
||||
definition rec_merid {P : suspension A → Type} (PN : P !north) (PS : P !south)
|
||||
(Pm : Π(a : A), merid a ▹ PN = PS) (a : A)
|
||||
: apD (rec PN PS Pm) (merid a) = sorry ⬝ Pm a ⬝ sorry :=
|
||||
sorry
|
||||
|
||||
protected definition elim {A : Type} {P : Type} (PN : P) (PS : P) (Pm : A → PN = PS)
|
||||
protected definition elim {P : Type} (PN : P) (PS : P) (Pm : A → PN = PS)
|
||||
(x : suspension A) : P :=
|
||||
rec PN PS (λa, !tr_constant ⬝ Pm a) x
|
||||
|
||||
protected definition elim_on [reducible] {A : Type} {P : Type} (x : suspension A)
|
||||
protected definition elim_on [reducible] {P : Type} (x : suspension A)
|
||||
(PN : P) (PS : P) (Pm : A → PN = PS) : P :=
|
||||
elim PN PS Pm x
|
||||
|
||||
protected definition elim_merid {A : Type} {P : Type} (PN : P) (PS : P) (Pm : A → PN = PS)
|
||||
protected definition elim_merid {P : Type} (PN : P) (PS : P) (Pm : A → PN = PS)
|
||||
(x : suspension A) (a : A) : ap (elim PN PS Pm) (merid a) = sorry ⬝ Pm a ⬝ sorry :=
|
||||
sorry
|
||||
|
||||
protected definition elim_type (PN : Type) (PS : Type) (Pm : A → PN ≃ PS)
|
||||
(x : suspension A) : Type :=
|
||||
elim PN PS (λa, ua (Pm a)) x
|
||||
|
||||
protected definition elim_type_on [reducible] (x : suspension A)
|
||||
(PN : Type) (PS : Type) (Pm : A → PN ≃ PS) : Type :=
|
||||
elim_type PN PS Pm x
|
||||
|
||||
protected definition elim_type_merid (PN : Type) (PS : Type) (Pm : A → PN ≃ PS)
|
||||
(x : suspension A) (a : A) : transport (elim_type PN PS Pm) (merid a) = sorry /-Pm a-/ :=
|
||||
sorry
|
||||
|
||||
|
||||
end suspension
|
||||
|
|
|
|||
|
|
@ -26,111 +26,4 @@ namespace trunc
|
|||
[Pt : is_trunc n P] (H : A → P) : P :=
|
||||
elim H aa
|
||||
|
||||
exit
|
||||
|
||||
variables {X Y Z : Type} {P : X → Type} (A B : Type) (n : trunc_index)
|
||||
|
||||
local attribute is_trunc_eq [instance]
|
||||
|
||||
definition is_equiv_tr [instance] [H : is_trunc n A] : is_equiv (@tr n A) :=
|
||||
adjointify _
|
||||
(trunc.rec id)
|
||||
(λaa, trunc.rec_on aa (λa, idp))
|
||||
(λa, idp)
|
||||
|
||||
definition equiv_trunc [H : is_trunc n A] : A ≃ trunc n A :=
|
||||
equiv.mk tr _
|
||||
|
||||
definition is_trunc_of_is_equiv_tr [H : is_equiv (@tr n A)] : is_trunc n A :=
|
||||
is_trunc_is_equiv_closed n tr⁻¹
|
||||
|
||||
definition untrunc_of_is_trunc [reducible] [H : is_trunc n A] : trunc n A → A :=
|
||||
tr⁻¹
|
||||
|
||||
/- Functoriality -/
|
||||
definition trunc_functor (f : X → Y) : trunc n X → trunc n Y :=
|
||||
λxx, trunc_rec_on xx (λx, tr (f x))
|
||||
-- by intro xx; apply (trunc_rec_on xx); intro x; exact (tr (f x))
|
||||
-- by intro xx; fapply (trunc_rec_on xx); intro x; exact (tr (f x))
|
||||
-- by intro xx; exact (trunc_rec_on xx (λx, (tr (f x))))
|
||||
|
||||
definition trunc_functor_compose (f : X → Y) (g : Y → Z)
|
||||
: trunc_functor n (g ∘ f) ∼ trunc_functor n g ∘ trunc_functor n f :=
|
||||
λxx, trunc_rec_on xx (λx, idp)
|
||||
|
||||
definition trunc_functor_id : trunc_functor n (@id A) ∼ id :=
|
||||
λxx, trunc_rec_on xx (λx, idp)
|
||||
|
||||
definition is_equiv_trunc_functor (f : X → Y) [H : is_equiv f] : is_equiv (trunc_functor n f) :=
|
||||
adjointify _
|
||||
(trunc_functor n f⁻¹)
|
||||
(λyy, trunc_rec_on yy (λy, ap tr !retr))
|
||||
(λxx, trunc_rec_on xx (λx, ap tr !sect))
|
||||
|
||||
section
|
||||
open prod.ops
|
||||
definition trunc_prod_equiv : trunc n (X × Y) ≃ trunc n X × trunc n Y :=
|
||||
sorry
|
||||
-- equiv.MK (λpp, trunc_rec_on pp (λp, (tr p.1, tr p.2)))
|
||||
-- (λp, trunc_rec_on p.1 (λx, trunc_rec_on p.2 (λy, tr (x,y))))
|
||||
-- sorry --(λp, trunc_rec_on p.1 (λx, trunc_rec_on p.2 (λy, idp)))
|
||||
-- (λpp, trunc_rec_on pp (λp, prod.rec_on p (λx y, idp)))
|
||||
|
||||
-- begin
|
||||
-- fapply equiv.MK,
|
||||
-- apply sorry, --{exact (λpp, trunc_rec_on pp (λp, (tr p.1, tr p.2)))},
|
||||
-- apply sorry, /-{intro p, cases p with (xx, yy),
|
||||
-- apply (trunc_rec_on xx), intro x,
|
||||
-- apply (trunc_rec_on yy), intro y, exact (tr (x,y))},-/
|
||||
-- apply sorry, /-{intro p, cases p with (xx, yy),
|
||||
-- apply (trunc_rec_on xx), intro x,
|
||||
-- apply (trunc_rec_on yy), intro y, apply idp},-/
|
||||
-- apply sorry --{intro pp, apply (trunc_rec_on pp), intro p, cases p, apply idp},
|
||||
-- end
|
||||
end
|
||||
|
||||
/- Propositional truncation -/
|
||||
|
||||
-- should this live in hprop?
|
||||
definition merely [reducible] (A : Type) : Type := trunc -1 A
|
||||
|
||||
notation `||`:max A `||`:0 := merely A
|
||||
notation `∥`:max A `∥`:0 := merely A
|
||||
|
||||
definition Exists [reducible] (P : X → Type) : Type := ∥ sigma P ∥
|
||||
definition or [reducible] (A B : Type) : Type := ∥ A ⊎ B ∥
|
||||
|
||||
notation `exists` binders `,` r:(scoped P, Exists P) := r
|
||||
notation `∃` binders `,` r:(scoped P, Exists P) := r
|
||||
notation A `\/` B := or A B
|
||||
notation A ∨ B := or A B
|
||||
|
||||
definition merely.intro [reducible] (a : A) : ∥ A ∥ := tr a
|
||||
definition exists.intro [reducible] (x : X) (p : P x) : ∃x, P x := tr ⟨x, p⟩
|
||||
definition or.intro_left [reducible] (x : X) : X ∨ Y := tr (inl x)
|
||||
definition or.intro_right [reducible] (y : Y) : X ∨ Y := tr (inr y)
|
||||
|
||||
definition is_contr_of_merely_hprop [H : is_hprop A] (aa : merely A) : is_contr A :=
|
||||
is_contr_of_inhabited_hprop (trunc_rec_on aa id)
|
||||
|
||||
section
|
||||
open sigma.ops
|
||||
definition trunc_sigma_equiv : trunc n (Σ x, P x) ≃ trunc n (Σ x, trunc n (P x)) :=
|
||||
equiv.MK (λpp, trunc_rec_on pp (λp, tr ⟨p.1, tr p.2⟩))
|
||||
(λpp, trunc_rec_on pp (λp, trunc_rec_on p.2 (λb, tr ⟨p.1, b⟩)))
|
||||
(λpp, trunc_rec_on pp (λp, sigma.rec_on p (λa bb, trunc_rec_on bb (λb, idp))))
|
||||
(λpp, trunc_rec_on pp (λp, sigma.rec_on p (λa b, idp)))
|
||||
|
||||
definition trunc_sigma_equiv_of_is_trunc [H : is_trunc n X]
|
||||
: trunc n (Σ x, P x) ≃ Σ x, trunc n (P x) :=
|
||||
calc
|
||||
trunc n (Σ x, P x) ≃ trunc n (Σ x, trunc n (P x)) : trunc_sigma_equiv
|
||||
... ≃ Σ x, trunc n (P x) : equiv.symm !equiv_trunc
|
||||
end
|
||||
|
||||
end trunc
|
||||
|
||||
|
||||
protected definition rec_on {n : trunc_index} {A : Type} {P : trunc n A → Type} (aa : trunc n A)
|
||||
[Pt : Πaa, is_trunc n (P aa)] (H : Πa, P (tr a)) : P aa :=
|
||||
trunc.rec H aa
|
||||
|
|
|
|||
|
|
@ -10,7 +10,7 @@ Type quotients (quotient without truncation)
|
|||
|
||||
/- The hit type_quotient is primitive, declared in init.hit. -/
|
||||
|
||||
open eq
|
||||
open eq equiv sigma.ops
|
||||
|
||||
namespace type_quotient
|
||||
|
||||
|
|
@ -29,4 +29,21 @@ namespace type_quotient
|
|||
: ap (elim Pc Pp) (eq_of_rel H) = sorry ⬝ Pp H ⬝ sorry :=
|
||||
sorry
|
||||
|
||||
protected definition elim_type (Pc : A → Type)
|
||||
(Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a ≃ Pc a') : type_quotient R → Type :=
|
||||
elim Pc (λa a' H, ua (Pp H))
|
||||
|
||||
protected definition elim_type_on [reducible] (x : type_quotient R) (Pc : A → Type)
|
||||
(Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a ≃ Pc a') : Type :=
|
||||
elim_type Pc Pp x
|
||||
|
||||
protected definition elim_type_eq_of_rel (Pc : A → Type)
|
||||
(Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a ≃ Pc a') {a a' : A} (H : R a a')
|
||||
: transport (elim_type Pc Pp) (eq_of_rel H) = sorry /-to_fun (Pp H)-/ :=
|
||||
sorry
|
||||
|
||||
definition elim_type_uncurried (H : Σ(Pc : A → Type), Π⦃a a' : A⦄ (H : R a a'), Pc a ≃ Pc a')
|
||||
: type_quotient R → Type :=
|
||||
elim_type H.1 H.2
|
||||
|
||||
end type_quotient
|
||||
|
|
|
|||
|
|
@ -23,11 +23,11 @@ open is_trunc eq
|
|||
- the type formation
|
||||
- the term and path constructors
|
||||
- the dependent recursor
|
||||
We add the computation rule for point constructors judgmentally to the kernel of Lean, and for the
|
||||
path constructors (undecided).
|
||||
We add the computation rule for point constructors judgmentally to the kernel of Lean.
|
||||
The computation rules for the path constructors are added (propositionally) as axioms
|
||||
|
||||
In this file we only define the dependent recursor. For the nondependent recursor and all other
|
||||
uses of these hits, see the folder /hott/hit/
|
||||
uses of these hits, see the folder ../hit/
|
||||
-/
|
||||
|
||||
constant trunc.{u} (n : trunc_index) (A : Type.{u}) : Type.{u}
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue