feat(circle): define circle as sphere 1, remove all but 1 sorry
This commit is contained in:
Floris van Doorn
Leonardo de Moura
parent
6c061991cc
commit
c23e707874
2 changed files with 40 additions and 25 deletions
|
|
@ -12,61 +12,62 @@ import .sphere
|
|||
|
||||
open eq suspension bool sphere_index equiv equiv.ops
|
||||
|
||||
definition circle [reducible] := suspension bool --redefine this as sphere 1
|
||||
definition circle [reducible] := sphere 1
|
||||
|
||||
namespace circle
|
||||
|
||||
definition base1 : circle := !north
|
||||
definition base2 : circle := !south
|
||||
definition seg1 : base1 = base2 := merid tt
|
||||
definition seg2 : base2 = base1 := (merid ff)⁻¹
|
||||
definition seg1 : base1 = base2 := merid !north
|
||||
definition seg2 : base1 = base2 := merid !south
|
||||
|
||||
definition base : circle := base1
|
||||
definition loop : base = base := seg1 ⬝ seg2
|
||||
definition loop : base = base := seg1 ⬝ seg2⁻¹
|
||||
|
||||
definition rec2 {P : circle → Type} (Pb1 : P base1) (Pb2 : P base2)
|
||||
(Ps1 : seg1 ▹ Pb1 = Pb2) (Ps2 : seg2 ▹ Pb2 = Pb1) (x : circle) : P x :=
|
||||
(Ps1 : seg1 ▹ Pb1 = Pb2) (Ps2 : seg2 ▹ Pb1 = Pb2) (x : circle) : P x :=
|
||||
begin
|
||||
fapply (suspension.rec_on x),
|
||||
{ exact Pb1},
|
||||
{ exact Pb2},
|
||||
{ intro b, cases b,
|
||||
apply tr_eq_of_eq_inv_tr, exact Ps2⁻¹,
|
||||
exact Ps1},
|
||||
{ esimp, intro b, fapply (suspension.rec_on b),
|
||||
{ exact Ps1},
|
||||
{ exact Ps2},
|
||||
{ intro x, cases x}},
|
||||
end
|
||||
|
||||
definition rec2_on [reducible] {P : circle → Type} (x : circle) (Pb1 : P base1) (Pb2 : P base2)
|
||||
(Ps1 : seg1 ▹ Pb1 = Pb2) (Ps2 : seg2 ▹ Pb2 = Pb1) : P x :=
|
||||
(Ps1 : seg1 ▹ Pb1 = Pb2) (Ps2 : seg2 ▹ Pb1 = Pb2) : P x :=
|
||||
circle.rec2 Pb1 Pb2 Ps1 Ps2 x
|
||||
|
||||
theorem rec2_seg1 {P : circle → Type} (Pb1 : P base1) (Pb2 : P base2)
|
||||
(Ps1 : seg1 ▹ Pb1 = Pb2) (Ps2 : seg2 ▹ Pb2 = Pb1)
|
||||
(Ps1 : seg1 ▹ Pb1 = Pb2) (Ps2 : seg2 ▹ Pb1 = Pb2)
|
||||
: apd (rec2 Pb1 Pb2 Ps1 Ps2) seg1 = Ps1 :=
|
||||
!rec_merid
|
||||
|
||||
theorem rec2_seg2 {P : circle → Type} (Pb1 : P base1) (Pb2 : P base2)
|
||||
(Ps1 : seg1 ▹ Pb1 = Pb2) (Ps2 : seg2 ▹ Pb2 = Pb1)
|
||||
(Ps1 : seg1 ▹ Pb1 = Pb2) (Ps2 : seg2 ▹ Pb1 = Pb2)
|
||||
: apd (rec2 Pb1 Pb2 Ps1 Ps2) seg2 = Ps2 :=
|
||||
sorry
|
||||
!rec_merid
|
||||
|
||||
definition elim2 {P : Type} (Pb1 Pb2 : P) (Ps1 : Pb1 = Pb2) (Ps2 : Pb2 = Pb1) (x : circle) : P :=
|
||||
definition elim2 {P : Type} (Pb1 Pb2 : P) (Ps1 : Pb1 = Pb2) (Ps2 : Pb1 = Pb2) (x : circle) : P :=
|
||||
rec2 Pb1 Pb2 (!tr_constant ⬝ Ps1) (!tr_constant ⬝ Ps2) x
|
||||
|
||||
definition elim2_on [reducible] {P : Type} (x : circle) (Pb1 Pb2 : P)
|
||||
(Ps1 : Pb1 = Pb2) (Ps2 : Pb2 = Pb1) : P :=
|
||||
(Ps1 : Pb1 = Pb2) (Ps2 : Pb1 = Pb2) : P :=
|
||||
elim2 Pb1 Pb2 Ps1 Ps2 x
|
||||
|
||||
theorem elim2_seg1 {P : Type} (Pb1 Pb2 : P) (Ps1 : Pb1 = Pb2) (Ps2 : Pb2 = Pb1)
|
||||
theorem elim2_seg1 {P : Type} (Pb1 Pb2 : P) (Ps1 : Pb1 = Pb2) (Ps2 : Pb1 = Pb2)
|
||||
: 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
|
||||
|
||||
theorem elim2_seg2 {P : Type} (Pb1 Pb2 : P) (Ps1 : Pb1 = Pb2) (Ps2 : Pb2 = Pb1)
|
||||
theorem elim2_seg2 {P : Type} (Pb1 Pb2 : P) (Ps1 : Pb1 = Pb2) (Ps2 : Pb1 = Pb2)
|
||||
: ap (elim2 Pb1 Pb2 Ps1 Ps2) seg2 = Ps2 :=
|
||||
begin
|
||||
apply (@cancel_left _ _ _ _ (tr_constant seg2 (elim2 Pb1 Pb2 Ps1 Ps2 base2))),
|
||||
apply (@cancel_left _ _ _ _ (tr_constant seg2 (elim2 Pb1 Pb2 Ps1 Ps2 base1))),
|
||||
rewrite [-apd_eq_tr_constant_con_ap,↑elim2,rec2_seg2],
|
||||
end
|
||||
|
||||
|
|
@ -77,7 +78,7 @@ namespace circle
|
|||
{ exact Pbase},
|
||||
{ exact (transport P seg1 Pbase)},
|
||||
{ apply idp},
|
||||
{ apply eq_tr_of_inv_tr_eq, rewrite -tr_con, apply Ploop},
|
||||
{ apply tr_eq_of_eq_inv_tr, rewrite -tr_con, exact Ploop⁻¹},
|
||||
end
|
||||
|
||||
example {P : circle → Type} (Pbase : P base) (Ploop : loop ▹ Pbase = Pbase) : rec Pbase Ploop base = Pbase := idp
|
||||
|
|
@ -85,10 +86,14 @@ namespace circle
|
|||
protected definition rec_on [reducible] {P : circle → Type} (x : circle) (Pbase : P base)
|
||||
(Ploop : loop ▹ Pbase = Pbase) : P x :=
|
||||
rec Pbase Ploop x
|
||||
|
||||
set_option pp.beta false
|
||||
theorem rec_loop {P : circle → Type} (Pbase : P base) (Ploop : loop ▹ Pbase = Pbase) :
|
||||
apd (rec Pbase Ploop) loop = Ploop :=
|
||||
sorry
|
||||
-- begin
|
||||
-- rewrite [↑loop,apd_con,↑rec,↑rec2_on,↑base,rec2_seg1,apd_inv,rec2_seg2,↑ap,↑eq.rec_on,▸*],
|
||||
-- esimp
|
||||
-- end
|
||||
|
||||
protected definition elim {P : Type} (Pbase : P) (Ploop : Pbase = Pbase)
|
||||
(x : circle) : P :=
|
||||
|
|
|
|||
|
|
@ -227,7 +227,7 @@ namespace eq
|
|||
definition ap11 {f g : A → B} (H : f = g) {x y : A} (p : x = y) : f x = g y :=
|
||||
eq.rec_on H (eq.rec_on p idp)
|
||||
|
||||
definition apd (f : Πa:A, P a) {x y : A} (p : x = y) : p ▹ (f x) = f y :=
|
||||
definition apd (f : Πa:A, P a) {x y : A} (p : x = y) : p ▹ f x = f y :=
|
||||
eq.rec_on p idp
|
||||
|
||||
/- calc enviroment -/
|
||||
|
|
@ -261,20 +261,19 @@ namespace eq
|
|||
-- functorial.
|
||||
|
||||
-- Functions take identity paths to identity paths
|
||||
definition ap_idp (x : A) (f : A → B) : ap f idp = idp :> (f x = f x) := idp
|
||||
definition apd_idp (x : A) (f : Πx, P x) : apd f idp = idp :> (f x = f x) := idp
|
||||
definition ap_idp (x : A) (f : A → B) : ap f idp = idp :> (f x = f x) := idp
|
||||
|
||||
-- Functions commute with concatenation.
|
||||
definition ap_con (f : A → B) {x y z : A} (p : x = y) (q : y = z) :
|
||||
ap f (p ⬝ q) = (ap f p) ⬝ (ap f q) :=
|
||||
ap f (p ⬝ q) = ap f p ⬝ ap f q :=
|
||||
eq.rec_on q (eq.rec_on p idp)
|
||||
|
||||
definition con_ap_con_eq_con_ap_con_ap (f : A → B) {w x y z : A} (r : f w = f x) (p : x = y) (q : y = z) :
|
||||
r ⬝ (ap f (p ⬝ q)) = (r ⬝ ap f p) ⬝ (ap f q) :=
|
||||
r ⬝ ap f (p ⬝ q) = (r ⬝ ap f p) ⬝ ap f q :=
|
||||
eq.rec_on q (take p, eq.rec_on p (con.assoc' r idp idp)) p
|
||||
|
||||
definition ap_con_con_eq_ap_con_ap_con (f : A → B) {w x y z : A} (p : x = y) (q : y = z) (r : f z = f w) :
|
||||
(ap f (p ⬝ q)) ⬝ r = (ap f p) ⬝ (ap f q ⬝ r) :=
|
||||
ap f (p ⬝ q) ⬝ r = ap f p ⬝ (ap f q ⬝ r) :=
|
||||
eq.rec_on q (eq.rec_on p (take r, con.assoc _ _ _)) r
|
||||
|
||||
-- Functions commute with path inverses.
|
||||
|
|
@ -431,6 +430,17 @@ namespace eq
|
|||
tr_inv_tr P p (transport P p z) = ap (transport P p) (inv_tr_tr P p z) :=
|
||||
eq.rec_on p idp
|
||||
|
||||
/- some properties for apd -/
|
||||
|
||||
definition apd_idp (x : A) (f : Πx, P x) : apd f idp = idp :> (f x = f x) := idp
|
||||
definition apd_con (f : Πx, P x) {x y z : A} (p : x = y) (q : y = z)
|
||||
: apd f (p ⬝ q) = tr_con P p q (f x) ⬝ ap (transport P q) (apd f p) ⬝ apd f q :=
|
||||
by cases p;cases q;apply idp
|
||||
definition apd_inv (f : Πx, P x) {x y : A} (p : x = y)
|
||||
: apd f p⁻¹ = (eq_inv_tr_of_tr_eq P (apd f p))⁻¹ :=
|
||||
by cases p;apply idp
|
||||
|
||||
|
||||
-- Dependent transport in a doubly dependent type.
|
||||
definition transportD {P : A → Type} (Q : Π a : A, P a → Type)
|
||||
{a a' : A} (p : a = a') (b : P a) (z : Q a b) : Q a' (p ▹ b) :=
|
||||
|
|
|
|||
Loading…
Reference in a new issue