From 28b4559a0f59030b2c233fe9e683146df988adb5 Mon Sep 17 00:00:00 2001 From: Egbert Rijke Date: Wed, 5 Jul 2017 14:56:03 +0100 Subject: [PATCH] induction on ~~* --- homotopy/pointed_cubes.hlean | 10 ++++++---- pointed_pi.hlean | 23 +++++++++++++++++++++++ 2 files changed, 29 insertions(+), 4 deletions(-) diff --git a/homotopy/pointed_cubes.hlean b/homotopy/pointed_cubes.hlean index 3c3641b..da13de3 100644 --- a/homotopy/pointed_cubes.hlean +++ b/homotopy/pointed_cubes.hlean @@ -10,7 +10,7 @@ The goal of this file is to extend the library of pointed types and pointed maps -/ -import types.pointed2 +import types.pointed2 ..pointed_pi open eq pointed @@ -122,18 +122,20 @@ structure p2homotopy {A B : Type*} {f g : A →* B} (H K : f ~* g) : Type := ( to_2htpy : H ~ K) ( respect_pt : p2homotopy_ty_respect_pt to_2htpy) -definition phsquare_of_p2homotopy {A B : Type*} {f g h i : A →* B} {phtpy_top : f ~* g} {phtpy_bot : h ~* i} {phtpy_left : f ~* h} {phtpy_right : g ~* i} (p2htpy : p2homotopy (phtpy_top ⬝* phtpy_right) (phtpy_left ⬝* phtpy_bot)) : phsquare phtpy_top phtpy_bot phtpy_left phtpy_right := +definition phsquare_of_p2homotopy {A B : Type*} {f g h i : A →* B} {phtpy_top : f ~* g} {phtpy_bot : h ~* i} {phtpy_left : f ~* h} {phtpy_right : g ~* i} (p2htpy : (phtpy_top ⬝* phtpy_right) ~~* (phtpy_left ⬝* phtpy_bot)) : phsquare phtpy_top phtpy_bot phtpy_left phtpy_right := begin induction p2htpy, induction phtpy_left using phomotopy_rec_on_idp, - induction phtpy_right using phomotopy_rec_on_idp, + induction phtpy_right using phomotopy_rec_on_idp, + induction to_2htpy, unfold phsquare, repeat exact sorry end definition ptube_v_phtpy_bot {A B C D : Type*} {ftop ftop' : A →* B} {phtpy_top : ftop ~* ftop'} {fbot fbot' fbot'' : C →* D} {phtpy_bot : fbot ~* fbot'} {phtpy_bot' : fbot' ~* fbot''} {fleft : A →* C} {fright : B →* D} {psq_back : psquare ftop fbot fleft fright} {psq_front : psquare ftop' fbot' fleft fright} {psq_front' : psquare ftop' fbot'' fleft fright} (ptb : ptube_v phtpy_top phtpy_bot psq_back psq_front) (ptb' : ptube_v phomotopy.rfl phtpy_bot' psq_front psq_front') : ptube_v phtpy_top (phtpy_bot ⬝* phtpy_bot') psq_back psq_front' := begin unfold ptube_v, - unfold phsquare + unfold phsquare, + repeat exact sorry end definition ptube_v_left_inv {A B C D : Type*} {ftop : A ≃* B} {fbot : C ≃* D} {fleft : A →* C} {fright : B →* D} diff --git a/pointed_pi.hlean b/pointed_pi.hlean index 49943d7..cb352b7 100644 --- a/pointed_pi.hlean +++ b/pointed_pi.hlean @@ -168,6 +168,29 @@ namespace pointed ppi_homotopy_of_eq (eq_of_ppi_homotopy h) = h := to_right_inv (ppi_eq_equiv k l) h + print pointed.phomotopy_rec_on_idp + print ppi_gen + + variable (k) + + definition eq_ppi_homotopy_refl_ppi_homotopy_of_eq_refl : ppi_homotopy.refl k = ppi_homotopy_of_eq (refl k) := + begin + induction k with k p, + induction p, reflexivity + end + + definition ppi_homotopy_rec_on_eq [recursor] {k' : ppi_gen B x₀} + {Q : (k ~~* k') → Type} (p : k ~~* k') (H : Π(q : k = k'), Q (ppi_homotopy_of_eq q)) : Q p := + ppi_homotopy_of_eq_of_ppi_homotopy p ▸ H (eq_of_ppi_homotopy p) + + definition ppi_homotopy_rec_on_idp [recursor] + {Q : Π {k' : ppi_gen B x₀}, (k ~~* k') → Type} + (q : Q (ppi_homotopy.refl k)) {k' : ppi_gen B x₀} (H : k ~~* k') : Q H := + begin + induction H using ppi_homotopy_rec_on_eq with t, + induction t, exact eq_ppi_homotopy_refl_ppi_homotopy_of_eq_refl k ▸ q, + end + definition ppi_loop_equiv_lemma (p : k ~ k) : (p pt ⬝ ppi_gen.resp_pt k = ppi_gen.resp_pt k) ≃ (p pt = idp) := calc (p pt ⬝ ppi_gen.resp_pt k = ppi_gen.resp_pt k)