diff --git a/hott/init/funext.hlean b/hott/init/funext.hlean index 64e7b0d35..4b5671d30 100644 --- a/hott/init/funext.hlean +++ b/hott/init/funext.hlean @@ -285,6 +285,25 @@ namespace eq induction p using homotopy.rec_on, induction q, exact H end + definition homotopy.rec_idp [recursor] {A : Type} {P : A → Type} {f : Πa, P a} + (Q : Π{g}, (f ~ g) → Type) (H : Q (homotopy.refl f)) {g : Π x, P x} (p : f ~ g) : Q p := + homotopy.rec_on_idp p H + + definition homotopy_rec_on_apd10 {A : Type} {P : A → Type} {f g : Πa, P a} + (Q : f ~ g → Type) (H : Π(q : f = g), Q (apd10 q)) (p : f = g) : + homotopy.rec_on (apd10 p) H = H p := + begin + unfold [homotopy.rec_on], + refine ap (λp, p ▸ _) !adj ⬝ _, + refine !tr_compose⁻¹ ⬝ _, + apply apdt + end + + definition homotopy_rec_idp_refl {A : Type} {P : A → Type} {f : Πa, P a} + (Q : Π{g}, f ~ g → Type) (H : Q homotopy.rfl) : + homotopy.rec_idp @Q H homotopy.rfl = H := + !homotopy_rec_on_apd10 + definition eq_of_homotopy_inv {f g : Π x, P x} (H : f ~ g) : eq_of_homotopy (λx, (H x)⁻¹) = (eq_of_homotopy H)⁻¹ := begin diff --git a/hott/init/pathover.hlean b/hott/init/pathover.hlean index 96f318dcb..382152f03 100644 --- a/hott/init/pathover.hlean +++ b/hott/init/pathover.hlean @@ -82,6 +82,9 @@ namespace eq definition change_path [unfold 9] (q : p = p') (r : b =[p] b₂) : b =[p'] b₂ := q ▸ r + definition change_path_idp [unfold_full] (r : b =[p] b₂) : change_path idp r = r := + by reflexivity + -- infix ` ⬝ ` := concato infix ` ⬝o `:72 := concato infix ` ⬝op `:73 := concato_eq @@ -103,25 +106,25 @@ namespace eq /- Some of the theorems analogous to theorems for = in init.path -/ - definition cono_idpo (r : b =[p] b₂) : r ⬝o idpo =[con_idp p] r := - pathover.rec_on r idpo + definition cono_idpo (r : b =[p] b₂) : r ⬝o idpo = r := + by reflexivity definition idpo_cono (r : b =[p] b₂) : idpo ⬝o r =[idp_con p] r := - pathover.rec_on r idpo + by induction r; constructor definition cono.assoc' (r : b =[p] b₂) (r₂ : b₂ =[p₂] b₃) (r₃ : b₃ =[p₃] b₄) : r ⬝o (r₂ ⬝o r₃) =[!con.assoc'] (r ⬝o r₂) ⬝o r₃ := - pathover.rec_on r₃ (pathover.rec_on r₂ (pathover.rec_on r idpo)) + by induction r₃; constructor definition cono.assoc (r : b =[p] b₂) (r₂ : b₂ =[p₂] b₃) (r₃ : b₃ =[p₃] b₄) : (r ⬝o r₂) ⬝o r₃ =[!con.assoc] r ⬝o (r₂ ⬝o r₃) := - pathover.rec_on r₃ (pathover.rec_on r₂ (pathover.rec_on r idpo)) + by induction r₃; constructor definition cono.right_inv (r : b =[p] b₂) : r ⬝o r⁻¹ᵒ =[!con.right_inv] idpo := - pathover.rec_on r idpo + by induction r; constructor definition cono.left_inv (r : b =[p] b₂) : r⁻¹ᵒ ⬝o r =[!con.left_inv] idpo := - pathover.rec_on r idpo + by induction r; constructor definition eq_of_pathover {a' a₂' : A'} (q : a' =[p] a₂') : a' = a₂' := by cases q;reflexivity @@ -159,6 +162,11 @@ namespace eq eq_of_pathover_idp (pathover_of_eq (idpath x) p) = p := by induction p; reflexivity + variable (B) + definition idpo_concato_eq (r : b = b') : eq_of_pathover_idp (@idpo A B a b ⬝op r) = r := + by induction r; reflexivity + variable {B} + -- definition pathover_idp (b : B a) (b' : B a) : b =[idpath a] b' ≃ b = b' := -- pathover_equiv_tr_eq idp b b' @@ -245,6 +253,9 @@ namespace eq definition apd [unfold 6] (f : Πa, B a) (p : a = a₂) : f a =[p] f a₂ := by induction p; constructor + definition apd_idp [unfold_full] (f : Πa, B a) : apd f idp = @idpo A B a (f a) := + by reflexivity + definition apo [unfold 12] {f : A → A'} (g : Πa, B a → B'' (f a)) (q : b =[p] b₂) : g a b =[p] g a₂ b₂ := by induction q; constructor @@ -388,19 +399,19 @@ namespace eq definition cono.right_inv_eq (q : b = b') : pathover_idp_of_eq q ⬝op q⁻¹ = (idpo : b =[refl a] b) := - by induction q;constructor + by induction q; constructor definition cono.right_inv_eq' (q : b = b') : q ⬝po (pathover_idp_of_eq q⁻¹) = (idpo : b =[refl a] b) := - by induction q;constructor + by induction q; constructor definition cono.left_inv_eq (q : b = b') : pathover_idp_of_eq q⁻¹ ⬝op q = (idpo : b' =[refl a] b') := - by induction q;constructor + by induction q; constructor definition cono.left_inv_eq' (q : b = b') : q⁻¹ ⬝po pathover_idp_of_eq q = (idpo : b' =[refl a] b') := - by induction q;constructor + by induction q; constructor definition pathover_of_fn_pathover_fn (f : Π{a}, B a ≃ B' a) (r : f b =[p] f b₂) : b =[p] b₂ := (left_inv f b)⁻¹ ⬝po apo (λa, f⁻¹ᵉ) r ⬝op left_inv f b₂ diff --git a/hott/init/pointed.hlean b/hott/init/pointed.hlean index 13b86e208..e7fad229c 100644 --- a/hott/init/pointed.hlean +++ b/hott/init/pointed.hlean @@ -88,31 +88,26 @@ structure ppi {A : Type*} (P : A → Type) (x₀ : P pt) := (to_fun : Π a : A, P a) (resp_pt : to_fun (Point A) = x₀) -definition ppi_const [constructor] {A : Type*} (P : A → Type*) : ppi P pt := -ppi.mk (λa, pt) idp - definition pppi' [reducible] {A : Type*} (P : A → Type*) : Type := ppi P pt +definition ppi_const [constructor] {A : Type*} (P : A → Type*) : pppi' P := +ppi.mk (λa, pt) idp + definition pppi [constructor] [reducible] {A : Type*} (P : A → Type*) : Type* := pointed.MK (pppi' P) (ppi_const P) +-- do we want to make this already pointed? +definition pmap [reducible] (A B : Type*) : Type := @pppi A (λa, B) + +attribute ppi.to_fun [coercion] + +infix ` →* `:28 := pmap notation `Π*` binders `, ` r:(scoped P, pppi P) := r --- We could try to define pmap as a special case of ppi --- definition pmap' (A B : Type*) : Type := @pppi' A (λa, B) --- todo: make this already pointed? -definition pmap [reducible] (A B : Type*) : Type := @pppi A (λa, B) --- structure pmap (A B : Type*) := --- (to_fun : A → B) --- (resp_pt : to_fun (Point A) = Point B) namespace pointed - attribute ppi.to_fun [coercion] - - notation `map₊` := pmap - infix ` →* `:28 := pmap definition pppi.mk [constructor] [reducible] {A : Type*} {P : A → Type*} (f : Πa, P a) (p : f pt = pt) : pppi P := @@ -126,7 +121,7 @@ namespace pointed (p : f (Point A) = Point B) : A →* B := pppi.mk f p - definition pmap.to_fun [unfold 3] [reducible] {A B : Type*} (f : A →* B) : A → B := + abbreviation pmap.to_fun [unfold 3] [reducible] [coercion] {A B : Type*} (f : A →* B) : A → B := pppi.to_fun f definition respect_pt [unfold 4] [reducible] {A : Type*} {P : A → Type} {p₀ : P pt} diff --git a/hott/types/pointed.hlean b/hott/types/pointed.hlean index bfe2ce8b4..08ad9c7c3 100644 --- a/hott/types/pointed.hlean +++ b/hott/types/pointed.hlean @@ -116,10 +116,10 @@ namespace pointed /- categorical properties of pointed maps -/ - definition pid [constructor] (A : Type*) : A →* A := + definition pid [constructor] [refl] (A : Type*) : A →* A := pmap.mk id idp - definition pcompose [constructor] {A B C : Type*} (g : B →* C) (f : A →* B) : A →* C := + definition pcompose [constructor] [trans] {A B C : Type*} (g : B →* C) (f : A →* B) : A →* C := pmap.mk (λa, g (f a)) (ap g (respect_pt f) ⬝ respect_pt g) infixr ` ∘* `:60 := pcompose @@ -323,7 +323,7 @@ namespace pointed protected definition phomotopy.refl [constructor] : k ~* k := phomotopy.mk homotopy.rfl !idp_con variable {k} - protected definition phomotopy.rfl [constructor] [refl] : k ~* k := + protected definition phomotopy.rfl [reducible] [constructor] [refl] : k ~* k := phomotopy.refl k protected definition phomotopy.symm [constructor] [symm] (p : k ~* l) : l ~* k := @@ -447,8 +447,7 @@ namespace pointed definition eq_of_phomotopy (p : k ~* l) : k = l := to_inv (ppi_eq_equiv k l) p - definition eq_of_phomotopy_refl {X Y : Type*} (f : X →* Y) : - eq_of_phomotopy (phomotopy.refl f) = idpath f := + definition eq_of_phomotopy_refl (k : ppi P p₀) : eq_of_phomotopy (phomotopy.refl k) = idpath k := begin apply to_inv_eq_of_eq, reflexivity end @@ -480,11 +479,17 @@ namespace pointed induction t, exact phomotopy_of_eq_idp k ▸ q, end + definition phomotopy_rec_idp' (Q : Π ⦃k' : ppi P p₀⦄, (k ~* k') → (k = k') → Type) + (q : Q phomotopy.rfl idp) ⦃k' : ppi P p₀⦄ (H : k ~* k') : Q H (eq_of_phomotopy H) := + begin + induction H using phomotopy_rec_idp, + exact transport (Q phomotopy.rfl) !eq_of_phomotopy_refl⁻¹ q + end + attribute phomotopy.rec' [recursor] - definition phomotopy_rec_eq_phomotopy_of_eq {A B : Type*} {f g: A →* B} - {Q : (f ~* g) → Type} (p : f = g) (H : Π(q : f = g), Q (phomotopy_of_eq q)) : - phomotopy_rec_eq (phomotopy_of_eq p) H = H p := + definition phomotopy_rec_eq_phomotopy_of_eq {Q : (k ~* l) → Type} (p : k = l) + (H : Π(q : k = l), Q (phomotopy_of_eq q)) : phomotopy_rec_eq (phomotopy_of_eq p) H = H p := begin unfold phomotopy_rec_eq, refine ap (λp, p ▸ _) !adj ⬝ _, @@ -492,11 +497,33 @@ namespace pointed apply apdt end - definition phomotopy_rec_idp_refl {A B : Type*} (f : A →* B) - {Q : Π{g}, (f ~* g) → Type} (H : Q (phomotopy.refl f)) : + definition phomotopy_rec_idp_refl {Q : Π{l}, (k ~* l) → Type} (H : Q (phomotopy.refl k)) : phomotopy_rec_idp phomotopy.rfl H = H := !phomotopy_rec_eq_phomotopy_of_eq + definition phomotopy_rec_idp'_refl (Q : Π ⦃k' : ppi P p₀⦄, (k ~* k') → (k = k') → Type) + (q : Q phomotopy.rfl idp) : + phomotopy_rec_idp' Q q phomotopy.rfl = transport (Q phomotopy.rfl) !eq_of_phomotopy_refl⁻¹ q := + !phomotopy_rec_idp_refl + + /- maps out of or into contractible types -/ + definition phomotopy_of_is_contr_cod [constructor] (k l : ppi P p₀) [Πa, is_contr (P a)] : + k ~* l := + phomotopy.mk (λa, !eq_of_is_contr) !eq_of_is_contr + + definition phomotopy_of_is_contr_cod_pmap [constructor] (f g : A →* B) [is_contr B] : f ~* g := + phomotopy_of_is_contr_cod f g + + definition phomotopy_of_is_contr_dom [constructor] (k l : ppi P p₀) [is_contr A] : k ~* l := + begin + fapply phomotopy.mk, + { intro a, exact eq_of_pathover_idp (change_path !is_prop.elim + (apd k !is_prop.elim ⬝op respect_pt k ⬝ (respect_pt l)⁻¹ ⬝o apd l !is_prop.elim)) }, + rewrite [▸*, +is_prop_elim_self, +apd_idp, cono_idpo], + refine ap (λx, eq_of_pathover_idp (change_path x _)) !is_prop_elim_self ◾ idp ⬝ _, + xrewrite [change_path_idp, idpo_concato_eq, inv_con_cancel_right], + end + /- adjunction between (-)₊ : Type → Type* and pType.carrier : Type* → Type -/ definition pmap_equiv_left (A : Type) (B : Type*) : A₊ →* B ≃ (A → B) := begin diff --git a/hott/types/pointed2.hlean b/hott/types/pointed2.hlean index ff62d2644..8e2d145d5 100644 --- a/hott/types/pointed2.hlean +++ b/hott/types/pointed2.hlean @@ -18,7 +18,7 @@ import algebra.homotopy_group eq2 open pointed eq unit is_trunc trunc nat group is_equiv equiv sigma function bool namespace pointed - variables {A B C : Type*} + variables {A B C : Type*} {P : A → Type} {p₀ : P pt} {k k' l m n : ppi P p₀} section psquare /- @@ -134,14 +134,35 @@ namespace pointed definition punit_pmap_phomotopy [constructor] {A : Type*} (f : punit →* A) : f ~* pconst punit A := + !phomotopy_of_is_contr_dom + + definition punit_ppi [constructor] (P : punit → Type*) (p₀ : P ⋆) : ppi P p₀ := begin - fapply phomotopy.mk, - { intro u, induction u, exact respect_pt f }, - { reflexivity } + fapply ppi.mk, intro u, induction u, exact p₀, + reflexivity end + definition punit_ppi_phomotopy [constructor] {P : punit → Type*} {p₀ : P ⋆} (f : ppi P p₀) : + f ~* punit_ppi P p₀ := + !phomotopy_of_is_contr_dom + + definition is_contr_punit_ppi (P : punit → Type*) (p₀ : P ⋆) : is_contr (ppi P p₀) := + is_contr.mk (punit_ppi P p₀) (λf, eq_of_phomotopy (punit_ppi_phomotopy f)⁻¹*) + definition is_contr_punit_pmap (A : Type*) : is_contr (punit →* A) := - is_contr.mk (pconst punit A) (λf, eq_of_phomotopy (punit_pmap_phomotopy f)⁻¹*) + !is_contr_punit_ppi + + -- definition phomotopy_eq_equiv (h₁ h₂ : k ~* l) : + -- (h₁ = h₂) ≃ Σ(p : to_homotopy h₁ ~ to_homotopy h₂), + -- whisker_right (respect_pt l) (p pt) ⬝ to_homotopy_pt h₂ = to_homotopy_pt h₁ := + -- begin + -- refine !ppi_eq_equiv ⬝e !phomotopy.sigma_char ⬝e sigma_equiv_sigma_right _, + -- intro p, + -- end + + /- Short term TODO: generalize to dependent maps (use ppi_eq_equiv?) + Long term TODO: use homotopies between pointed homotopies, not equalities + -/ definition phomotopy_eq_equiv {A B : Type*} {f g : A →* B} (h k : f ~* g) : (h = k) ≃ Σ(p : to_homotopy h ~ to_homotopy k), @@ -173,12 +194,11 @@ namespace pointed (q : square (to_homotopy_pt h) (to_homotopy_pt k) (whisker_right (respect_pt g) (p pt)) idp) : h = k := phomotopy_eq p (eq_of_square q)⁻¹ - definition trans_refl {A B : Type*} {f g : A →* B} (p : f ~* g) : p ⬝* phomotopy.refl g = p := + definition trans_refl (p : k ~* l) : p ⬝* phomotopy.rfl = p := begin - induction A with A a₀, induction B with B b₀, - induction f with f f₀, induction g with g g₀, induction p with p p₀, - esimp at *, induction g₀, induction p₀, - reflexivity + induction A with A a₀, + induction k with k k₀, induction l with l l₀, induction p with p p₀', esimp at * ⊢, + induction l₀, induction p₀', reflexivity, end definition eq_of_phomotopy_trans {X Y : Type*} {f g h : X →* Y} (p : f ~* g) (q : g ~* h) : @@ -188,77 +208,66 @@ namespace pointed exact ap eq_of_phomotopy !trans_refl ⬝ whisker_left _ !eq_of_phomotopy_refl⁻¹ end - definition refl_trans {A B : Type*} {f g : A →* B} (p : f ~* g) : phomotopy.refl f ⬝* p = p := + definition refl_trans (p : k ~* l) : phomotopy.rfl ⬝* p = p := begin induction p using phomotopy_rec_idp, - induction A with A a₀, induction B with B b₀, - induction f with f f₀, esimp at *, induction f₀, - reflexivity + apply trans_refl end - definition trans_assoc {A B : Type*} {f g h i : A →* B} (p : f ~* g) (q : g ~* h) - (r : h ~* i) : p ⬝* q ⬝* r = p ⬝* (q ⬝* r) := + definition trans_assoc (p : k ~* l) (q : l ~* m) (r : m ~* n) : p ⬝* q ⬝* r = p ⬝* (q ⬝* r) := begin induction r using phomotopy_rec_idp, induction q using phomotopy_rec_idp, induction p using phomotopy_rec_idp, - induction B with B b₀, - induction f with f f₀, esimp at *, induction f₀, + induction k with k k₀, induction k₀, reflexivity end - definition refl_symm {A B : Type*} (f : A →* B) : phomotopy.rfl⁻¹* = phomotopy.refl f := + definition refl_symm : phomotopy.rfl⁻¹* = phomotopy.refl k := begin - induction B with B b₀, - induction f with f f₀, esimp at *, induction f₀, + induction k with k k₀, induction k₀, reflexivity end - definition symm_symm {A B : Type*} {f g : A →* B} (p : f ~* g) : p⁻¹*⁻¹* = p := - phomotopy_eq (λa, !inv_inv) - begin - induction p using phomotopy_rec_idp, induction f with f f₀, induction B with B b₀, - esimp at *, induction f₀, reflexivity - end + definition symm_symm (p : k ~* l) : p⁻¹*⁻¹* = p := + begin + induction p using phomotopy_rec_idp, induction k with k k₀, induction k₀, reflexivity + end - definition trans_right_inv {A B : Type*} {f g : A →* B} (p : f ~* g) : p ⬝* p⁻¹* = phomotopy.rfl := + definition trans_right_inv (p : k ~* l) : p ⬝* p⁻¹* = phomotopy.rfl := begin induction p using phomotopy_rec_idp, exact !refl_trans ⬝ !refl_symm end - definition trans_left_inv {A B : Type*} {f g : A →* B} (p : f ~* g) : p⁻¹* ⬝* p = phomotopy.rfl := + definition trans_left_inv (p : k ~* l) : p⁻¹* ⬝* p = phomotopy.rfl := begin induction p using phomotopy_rec_idp, exact !trans_refl ⬝ !refl_symm end - definition trans2 {A B : Type*} {f g h : A →* B} {p p' : f ~* g} {q q' : g ~* h} - (r : p = p') (s : q = q') : p ⬝* q = p' ⬝* q' := + definition trans2 {p p' : k ~* l} {q q' : l ~* m} (r : p = p') (s : q = q') : p ⬝* q = p' ⬝* q' := ap011 phomotopy.trans r s definition pcompose3 {A B C : Type*} {g g' : B →* C} {f f' : A →* B} {p p' : g ~* g'} {q q' : f ~* f'} (r : p = p') (s : q = q') : p ◾* q = p' ◾* q' := ap011 pcompose2 r s - definition symm2 {A B : Type*} {f g : A →* B} {p p' : f ~* g} (r : p = p') : p⁻¹* = p'⁻¹* := + definition symm2 {p p' : k ~* l} (r : p = p') : p⁻¹* = p'⁻¹* := ap phomotopy.symm r infixl ` ◾** `:80 := pointed.trans2 infixl ` ◽* `:81 := pointed.pcompose3 postfix `⁻²**`:(max+1) := pointed.symm2 - definition trans_symm {A B : Type*} {f g h : A →* B} (p : f ~* g) (q : g ~* h) : - (p ⬝* q)⁻¹* = q⁻¹* ⬝* p⁻¹* := + definition trans_symm (p : k ~* l) (q : l ~* m) : (p ⬝* q)⁻¹* = q⁻¹* ⬝* p⁻¹* := begin induction p using phomotopy_rec_idp, induction q using phomotopy_rec_idp, exact !trans_refl⁻²** ⬝ !trans_refl⁻¹ ⬝ idp ◾** !refl_symm⁻¹ end - definition phwhisker_left {A B : Type*} {f g h : A →* B} (p : f ~* g) {q q' : g ~* h} - (s : q = q') : p ⬝* q = p ⬝* q' := + definition phwhisker_left (p : k ~* l) {q q' : l ~* m} (s : q = q') : p ⬝* q = p ⬝* q' := idp ◾** s - definition phwhisker_right {A B : Type*} {f g h : A →* B} {p p' : f ~* g} (q : g ~* h) - (r : p = p') : p ⬝* q = p' ⬝* q := + definition phwhisker_right {p p' : k ~* l} (q : l ~* m) (r : p = p') : p ⬝* q = p' ⬝* q := r ◾** idp definition pwhisker_left_refl {A B C : Type*} (g : B →* C) (f : A →* B) : @@ -325,36 +334,36 @@ namespace pointed refine ap (pwhisker_right f) !refl_symm ⬝ !pwhisker_right_refl ⬝ !refl_symm⁻¹ end - definition trans_eq_of_eq_symm_trans {A B : Type*} {f g h : A →* B} {p : f ~* g} {q : g ~* h} - {r : f ~* h} (s : q = p⁻¹* ⬝* r) : p ⬝* q = r := + definition trans_eq_of_eq_symm_trans {p : k ~* l} {q : l ~* m} {r : k ~* m} (s : q = p⁻¹* ⬝* r) : + p ⬝* q = r := idp ◾** s ⬝ !trans_assoc⁻¹ ⬝ trans_right_inv p ◾** idp ⬝ !refl_trans - definition eq_symm_trans_of_trans_eq {A B : Type*} {f g h : A →* B} {p : f ~* g} {q : g ~* h} - {r : f ~* h} (s : p ⬝* q = r) : q = p⁻¹* ⬝* r := + definition eq_symm_trans_of_trans_eq {p : k ~* l} {q : l ~* m} {r : k ~* m} (s : p ⬝* q = r) : + q = p⁻¹* ⬝* r := !refl_trans⁻¹ ⬝ !trans_left_inv⁻¹ ◾** idp ⬝ !trans_assoc ⬝ idp ◾** s - definition trans_eq_of_eq_trans_symm {A B : Type*} {f g h : A →* B} {p : f ~* g} {q : g ~* h} - {r : f ~* h} (s : p = r ⬝* q⁻¹*) : p ⬝* q = r := + definition trans_eq_of_eq_trans_symm {p : k ~* l} {q : l ~* m} {r : k ~* m} (s : p = r ⬝* q⁻¹*) : + p ⬝* q = r := s ◾** idp ⬝ !trans_assoc ⬝ idp ◾** trans_left_inv q ⬝ !trans_refl - definition eq_trans_symm_of_trans_eq {A B : Type*} {f g h : A →* B} {p : f ~* g} {q : g ~* h} - {r : f ~* h} (s : p ⬝* q = r) : p = r ⬝* q⁻¹* := + definition eq_trans_symm_of_trans_eq {p : k ~* l} {q : l ~* m} {r : k ~* m} (s : p ⬝* q = r) : + p = r ⬝* q⁻¹* := !trans_refl⁻¹ ⬝ idp ◾** !trans_right_inv⁻¹ ⬝ !trans_assoc⁻¹ ⬝ s ◾** idp - definition eq_trans_of_symm_trans_eq {A B : Type*} {f g h : A →* B} {p : f ~* g} {q : g ~* h} - {r : f ~* h} (s : p⁻¹* ⬝* r = q) : r = p ⬝* q := + definition eq_trans_of_symm_trans_eq {p : k ~* l} {q : l ~* m} {r : k ~* m} (s : p⁻¹* ⬝* r = q) : + r = p ⬝* q := !refl_trans⁻¹ ⬝ !trans_right_inv⁻¹ ◾** idp ⬝ !trans_assoc ⬝ idp ◾** s - definition symm_trans_eq_of_eq_trans {A B : Type*} {f g h : A →* B} {p : f ~* g} {q : g ~* h} - {r : f ~* h} (s : r = p ⬝* q) : p⁻¹* ⬝* r = q := + definition symm_trans_eq_of_eq_trans {p : k ~* l} {q : l ~* m} {r : k ~* m} (s : r = p ⬝* q) : + p⁻¹* ⬝* r = q := idp ◾** s ⬝ !trans_assoc⁻¹ ⬝ trans_left_inv p ◾** idp ⬝ !refl_trans - definition eq_trans_of_trans_symm_eq {A B : Type*} {f g h : A →* B} {p : f ~* g} {q : g ~* h} - {r : f ~* h} (s : r ⬝* q⁻¹* = p) : r = p ⬝* q := + definition eq_trans_of_trans_symm_eq {p : k ~* l} {q : l ~* m} {r : k ~* m} (s : r ⬝* q⁻¹* = p) : + r = p ⬝* q := !trans_refl⁻¹ ⬝ idp ◾** !trans_left_inv⁻¹ ⬝ !trans_assoc⁻¹ ⬝ s ◾** idp - definition trans_symm_eq_of_eq_trans {A B : Type*} {f g h : A →* B} {p : f ~* g} {q : g ~* h} - {r : f ~* h} (s : r = p ⬝* q) : r ⬝* q⁻¹* = p := + definition trans_symm_eq_of_eq_trans {p : k ~* l} {q : l ~* m} {r : k ~* m} (s : r = p ⬝* q) : + r ⬝* q⁻¹* = p := s ◾** idp ⬝ !trans_assoc ⬝ idp ◾** trans_right_inv q ⬝ !trans_refl section phsquare @@ -362,7 +371,7 @@ namespace pointed Squares of pointed homotopies -/ - variables {f f' f₀₀ f₂₀ f₄₀ f₀₂ f₂₂ f₄₂ f₀₄ f₂₄ f₄₄ : A →* B} + variables {f f' f₀₀ f₂₀ f₄₀ f₀₂ f₂₂ f₄₂ f₀₄ f₂₄ f₄₄ : ppi P p₀} {p₁₀ : f₀₀ ~* f₂₀} {p₃₀ : f₂₀ ~* f₄₀} {p₀₁ : f₀₀ ~* f₀₂} {p₂₁ : f₂₀ ~* f₂₂} {p₄₁ : f₄₀ ~* f₄₂} {p₁₂ : f₀₂ ~* f₂₂} {p₃₂ : f₂₂ ~* f₄₂} @@ -495,6 +504,13 @@ namespace pointed !pwhisker_left_refl⁻¹ ◾** !pwhisker_right_refl⁻¹ end + end phsquare + + section nondep_phsquare + + variables {f f' f₀₀ f₂₀ f₀₂ f₂₂ : A →* B} + {p₁₀ : f₀₀ ~* f₂₀} {p₀₁ : f₀₀ ~* f₀₂} {p₂₁ : f₂₀ ~* f₂₂} {p₁₂ : f₀₂ ~* f₂₂} + definition pwhisker_left_phsquare (f : B →* C) (p : phsquare p₁₀ p₁₂ p₀₁ p₂₁) : phsquare (pwhisker_left f p₁₀) (pwhisker_left f p₁₂) (pwhisker_left f p₀₁) (pwhisker_left f p₂₁) := @@ -505,9 +521,9 @@ namespace pointed (pwhisker_right f p₀₁) (pwhisker_right f p₂₁) := !pwhisker_right_trans⁻¹ ⬝ ap (pwhisker_right f) p ⬝ !pwhisker_right_trans - end phsquare + end nondep_phsquare - definition phomotopy_of_eq_con {A B : Type*} {f g h : A →* B} (p : f = g) (q : g = h) : + definition phomotopy_of_eq_con (p : k = l) (q : l = m) : phomotopy_of_eq (p ⬝ q) = phomotopy_of_eq p ⬝* phomotopy_of_eq q := begin induction q, induction p, exact !trans_refl⁻¹ end diff --git a/hott/types/unit.hlean b/hott/types/unit.hlean index 38d8a9ed5..1ab63bc8e 100644 --- a/hott/types/unit.hlean +++ b/hott/types/unit.hlean @@ -32,6 +32,9 @@ namespace unit notation `unit*` := punit + definition is_contr_punit [instance] : is_contr punit := + is_contr_unit + definition unit_arrow_eq {X : Type} (f : unit → X) : (λx, f ⋆) = f := by apply eq_of_homotopy; intro u; induction u; reflexivity