feat(hit): derive path computation rule for elim and elim_type for every hit
also make argument of eq_of_rel implicit also remove most sorry's for hits path computation rule for rec still needs to be done for all hits
This commit is contained in:
Floris van Doorn
Leonardo de Moura
parent
4173c958f7
commit
70a2f6534c
12 changed files with 151 additions and 116 deletions
|
|
@ -10,7 +10,7 @@ Declaration of the circle
|
|||
|
||||
import .sphere
|
||||
|
||||
open eq suspension bool sphere_index equiv
|
||||
open eq suspension bool sphere_index equiv equiv.ops
|
||||
|
||||
definition circle [reducible] := suspension bool --redefine this as sphere 1
|
||||
|
||||
|
|
@ -39,14 +39,14 @@ namespace circle
|
|||
(Ps1 : seg1 ▹ Pb1 = Pb2) (Ps2 : seg2 ▹ Pb2 = Pb1) : P x :=
|
||||
circle.rec2 Pb1 Pb2 Ps1 Ps2 x
|
||||
|
||||
definition rec2_seg1 {P : circle → Type} (Pb1 : P base1) (Pb2 : P base2)
|
||||
theorem rec2_seg1 {P : circle → Type} (Pb1 : P base1) (Pb2 : P base2)
|
||||
(Ps1 : seg1 ▹ Pb1 = Pb2) (Ps2 : seg2 ▹ Pb2 = Pb1)
|
||||
: apd (rec2 Pb1 Pb2 Ps1 Ps2) seg1 = sorry ⬝ Ps1 ⬝ sorry :=
|
||||
: apd (rec2 Pb1 Pb2 Ps1 Ps2) seg1 = Ps1 :=
|
||||
sorry
|
||||
|
||||
definition rec2_seg2 {P : circle → Type} (Pb1 : P base1) (Pb2 : P base2)
|
||||
theorem rec2_seg2 {P : circle → Type} (Pb1 : P base1) (Pb2 : P base2)
|
||||
(Ps1 : seg1 ▹ Pb1 = Pb2) (Ps2 : seg2 ▹ Pb2 = Pb1)
|
||||
: apd (rec2 Pb1 Pb2 Ps1 Ps2) seg2 = sorry ⬝ Ps2 ⬝ sorry :=
|
||||
: apd (rec2 Pb1 Pb2 Ps1 Ps2) seg2 = Ps2 :=
|
||||
sorry
|
||||
|
||||
definition elim2 {P : Type} (Pb1 Pb2 : P) (Ps1 : Pb1 = Pb2) (Ps2 : Pb2 = Pb1) (x : circle) : P :=
|
||||
|
|
@ -56,13 +56,19 @@ namespace circle
|
|||
(Ps1 : Pb1 = Pb2) (Ps2 : Pb2 = Pb1) : P :=
|
||||
elim2 Pb1 Pb2 Ps1 Ps2 x
|
||||
|
||||
definition elim2_seg1 {P : Type} (Pb1 Pb2 : P) (Ps1 : Pb1 = Pb2) (Ps2 : Pb2 = Pb1)
|
||||
: ap (elim2 Pb1 Pb2 Ps1 Ps2) seg1 = sorry ⬝ Ps1 ⬝ sorry :=
|
||||
sorry
|
||||
theorem elim2_seg1 {P : Type} (Pb1 Pb2 : P) (Ps1 : Pb1 = Pb2) (Ps2 : Pb2 = Pb1)
|
||||
: ap (elim2 Pb1 Pb2 Ps1 Ps2) seg1 = Ps1 :=
|
||||
begin
|
||||
apply (@cancel_left _ _ _ _ (tr_constant seg1 (elim2 Pb1 Pb2 Ps1 Ps2 base1))),
|
||||
rewrite [-apd_eq_tr_constant_con_ap,↑elim2,rec2_seg1],
|
||||
end
|
||||
|
||||
definition elim2_seg2 {P : Type} (Pb1 Pb2 : P) (Ps1 : Pb1 = Pb2) (Ps2 : Pb2 = Pb1)
|
||||
: ap (elim2 Pb1 Pb2 Ps1 Ps2) seg2 = sorry ⬝ Ps2 ⬝ sorry :=
|
||||
sorry
|
||||
theorem elim2_seg2 {P : Type} (Pb1 Pb2 : P) (Ps1 : Pb1 = Pb2) (Ps2 : Pb2 = Pb1)
|
||||
: ap (elim2 Pb1 Pb2 Ps1 Ps2) seg2 = Ps2 :=
|
||||
begin
|
||||
apply (@cancel_left _ _ _ _ (tr_constant seg2 (elim2 Pb1 Pb2 Ps1 Ps2 base2))),
|
||||
rewrite [-apd_eq_tr_constant_con_ap,↑elim2,rec2_seg2],
|
||||
end
|
||||
|
||||
protected definition rec {P : circle → Type} (Pbase : P base) (Ploop : loop ▹ Pbase = Pbase)
|
||||
(x : circle) : P x :=
|
||||
|
|
@ -74,12 +80,14 @@ namespace circle
|
|||
{ apply eq_tr_of_inv_tr_eq, rewrite -tr_con, apply Ploop},
|
||||
end
|
||||
|
||||
example {P : circle → Type} (Pbase : P base) (Ploop : loop ▹ Pbase = Pbase) : rec Pbase Ploop base = Pbase := idp
|
||||
|
||||
protected definition rec_on [reducible] {P : circle → Type} (x : circle) (Pbase : P base)
|
||||
(Ploop : loop ▹ Pbase = Pbase) : P 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 :=
|
||||
theorem rec_loop {P : circle → Type} (Pbase : P base) (Ploop : loop ▹ Pbase = Pbase) :
|
||||
apd (rec Pbase Ploop) loop = Ploop :=
|
||||
sorry
|
||||
|
||||
protected definition elim {P : Type} (Pbase : P) (Ploop : Pbase = Pbase)
|
||||
|
|
@ -90,9 +98,12 @@ namespace circle
|
|||
(Ploop : Pbase = Pbase) : P :=
|
||||
elim Pbase Ploop x
|
||||
|
||||
definition elim_loop {P : Type} (Pbase : P) (Ploop : Pbase = Pbase) :
|
||||
ap (elim Pbase Ploop) loop = sorry ⬝ Ploop ⬝ sorry :=
|
||||
sorry
|
||||
theorem elim_loop {P : Type} (Pbase : P) (Ploop : Pbase = Pbase) :
|
||||
ap (elim Pbase Ploop) loop = Ploop :=
|
||||
begin
|
||||
apply (@cancel_left _ _ _ _ (tr_constant loop (elim Pbase Ploop base))),
|
||||
rewrite [-apd_eq_tr_constant_con_ap,↑elim,rec_loop],
|
||||
end
|
||||
|
||||
protected definition elim_type (Pbase : Type) (Ploop : Pbase ≃ Pbase)
|
||||
(x : circle) : Type :=
|
||||
|
|
@ -102,8 +113,8 @@ namespace circle
|
|||
(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
|
||||
theorem elim_type_loop (Pbase : Type) (Ploop : Pbase ≃ Pbase) :
|
||||
transport (elim_type Pbase Ploop) loop = Ploop :=
|
||||
by rewrite [tr_eq_cast_ap_fn,↑elim_type,elim_loop];apply cast_ua_fn
|
||||
|
||||
end circle
|
||||
|
|
|
|||
|
|
@ -10,7 +10,7 @@ Declaration of the coequalizer
|
|||
|
||||
import .type_quotient
|
||||
|
||||
open type_quotient eq equiv
|
||||
open type_quotient eq equiv equiv.ops
|
||||
|
||||
namespace coeq
|
||||
section
|
||||
|
|
@ -30,7 +30,7 @@ parameters {A B : Type.{u}} (f g : A → B)
|
|||
|
||||
/- cp is the name Coq uses. I don't know what it abbreviates, but at least it's short :-) -/
|
||||
definition cp (x : A) : coeq_i (f x) = coeq_i (g x) :=
|
||||
eq_of_rel (Rmk f g x)
|
||||
eq_of_rel coeq_rel (Rmk f g x)
|
||||
|
||||
protected definition rec {P : coeq → Type} (P_i : Π(x : B), P (coeq_i x))
|
||||
(Pcp : Π(x : A), cp x ▹ P_i (f x) = P_i (g x)) (y : coeq) : P y :=
|
||||
|
|
@ -44,9 +44,9 @@ 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))
|
||||
theorem 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 :=
|
||||
(x : A) : apd (rec P_i Pcp) (cp x) = Pcp x :=
|
||||
sorry
|
||||
|
||||
protected definition elim {P : Type} (P_i : B → P)
|
||||
|
|
@ -57,9 +57,12 @@ 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 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
|
||||
theorem 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) = Pcp x :=
|
||||
begin
|
||||
apply (@cancel_left _ _ _ _ (tr_constant (cp x) (elim P_i Pcp (coeq_i (f x))))),
|
||||
rewrite [-apd_eq_tr_constant_con_ap,↑elim,rec_cp],
|
||||
end
|
||||
|
||||
protected definition elim_type (P_i : B → Type)
|
||||
(Pcp : Π(x : A), P_i (f x) ≃ P_i (g x)) (y : coeq) : Type :=
|
||||
|
|
@ -69,10 +72,9 @@ parameters {A B : Type.{u}} (f g : A → B)
|
|||
(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
|
||||
|
||||
theorem 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) = Pcp x :=
|
||||
by rewrite [tr_eq_cast_ap_fn,↑elim_type,elim_cp];apply cast_ua_fn
|
||||
|
||||
end
|
||||
|
||||
|
|
|
|||
|
|
@ -9,7 +9,7 @@ Definition of general colimits and sequential colimits.
|
|||
-/
|
||||
|
||||
/- definition of a general colimit -/
|
||||
open eq nat type_quotient sigma equiv
|
||||
open eq nat type_quotient sigma equiv equiv.ops
|
||||
|
||||
namespace colimit
|
||||
section
|
||||
|
|
@ -32,7 +32,7 @@ section
|
|||
abbreviation ι := @incl
|
||||
|
||||
definition cglue : ι (f j b) = ι b :=
|
||||
eq_of_rel (Rmk f b)
|
||||
eq_of_rel colim_rel (Rmk f b)
|
||||
|
||||
protected definition rec {P : colimit → Type}
|
||||
(Pincl : Π⦃i : I⦄ (x : A i), P (ι x))
|
||||
|
|
@ -49,7 +49,7 @@ section
|
|||
(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}
|
||||
theorem rec_cglue {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 :=
|
||||
|
|
@ -64,11 +64,14 @@ section
|
|||
(Pglue : Π(j : J) (x : A (dom j)), Pincl (f j x) = Pincl x) : P :=
|
||||
elim Pincl Pglue y
|
||||
|
||||
definition elim_cglue [reducible] {P : Type}
|
||||
theorem elim_cglue {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
|
||||
begin
|
||||
apply (@cancel_left _ _ _ _ (tr_constant (cglue j x) (elim Pincl Pglue (ι (f j x))))),
|
||||
rewrite [-apd_eq_tr_constant_con_ap,↑elim,rec_cglue],
|
||||
end
|
||||
|
||||
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 :=
|
||||
|
|
@ -79,10 +82,10 @@ section
|
|||
(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)
|
||||
theorem elim_type_cglue (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
|
||||
{j : J} (x : A (dom j)) : transport (elim_type Pincl Pglue) (cglue j x) = Pglue j x :=
|
||||
by rewrite [tr_eq_cast_ap_fn,↑elim_type,elim_cglue];apply cast_ua_fn
|
||||
|
||||
end
|
||||
end colimit
|
||||
|
|
@ -109,9 +112,9 @@ section
|
|||
abbreviation sι := @inclusion
|
||||
|
||||
definition glue : sι (f a) = sι a :=
|
||||
eq_of_rel (Rmk f a)
|
||||
eq_of_rel seq_rel (Rmk f a)
|
||||
|
||||
protected definition rec [reducible] {P : seq_colim → Type}
|
||||
protected definition rec {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
|
||||
|
|
@ -126,6 +129,11 @@ section
|
|||
: P aa :=
|
||||
rec Pincl Pglue aa
|
||||
|
||||
theorem 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) = Pglue a :=
|
||||
sorry
|
||||
|
||||
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)
|
||||
|
|
@ -135,15 +143,13 @@ section
|
|||
(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)
|
||||
theorem 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
|
||||
: ap (elim Pincl Pglue) (glue a) = Pglue a :=
|
||||
begin
|
||||
apply (@cancel_left _ _ _ _ (tr_constant (glue a) (elim Pincl Pglue (sι (f a))))),
|
||||
rewrite [-apd_eq_tr_constant_con_ap,↑elim,rec_glue],
|
||||
end
|
||||
|
||||
protected definition elim_type (Pincl : Π⦃n : ℕ⦄ (a : A n), Type)
|
||||
(Pglue : Π⦃n : ℕ⦄ (a : A n), Pincl (f a) ≃ Pincl a) : seq_colim → Type :=
|
||||
|
|
@ -154,10 +160,10 @@ section
|
|||
(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)
|
||||
theorem 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
|
||||
: transport (elim_type Pincl Pglue) (glue a) = Pglue a :=
|
||||
by rewrite [tr_eq_cast_ap_fn,↑elim_type,elim_glue];apply cast_ua_fn
|
||||
|
||||
end
|
||||
end seq_colim
|
||||
|
|
|
|||
|
|
@ -10,7 +10,7 @@ Declaration of mapping cylinders
|
|||
|
||||
import .type_quotient
|
||||
|
||||
open type_quotient eq sum equiv
|
||||
open type_quotient eq sum equiv equiv.ops
|
||||
|
||||
namespace cylinder
|
||||
section
|
||||
|
|
@ -33,7 +33,7 @@ parameters {A B : Type.{u}} (f : A → B)
|
|||
class_of R (inr a)
|
||||
|
||||
definition seg (a : A) : base (f a) = top a :=
|
||||
eq_of_rel (Rmk f a)
|
||||
eq_of_rel cylinder_rel (Rmk f a)
|
||||
|
||||
protected definition rec {P : cylinder → Type}
|
||||
(Pbase : Π(b : B), P (base b)) (Ptop : Π(a : A), P (top a))
|
||||
|
|
@ -51,10 +51,10 @@ 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}
|
||||
theorem 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 :=
|
||||
(a : A) : apd (rec Pbase Ptop Pseg) (seg a) = Pseg a :=
|
||||
sorry
|
||||
|
||||
protected definition elim {P : Type} (Pbase : B → P) (Ptop : A → P)
|
||||
|
|
@ -65,10 +65,13 @@ parameters {A B : Type.{u}} (f : A → B)
|
|||
(Pseg : Π(a : A), Pbase (f a) = Ptop a) : P :=
|
||||
elim Pbase Ptop Pseg x
|
||||
|
||||
definition elim_seg {P : Type} (Pbase : B → P) (Ptop : A → P)
|
||||
theorem 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
|
||||
(a : A) : ap (elim Pbase Ptop Pseg) (seg a) = Pseg a :=
|
||||
begin
|
||||
apply (@cancel_left _ _ _ _ (tr_constant (seg a) (elim Pbase Ptop Pseg (base (f a))))),
|
||||
rewrite [-apd_eq_tr_constant_con_ap,↑elim,rec_seg],
|
||||
end
|
||||
|
||||
protected definition elim_type (Pbase : B → Type) (Ptop : A → Type)
|
||||
(Pseg : Π(a : A), Pbase (f a) ≃ Ptop a) (x : cylinder) : Type :=
|
||||
|
|
@ -78,10 +81,10 @@ parameters {A B : Type.{u}} (f : A → B)
|
|||
(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)
|
||||
theorem 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
|
||||
(a : A) : transport (elim_type Pbase Ptop Pseg) (seg a) = Pseg a :=
|
||||
by rewrite [tr_eq_cast_ap_fn,↑elim_type,elim_seg];apply cast_ua_fn
|
||||
|
||||
end
|
||||
|
||||
|
|
|
|||
|
|
@ -10,7 +10,7 @@ Declaration of the pushout
|
|||
|
||||
import .type_quotient
|
||||
|
||||
open type_quotient eq sum equiv
|
||||
open type_quotient eq sum equiv equiv.ops
|
||||
|
||||
namespace pushout
|
||||
section
|
||||
|
|
@ -32,7 +32,7 @@ parameters {TL BL TR : Type} (f : TL → BL) (g : TL → TR)
|
|||
class_of R (inr x)
|
||||
|
||||
definition glue (x : TL) : inl (f x) = inr (g x) :=
|
||||
eq_of_rel (Rmk f g x)
|
||||
eq_of_rel pushout_rel (Rmk f g x)
|
||||
|
||||
protected definition rec {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))
|
||||
|
|
@ -50,18 +50,7 @@ parameters {TL BL TR : Type} (f : TL → BL) (g : TL → TR)
|
|||
(Pglue : Π(x : TL), glue x ▹ Pinl (f x) = Pinr (g x)) : P y :=
|
||||
rec Pinl Pinr Pglue y
|
||||
|
||||
--these definitions are needed until we have them definitionally
|
||||
definition rec_inl {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 : BL) : rec Pinl Pinr Pglue (inl x) = Pinl x :=
|
||||
idp
|
||||
|
||||
definition rec_inr {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 : TR) : rec Pinl Pinr Pglue (inr x) = Pinr x :=
|
||||
idp
|
||||
|
||||
definition rec_glue {P : pushout → Type} (Pinl : Π(x : BL), P (inl x))
|
||||
theorem 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) = Pglue x :=
|
||||
sorry
|
||||
|
|
@ -74,10 +63,13 @@ parameters {TL BL TR : Type} (f : TL → BL) (g : TL → TR)
|
|||
(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)
|
||||
theorem elim_glue {P : Type} (Pinl : BL → P) (Pinr : TR → P)
|
||||
(Pglue : Π(x : TL), Pinl (f x) = Pinr (g x)) (x : TL)
|
||||
: ap (elim Pinl Pinr Pglue) (glue x) = Pglue x :=
|
||||
sorry
|
||||
begin
|
||||
apply (@cancel_left _ _ _ _ (tr_constant (glue x) (elim Pinl Pinr Pglue (inl (f x))))),
|
||||
rewrite [-apd_eq_tr_constant_con_ap,↑elim,rec_glue],
|
||||
end
|
||||
|
||||
protected definition elim_type (Pinl : BL → Type) (Pinr : TR → Type)
|
||||
(Pglue : Π(x : TL), Pinl (f x) ≃ Pinr (g x)) (y : pushout) : Type :=
|
||||
|
|
@ -87,17 +79,18 @@ parameters {TL BL TR : Type} (f : TL → BL) (g : TL → TR)
|
|||
(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)
|
||||
theorem 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
|
||||
: transport (elim_type Pinl Pinr Pglue) (glue x) = Pglue x :=
|
||||
by rewrite [tr_eq_cast_ap_fn,↑elim_type,elim_glue];apply cast_ua_fn
|
||||
|
||||
end
|
||||
|
||||
open pushout equiv is_equiv unit bool
|
||||
|
||||
|
||||
namespace test
|
||||
definition unit_of_empty (u : empty) : unit := star
|
||||
open pushout equiv is_equiv unit bool
|
||||
private definition unit_of_empty (u : empty) : unit := star
|
||||
|
||||
example : pushout unit_of_empty unit_of_empty ≃ bool :=
|
||||
begin
|
||||
|
|
@ -111,8 +104,8 @@ end
|
|||
exact (inr _ _ ⋆)},
|
||||
{ intro b, cases b, esimp, esimp},
|
||||
{ intro x, fapply (pushout.rec_on _ _ x),
|
||||
intro u, cases u, rewrite [↑function.compose,↑pushout.rec_on,rec_inl],
|
||||
intro u, cases u, rewrite [↑function.compose,↑pushout.rec_on,rec_inr],
|
||||
intro u, cases u, esimp,
|
||||
intro u, cases u, esimp,
|
||||
intro c, cases c},
|
||||
end
|
||||
|
||||
|
|
|
|||
|
|
@ -22,7 +22,7 @@ parameters {A : Type} (R : A → A → hprop)
|
|||
tr (class_of _ a)
|
||||
|
||||
definition eq_of_rel {a a' : A} (H : R a a') : class_of a = class_of a' :=
|
||||
ap tr (eq_of_rel H)
|
||||
ap tr (eq_of_rel _ H)
|
||||
|
||||
theorem is_hset_quotient : is_hset quotient :=
|
||||
begin unfold quotient, exact _ end
|
||||
|
|
@ -44,9 +44,9 @@ parameters {A : Type} (R : A → A → hprop)
|
|||
(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_hset (P aa)]
|
||||
theorem 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 :=
|
||||
{a a' : A} (H : R a a') : apd (rec Pc Pp) (eq_of_rel H) = Pp H :=
|
||||
sorry
|
||||
|
||||
protected definition elim {P : Type} [Pt : is_hset P] (Pc : A → P)
|
||||
|
|
@ -57,10 +57,18 @@ parameters {A : Type} (R : A → A → hprop)
|
|||
(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_hset P] (Pc : A → P)
|
||||
theorem 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
|
||||
: ap (elim Pc Pp) (eq_of_rel H) = Pp H :=
|
||||
begin
|
||||
apply (@cancel_left _ _ _ _ (tr_constant (eq_of_rel H) (elim Pc Pp (class_of a)))),
|
||||
rewrite [-apd_eq_tr_constant_con_ap,↑elim,rec_eq_of_rel],
|
||||
end
|
||||
|
||||
/-
|
||||
there are no theorems to eliminate to the universe here,
|
||||
because the universe is generally not a set
|
||||
-/
|
||||
|
||||
end
|
||||
end quotient
|
||||
|
|
|
|||
|
|
@ -82,7 +82,7 @@ namespace sphere
|
|||
definition sphere_equiv_bool : sphere 0 ≃ bool :=
|
||||
equiv.MK bool_of_sphere
|
||||
sphere_of_bool
|
||||
sorry --idp
|
||||
sorry --idp
|
||||
(λb, match b with | tt := idp | ff := idp end)
|
||||
(λx, suspension.rec_on x idp idp (empty.rec _))
|
||||
|
||||
end sphere
|
||||
|
|
|
|||
|
|
@ -10,7 +10,7 @@ Declaration of suspension
|
|||
|
||||
import .pushout
|
||||
|
||||
open pushout unit eq equiv
|
||||
open pushout unit eq equiv equiv.ops
|
||||
|
||||
definition suspension (A : Type) : Type := pushout (λ(a : A), star.{0}) (λ(a : A), star.{0})
|
||||
|
||||
|
|
@ -39,9 +39,9 @@ namespace suspension
|
|||
(PN : P !north) (PS : P !south) (Pm : Π(a : A), merid a ▹ PN = PS) : P y :=
|
||||
rec PN PS Pm y
|
||||
|
||||
definition rec_merid {P : suspension A → Type} (PN : P !north) (PS : P !south)
|
||||
theorem 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 :=
|
||||
: apd (rec PN PS Pm) (merid a) = Pm a :=
|
||||
sorry
|
||||
|
||||
protected definition elim {P : Type} (PN : P) (PS : P) (Pm : A → PN = PS)
|
||||
|
|
@ -52,9 +52,12 @@ namespace suspension
|
|||
(PN : P) (PS : P) (Pm : A → PN = PS) : P :=
|
||||
elim PN PS Pm x
|
||||
|
||||
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
|
||||
theorem elim_merid {P : Type} (PN : P) (PS : P) (Pm : A → PN = PS) (a : A)
|
||||
: ap (elim PN PS Pm) (merid a) = Pm a :=
|
||||
begin
|
||||
apply (@cancel_left _ _ _ _ (tr_constant (merid a) (elim PN PS Pm !north))),
|
||||
rewrite [-apd_eq_tr_constant_con_ap,↑elim,rec_merid],
|
||||
end
|
||||
|
||||
protected definition elim_type (PN : Type) (PS : Type) (Pm : A → PN ≃ PS)
|
||||
(x : suspension A) : Type :=
|
||||
|
|
@ -64,9 +67,8 @@ namespace suspension
|
|||
(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
|
||||
|
||||
theorem elim_type_merid (PN : Type) (PS : Type) (Pm : A → PN ≃ PS)
|
||||
(x : suspension A) (a : A) : transport (elim_type PN PS Pm) (merid a) = Pm a :=
|
||||
by rewrite [tr_eq_cast_ap_fn,↑elim_type,elim_merid];apply cast_ua_fn
|
||||
|
||||
end suspension
|
||||
|
|
|
|||
|
|
@ -26,4 +26,9 @@ namespace trunc
|
|||
[Pt : is_trunc n P] (H : A → P) : P :=
|
||||
elim H aa
|
||||
|
||||
/-
|
||||
there are no theorems to eliminate to the universe here,
|
||||
because the universe is generally not a set
|
||||
-/
|
||||
|
||||
end trunc
|
||||
|
|
|
|||
|
|
@ -19,15 +19,18 @@ namespace type_quotient
|
|||
protected definition elim {P : Type} (Pc : A → P) (Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a = Pc a')
|
||||
(x : type_quotient R) : P :=
|
||||
type_quotient.rec Pc (λa a' H, !tr_constant ⬝ Pp H) x
|
||||
|
||||
attribute elim [unfold-c 6]
|
||||
protected definition elim_on [reducible] {P : Type} (x : type_quotient R)
|
||||
(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} (Pc : A → P)
|
||||
theorem elim_eq_of_rel {P : Type} (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) = Pp H :=
|
||||
sorry
|
||||
: ap (elim Pc Pp) (eq_of_rel R H) = Pp H :=
|
||||
begin
|
||||
apply (@cancel_left _ _ _ _ (tr_constant (eq_of_rel R H) (elim Pc Pp (class_of R a)))),
|
||||
rewrite [-apd_eq_tr_constant_con_ap,↑elim,rec_eq_of_rel],
|
||||
end
|
||||
|
||||
protected definition elim_type (Pc : A → Type)
|
||||
(Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a ≃ Pc a') : type_quotient R → Type :=
|
||||
|
|
@ -37,10 +40,10 @@ namespace type_quotient
|
|||
(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)
|
||||
theorem 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) = to_fun (Pp H) :=
|
||||
sorry
|
||||
: transport (elim_type Pc Pp) (eq_of_rel R H) = to_fun (Pp H) :=
|
||||
by rewrite [tr_eq_cast_ap_fn, ↑elim_type, elim_eq_of_rel];apply cast_ua_fn
|
||||
|
||||
definition elim_type_uncurried (H : Σ(Pc : A → Type), Π⦃a a' : A⦄ (H : R a a'), Pc a ≃ Pc a')
|
||||
: type_quotient R → Type :=
|
||||
|
|
|
|||
|
|
@ -52,16 +52,16 @@ namespace type_quotient
|
|||
|
||||
constant class_of {A : Type} (R : A → A → Type) (a : A) : type_quotient R
|
||||
|
||||
constant eq_of_rel {A : Type} {R : A → A → Type} {a a' : A} (H : R a a')
|
||||
constant eq_of_rel {A : Type} (R : A → A → Type) {a a' : A} (H : R a a')
|
||||
: class_of R a = class_of R a'
|
||||
|
||||
protected constant rec {A : Type} {R : A → A → Type} {P : type_quotient R → Type}
|
||||
(Pc : Π(a : A), P (class_of R a)) (Pp : Π⦃a a' : A⦄ (H : R a a'), eq_of_rel H ▹ Pc a = Pc a')
|
||||
(Pc : Π(a : A), P (class_of R a)) (Pp : Π⦃a a' : A⦄ (H : R a a'), eq_of_rel R H ▹ Pc a = Pc a')
|
||||
(x : type_quotient R) : P x
|
||||
|
||||
protected definition rec_on [reducible] {A : Type} {R : A → A → Type} {P : type_quotient R → Type}
|
||||
(x : type_quotient R) (Pc : Π(a : A), P (class_of R a))
|
||||
(Pp : Π⦃a a' : A⦄ (H : R a a'), eq_of_rel H ▹ Pc a = Pc a') : P x :=
|
||||
(Pp : Π⦃a a' : A⦄ (H : R a a'), eq_of_rel R H ▹ Pc a = Pc a') : P x :=
|
||||
rec Pc Pp x
|
||||
|
||||
end type_quotient
|
||||
|
|
@ -76,11 +76,11 @@ end trunc
|
|||
|
||||
namespace type_quotient
|
||||
definition rec_class_of {A : Type} {R : A → A → Type} {P : type_quotient R → Type}
|
||||
(Pc : Π(a : A), P (class_of R a)) (Pp : Π⦃a a' : A⦄ (H : R a a'), eq_of_rel H ▹ Pc a = Pc a')
|
||||
(Pc : Π(a : A), P (class_of R a)) (Pp : Π⦃a a' : A⦄ (H : R a a'), eq_of_rel R H ▹ Pc a = Pc a')
|
||||
(a : A) : type_quotient.rec Pc Pp (class_of R a) = Pc a :=
|
||||
idp
|
||||
|
||||
constant rec_eq_of_rel {A : Type} {R : A → A → Type} {P : type_quotient R → Type}
|
||||
(Pc : Π(a : A), P (class_of R 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 (type_quotient.rec Pc Pp) (eq_of_rel H) = Pp H
|
||||
(Pc : Π(a : A), P (class_of R a)) (Pp : Π⦃a a' : A⦄ (H : R a a'), eq_of_rel R H ▹ Pc a = Pc a')
|
||||
{a a' : A} (H : R a a') : apd (type_quotient.rec Pc Pp) (eq_of_rel R H) = Pp H
|
||||
end type_quotient
|
||||
|
|
|
|||
|
|
@ -518,6 +518,8 @@ namespace eq
|
|||
definition tr_eq_cast_ap (P : A → Type) {x y} (p : x = y) (u : P x) : p ▹ u = cast (ap P p) u :=
|
||||
eq.rec_on p idp
|
||||
|
||||
definition tr_eq_cast_ap_fn (P : A → Type) {x y} (p : x = y) : transport P p = cast (ap P p) :=
|
||||
eq.rec_on p idp
|
||||
|
||||
/- The behavior of [ap] and [apd] -/
|
||||
|
||||
|
|
|
|||
Loading…
Reference in a new issue