From 816237315c12d1aa4cb5c8ab1942e60616f5f6db Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Mon, 15 Feb 2016 14:40:25 -0500 Subject: [PATCH] feat(hott): various additions, especially for pointed maps/homotopies/equivalences --- hott/algebra/homotopy_group.hlean | 2 +- hott/hit/pointed_pushout.hlean | 17 +- hott/homotopy/cofiber.hlean | 16 +- hott/homotopy/sphere.hlean | 2 +- hott/homotopy/wedge.hlean | 16 +- hott/init/default.hlean | 2 +- hott/init/equiv.hlean | 48 ++++-- hott/init/trunc.hlean | 30 +++- hott/types/fiber.hlean | 14 +- hott/types/fin.hlean | 32 ++-- hott/types/pointed.hlean | 274 +++++++++++++++++------------- hott/types/pointed2.hlean | 104 ++++++++++++ hott/types/sigma.hlean | 9 + hott/types/trunc.hlean | 15 +- hott/types/types.md | 5 +- src/emacs/lean-syntax.el | 4 +- 16 files changed, 395 insertions(+), 195 deletions(-) create mode 100644 hott/types/pointed2.hlean diff --git a/hott/algebra/homotopy_group.hlean b/hott/algebra/homotopy_group.hlean index c66587949..ce2db14c8 100644 --- a/hott/algebra/homotopy_group.hlean +++ b/hott/algebra/homotopy_group.hlean @@ -32,7 +32,7 @@ namespace eq local attribute comm_group_homotopy_group [instance] definition Pointed_homotopy_group [constructor] (n : ℕ) (A : Type*) : Type* := - Pointed.mk (π[n] A) + pointed.Mk (π[n] A) definition Group_homotopy_group [constructor] (n : ℕ) (A : Type*) : Group := Group.mk (π[succ n] A) _ diff --git a/hott/hit/pointed_pushout.hlean b/hott/hit/pointed_pushout.hlean index 34a3ccda5..3f8bf339e 100644 --- a/hott/hit/pointed_pushout.hlean +++ b/hott/hit/pointed_pushout.hlean @@ -1,16 +1,16 @@ /- Copyright (c) 2016 Jakob von Raumer. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Jakob von Raumer +Authors: Jakob von Raumer, Floris van Doorn Pointed Pushouts -/ -import .pushout types.pointed +import .pushout types.pointed2 open eq pushout namespace pointed - + definition pointed_pushout [instance] [constructor] {TL BL TR : Type} [HTL : pointed TL] [HBL : pointed BL] [HTR : pointed TR] (f : TL → BL) (g : TL → TR) : pointed (pushout f g) := pointed.mk (inl (point _)) @@ -25,7 +25,7 @@ namespace pushout definition Pushout [constructor] : Type* := pointed.mk' (pushout f g) - + parameters {f g} definition pinl [constructor] : BL →* Pushout := pmap.mk inl idp @@ -44,12 +44,11 @@ namespace pushout section variables {TL BL TR : Type*} (f : TL →* BL) (g : TL →* TR) - protected definition psymm : Pushout f g ≃* Pushout g f := + protected definition psymm [constructor] : Pushout f g ≃* Pushout g f := begin - fapply pequiv.mk, - { fapply pmap.mk, exact !pushout.transpose, - exact ap inr (respect_pt f)⁻¹ ⬝ !glue⁻¹ ⬝ ap inl (respect_pt g) }, - { esimp, apply equiv.to_is_equiv !pushout.symm }, + fapply pequiv_of_equiv, + { apply pushout.symm}, + { exact ap inr (respect_pt f)⁻¹ ⬝ !glue⁻¹ ⬝ ap inl (respect_pt g)} end end diff --git a/hott/homotopy/cofiber.hlean b/hott/homotopy/cofiber.hlean index a005644ae..fa0314789 100644 --- a/hott/homotopy/cofiber.hlean +++ b/hott/homotopy/cofiber.hlean @@ -25,7 +25,7 @@ namespace cofiber intro a, induction a with [u, b], { cases u, reflexivity }, { exact !glue ⬝ ap inr (right_inv f b) }, - { apply eq_pathover, refine _ ⬝hp !ap_id⁻¹, refine !ap_constant ⬝ph _, + { apply eq_pathover, refine _ ⬝hp !ap_id⁻¹, refine !ap_constant ⬝ph _, apply move_bot_of_left, refine !idp_con ⬝ph _, apply transpose, esimp, refine _ ⬝hp (ap (ap inr) !adj⁻¹), refine _ ⬝hp !ap_compose, apply square_Flr_idp_ap }, end @@ -69,7 +69,7 @@ namespace cofiber induction y, induction x, exact Pinl, exact Pinr x, esimp, exact Pglue x end - protected definition pelim_on {A B C : Type*} {f : A →* B} (y : Cofiber f) + protected definition pelim_on {A B C : Type*} {f : A →* B} (y : Cofiber f) (c : C) (g : B → C) (p : Π x, c = g (f x)) : C := begin fapply pushout.elim_on y, exact (λ x, c), exact g, exact p @@ -81,18 +81,18 @@ namespace cofiber definition cofiber_unit : Cofiber (pconst A Unit) ≃* Susp A := begin - fconstructor, + fapply pequiv_of_pmap, { fconstructor, intro x, induction x, exact north, exact south, exact merid x, reflexivity }, { esimp, fapply adjointify, intro s, induction s, exact inl ⋆, exact inr ⋆, apply glue a, intro s, induction s, do 2 reflexivity, esimp, - apply eq_pathover, refine _ ⬝hp !ap_id⁻¹, apply hdeg_square, - refine !(ap_compose (pushout.elim _ _ _)) ⬝ _, + apply eq_pathover, refine _ ⬝hp !ap_id⁻¹, apply hdeg_square, + refine !(ap_compose (pushout.elim _ _ _)) ⬝ _, refine ap _ !elim_merid ⬝ _, apply elim_glue, - intro c, induction c with [n, s], induction n, reflexivity, - induction s, reflexivity, esimp, apply eq_pathover, apply hdeg_square, - refine _ ⬝ !ap_id⁻¹, refine !(ap_compose (pushout.elim _ _ _)) ⬝ _, + intro c, induction c with [n, s], induction n, reflexivity, + induction s, reflexivity, esimp, apply eq_pathover, apply hdeg_square, + refine _ ⬝ !ap_id⁻¹, refine !(ap_compose (pushout.elim _ _ _)) ⬝ _, refine ap _ !elim_glue ⬝ _, apply elim_merid }, end diff --git a/hott/homotopy/sphere.hlean b/hott/homotopy/sphere.hlean index b7dd1f3fe..0c612909e 100644 --- a/hott/homotopy/sphere.hlean +++ b/hott/homotopy/sphere.hlean @@ -191,7 +191,7 @@ namespace is_trunc note H'' := @is_trunc_equiv_closed_rev _ _ _ !pmap_sphere H', assert p : (f = pmap.mk (λx, f base) (respect_pt f)), apply is_hprop.elim, - exact ap10 (ap pmap.map p) x + exact ap10 (ap pmap.to_fun p) x end definition pmap_sphere_constant_of_is_trunc [H : is_trunc (n.-2.+1) A] diff --git a/hott/homotopy/wedge.hlean b/hott/homotopy/wedge.hlean index 103d9596f..6b17d6af2 100644 --- a/hott/homotopy/wedge.hlean +++ b/hott/homotopy/wedge.hlean @@ -16,17 +16,17 @@ namespace wedge -- TODO maybe find a cleaner proof protected definition unit (A : Type*) : A ≃* Wedge Unit A := begin - fconstructor, + fapply pequiv_of_pmap, { fapply pmap.mk, intro a, apply pinr a, apply respect_pt }, - { fapply is_equiv.adjointify, intro x, fapply pushout.elim_on x, - exact λ x, Point A, exact id, intro u, reflexivity, - intro x, fapply pushout.rec_on x, intro u, cases u, esimp, apply (glue unit.star)⁻¹, + { fapply is_equiv.adjointify, intro x, fapply pushout.elim_on x, + exact λ x, Point A, exact id, intro u, reflexivity, + intro x, fapply pushout.rec_on x, intro u, cases u, esimp, apply (glue unit.star)⁻¹, intro a, reflexivity, intro u, cases u, esimp, apply eq_pathover, - refine _ ⬝hp !ap_id⁻¹, fapply eq_hconcat, apply ap_compose inr, - krewrite elim_glue, fapply eq_hconcat, apply ap_idp, apply square_of_eq, - apply con.left_inv, - intro a, reflexivity }, + refine _ ⬝hp !ap_id⁻¹, fapply eq_hconcat, apply ap_compose inr, + krewrite elim_glue, fapply eq_hconcat, apply ap_idp, apply square_of_eq, + apply con.left_inv, + intro a, reflexivity}, end end wedge diff --git a/hott/init/default.hlean b/hott/init/default.hlean index f083de41e..4967c126d 100644 --- a/hott/init/default.hlean +++ b/hott/init/default.hlean @@ -23,5 +23,5 @@ namespace core export [declaration] function export equiv (to_inv to_right_inv to_left_inv) export is_equiv (inv right_inv left_inv adjointify) - export [abbreviation] [declaration] is_trunc (trunctype hprop.mk hset.mk) + export [abbreviation] [declaration] is_trunc (hprop.mk hset.mk) end core diff --git a/hott/init/equiv.hlean b/hott/init/equiv.hlean index a96dd40e9..993c24c2d 100644 --- a/hott/init/equiv.hlean +++ b/hott/init/equiv.hlean @@ -223,19 +223,20 @@ namespace is_equiv section variables {A : Type} {B C : A → Type} (f : Π{a}, B a → C a) [H : Πa, is_equiv (@f a)] - {g : A → A} (h : Π{a}, B a → B (g a)) (h' : Π{a}, C a → C (g a)) + {g : A → A} {g' : A → A} (h : Π{a}, B (g' a) → B (g a)) (h' : Π{a}, C (g' a) → C (g a)) + include H - definition inv_commute' (p : Π⦃a : A⦄ (b : B a), f (h b) = h' (f b)) {a : A} (c : C a) : - f⁻¹ (h' c) = h (f⁻¹ c) := + definition inv_commute' (p : Π⦃a : A⦄ (b : B (g' a)), f (h b) = h' (f b)) {a : A} + (c : C (g' a)) : f⁻¹ (h' c) = h (f⁻¹ c) := eq_of_fn_eq_fn' f (right_inv f (h' c) ⬝ ap h' (right_inv f c)⁻¹ ⬝ (p (f⁻¹ c))⁻¹) - definition fun_commute_of_inv_commute' (p : Π⦃a : A⦄ (c : C a), f⁻¹ (h' c) = h (f⁻¹ c)) - {a : A} (b : B a) : f (h b) = h' (f b) := + definition fun_commute_of_inv_commute' (p : Π⦃a : A⦄ (c : C (g' a)), f⁻¹ (h' c) = h (f⁻¹ c)) + {a : A} (b : B (g' a)) : f (h b) = h' (f b) := eq_of_fn_eq_fn' f⁻¹ (left_inv f (h b) ⬝ ap h (left_inv f b)⁻¹ ⬝ (p (f b))⁻¹) - definition ap_inv_commute' (p : Π⦃a : A⦄ (b : B a), f (h b) = h' (f b)) {a : A} (c : C a) : - ap f (inv_commute' @f @h @h' p c) - = right_inv f (h' c) ⬝ ap h' (right_inv f c)⁻¹ ⬝ (p (f⁻¹ c))⁻¹ := + definition ap_inv_commute' (p : Π⦃a : A⦄ (b : B (g' a)), f (h b) = h' (f b)) {a : A} + (c : C (g' a)) : ap f (inv_commute' @f @h @h' p c) + = right_inv f (h' c) ⬝ ap h' (right_inv f c)⁻¹ ⬝ (p (f⁻¹ c))⁻¹ := !ap_eq_of_fn_eq_fn' end @@ -287,7 +288,7 @@ namespace equiv equiv.mk (g ∘ f) !is_equiv_compose infixl ` ⬝e `:75 := equiv.trans - postfix [parsing_only] `⁻¹ᵉ`:(max + 1) := equiv.symm + postfix `⁻¹ᵉ`:(max + 1) := equiv.symm -- notation for inverse which is not overloaded abbreviation erfl [constructor] := @equiv.refl @@ -310,9 +311,12 @@ namespace equiv definition eq_equiv_fn_eq_of_equiv [constructor] (f : A ≃ B) (a b : A) : (a = b) ≃ (f a = f b) := equiv.mk (ap f) !is_equiv_ap - definition equiv_ap [constructor] (P : A → Type) {a b : A} (p : a = b) : (P a) ≃ (P b) := + definition equiv_ap [constructor] (P : A → Type) {a b : A} (p : a = b) : P a ≃ P b := equiv.mk (transport P p) !is_equiv_tr + definition equiv_of_eq [constructor] {A B : Type} (p : A = B) : A ≃ B := + equiv_ap (λX, X) p + definition eq_of_fn_eq_fn (f : A ≃ B) {x y : A} (q : f x = f y) : x = y := (left_inv f x)⁻¹ ⬝ ap f⁻¹ q ⬝ left_inv f y @@ -323,8 +327,10 @@ namespace equiv theorem inv_eq {A B : Type} (eqf eqg : A ≃ B) (p : eqf = eqg) : (to_fun eqf)⁻¹ = (to_fun eqg)⁻¹ := eq.rec_on p idp - definition equiv_of_equiv_of_eq [trans] {A B C : Type} (p : A = B) (q : B ≃ C) : A ≃ C := p⁻¹ ▸ q - definition equiv_of_eq_of_equiv [trans] {A B C : Type} (p : A ≃ B) (q : B = C) : A ≃ C := q ▸ p + definition equiv_of_equiv_of_eq [trans] {A B C : Type} (p : A = B) (q : B ≃ C) : A ≃ C := + equiv_of_eq p ⬝e q + definition equiv_of_eq_of_equiv [trans] {A B C : Type} (p : A ≃ B) (q : B = C) : A ≃ C := + p ⬝e equiv_of_eq q definition equiv_lift [constructor] (A : Type) : A ≃ lift A := equiv.mk up _ @@ -345,22 +351,28 @@ namespace equiv end section - variables {A : Type} {B C : A → Type} (f : Π{a}, B a ≃ C a) - {g : A → A} (h : Π{a}, B a → B (g a)) (h' : Π{a}, C a → C (g a)) - definition inv_commute (p : Π⦃a : A⦄ (b : B a), f (h b) = h' (f b)) {a : A} (c : C a) : - f⁻¹ (h' c) = h (f⁻¹ c) := + variables {A : Type} {B C : A → Type} (f : Π{a}, B a ≃ C a) + {g : A → A} {g' : A → A} (h : Π{a}, B (g' a) → B (g a)) (h' : Π{a}, C (g' a) → C (g a)) + + definition inv_commute (p : Π⦃a : A⦄ (b : B (g' a)), f (h b) = h' (f b)) {a : A} + (c : C (g' a)) : f⁻¹ (h' c) = h (f⁻¹ c) := inv_commute' @f @h @h' p c - definition fun_commute_of_inv_commute (p : Π⦃a : A⦄ (c : C a), f⁻¹ (h' c) = h (f⁻¹ c)) - {a : A} (b : B a) : f (h b) = h' (f b) := + definition fun_commute_of_inv_commute (p : Π⦃a : A⦄ (c : C (g' a)), f⁻¹ (h' c) = h (f⁻¹ c)) + {a : A} (b : B (g' a)) : f (h b) = h' (f b) := fun_commute_of_inv_commute' @f @h @h' p b + end namespace ops postfix ⁻¹ := equiv.symm -- overloaded notation for inverse end ops + + infixl ` ⬝pe `:75 := equiv_of_equiv_of_eq + infixl ` ⬝ep `:75 := equiv_of_eq_of_equiv + end equiv open equiv equiv.ops diff --git a/hott/init/trunc.hlean b/hott/init/trunc.hlean index d78e59538..efa75fe9f 100644 --- a/hott/init/trunc.hlean +++ b/hott/init/trunc.hlean @@ -12,7 +12,7 @@ Ported from Coq HoTT. prelude import .nat .logic .equiv .pathover -open eq nat sigma unit +open eq nat sigma unit sigma.ops --set_option class.force_new true namespace is_trunc @@ -99,9 +99,12 @@ namespace is_trunc (λn trunc_n A, (Π(x y : A), trunc_n (x = y))) end is_trunc open is_trunc + structure is_trunc [class] (n : trunc_index) (A : Type) := (to_internal : is_trunc_internal n A) + open nat num is_trunc.trunc_index + namespace is_trunc abbreviation is_contr := is_trunc -2 @@ -227,6 +230,14 @@ namespace is_trunc : is_contr (Σ(x : A), x = a) := is_contr.mk (sigma.mk a idp) (λp, sigma.rec_on p (λ b q, eq.rec_on q idp)) + definition ap_pr1_center_eq_sigma_eq {A : Type} {a x : A} (p : a = x) + : ap pr₁ (center_eq ⟨x, p⟩) = p := + by induction p; reflexivity + + definition ap_pr1_center_eq_sigma_eq' {A : Type} {a x : A} (p : x = a) + : ap pr₁ (center_eq ⟨x, p⟩) = p⁻¹ := + by induction p; reflexivity + definition is_contr_unit : is_contr unit := is_contr.mk star (λp, unit.rec_on p idp) @@ -246,8 +257,6 @@ namespace is_trunc section open is_equiv equiv - --should we remove the following two theorems as they are special cases of - --"is_trunc_is_equiv_closed" definition is_contr_is_equiv_closed (f : A → B) [Hf : is_equiv f] [HA: is_contr A] : (is_contr B) := is_contr.mk (f (center A)) (λp, eq_of_eq_inv !center_eq) @@ -301,7 +310,7 @@ namespace is_trunc /- interaction with the Unit type -/ open equiv - -- A contractible type is equivalent to [Unit]. *) + /- A contractible type is equivalent to unit. -/ variable (A) definition equiv_unit_of_is_contr [H : is_contr A] : A ≃ unit := equiv.MK (λ (x : A), ⋆) @@ -330,9 +339,14 @@ namespace is_trunc /- truncated universe -/ - -- TODO: move to root namespace? - structure trunctype (n : trunc_index) := - (carrier : Type) (struct : is_trunc n carrier) +end is_trunc + +structure trunctype (n : trunc_index) := + (carrier : Type) + (struct : is_trunc n carrier) + +namespace is_trunc + attribute trunctype.carrier [coercion] attribute trunctype.struct [instance] [priority 1400] @@ -349,6 +363,6 @@ namespace is_trunc definition tlift.{u v} [constructor] {n : trunc_index} (A : trunctype.{u} n) : trunctype.{max u v} n := - trunctype.mk (lift A) (is_trunc_lift _ _) + trunctype.mk (lift A) !is_trunc_lift end is_trunc diff --git a/hott/types/fiber.hlean b/hott/types/fiber.hlean index 9aaace851..18a429a48 100644 --- a/hott/types/fiber.hlean +++ b/hott/types/fiber.hlean @@ -8,13 +8,12 @@ Theorems about fibers -/ import .sigma .eq .pi .pointed +open equiv sigma sigma.ops eq pi structure fiber {A B : Type} (f : A → B) (b : B) := (point : A) (point_eq : f point = b) -open equiv sigma sigma.ops eq pi - namespace fiber variables {A B : Type} {f : A → B} {b : B} @@ -64,7 +63,7 @@ namespace fiber pointed.mk (fiber.mk a idp) definition pointed_fiber [constructor] (f : A → B) (a : A) : Type* := - Pointed.mk (fiber.mk a (idpath (f a))) + pointed.Mk (fiber.mk a (idpath (f a))) definition is_trunc_fun [reducible] (n : trunc_index) (f : A → B) := Π(b : B), is_trunc n (fiber f b) @@ -95,7 +94,7 @@ namespace fiber end fiber -open unit is_trunc +open unit is_trunc pointed namespace fiber @@ -116,6 +115,13 @@ namespace fiber ≃ Σz : unit, a₀ = a : fiber.sigma_char ... ≃ a₀ = a : sigma_unit_left + -- the pointed fiber of a pointed map, which is the fiber over the basepoint + definition pfiber [constructor] {X Y : Type*} (f : X →* Y) : Type* := + pointed.MK (fiber f pt) (fiber.mk pt !respect_pt) + + definition ppoint [constructor] {X Y : Type*} (f : X →* Y) : pfiber f →* X := + pmap.mk point idp + end fiber open function is_equiv diff --git a/hott/types/fin.hlean b/hott/types/fin.hlean index 4d2be9265..46dc6a07e 100644 --- a/hott/types/fin.hlean +++ b/hott/types/fin.hlean @@ -220,7 +220,7 @@ end lemma lift_fun_of_inj {f : fin n → fin n} : is_embedding f → is_embedding (lift_fun f) := begin intro Pemb, apply is_embedding_of_is_injective, intro i j, - assert Pdi : decidable (i = maxi), apply _, + assert Pdi : decidable (i = maxi), apply _, assert Pdj : decidable (j = maxi), apply _, cases Pdi with Pimax Pinmax, cases Pdj with Pjmax Pjnmax, @@ -231,7 +231,7 @@ begin substvars, rewrite [lift_fun_max, lift_fun_of_ne_max Pinmax], intro Plmax, apply absurd Plmax lift_succ_ne_max, rewrite [lift_fun_of_ne_max Pinmax, lift_fun_of_ne_max Pjnmax], - intro Peq, apply eq_of_veq, + intro Peq, apply eq_of_veq, cases i with i ilt, cases j with j jlt, esimp at *, fapply veq_of_eq, apply is_injective_of_is_embedding, apply @is_injective_of_is_embedding _ _ lift_succ _ _ _ Peq, @@ -474,18 +474,18 @@ begin exact if h : v < n then sum.inl (mk v h) else sum.inr (mk (v-n) (nat.sub_lt_of_lt_add vlt (le_of_not_gt h))) }, - { intro f, cases f with v vlt, esimp, apply @by_cases (v < n), + { intro f, cases f with v vlt, esimp, apply @by_cases (v < n), intro vltn, rewrite [dif_pos vltn], apply eq_of_veq, reflexivity, - intro nvltn, rewrite [dif_neg nvltn], apply eq_of_veq, esimp, + intro nvltn, rewrite [dif_neg nvltn], apply eq_of_veq, esimp, apply nat.sub_add_cancel, apply le_of_not_gt, apply nvltn }, { intro s, cases s with f g, - cases f with v vlt, rewrite [dif_pos vlt], + cases f with v vlt, rewrite [dif_pos vlt], cases g with v vlt, esimp, have ¬ v + n < n, from suppose v + n < n, assert v < n - n, from nat.lt_sub_of_add_lt this !le.refl, have v < 0, by rewrite [nat.sub_self at this]; exact this, absurd this !not_lt_zero, - apply concat, apply dif_neg this, apply ap inr, apply eq_of_veq, esimp, + apply concat, apply dif_neg this, apply ap inr, apply eq_of_veq, esimp, apply nat.add_sub_cancel }, end @@ -494,7 +494,7 @@ begin fapply equiv.MK, { apply succ_maxi_cases, esimp, apply inl, apply inr unit.star }, { intro d, cases d, apply lift_succ a, apply maxi }, - { intro d, cases d, + { intro d, cases d, cases a with a alt, esimp, apply elim_succ_maxi_cases_lift_succ, cases a, apply elim_succ_maxi_cases_maxi }, { intro a, apply succ_maxi_cases, esimp, @@ -513,14 +513,14 @@ begin ... ≃ empty : prod_empty_equiv ... ≃ fin 0 : fin_zero_equiv_empty }, { assert H : (a + 1) * m = a * m + m, rewrite [nat.right_distrib, one_mul], - calc fin (a + 1) × fin m + calc fin (a + 1) × fin m ≃ (fin a + unit) × fin m : prod.prod_equiv_prod_right !fin_succ_equiv ... ≃ (fin a × fin m) + (unit × fin m) : sum_prod_right_distrib ... ≃ (fin a × fin m) + (fin m × unit) : prod_comm_equiv ... ≃ fin (a * m) + (fin m × unit) : v_0 ... ≃ fin (a * m) + fin m : prod_unit_equiv ... ≃ fin (a * m + m) : fin_sum_equiv - ... ≃ fin ((a + 1) * m) : equiv_of_eq (ap fin H) }, + ... ≃ fin ((a + 1) * m) : equiv_of_eq (ap fin H⁻¹) }, end definition fin_two_equiv_bool : fin 2 ≃ bool := @@ -543,13 +543,13 @@ begin induction n with n IH, { calc A ≃ A + empty : sum_empty_equiv ... ≃ empty + A : sum_comm_equiv - ... ≃ fin 0 + A : fin_zero_equiv_empty + ... ≃ fin 0 + A : fin_zero_equiv_empty ... ≃ fin 0 + B : H ... ≃ empty + B : fin_zero_equiv_empty ... ≃ B + empty : sum_comm_equiv ... ≃ B : sum_empty_equiv }, - { apply IH, apply unit_sum_equiv_cancel, - calc unit + (fin n + A) ≃ (unit + fin n) + A : sum_assoc_equiv + { apply IH, apply unit_sum_equiv_cancel, + calc unit + (fin n + A) ≃ (unit + fin n) + A : sum_assoc_equiv ... ≃ (fin n + unit) + A : sum_comm_equiv ... ≃ fin (nat.succ n) + A : fin_sum_unit_equiv ... ≃ fin (nat.succ n) + B : H @@ -564,14 +564,14 @@ begin revert n H, induction m with m IH IH, { intro n H, cases n, reflexivity, exfalso, apply to_fun fin_zero_equiv_empty, apply to_inv H, apply fin.zero }, - { intro n H, cases n with n, exfalso, - apply to_fun fin_zero_equiv_empty, apply to_fun H, apply fin.zero, - have unit + fin m ≃ unit + fin n, from + { intro n H, cases n with n, exfalso, + apply to_fun fin_zero_equiv_empty, apply to_fun H, apply fin.zero, + have unit + fin m ≃ unit + fin n, from calc unit + fin m ≃ fin m + unit : sum_comm_equiv ... ≃ fin (nat.succ m) : fin_succ_equiv ... ≃ fin (nat.succ n) : H ... ≃ fin n + unit : fin_succ_equiv - ... ≃ unit + fin n : sum_comm_equiv, + ... ≃ unit + fin n : sum_comm_equiv, have fin m ≃ fin n, from unit_sum_equiv_cancel this, apply ap nat.succ, apply IH _ this }, end diff --git a/hott/types/pointed.hlean b/hott/types/pointed.hlean index 635814563..5c4f3c782 100644 --- a/hott/types/pointed.hlean +++ b/hott/types/pointed.hlean @@ -7,13 +7,13 @@ Ported from Coq HoTT -/ import arity .eq .bool .unit .sigma .nat.basic -open is_trunc eq prod sigma nat equiv option is_equiv bool unit algebra +open is_trunc eq prod sigma nat equiv option is_equiv bool unit algebra equiv.ops structure pointed [class] (A : Type) := (point : A) structure Pointed := - {carrier : Type} + (carrier : Type) (Point : carrier) open Pointed @@ -25,10 +25,10 @@ namespace pointed variables {A B : Type} definition pt [unfold 2] [H : pointed A] := point A - protected definition Mk [constructor] := @Pointed.mk - protected definition MK [constructor] (A : Type) (a : A) := Pointed.mk a + protected definition Mk [constructor] {A : Type} (a : A) := Pointed.mk A a + protected definition MK [constructor] (A : Type) (a : A) := Pointed.mk A a protected definition mk' [constructor] (A : Type) [H : pointed A] : Type* := - Pointed.mk (point A) + Pointed.mk A (point A) definition pointed_carrier [instance] [constructor] (A : Type*) : pointed A := pointed.mk (Point A) @@ -66,7 +66,7 @@ namespace pointed pointed.mk' bool definition Unit [constructor] : Type* := - Pointed.mk unit.star + pointed.Mk unit.star definition pointed_fun_closed [constructor] (f : A → B) [H : pointed A] : pointed B := pointed.mk (f pt) @@ -108,35 +108,90 @@ namespace pointed definition add_point [constructor] (A : Type) : Type* := - Pointed.mk (none : option A) + pointed.Mk (none : option A) postfix `₊`:(max+1) := add_point -- the inclusion A → A₊ is called "some", the extra point "pt" or "none" ("@none A") + end pointed -open pointed -structure pmap (A B : Type*) := - (map : A → B) - (resp_pt : map (Point A) = Point B) +namespace pointed + /- properties of iterated loop space -/ + variable (A : Type*) + definition loop_space_succ_eq_in (n : ℕ) : Ω[succ n] A = Ω[n] (Ω A) := + begin + induction n with n IH, + { reflexivity}, + { exact ap Loop_space IH} + end -open pmap + definition loop_space_add (n m : ℕ) : Ω[n] (Ω[m] A) = Ω[m+n] (A) := + begin + induction n with n IH, + { reflexivity}, + { exact ap Loop_space IH} + end + + definition loop_space_succ_eq_out (n : ℕ) : Ω[succ n] A = Ω(Ω[n] A) := + idp + + variable {A} + + /- the equality [loop_space_succ_eq_in] preserves concatenation -/ + theorem loop_space_succ_eq_in_concat {n : ℕ} (p q : Ω[succ (succ n)] A) : + transport carrier (ap Loop_space (loop_space_succ_eq_in A n)) (p ⬝ q) + = transport carrier (ap Loop_space (loop_space_succ_eq_in A n)) p + ⬝ transport carrier (ap Loop_space (loop_space_succ_eq_in A n)) q := + begin + rewrite [-+tr_compose, ↑function.compose], + rewrite [+@transport_eq_FlFr_D _ _ _ _ Point Point, +con.assoc], apply whisker_left, + rewrite [-+con.assoc], apply whisker_right, rewrite [con_inv_cancel_right, ▸*, -ap_con] + end + + definition loop_space_loop_irrel (p : point A = point A) : Ω(pointed.Mk p) = Ω[2] A := + begin + intros, fapply Pointed_eq, + { esimp, transitivity _, + apply eq_equiv_fn_eq_of_equiv (equiv_eq_closed_right _ p⁻¹), + esimp, apply eq_equiv_eq_closed, apply con.right_inv, apply con.right_inv}, + { esimp, apply con.left_inv} + end + + definition iterated_loop_space_loop_irrel (n : ℕ) (p : point A = point A) + : Ω[succ n](pointed.Mk p) = Ω[succ (succ n)] A :> Pointed := + calc + Ω[succ n](pointed.Mk p) = Ω[n](Ω (pointed.Mk p)) : loop_space_succ_eq_in + ... = Ω[n] (Ω[2] A) : loop_space_loop_irrel + ... = Ω[2+n] A : loop_space_add + ... = Ω[n+2] A : by rewrite [algebra.add.comm] + +end pointed open pointed + +/- pointed maps -/ +structure pmap (A B : Type*) := + (to_fun : A → B) + (resp_pt : to_fun (Point A) = Point B) namespace pointed - abbreviation respect_pt [unfold 3] := @pmap.resp_pt notation `map₊` := pmap infix ` →* `:30 := pmap - attribute pmap.map [coercion] + attribute pmap.to_fun [coercion] +end pointed open pointed + +/- pointed homotopies -/ +structure phomotopy {A B : Type*} (f g : A →* B) := + (homotopy : f ~ g) + (homotopy_pt : homotopy pt ⬝ respect_pt g = respect_pt f) + +namespace pointed variables {A B C D : Type*} {f g h : A →* B} - definition pmap_eq (r : Πa, f a = g a) (s : respect_pt f = (r pt) ⬝ respect_pt g) : f = g := - begin - cases f with f p, cases g with g q, - esimp at *, - fapply apo011 pmap.mk, - { exact eq_of_homotopy r}, - { apply concato_eq, apply pathover_eq_Fl, apply inv_con_eq_of_eq_con, - rewrite [ap_eq_ap10,↑ap10,apd10_eq_of_homotopy,s]} - end + infix ` ~* `:50 := phomotopy + abbreviation to_homotopy_pt [unfold 5] := @phomotopy.homotopy_pt + abbreviation to_homotopy [coercion] [unfold 5] (p : f ~* g) : Πa, f a = g a := + phomotopy.homotopy p + + /- categorical properties of pointed maps -/ definition pid [constructor] (A : Type*) : A →* A := pmap.mk id idp @@ -146,19 +201,6 @@ namespace pointed infixr ` ∘* `:60 := pcompose - -- The constant pointed map between any two types - definition pconst [constructor] (A B : Type*) : A →* B := - pmap.mk (λ a, Point B) idp - - structure phomotopy (f g : A →* B) := - (homotopy : f ~ g) - (homotopy_pt : homotopy pt ⬝ respect_pt g = respect_pt f) - - infix ` ~* `:50 := phomotopy - abbreviation to_homotopy_pt [unfold 5] := @phomotopy.homotopy_pt - abbreviation to_homotopy [coercion] [unfold 5] (p : f ~* g) : Πa, f a = g a := - phomotopy.homotopy p - definition passoc (h : C →* D) (g : B →* C) (f : A →* B) : (h ∘* g) ∘* f ~* h ∘* (g ∘* f) := begin fconstructor, intro a, reflexivity, @@ -181,6 +223,18 @@ namespace pointed { reflexivity} end + /- equivalences and equalities -/ + + definition pmap_eq (r : Πa, f a = g a) (s : respect_pt f = (r pt) ⬝ respect_pt g) : f = g := + begin + cases f with f p, cases g with g q, + esimp at *, + fapply apo011 pmap.mk, + { exact eq_of_homotopy r}, + { apply concato_eq, apply pathover_eq_Fl, apply inv_con_eq_of_eq_con, + rewrite [ap_eq_ap10,↑ap10,apd10_eq_of_homotopy,s]} + end + definition pmap_equiv_left (A : Type) (B : Type*) : A₊ →* B ≃ (A → B) := begin fapply equiv.MK, @@ -222,6 +276,12 @@ namespace pointed { esimp, exact !con.left_inv⁻¹}}, end + /- instances of pointed maps -/ + + -- The constant pointed map between any two types + definition pconst [constructor] (A B : Type*) : A →* B := + pmap.mk (λ a, Point B) idp + definition ap1 [constructor] (f : A →* B) : Ω A →* Ω B := begin fconstructor, @@ -236,54 +296,21 @@ namespace pointed { esimp [Iterated_loop_space], exact ap1 IH} end - variable (A) - definition loop_space_succ_eq_in (n : ℕ) : Ω[succ n] A = Ω[n] (Ω A) := + definition pcast [constructor] {A B : Type*} (p : A = B) : A →* B := + proof pmap.mk (cast (ap Pointed.carrier p)) (by induction p; reflexivity) qed + + definition pinverse [constructor] {X : Type*} : Ω X →* Ω X := + pmap.mk eq.inverse idp + + /- properties about these instances -/ + + definition is_equiv_ap1 {A B : Type*} (f : A →* B) [is_equiv f] : is_equiv (ap1 f) := begin - induction n with n IH, - { reflexivity}, - { exact ap Loop_space IH} + induction B with B b, induction f with f pf, esimp at *, cases pf, esimp, + apply is_equiv.homotopy_closed (ap f), + intro p, exact !idp_con⁻¹ end - definition loop_space_add (n m : ℕ) : Ω[n] (Ω[m] A) = Ω[m+n] (A) := - begin - induction n with n IH, - { reflexivity}, - { exact ap Loop_space IH} - end - - definition loop_space_succ_eq_out (n : ℕ) : Ω[succ n] A = Ω(Ω[n] A) := - idp - - variable {A} - - /- the equality [loop_space_succ_eq_in] preserves concatenation -/ - theorem loop_space_succ_eq_in_concat {n : ℕ} (p q : Ω[succ (succ n)] A) : - transport carrier (ap Loop_space (loop_space_succ_eq_in A n)) (p ⬝ q) - = transport carrier (ap Loop_space (loop_space_succ_eq_in A n)) p - ⬝ transport carrier (ap Loop_space (loop_space_succ_eq_in A n)) q := - begin - rewrite [-+tr_compose, ↑function.compose], - rewrite [+@transport_eq_FlFr_D _ _ _ _ Point Point, +con.assoc], apply whisker_left, - rewrite [-+con.assoc], apply whisker_right, rewrite [con_inv_cancel_right, ▸*, -ap_con] - end - - definition loop_space_loop_irrel (p : point A = point A) : Ω(Pointed.mk p) = Ω[2] A := - begin - intros, fapply Pointed_eq, - { esimp, transitivity _, - apply eq_equiv_fn_eq_of_equiv (equiv_eq_closed_right _ p⁻¹), - esimp, apply eq_equiv_eq_closed, apply con.right_inv, apply con.right_inv}, - { esimp, apply con.left_inv} - end - - definition iterated_loop_space_loop_irrel (n : ℕ) (p : point A = point A) - : Ω[succ n](Pointed.mk p) = Ω[succ (succ n)] A :> Pointed := - calc - Ω[succ n](Pointed.mk p) = Ω[n](Ω (Pointed.mk p)) : loop_space_succ_eq_in - ... = Ω[n] (Ω[2] A) : loop_space_loop_irrel - ... = Ω[2+n] A : loop_space_add - ... = Ω[n+2] A : by rewrite [algebra.add.comm] - -- TODO: -- definition apn_compose (n : ℕ) (g : B →* C) (f : A →* B) : apn n (g ∘* f) ~* apn n g ∘* apn n f := -- _ @@ -297,6 +324,8 @@ namespace pointed { reflexivity} end + /- categorical properties of pointed homotopies -/ + protected definition phomotopy.refl [refl] (f : A →* B) : f ~* f := begin fconstructor, @@ -304,6 +333,9 @@ namespace pointed { apply idp_con} end + protected definition phomotopy.rfl [constructor] {A B : Type*} {f : A →* B} : f ~* f := + phomotopy.refl f + protected definition phomotopy.trans [trans] (p : f ~* g) (q : g ~* h) : f ~* h := begin @@ -324,12 +356,16 @@ namespace pointed infix ` ⬝* `:75 := phomotopy.trans postfix `⁻¹*`:(max+1) := phomotopy.symm - definition eq_of_phomotopy (p : f ~* g) : f = g := - begin - fapply pmap_eq, - { intro a, exact p a}, - { exact !to_homotopy_pt⁻¹} - end + definition phomotopy_of_eq [constructor] {A B : Type*} {f g : A →* B} (p : f = g) : f ~* g := + phomotopy.mk (ap010 pmap.to_fun p) begin induction p, apply idp_con end + + definition pconcat_eq [constructor] {A B : Type*} {f g h : A →* B} (p : f ~* g) (q : g = h) + : f ~* h := + p ⬝* phomotopy_of_eq q + + definition eq_pconcat [constructor] {A B : Type*} {f g h : A →* B} (p : f = g) (q : g ~* h) + : f ~* h := + phomotopy_of_eq p ⬝* q definition pwhisker_left [constructor] (h : B →* C) (p : f ~* g) : h ∘* f ~* h ∘* g := begin @@ -350,38 +386,48 @@ namespace pointed exact !idp_con⁻¹} end - structure pequiv (A B : Type*) := - (to_pmap : A →* B) - (is_equiv_to_pmap : is_equiv to_pmap) + definition pconcat2 [constructor] {A B C : Type*} {h i : B →* C} {f g : A →* B} + (q : h ~* i) (p : f ~* g) : h ∘* f ~* i ∘* g := + pwhisker_left _ p ⬝* pwhisker_right _ q - infix ` ≃* `:25 := pequiv - attribute pequiv.to_pmap [coercion] - attribute pequiv.is_equiv_to_pmap [instance] + definition ap1_pinverse {A : Type*} : ap1 (@pinverse A) ~* @pinverse (Ω A) := + begin + fapply phomotopy.mk, + { intro p, esimp, refine !idp_con ⬝ _, exact !inverse_eq_inverse2⁻¹ }, + { reflexivity} + end - definition pequiv.mk' [constructor] (to_pmap : A →* B) [is_equiv_to_pmap : is_equiv to_pmap] : - pequiv A B := - pequiv.mk to_pmap is_equiv_to_pmap + definition ap1_id [constructor] {A : Type*} : ap1 (pid A) ~* pid (Ω A) := + begin + fapply phomotopy.mk, + { intro p, esimp, refine !idp_con ⬝ !ap_id}, + { reflexivity} + end - definition pequiv_of_equiv [constructor] - (eqv : A ≃ B) (resp : equiv.to_fun eqv (point A) = point B) : A ≃* B := - pequiv.mk' (pmap.mk (equiv.to_fun eqv) resp) + -- TODO: finish this proof + /- definition ap1_phomotopy {A B : Type*} {f g : A →* B} (p : f ~* g) + : ap1 f ~* ap1 g := + begin + induction p with p q, induction f with f pf, induction g with g pg, induction B with B b, + esimp at *, induction q, induction pg, + fapply phomotopy.mk, + { intro l, esimp, refine _ ⬝ !idp_con⁻¹, refine !con.assoc ⬝ _, apply inv_con_eq_of_eq_con, + apply ap_con_eq_con_ap}, + { esimp, } + end -/ - definition equiv_of_pequiv [constructor] (f : A ≃* B) : A ≃ B := - equiv.mk f _ + definition eq_of_phomotopy (p : f ~* g) : f = g := + begin + fapply pmap_eq, + { intro a, exact p a}, + { exact !to_homotopy_pt⁻¹} + end - definition to_pinv [constructor] (f : A ≃* B) : B →* A := - pmap.mk f⁻¹ (ap f⁻¹ (respect_pt f)⁻¹ ⬝ !left_inv) + definition pap {A B C D : Type*} (F : (A →* B) → (C →* D)) + {f g : A →* B} (p : f ~* g) : F f ~* F g := + phomotopy.mk (ap010 F (eq_of_phomotopy p)) begin cases eq_of_phomotopy p, apply idp_con end - definition pua {A B : Type*} (f : A ≃* B) : A = B := - Pointed_eq (equiv_of_pequiv f) !respect_pt - - definition pequiv_refl [refl] [constructor] : A ≃* A := - pequiv.mk !pid !is_equiv_id - - definition pequiv_symm [symm] (f : A ≃* B) : B ≃* A := - pequiv.mk (to_pinv f) !is_equiv_inv - - definition pequiv_trans [trans] (f : A ≃* B) (g : B ≃*C) : A ≃* C := - pequiv.mk (pcompose g f) !is_equiv_compose + infix ` ⬝*p `:75 := pconcat_eq + infix ` ⬝p* `:75 := eq_pconcat end pointed diff --git a/hott/types/pointed2.hlean b/hott/types/pointed2.hlean new file mode 100644 index 000000000..3ff51e5a3 --- /dev/null +++ b/hott/types/pointed2.hlean @@ -0,0 +1,104 @@ +/- +Copyright (c) 2014 Jakob von Raumer. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Floris van Doorn + +Ported from Coq HoTT +-/ + + +import .equiv + +open eq is_equiv equiv equiv.ops pointed is_trunc + +-- structure pequiv (A B : Type*) := +-- (to_pmap : A →* B) +-- (is_equiv_to_pmap : is_equiv to_pmap) + +structure pequiv (A B : Type*) extends equiv A B, pmap A B + +section + universe variable u + structure ptrunctype (n : trunc_index) extends trunctype.{u} n, Pointed.{u} +end + +namespace pointed + + variables {A B C : Type*} + + /- pointed equivalences -/ + + infix ` ≃* `:25 := pequiv + attribute pequiv.to_pmap [coercion] + attribute pequiv.to_is_equiv [instance] + + definition pequiv_of_pmap [constructor] (f : A →* B) (H : is_equiv f) : A ≃* B := + pequiv.mk f _ (respect_pt f) + + definition pequiv_of_equiv [constructor] (f : A ≃ B) (H : f pt = pt) : A ≃* B := + pequiv.mk f _ H + + definition equiv_of_pequiv [constructor] (f : A ≃* B) : A ≃ B := + equiv.mk f _ + + definition to_pinv [constructor] (f : A ≃* B) : B →* A := + pmap.mk f⁻¹ (ap f⁻¹ (respect_pt f)⁻¹ ⬝ !left_inv) + + definition pua {A B : Type*} (f : A ≃* B) : A = B := + Pointed_eq (equiv_of_pequiv f) !respect_pt + + protected definition pequiv.refl [refl] [constructor] (A : Type*) : A ≃* A := + pequiv_of_pmap !pid !is_equiv_id + + protected definition pequiv.rfl [constructor] : A ≃* A := + pequiv.refl A + + protected definition pequiv.symm [symm] (f : A ≃* B) : B ≃* A := + pequiv_of_pmap (to_pinv f) !is_equiv_inv + + protected definition pequiv.trans [trans] (f : A ≃* B) (g : B ≃* C) : A ≃* C := + pequiv_of_pmap (pcompose g f) !is_equiv_compose + + postfix `⁻¹ᵉ*`:(max + 1) := pequiv.symm + infix ` ⬝e* `:75 := pequiv.trans + + definition pequiv_rect' (f : A ≃* B) (P : A → B → Type) + (g : Πb, P (f⁻¹ b) b) (a : A) : P a (f a) := + left_inv f a ▸ g (f a) + + definition pequiv_of_eq [constructor] {A B : Type*} (p : A = B) : A ≃* B := + pequiv_of_pmap (pcast p) !is_equiv_tr + + definition peconcat_eq {A B C : Type*} (p : A ≃* B) (q : B = C) : A ≃* C := + p ⬝e* pequiv_of_eq q + + definition eq_peconcat {A B C : Type*} (p : A = B) (q : B ≃* C) : A ≃* C := + pequiv_of_eq p ⬝e* q + + definition eq_of_pequiv {A B : Type*} (p : A ≃* B) : A = B := + Pointed_eq (equiv_of_pequiv p) !respect_pt + + definition peap {A B : Type*} (F : Type* → Type*) (p : A ≃* B) : F A ≃* F B := + pequiv_of_pmap (pcast (ap F (eq_of_pequiv p))) begin cases eq_of_pequiv p, apply is_equiv_id end + + definition loop_space_pequiv [constructor] (p : A ≃* B) : Ω A ≃* Ω B := + pequiv_of_pmap (ap1 p) (is_equiv_ap1 p) + + definition pequiv_eq {p q : A ≃* B} (H : p = q :> (A →* B)) : p = q := + begin + cases p with f Hf, cases q with g Hg, esimp at *, + exact apd011 pequiv_of_pmap H !is_hprop.elim + end + + definition loop_space_pequiv_rfl + : loop_space_pequiv (@pequiv.refl A) = @pequiv.refl (Ω A) := + begin + apply pequiv_eq, fapply pmap_eq: esimp, + { intro p, exact !idp_con ⬝ !ap_id}, + { reflexivity} + end + + infix ` ⬝e*p `:75 := peconcat_eq + infix ` ⬝pe* `:75 := eq_peconcat + +end pointed diff --git a/hott/types/sigma.hlean b/hott/types/sigma.hlean index 68efb57bb..82eed52e5 100644 --- a/hott/types/sigma.hlean +++ b/hott/types/sigma.hlean @@ -328,6 +328,15 @@ namespace sigma ... ≃ B × A : prod_comm_equiv ... ≃ Σ(b : B), A : equiv_prod + definition sigma_assoc_comm_equiv {A : Type} (B C : A → Type) + : (Σ(v : Σa, B a), C v.1) ≃ (Σ(u : Σa, C a), B u.1) := + calc (Σ(v : Σa, B a), C v.1) + ≃ (Σa (b : B a), C a) : !sigma_assoc_equiv⁻¹ᵉ + ... ≃ (Σa, B a × C a) : sigma_equiv_sigma_id (λa, !equiv_prod) + ... ≃ (Σa, C a × B a) : sigma_equiv_sigma_id (λa, !prod_comm_equiv) + ... ≃ (Σa (c : C a), B a) : sigma_equiv_sigma_id (λa, !equiv_prod) + ... ≃ (Σ(u : Σa, C a), B u.1) : sigma_assoc_equiv + /- Interaction with other type constructors -/ definition sigma_empty_left [constructor] (B : empty → Type) : (Σx, B x) ≃ empty := diff --git a/hott/types/trunc.hlean b/hott/types/trunc.hlean index 4dd8112a9..89d6d0e30 100644 --- a/hott/types/trunc.hlean +++ b/hott/types/trunc.hlean @@ -10,7 +10,7 @@ Properties of is_trunc and trunctype import types.pi types.eq types.equiv ..function -open eq sigma sigma.ops pi function equiv is_trunc.trunctype +open eq sigma sigma.ops pi function equiv trunctype is_equiv prod is_trunc.trunc_index pointed nat namespace is_trunc @@ -147,7 +147,7 @@ namespace is_trunc iff.intro _ (is_trunc_succ_of_is_trunc_loop Hn) theorem is_trunc_iff_is_contr_loop_succ (n : ℕ) (A : Type) - : is_trunc n A ↔ Π(a : A), is_contr (Ω[succ n](Pointed.mk a)) := + : is_trunc n A ↔ Π(a : A), is_contr (Ω[succ n](pointed.Mk a)) := begin revert A, induction n with n IH, { intro A, esimp [Iterated_loop_space], transitivity _, @@ -242,7 +242,16 @@ namespace trunc : transport (λa, trunc n (P a)) p (tr x) = tr (p ▸ x) := by induction p; reflexivity - definition image {A B : Type} (f : A → B) (b : B) : hprop := ∃(a : A), f a = b + definition image {A B : Type} (f : A → B) (b : B) : hprop := ∥ fiber f b ∥ + + -- truncation of pointed types + definition ptrunc [constructor] (n : trunc_index) (X : Type*) : Type* := + pointed.MK (trunc n X) (tr pt) + + definition ptrunc_functor [constructor] {X Y : Type*} (n : ℕ₋₂) (f : X →* Y) + : ptrunc n X →* ptrunc n Y := + pmap.mk (trunc_functor n f) (ap tr (respect_pt f)) + end trunc open trunc diff --git a/hott/types/types.md b/hott/types/types.md index 88490a378..c5e270f59 100644 --- a/hott/types/types.md +++ b/hott/types/types.md @@ -23,9 +23,10 @@ The number systems (num, nat, int, ...) are for a large part ported from the sta Specific HoTT types * [eq](eq.hlean): show that functions related to the identity type are equivalences -* [pointed](pointed.hlean): pointed types, maps, homotopies, and equivalences +* [pointed](pointed.hlean): pointed types, pointed maps, pointed homotopies * [fiber](fiber.hlean) * [equiv](equiv.hlean) -* [trunc](trunc.hlean): truncation levels, n-Types, truncation +* [pointed2](pointed2.hlean): pointed equivalences and pointed truncated types (this is a separate file, because it depends on types.equiv) +* [trunc](trunc.hlean): truncation levels, n-types, truncation * [pullback](pullback.hlean) * [univ](univ.hlean) \ No newline at end of file diff --git a/src/emacs/lean-syntax.el b/src/emacs/lean-syntax.el index f2a71b6cc..79ff2e6c5 100644 --- a/src/emacs/lean-syntax.el +++ b/src/emacs/lean-syntax.el @@ -27,7 +27,7 @@ (defconst lean-keywords1-regexp (eval `(rx word-start (or ,@lean-keywords1) word-end))) (defconst lean-keywords2 - '("by+" "begin+") + '("by+" "begin+" "example.") "lean keywords ending with 'symbol'") (defconst lean-keywords2-regexp (eval `(rx word-start (or ,@lean-keywords2) symbol-end))) @@ -174,7 +174,7 @@ (,lean-keywords1-regexp . 'font-lock-keyword-face) (,(rx (or "∎")) . 'font-lock-keyword-face) ;; Types - (,(rx word-start (or "Prop" "Type" "Type'" "Type₊" "Type₀" "Type₁" "Type₂" "Type₃" "Type*") symbol-end) . 'font-lock-type-face) + (,(rx word-start (or "Prop" "Type" "Type'" "Type₊" "Type₀" "Type₁" "Type₂" "Type₃" "Type*" "Set") symbol-end) . 'font-lock-type-face) (,(rx word-start (group "Type") ".") (1 'font-lock-type-face)) ;; String ("\"[^\"]*\"" . 'font-lock-string-face)