From 087c44d6146a006b74746c2c241e05938074a597 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Mon, 15 Feb 2016 18:23:28 -0500 Subject: [PATCH] style(hott): rename instances of pType using pfoo instead of Foo For example, the pointed suspension operation was called Susp before this commit, but now is called psusp --- hott/algebra/homotopy_group.hlean | 2 +- hott/hit/pointed_pushout.hlean | 12 +++++----- hott/hit/quotient.hlean | 7 ++++-- hott/homotopy/circle.hlean | 6 ++--- hott/homotopy/cofiber.hlean | 16 ++++++------- hott/homotopy/connectedness.hlean | 4 ++-- hott/homotopy/smash.hlean | 12 +++++----- hott/homotopy/sphere.hlean | 18 ++++++-------- hott/homotopy/susp.hlean | 34 +++++++++++++-------------- hott/homotopy/wedge.hlean | 4 ++-- hott/types/lift.hlean | 8 ++++++- hott/types/nat/hott.hlean | 7 ++++-- hott/types/pointed.hlean | 39 +++++++++++++++---------------- hott/types/trunc.hlean | 6 ++--- 14 files changed, 91 insertions(+), 84 deletions(-) diff --git a/hott/algebra/homotopy_group.hlean b/hott/algebra/homotopy_group.hlean index 898bfeeeb1..e97dabcd5a 100644 --- a/hott/algebra/homotopy_group.hlean +++ b/hott/algebra/homotopy_group.hlean @@ -73,7 +73,7 @@ namespace eq begin revert A, induction m with m IH: intro A, { reflexivity}, - { esimp [Iterated_loop_space, nat.add], refine !homotopy_group_succ_in ⬝ _, refine !IH ⬝ _, + { esimp [iterated_ploop_space, nat.add], refine !homotopy_group_succ_in ⬝ _, refine !IH ⬝ _, exact ap (Group_homotopy_group n) !loop_space_succ_eq_in⁻¹} end diff --git a/hott/hit/pointed_pushout.hlean b/hott/hit/pointed_pushout.hlean index d034ce3692..2431ae8a01 100644 --- a/hott/hit/pointed_pushout.hlean +++ b/hott/hit/pointed_pushout.hlean @@ -3,7 +3,7 @@ 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, Floris van Doorn -pType Pushouts +Pointed Pushouts -/ import .pushout types.pointed2 @@ -23,20 +23,20 @@ namespace pushout section parameters {TL BL TR : Type*} (f : TL →* BL) (g : TL →* TR) - definition Pushout [constructor] : Type* := + definition ppushout [constructor] : Type* := pointed.mk' (pushout f g) parameters {f g} - definition pinl [constructor] : BL →* Pushout := + definition pinl [constructor] : BL →* ppushout := pmap.mk inl idp - definition pinr [constructor] : TR →* Pushout := + definition pinr [constructor] : TR →* ppushout := pmap.mk inr ((ap inr (respect_pt g))⁻¹ ⬝ !glue⁻¹ ⬝ (ap inl (respect_pt f))) definition pglue (x : TL) : pinl (f x) = pinr (g x) := -- TODO do we need this? !glue - definition prec {P : Pushout → Type} (Pinl : Π x, P (pinl x)) (Pinr : Π x, P (pinr x)) + definition prec {P : ppushout → Type} (Pinl : Π x, P (pinl x)) (Pinr : Π x, P (pinr x)) (H : Π x, Pinl (f x) =[pglue x] Pinr (g x)) : (Π y, P y) := pushout.rec Pinl Pinr H end @@ -44,7 +44,7 @@ namespace pushout section variables {TL BL TR : Type*} (f : TL →* BL) (g : TL →* TR) - protected definition psymm [constructor] : Pushout f g ≃* Pushout g f := + protected definition psymm [constructor] : ppushout f g ≃* ppushout g f := begin fapply pequiv_of_equiv, { apply pushout.symm}, diff --git a/hott/hit/quotient.hlean b/hott/hit/quotient.hlean index f8f53aa311..c91f6fba23 100644 --- a/hott/hit/quotient.hlean +++ b/hott/hit/quotient.hlean @@ -14,9 +14,9 @@ See also .set_quotient * eq_of_rel : Π{a a' : A}, R a a' → class_of a = class_of a' (R explicit) -/ -import arity cubical.squareover types.arrow cubical.pathover2 +import arity cubical.squareover types.arrow cubical.pathover2 types.pointed -open eq equiv sigma sigma.ops equiv.ops pi is_trunc +open eq equiv sigma sigma.ops equiv.ops pi is_trunc pointed namespace quotient @@ -100,6 +100,9 @@ namespace quotient end end + definition pquotient [constructor] {A : Type*} (R : A → A → Type) : Type* := + pType.mk (quotient R) (class_of R pt) + /- the flattening lemma -/ namespace flattening diff --git a/hott/homotopy/circle.hlean b/hott/homotopy/circle.hlean index 5bdf06cfb3..b5fcce2441 100644 --- a/hott/homotopy/circle.hlean +++ b/hott/homotopy/circle.hlean @@ -158,11 +158,11 @@ attribute circle.rec_on circle.elim_on [unfold 2] attribute circle.elim_type_on [unfold 1] namespace circle - definition pointed_circle [instance] [constructor] : pointed circle := + definition pointed_circle [instance] [constructor] : pointed S¹ := pointed.mk base - definition Circle [constructor] : Type* := pointed.mk' circle - notation `S¹.` := Circle + definition pcircle [constructor] : Type* := pointed.mk' S¹ + notation `S¹.` := pcircle definition loop_neq_idp : loop ≠ idp := assume H : loop = idp, diff --git a/hott/homotopy/cofiber.hlean b/hott/homotopy/cofiber.hlean index 319cb8fe04..7ff1801e0d 100644 --- a/hott/homotopy/cofiber.hlean +++ b/hott/homotopy/cofiber.hlean @@ -48,28 +48,28 @@ namespace cofiber end end cofiber --- pType version +-- pointed version -definition Cofiber {A B : Type*} (f : A →* B) : Type* := Pushout (pconst A Unit) f +definition pcofiber {A B : Type*} (f : A →* B) : Type* := ppushout (pconst A punit) f namespace cofiber - protected definition prec {A B : Type*} {f : A →* B} {P : Cofiber f → Type} + protected definition prec {A B : Type*} {f : A →* B} {P : pcofiber f → Type} (Pinl : P (inl ⋆)) (Pinr : Π (x : B), P (inr x)) (Pglue : Π (x : A), pathover P Pinl (pglue x) (Pinr (f x))) : - (Π (y : Cofiber f), P y) := + (Π (y : pcofiber f), P y) := begin intro y, induction y, induction x, exact Pinl, exact Pinr x, esimp, exact Pglue x end - protected definition prec_on {A B : Type*} {f : A →* B} {P : Cofiber f → Type} - (y : Cofiber f) (Pinl : P (inl ⋆)) (Pinr : Π (x : B), P (inr x)) + protected definition prec_on {A B : Type*} {f : A →* B} {P : pcofiber f → Type} + (y : pcofiber f) (Pinl : P (inl ⋆)) (Pinr : Π (x : B), P (inr x)) (Pglue : Π (x : A), pathover P Pinl (pglue x) (Pinr (f x))) : P y := begin 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 : pcofiber 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 @@ -79,7 +79,7 @@ namespace cofiber variables (A : Type*) - definition cofiber_unit : Cofiber (pconst A Unit) ≃* Susp A := + definition cofiber_unit : pcofiber (pconst A punit) ≃* psusp A := begin fapply pequiv_of_pmap, { fconstructor, intro x, induction x, exact north, exact south, exact merid x, diff --git a/hott/homotopy/connectedness.hlean b/hott/homotopy/connectedness.hlean index 600bbe17d5..2c6b5dba9c 100644 --- a/hott/homotopy/connectedness.hlean +++ b/hott/homotopy/connectedness.hlean @@ -155,10 +155,10 @@ namespace homotopy -- as special case we get elimination principles for pointed connected types namespace is_conn - open pointed pType unit + open pointed unit section parameters {n : trunc_index} {A : Type*} - [H : is_conn n .+1 A] (P : A → n -Type) + [H : is_conn n .+1 A] (P : A → n-Type) include H protected definition rec : is_equiv (λs : Πa : A, P a, s (Point A)) := diff --git a/hott/homotopy/smash.hlean b/hott/homotopy/smash.hlean index 6ff352569e..839847b0fa 100644 --- a/hott/homotopy/smash.hlean +++ b/hott/homotopy/smash.hlean @@ -10,20 +10,20 @@ import hit.pushout .wedge .cofiber .susp .sphere open eq pushout prod pointed pType is_trunc -definition product_of_wedge [constructor] (A B : Type*) : Wedge A B →* A ×* B := +definition product_of_wedge [constructor] (A B : Type*) : pwedge A B →* A ×* B := begin fconstructor, intro x, induction x with [a, b], exact (a, point B), exact (point A, b), do 2 reflexivity end -definition Smash (A B : Type*) := Cofiber (product_of_wedge A B) +definition psmash (A B : Type*) := pcofiber (product_of_wedge A B) open sphere susp unit namespace smash - protected definition prec {X Y : Type*} {P : Smash X Y → Type} + protected definition prec {X Y : Type*} {P : psmash X Y → Type} (pxy : Π x y, P (inr (x, y))) (ps : P (inl ⋆)) (px : Π x, pathover P ps (glue (inl x)) (pxy x (point Y))) (py : Π y, pathover P ps (glue (inr y)) (pxy (point X) y)) @@ -37,7 +37,7 @@ namespace smash induction u, exact pg, end - protected definition prec_on {X Y : Type*} {P : Smash X Y → Type} (s : Smash X Y) + protected definition prec_on {X Y : Type*} {P : psmash X Y → Type} (s : psmash X Y) (pxy : Π x y, P (inr (x, y))) (ps : P (inl ⋆)) (px : Π x, pathover P ps (glue (inl x)) (pxy x (point Y))) (py : Π y, pathover P ps (glue (inr y)) (pxy (point X) y)) @@ -46,7 +46,7 @@ namespace smash (px (Point X)) (glue ⋆) (py (Point Y))) : P s := smash.prec pxy ps px py pg s -/- definition smash_bool (X : Type*) : Smash X Bool ≃* X := +/- definition smash_bool (X : Type*) : psmash X pbool ≃* X := begin fconstructor, { fconstructor, @@ -74,7 +74,7 @@ namespace smash apply inverse, apply concat, apply ap (ap _), } } } - definition susp_equiv_circle_smash (X : Type*) : Susp X ≃* Smash (Sphere 1) X := + definition susp_equiv_circle_smash (X : Type*) : psusp X ≃* psmash (psphere 1) X := begin fconstructor, { fconstructor, intro x, induction x, }, diff --git a/hott/homotopy/sphere.hlean b/hott/homotopy/sphere.hlean index c3d1cab3c8..19c46b28aa 100644 --- a/hott/homotopy/sphere.hlean +++ b/hott/homotopy/sphere.hlean @@ -92,11 +92,11 @@ namespace sphere definition base {n : ℕ} : sphere n := north definition pointed_sphere [instance] [constructor] (n : ℕ) : pointed (sphere n) := pointed.mk base - definition Sphere [constructor] (n : ℕ) : pType := pointed.mk' (sphere n) + definition psphere [constructor] (n : ℕ) : Type* := pointed.mk' (sphere n) namespace ops abbreviation S := sphere - notation `S.`:max := Sphere + notation `S.` := psphere end ops open sphere.ops @@ -106,7 +106,7 @@ namespace sphere definition surf {n : ℕ} : Ω[n] S. n := nat.rec_on n (proof base qed) (begin intro m s, refine cast _ (apn m (equator m) s), - exact ap pType.carrier !loop_space_succ_eq_in⁻¹ end) + exact ap carrier !loop_space_succ_eq_in⁻¹ end) definition bool_of_sphere : S 0 → bool := @@ -125,11 +125,11 @@ namespace sphere definition sphere_eq_bool : S 0 = bool := ua sphere_equiv_bool - definition sphere_eq_bool_pointed : S. 0 = Bool := + definition sphere_eq_bool_pointed : S. 0 = pbool := pType_eq sphere_equiv_bool idp -- TODO: the commented-out part makes the forward function below "apn _ surf" - definition pmap_sphere (A : pType) (n : ℕ) : map₊ (S. n) A ≃ Ω[n] A := + definition pmap_sphere (A : Type*) (n : ℕ) : map₊ (S. n) A ≃ Ω[n] A := begin -- fapply equiv_change_fun, -- { @@ -143,10 +143,10 @@ namespace sphere -- { exact sorry}} end - protected definition elim {n : ℕ} {P : pType} (p : Ω[n] P) : map₊ (S. n) P := + protected definition elim {n : ℕ} {P : Type*} (p : Ω[n] P) : map₊ (S. n) P := to_inv !pmap_sphere p - -- definition elim_surf {n : ℕ} {P : pType} (p : Ω[n] P) : apn n (sphere.elim p) surf = p := + -- definition elim_surf {n : ℕ} {P : Type*} (p : Ω[n] P) : apn n (sphere.elim p) surf = p := -- begin -- induction n with n IH, -- { esimp [apn,surf,sphere.elim,pmap_sphere], apply sorry}, @@ -157,10 +157,6 @@ end sphere open sphere sphere.ops -structure weakly_constant [class] {A B : Type} (f : A → B) := --move - (is_weakly_constant : Πa a', f a = f a') -abbreviation wconst := @weakly_constant.is_weakly_constant - namespace is_trunc open trunc_index variables {n : ℕ} {A : Type} diff --git a/hott/homotopy/susp.hlean b/hott/homotopy/susp.hlean index 464c2ed59a..d40c877c94 100644 --- a/hott/homotopy/susp.hlean +++ b/hott/homotopy/susp.hlean @@ -85,10 +85,10 @@ namespace susp definition pointed_susp [instance] [constructor] (X : Type) : pointed (susp X) := pointed.mk north - definition Susp [constructor] (X : Type) : pType := + definition psusp [constructor] (X : Type) : pType := pointed.mk' (susp X) - definition Susp_functor (f : X →* Y) : Susp X →* Susp Y := + definition psusp_functor (f : X →* Y) : psusp X →* psusp Y := begin fconstructor, { intro x, induction x, @@ -98,21 +98,21 @@ namespace susp { reflexivity} end - definition Susp_functor_compose (g : Y →* Z) (f : X →* Y) - : Susp_functor (g ∘* f) ~* Susp_functor g ∘* Susp_functor f := + definition psusp_functor_compose (g : Y →* Z) (f : X →* Y) + : psusp_functor (g ∘* f) ~* psusp_functor g ∘* psusp_functor f := begin fconstructor, { intro a, induction a, { reflexivity}, { reflexivity}, { apply eq_pathover, apply hdeg_square, - rewrite [▸*,ap_compose' _ (Susp_functor f),↑Susp_functor,+elim_merid]}}, + rewrite [▸*,ap_compose' _ (psusp_functor f),↑psusp_functor,+elim_merid]}}, { reflexivity} end -- adjunction from Coq-HoTT - definition loop_susp_unit [constructor] (X : pType) : X →* Ω(Susp X) := + definition loop_susp_unit [constructor] (X : pType) : X →* Ω(psusp X) := begin fconstructor, { intro x, exact merid x ⬝ (merid pt)⁻¹}, @@ -120,11 +120,11 @@ namespace susp end definition loop_susp_unit_natural (f : X →* Y) - : loop_susp_unit Y ∘* f ~* ap1 (Susp_functor f) ∘* loop_susp_unit X := + : loop_susp_unit Y ∘* f ~* ap1 (psusp_functor f) ∘* loop_susp_unit X := begin induction X with X x, induction Y with Y y, induction f with f pf, esimp at *, induction pf, fconstructor, - { intro x', esimp [Susp_functor], symmetry, + { intro x', esimp [psusp_functor], symmetry, exact !idp_con ⬝ (!ap_con ⬝ @@ -137,11 +137,11 @@ namespace susp rewrite inverse2_right_inv, refine _ ⬝ !con.assoc', rewrite [ap_con_right_inv], - unfold Susp_functor, + unfold psusp_functor, xrewrite [idp_con_idp, -ap_compose (concat idp)]}, end - definition loop_susp_counit [constructor] (X : pType) : Susp (Ω X) →* X := + definition loop_susp_counit [constructor] (X : pType) : psusp (Ω X) →* X := begin fconstructor, { intro x, induction x, exact pt, exact pt, exact a}, @@ -149,7 +149,7 @@ namespace susp end definition loop_susp_counit_natural (f : X →* Y) - : f ∘* loop_susp_counit X ~* loop_susp_counit Y ∘* (Susp_functor (ap1 f)) := + : f ∘* loop_susp_counit X ~* loop_susp_counit Y ∘* (psusp_functor (ap1 f)) := begin induction X with X x, induction Y with Y y, induction f with f pf, esimp at *, induction pf, fconstructor, @@ -177,7 +177,7 @@ namespace susp end definition loop_susp_unit_counit (X : pType) - : loop_susp_counit (Susp X) ∘* Susp_functor (loop_susp_unit X) ~* pid (Susp X) := + : loop_susp_counit (psusp X) ∘* psusp_functor (loop_susp_unit X) ~* pid (psusp X) := begin induction X with X x, fconstructor, { intro x', induction x', @@ -193,7 +193,7 @@ namespace susp begin fapply equiv.MK, { intro f, exact ap1 f ∘* loop_susp_unit X}, - { intro g, exact loop_susp_counit Y ∘* Susp_functor g}, + { intro g, exact loop_susp_counit Y ∘* psusp_functor g}, { intro g, apply eq_of_phomotopy, esimp, refine !pwhisker_right !ap1_compose ⬝* _, refine !passoc ⬝* _, @@ -202,7 +202,7 @@ namespace susp refine !pwhisker_right !loop_susp_counit_unit ⬝* _, apply pid_comp}, { intro f, apply eq_of_phomotopy, esimp, - refine !pwhisker_left !Susp_functor_compose ⬝* _, + refine !pwhisker_left !psusp_functor_compose ⬝* _, refine !passoc⁻¹* ⬝* _, refine !pwhisker_right !loop_susp_counit_natural⁻¹* ⬝* _, refine !passoc ⬝* _, @@ -210,7 +210,7 @@ namespace susp apply comp_pid}, end - definition susp_adjoint_loop_nat_right (f : Susp X →* Y) (g : Y →* Z) + definition susp_adjoint_loop_nat_right (f : psusp X →* Y) (g : Y →* Z) : susp_adjoint_loop X Z (g ∘* f) ~* ap1 g ∘* susp_adjoint_loop X Y f := begin esimp [susp_adjoint_loop], @@ -220,12 +220,12 @@ namespace susp end definition susp_adjoint_loop_nat_left (f : Y →* Ω Z) (g : X →* Y) - : (susp_adjoint_loop X Z)⁻¹ (f ∘* g) ~* (susp_adjoint_loop Y Z)⁻¹ f ∘* Susp_functor g := + : (susp_adjoint_loop X Z)⁻¹ (f ∘* g) ~* (susp_adjoint_loop Y Z)⁻¹ f ∘* psusp_functor g := begin esimp [susp_adjoint_loop], refine _ ⬝* !passoc⁻¹*, apply pwhisker_left, - apply Susp_functor_compose + apply psusp_functor_compose end end susp diff --git a/hott/homotopy/wedge.hlean b/hott/homotopy/wedge.hlean index 74e7aecf49..1c1bd4d7a7 100644 --- a/hott/homotopy/wedge.hlean +++ b/hott/homotopy/wedge.hlean @@ -9,12 +9,12 @@ import hit.pointed_pushout .connectedness open eq pushout pointed pType unit -definition Wedge (A B : Type*) : Type* := Pushout (pconst Unit A) (pconst Unit B) +definition pwedge (A B : Type*) : Type* := ppushout (pconst punit A) (pconst punit B) namespace wedge -- TODO maybe find a cleaner proof - protected definition unit (A : Type*) : A ≃* Wedge Unit A := + protected definition unit (A : Type*) : A ≃* pwedge punit A := begin fapply pequiv_of_pmap, { fapply pmap.mk, intro a, apply pinr a, apply respect_pt }, diff --git a/hott/types/lift.hlean b/hott/types/lift.hlean index 13fdd7a084..26236eeee5 100644 --- a/hott/types/lift.hlean +++ b/hott/types/lift.hlean @@ -7,7 +7,7 @@ Theorems about lift -/ import ..function -open eq equiv equiv.ops is_equiv is_trunc +open eq equiv equiv.ops is_equiv is_trunc pointed namespace lift @@ -138,6 +138,12 @@ namespace lift apply ua_refl} end + definition plift [constructor] (A : pType.{u}) : pType.{max u v} := + pType.mk (lift A) (up pt) + + definition plift_functor [constructor] {A B : Type*} (f : A →* B) : plift A →* plift B := + pmap.mk (lift_functor f) (ap up (respect_pt f)) + -- is_trunc_lift is defined in init.trunc diff --git a/hott/types/nat/hott.hlean b/hott/types/nat/hott.hlean index 8ca4d04767..d23f5fda72 100644 --- a/hott/types/nat/hott.hlean +++ b/hott/types/nat/hott.hlean @@ -6,9 +6,9 @@ Author: Floris van Doorn Theorems about the natural numbers specific to HoTT -/ -import .order +import .order types.pointed -open is_trunc unit empty eq equiv algebra +open is_trunc unit empty eq equiv algebra pointed namespace nat definition is_prop_le [instance] (n m : ℕ) : is_prop (n ≤ m) := @@ -114,4 +114,7 @@ namespace nat rewrite [↑nat.decode,↑nat.refl,v_0] end + definition pointed_nat [instance] [constructor] : pointed ℕ := + pointed.mk 0 + end nat diff --git a/hott/types/pointed.hlean b/hott/types/pointed.hlean index f9d739ee7a..ea710e7d47 100644 --- a/hott/types/pointed.hlean +++ b/hott/types/pointed.hlean @@ -16,8 +16,6 @@ structure pType := (carrier : Type) (Point : carrier) -open pType - notation `Type*` := pType namespace pointed @@ -25,6 +23,8 @@ namespace pointed variables {A B : Type} definition pt [unfold 2] [H : pointed A] := point A + definition Point [unfold 1] (A : Type*) := pType.Point A + definition carrier [unfold 1] (A : Type*) := pType.carrier A protected definition Mk [constructor] {A : Type} (a : A) := pType.mk A a protected definition MK [constructor] (A : Type) (a : A) := pType.mk A a protected definition mk' [constructor] (A : Type) [H : pointed A] : Type* := @@ -57,29 +57,29 @@ namespace pointed definition pointed_bool [instance] [constructor] : pointed bool := pointed.mk ff - definition Prod [constructor] (A B : Type*) : Type* := + definition pprod [constructor] (A B : Type*) : Type* := pointed.mk' (A × B) - infixr ` ×* `:35 := Prod + infixr ` ×* `:35 := pprod - definition Bool [constructor] : Type* := + definition pbool [constructor] : Type* := pointed.mk' bool - definition Unit [constructor] : Type* := + definition punit [constructor] : Type* := pointed.Mk unit.star definition pointed_fun_closed [constructor] (f : A → B) [H : pointed A] : pointed B := pointed.mk (f pt) - definition Loop_space [reducible] [constructor] (A : Type*) : Type* := + definition ploop_space [reducible] [constructor] (A : Type*) : Type* := pointed.mk' (point A = point A) - definition Iterated_loop_space [unfold 1] [reducible] : ℕ → Type* → Type* - | Iterated_loop_space 0 X := X - | Iterated_loop_space (n+1) X := Loop_space (Iterated_loop_space n X) + definition iterated_ploop_space [unfold 1] [reducible] : ℕ → Type* → Type* + | iterated_ploop_space 0 X := X + | iterated_ploop_space (n+1) X := ploop_space (iterated_ploop_space n X) - prefix `Ω`:(max+5) := Loop_space - notation `Ω[`:95 n:0 `] `:0 A:95 := Iterated_loop_space n A + prefix `Ω`:(max+5) := ploop_space + notation `Ω[`:95 n:0 `] `:0 A:95 := iterated_ploop_space n A definition rfln [constructor] [reducible] {A : Type*} {n : ℕ} : Ω[n] A := pt definition refln [constructor] [reducible] (A : Type*) (n : ℕ) : Ω[n] A := pt @@ -106,7 +106,6 @@ namespace pointed { intro x, induction x with X x, reflexivity}, end - definition add_point [constructor] (A : Type) : Type* := pointed.Mk (none : option A) postfix `₊`:(max+1) := add_point @@ -121,14 +120,14 @@ namespace pointed begin induction n with n IH, { reflexivity}, - { exact ap Loop_space IH} + { exact ap ploop_space IH} 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} + { exact ap ploop_space IH} end definition loop_space_succ_eq_out (n : ℕ) : Ω[succ n] A = Ω(Ω[n] A) := @@ -138,9 +137,9 @@ namespace pointed /- 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 := + transport carrier (ap ploop_space (loop_space_succ_eq_in A n)) (p ⬝ q) + = transport carrier (ap ploop_space (loop_space_succ_eq_in A n)) p + ⬝ transport carrier (ap ploop_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, @@ -263,7 +262,7 @@ namespace pointed -- } -- end - definition pmap_bool_equiv (B : Type*) : map₊ Bool B ≃ B := + definition pmap_bool_equiv (B : Type*) : map₊ pbool B ≃ B := begin fapply equiv.MK, { intro f, cases f with f p, exact f tt}, @@ -293,7 +292,7 @@ namespace pointed begin induction n with n IH, { exact f}, - { esimp [Iterated_loop_space], exact ap1 IH} + { esimp [iterated_ploop_space], exact ap1 IH} end definition pcast [constructor] {A B : Type*} (p : A = B) : A →* B := diff --git a/hott/types/trunc.hlean b/hott/types/trunc.hlean index 8d1ef90473..f1d6bd9bfd 100644 --- a/hott/types/trunc.hlean +++ b/hott/types/trunc.hlean @@ -150,10 +150,10 @@ namespace is_trunc : 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 _, + { intro A, esimp [iterated_ploop_space], transitivity _, { apply is_trunc_succ_iff_is_trunc_loop, apply le.refl}, { apply pi_iff_pi, intro a, esimp, apply is_prop_iff_is_contr, reflexivity}}, - { intro A, esimp [Iterated_loop_space], + { intro A, esimp [iterated_ploop_space], transitivity _, apply @is_trunc_succ_iff_is_trunc_loop @n, esimp, constructor, apply pi_iff_pi, intro a, transitivity _, apply IH, transitivity _, apply pi_iff_pi, intro p, @@ -165,7 +165,7 @@ namespace is_trunc : is_trunc (n.-2.+1) A ↔ (Π(a : A), is_contr (Ω[n](pointed.Mk a))) := begin induction n with n, - { esimp [sub_two,Iterated_loop_space], apply iff.intro, + { esimp [sub_two,iterated_ploop_space], apply iff.intro, intro H a, exact is_contr_of_inhabited_prop a, intro H, apply is_prop_of_imp_is_contr, exact H}, { apply is_trunc_iff_is_contr_loop_succ},