From 70a2f6534cf2b2ffc28372ee6d83c33f6a5de4bf Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Mon, 27 Apr 2015 17:34:55 -0400 Subject: [PATCH] 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 --- hott/hit/circle.hlean | 49 ++++++++++++++++++++++-------------- hott/hit/coeq.hlean | 24 ++++++++++-------- hott/hit/colimit.hlean | 48 +++++++++++++++++++---------------- hott/hit/cylinder.hlean | 23 +++++++++-------- hott/hit/pushout.hlean | 41 +++++++++++++----------------- hott/hit/quotient.hlean | 20 ++++++++++----- hott/hit/sphere.hlean | 4 +-- hott/hit/suspension.hlean | 22 ++++++++-------- hott/hit/trunc.hlean | 5 ++++ hott/hit/type_quotient.hlean | 17 +++++++------ hott/init/hit.hlean | 12 ++++----- hott/init/path.hlean | 2 ++ 12 files changed, 151 insertions(+), 116 deletions(-) diff --git a/hott/hit/circle.hlean b/hott/hit/circle.hlean index f505959151..74925be2f8 100644 --- a/hott/hit/circle.hlean +++ b/hott/hit/circle.hlean @@ -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 diff --git a/hott/hit/coeq.hlean b/hott/hit/coeq.hlean index 2e7ae7a1a1..8cc56c1929 100644 --- a/hott/hit/coeq.hlean +++ b/hott/hit/coeq.hlean @@ -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 diff --git a/hott/hit/colimit.hlean b/hott/hit/colimit.hlean index a67ab835d0..f230af0507 100644 --- a/hott/hit/colimit.hlean +++ b/hott/hit/colimit.hlean @@ -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 diff --git a/hott/hit/cylinder.hlean b/hott/hit/cylinder.hlean index f4f0009597..f7ac621ea9 100644 --- a/hott/hit/cylinder.hlean +++ b/hott/hit/cylinder.hlean @@ -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 diff --git a/hott/hit/pushout.hlean b/hott/hit/pushout.hlean index 8c586ff054..8845fcc546 100644 --- a/hott/hit/pushout.hlean +++ b/hott/hit/pushout.hlean @@ -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 diff --git a/hott/hit/quotient.hlean b/hott/hit/quotient.hlean index 3c1fe19013..55e3c4ef5a 100644 --- a/hott/hit/quotient.hlean +++ b/hott/hit/quotient.hlean @@ -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 diff --git a/hott/hit/sphere.hlean b/hott/hit/sphere.hlean index 76fa231203..1a9d24f5a1 100644 --- a/hott/hit/sphere.hlean +++ b/hott/hit/sphere.hlean @@ -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 diff --git a/hott/hit/suspension.hlean b/hott/hit/suspension.hlean index 40c8c8e112..d094c4e4c3 100644 --- a/hott/hit/suspension.hlean +++ b/hott/hit/suspension.hlean @@ -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 diff --git a/hott/hit/trunc.hlean b/hott/hit/trunc.hlean index 3bf63c0088..d1935e79e6 100644 --- a/hott/hit/trunc.hlean +++ b/hott/hit/trunc.hlean @@ -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 diff --git a/hott/hit/type_quotient.hlean b/hott/hit/type_quotient.hlean index b5db8e5a2d..ed226aadea 100644 --- a/hott/hit/type_quotient.hlean +++ b/hott/hit/type_quotient.hlean @@ -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 := diff --git a/hott/init/hit.hlean b/hott/init/hit.hlean index 8c46bbc897..4fe0daf02b 100644 --- a/hott/init/hit.hlean +++ b/hott/init/hit.hlean @@ -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 diff --git a/hott/init/path.hlean b/hott/init/path.hlean index 5724c00069..3d73fc10dc 100644 --- a/hott/init/path.hlean +++ b/hott/init/path.hlean @@ -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] -/