From 4e2cc660616c8ff6a4d8831c33dcd4010f39db98 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Mon, 15 Feb 2016 15:18:07 -0500 Subject: [PATCH] style(*): rename is_hprop/is_hset to is_prop/is_set --- hott/algebra/category/category.hlean | 2 +- .../category/constructions/comma.hlean | 6 +- .../algebra/category/constructions/cone.hlean | 8 +-- .../category/constructions/discrete.hlean | 8 +-- .../category/constructions/finite_cats.hlean | 12 ++-- .../category/constructions/functor.hlean | 4 +- .../category/constructions/initial.hlean | 4 +- .../category/constructions/opposite.hlean | 2 +- hott/algebra/category/constructions/sum.hlean | 6 +- .../category/constructions/terminal.hlean | 4 +- hott/algebra/category/functor/adjoint.hlean | 8 +-- .../algebra/category/functor/attributes.hlean | 14 ++--- hott/algebra/category/functor/basic.hlean | 14 ++--- .../category/functor/equivalence.hlean | 10 ++-- hott/algebra/category/functor/yoneda.hlean | 6 +- hott/algebra/category/groupoid.hlean | 4 +- hott/algebra/category/iso.hlean | 12 ++-- hott/algebra/category/limits/colimits.hlean | 22 +++---- hott/algebra/category/limits/limits.hlean | 22 +++---- hott/algebra/category/limits/set.hlean | 6 +- hott/algebra/category/nat_trans.hlean | 6 +- hott/algebra/category/precategory.hlean | 16 ++--- hott/algebra/category/strict.hlean | 6 +- hott/algebra/group.hlean | 12 ++-- hott/algebra/homotopy_group.hlean | 8 +-- hott/algebra/hott.hlean | 10 ++-- hott/algebra/trunc_group.hlean | 2 +- hott/choice.hlean | 26 ++++---- hott/cubical/square.hlean | 10 ++-- hott/function.hlean | 46 +++++++------- hott/hit/coeq.hlean | 8 +-- hott/hit/colimit.hlean | 16 ++--- hott/hit/pushout.hlean | 10 ++-- hott/hit/quotient.hlean | 8 +-- hott/hit/set_quotient.hlean | 32 +++++----- hott/hit/trunc.hlean | 2 +- hott/homotopy/circle.hlean | 4 +- hott/homotopy/connectedness.hlean | 4 +- hott/homotopy/sphere.hlean | 2 +- hott/hprop_trunc.hlean | 8 +-- hott/init/hedberg.hlean | 6 +- hott/init/trunc.hlean | 60 +++++++++---------- hott/init/util.hlean | 4 +- hott/logic.hlean | 6 +- hott/types/bool.hlean | 6 +- hott/types/eq.hlean | 6 +- hott/types/equiv.hlean | 42 ++++++------- hott/types/fiber.hlean | 2 +- hott/types/fin.hlean | 14 ++--- hott/types/int/basic.hlean | 2 +- hott/types/list.hlean | 2 +- hott/types/nat/basic.hlean | 2 +- hott/types/nat/hott.hlean | 24 ++++---- hott/types/pi.hlean | 10 ++-- hott/types/pointed2.hlean | 2 +- hott/types/pullback.hlean | 2 +- hott/types/sigma.hlean | 14 ++--- hott/types/sum.hlean | 30 +++++----- hott/types/trunc.hlean | 48 +++++++-------- hott/types/univ.hlean | 14 ++--- src/library/class_instance_resolution.cpp | 6 +- src/library/class_instance_resolution.h | 2 +- src/library/constants.cpp | 24 ++++---- src/library/constants.h | 6 +- src/library/constants.txt | 6 +- src/library/tactic/inversion_tactic.cpp | 10 ++-- src/library/type_context.cpp | 2 +- src/library/util.cpp | 2 +- src/library/util.h | 2 +- tests/lean/simplifier1.hlean | 2 +- 70 files changed, 384 insertions(+), 384 deletions(-) diff --git a/hott/algebra/category/category.hlean b/hott/algebra/category/category.hlean index e07f82ab0..dc0a85f8d 100644 --- a/hott/algebra/category/category.hlean +++ b/hott/algebra/category/category.hlean @@ -116,7 +116,7 @@ namespace category apply eq_of_fn_eq_fn !category.sigma_char, fapply sigma_eq, { induction C, induction D, esimp, exact precategory_eq @p q}, - { unfold is_univalent, apply is_hprop.elimo}, + { unfold is_univalent, apply is_prop.elimo}, end definition category_eq_of_equiv {ob : Type} diff --git a/hott/algebra/category/constructions/comma.hlean b/hott/algebra/category/constructions/comma.hlean index f6477420a..5f51b89d1 100644 --- a/hott/algebra/category/constructions/comma.hlean +++ b/hott/algebra/category/constructions/comma.hlean @@ -98,7 +98,7 @@ namespace category { intro u, exact (comma_morphism.mk u.1 u.2.1 u.2.2)}, { intro f, cases f with g h p p', exact ⟨g, h, p⟩}, { intro f, cases f with g h p p', esimp, - apply ap (comma_morphism.mk' g h p), apply is_hprop.elim}, + apply ap (comma_morphism.mk' g h p), apply is_prop.elim}, { intro u, cases u with u1 u2, cases u2 with u2 u3, reflexivity}, end @@ -113,8 +113,8 @@ namespace category begin cases f with g h p₁ p₁', cases f' with g' h' p₂ p₂', cases p, cases q, apply ap011 (comma_morphism.mk' g' h'), - apply is_hprop.elim, - apply is_hprop.elim + apply is_prop.elim, + apply is_prop.elim end definition comma_compose (g : comma_morphism y z) (f : comma_morphism x y) : comma_morphism x z := diff --git a/hott/algebra/category/constructions/cone.hlean b/hott/algebra/category/constructions/cone.hlean index cfa52ac23..00be3a142 100644 --- a/hott/algebra/category/constructions/cone.hlean +++ b/hott/algebra/category/constructions/cone.hlean @@ -60,7 +60,7 @@ namespace category theorem cone_hom_eq {f f' : cone_hom x y} (q : cone_to_hom f = cone_to_hom f') : f = f' := begin induction f, induction f', esimp at *, induction q, apply ap (cone_hom.mk f), - apply @is_hprop.elim, apply pi.is_trunc_pi, intro x, apply is_trunc_eq, -- type class fails + apply @is_prop.elim, apply pi.is_trunc_pi, intro x, apply is_trunc_eq, -- type class fails end variable (F) @@ -120,7 +120,7 @@ namespace category { intro v, exact cone_iso.mk v.1 v.2}, { intro v, induction v with f p, fapply sigma_eq: esimp, { apply iso_eq, reflexivity}, - { apply is_hprop.elimo, apply is_trunc_pi, intro i, apply is_hprop_hom_eq}}, + { apply is_prop.elimo, apply is_trunc_pi, intro i, apply is_prop_hom_eq}}, { intro h, esimp, apply iso_eq, apply cone_hom_eq, reflexivity}, end @@ -134,8 +134,8 @@ namespace category { intro v, induction v with p q, induction x with c η, induction y with c' η', esimp at *, induction p, esimp, fapply sigma_eq: esimp, { apply c_cone_obj_eq}, - { apply is_hprop.elimo, apply is_trunc_pi, intro i, apply is_hprop_hom_eq}}, - { intro r, induction r, esimp, induction x, esimp, apply ap02, apply is_hprop.elim}, + { apply is_prop.elimo, apply is_trunc_pi, intro i, apply is_prop_hom_eq}}, + { intro r, induction r, esimp, induction x, esimp, apply ap02, apply is_prop.elim}, end section is_univalent diff --git a/hott/algebra/category/constructions/discrete.hlean b/hott/algebra/category/constructions/discrete.hlean index 553f1fce0..c2e6b9da0 100644 --- a/hott/algebra/category/constructions/discrete.hlean +++ b/hott/algebra/category/constructions/discrete.hlean @@ -31,16 +31,16 @@ namespace category definition Groupoid_of_1_type [constructor] (A : Type) [H : is_trunc 1 A] : Groupoid := groupoid.Mk _ (groupoid_of_1_type A) - definition discrete_precategory [constructor] (A : Type) [H : is_hset A] : precategory A := + definition discrete_precategory [constructor] (A : Type) [H : is_set A] : precategory A := precategory_of_1_type A - definition discrete_groupoid [constructor] (A : Type) [H : is_hset A] : groupoid A := + definition discrete_groupoid [constructor] (A : Type) [H : is_set A] : groupoid A := groupoid_of_1_type A - definition Discrete_precategory [constructor] (A : Type) [H : is_hset A] : Precategory := + definition Discrete_precategory [constructor] (A : Type) [H : is_set A] : Precategory := precategory.Mk (discrete_precategory A) - definition Discrete_groupoid [constructor] (A : Type) [H : is_hset A] : Groupoid := + definition Discrete_groupoid [constructor] (A : Type) [H : is_set A] : Groupoid := groupoid.Mk _ (discrete_groupoid A) definition c2 [constructor] : Precategory := Discrete_precategory bool diff --git a/hott/algebra/category/constructions/finite_cats.hlean b/hott/algebra/category/constructions/finite_cats.hlean index 78a2d339b..2ff326f3d 100644 --- a/hott/algebra/category/constructions/finite_cats.hlean +++ b/hott/algebra/category/constructions/finite_cats.hlean @@ -14,7 +14,7 @@ open bool unit is_trunc sum eq functor equiv namespace category variables {A : Type} (R : A → A → Type) (H : Π⦃a b c⦄, R a b → R b c → empty) - [HR : Πa b, is_hset (R a b)] [HA : is_trunc 1 A] + [HR : Πa b, is_set (R a b)] [HA : is_trunc 1 A] include H HR HA @@ -63,7 +63,7 @@ namespace category | f2 : equalizer_category_hom ff tt open equalizer_category_hom - theorem is_hset_equalizer_category_hom (b₁ b₂ : bool) : is_hset (equalizer_category_hom b₁ b₂) := + theorem is_set_equalizer_category_hom (b₁ b₂ : bool) : is_set (equalizer_category_hom b₁ b₂) := begin assert H : Πb b', equalizer_category_hom b b' ≃ bool.rec (bool.rec empty bool) (λb, empty) b b', { intro b b', fapply equiv.MK, @@ -75,7 +75,7 @@ namespace category induction b₁: induction b₂: exact _ end - local attribute is_hset_equalizer_category_hom [instance] + local attribute is_set_equalizer_category_hom [instance] definition equalizer_category [constructor] : Precategory := sparse_category equalizer_category_hom @@ -107,8 +107,8 @@ namespace category | f2 : pullback_category_hom BL BR open pullback_category_hom - theorem is_hset_pullback_category_hom (b₁ b₂ : pullback_category_ob) - : is_hset (pullback_category_hom b₁ b₂) := + theorem is_set_pullback_category_hom (b₁ b₂ : pullback_category_ob) + : is_set (pullback_category_hom b₁ b₂) := begin assert H : Πb b', pullback_category_hom b b' ≃ pullback_category_ob.rec (λb, empty) (λb, empty) @@ -122,7 +122,7 @@ namespace category induction b₁: induction b₂: exact _ end - local attribute is_hset_pullback_category_hom pullback_category_ob_decidable_equality [instance] + local attribute is_set_pullback_category_hom pullback_category_ob_decidable_equality [instance] definition pullback_category [constructor] : Precategory := sparse_category pullback_category_hom diff --git a/hott/algebra/category/constructions/functor.hlean b/hott/algebra/category/constructions/functor.hlean index debbfe89f..93534f2c1 100644 --- a/hott/algebra/category/constructions/functor.hlean +++ b/hott/algebra/category/constructions/functor.hlean @@ -47,7 +47,7 @@ namespace functor fapply (apd011 nat_trans.mk), apply eq_of_homotopy, intro c, apply left_inverse, apply eq_of_homotopy, intros, apply eq_of_homotopy, intros, apply eq_of_homotopy, intros, - apply is_hset.elim + apply is_set.elim end definition nat_trans_right_inverse : η ∘n nat_trans_inverse η = 1 := @@ -55,7 +55,7 @@ namespace functor fapply (apd011 nat_trans.mk), apply eq_of_homotopy, intro c, apply right_inverse, apply eq_of_homotopy, intros, apply eq_of_homotopy, intros, apply eq_of_homotopy, intros, - apply is_hset.elim + apply is_set.elim end definition is_natural_iso [constructor] : is_iso η := diff --git a/hott/algebra/category/constructions/initial.hlean b/hott/algebra/category/constructions/initial.hlean index 0cf3dfcb0..e73038823 100644 --- a/hott/algebra/category/constructions/initial.hlean +++ b/hott/algebra/category/constructions/initial.hlean @@ -38,10 +38,10 @@ namespace category definition initial_functor_op (C : Precategory) : (initial_functor C)ᵒᵖᶠ = initial_functor Cᵒᵖ := - by apply @is_hprop.elim (0 ⇒ Cᵒᵖ) + by apply @is_prop.elim (0 ⇒ Cᵒᵖ) definition initial_functor_comp {C D : Precategory} (F : C ⇒ D) : F ∘f initial_functor C = initial_functor D := - by apply @is_hprop.elim (0 ⇒ D) + by apply @is_prop.elim (0 ⇒ D) end category diff --git a/hott/algebra/category/constructions/opposite.hlean b/hott/algebra/category/constructions/opposite.hlean index a1994060b..1af224bc6 100644 --- a/hott/algebra/category/constructions/opposite.hlean +++ b/hott/algebra/category/constructions/opposite.hlean @@ -21,7 +21,7 @@ namespace category (λ a b f, !id_right) (λ a b f, !id_left) (λ a, !id_id) - (λ a b, !is_hset_hom) + (λ a b, !is_set_hom) definition Opposite [reducible] [constructor] (C : Precategory) : Precategory := precategory.Mk (opposite C) diff --git a/hott/algebra/category/constructions/sum.hlean b/hott/algebra/category/constructions/sum.hlean index 9af9b5130..0460a0d0a 100644 --- a/hott/algebra/category/constructions/sum.hlean +++ b/hott/algebra/category/constructions/sum.hlean @@ -19,12 +19,12 @@ namespace category sum.rec (λc, sum.rec (λc', lift (c ⟶ c')) (λd, lift empty)) (λd, sum.rec (λc, lift empty) (λd', lift (d ⟶ d'))) - theorem is_hset_sum_hom {obC : Type} {obD : Type} + theorem is_set_sum_hom {obC : Type} {obD : Type} (C : precategory obC) (D : precategory obD) (x y : obC + obD) - : is_hset (sum_hom C D x y) := + : is_set (sum_hom C D x y) := by induction x: induction y: esimp at *: exact _ - local attribute is_hset_sum_hom [instance] + local attribute is_set_sum_hom [instance] definition precategory_sum [constructor] [instance] (obC obD : Type) [C : precategory obC] [D : precategory obD] : precategory (obC + obD) := diff --git a/hott/algebra/category/constructions/terminal.hlean b/hott/algebra/category/constructions/terminal.hlean index 4449a1b82..444107903 100644 --- a/hott/algebra/category/constructions/terminal.hlean +++ b/hott/algebra/category/constructions/terminal.hlean @@ -32,8 +32,8 @@ namespace category is_contr.mk (terminal_functor C) begin intro F, fapply functor_eq, - { intro x, apply @is_hprop.elim unit}, - { intro x y f, apply @is_hprop.elim unit} + { intro x, apply @is_prop.elim unit}, + { intro x y f, apply @is_prop.elim unit} end definition terminal_functor_op (C : Precategory) diff --git a/hott/algebra/category/functor/adjoint.hlean b/hott/algebra/category/functor/adjoint.hlean index 75a4fb9b2..7121c9af7 100644 --- a/hott/algebra/category/functor/adjoint.hlean +++ b/hott/algebra/category/functor/adjoint.hlean @@ -43,15 +43,15 @@ namespace category abbreviation counit_unit_eq [unfold 4] := @is_left_adjoint.H abbreviation unit_counit_eq [unfold 4] := @is_left_adjoint.K - theorem is_hprop_is_left_adjoint [instance] {C : Category} {D : Precategory} (F : C ⇒ D) - : is_hprop (is_left_adjoint F) := + theorem is_prop_is_left_adjoint [instance] {C : Category} {D : Precategory} (F : C ⇒ D) + : is_prop (is_left_adjoint F) := begin - apply is_hprop.mk, + apply is_prop.mk, intro G G', cases G with G η ε H K, cases G' with G' η' ε' H' K', assert lem₁ : Π(p : G = G'), p ▸ η = η' → p ▸ ε = ε' → is_left_adjoint.mk G η ε H K = is_left_adjoint.mk G' η' ε' H' K', { intros p q r, induction p, induction q, induction r, esimp, - apply apd011 (is_left_adjoint.mk G η ε) !is_hprop.elim !is_hprop.elim}, + apply apd011 (is_left_adjoint.mk G η ε) !is_prop.elim !is_prop.elim}, assert lem₂ : Π (d : carrier D), (to_fun_hom G (natural_map ε' d) ∘ natural_map η (to_fun_ob G' d)) ∘ diff --git a/hott/algebra/category/functor/attributes.hlean b/hott/algebra/category/functor/attributes.hlean index 1534c5e9c..223d00795 100644 --- a/hott/algebra/category/functor/attributes.hlean +++ b/hott/algebra/category/functor/attributes.hlean @@ -117,24 +117,24 @@ namespace category apply is_equiv_of_is_surjective_of_is_embedding, end - theorem is_hprop_fully_faithful [instance] (F : C ⇒ D) : is_hprop (fully_faithful F) := + theorem is_prop_fully_faithful [instance] (F : C ⇒ D) : is_prop (fully_faithful F) := by unfold fully_faithful; exact _ - theorem is_hprop_full [instance] (F : C ⇒ D) : is_hprop (full F) := + theorem is_prop_full [instance] (F : C ⇒ D) : is_prop (full F) := by unfold full; exact _ - theorem is_hprop_faithful [instance] (F : C ⇒ D) : is_hprop (faithful F) := + theorem is_prop_faithful [instance] (F : C ⇒ D) : is_prop (faithful F) := by unfold faithful; exact _ - theorem is_hprop_essentially_surjective [instance] (F : C ⇒ D) - : is_hprop (essentially_surjective F) := + theorem is_prop_essentially_surjective [instance] (F : C ⇒ D) + : is_prop (essentially_surjective F) := by unfold essentially_surjective; exact _ - theorem is_hprop_is_weak_equivalence [instance] (F : C ⇒ D) : is_hprop (is_weak_equivalence F) := + theorem is_prop_is_weak_equivalence [instance] (F : C ⇒ D) : is_prop (is_weak_equivalence F) := by unfold is_weak_equivalence; exact _ definition fully_faithful_equiv (F : C ⇒ D) : fully_faithful F ≃ (faithful F × full F) := - equiv_of_is_hprop (λH, (faithful_of_fully_faithful F, full_of_fully_faithful F)) + equiv_of_is_prop (λH, (faithful_of_fully_faithful F, full_of_fully_faithful F)) (λH, fully_faithful_of_full_of_faithful (pr1 H) (pr2 H)) /- alternative proof using direct calculation with equivalences diff --git a/hott/algebra/category/functor/basic.hlean b/hott/algebra/category/functor/basic.hlean index c7110b707..9a7f6007f 100644 --- a/hott/algebra/category/functor/basic.hlean +++ b/hott/algebra/category/functor/basic.hlean @@ -56,7 +56,7 @@ namespace functor {H₂ : Π(a b : C), hom a b → hom (F₂ a) (F₂ b)} (id₁ id₂ comp₁ comp₂) (pF : F₁ = F₂) (pH : pF ▸ H₁ = H₂) : functor.mk F₁ H₁ id₁ comp₁ = functor.mk F₂ H₂ id₂ comp₂ := - apd01111 functor.mk pF pH !is_hprop.elim !is_hprop.elim + apd01111 functor.mk pF pH !is_prop.elim !is_prop.elim definition functor_eq' {F₁ F₂ : C ⇒ D} : Π(p : to_fun_ob F₁ = to_fun_ob F₂), (transport (λx, Πa b f, hom (x a) (x b)) p @(to_fun_hom F₁) = @(to_fun_hom F₂)) → F₁ = F₂ := @@ -181,10 +181,10 @@ namespace functor q (respect_comp F g f) end qed section - local attribute precategory.is_hset_hom [instance] [priority 1001] + local attribute precategory.is_set_hom [instance] [priority 1001] local attribute trunctype.struct [instance] [priority 1] -- remove after #842 is closed - protected theorem is_hset_functor [instance] - [HD : is_hset D] : is_hset (functor C D) := + protected theorem is_set_functor [instance] + [HD : is_set D] : is_set (functor C D) := by apply is_trunc_equiv_closed; apply functor.sigma_char end @@ -193,8 +193,8 @@ namespace functor (id comp) : functor_mk_eq' id id comp comp (idpath F) (idpath H) = idp := begin fapply apd011 (apd01111 functor.mk idp idp), - apply is_hset.elim, - apply is_hset.elim + apply is_set.elim, + apply is_set.elim end definition functor_eq'_idp (F : C ⇒ D) : functor_eq' idp idp = (idpath F) := @@ -210,7 +210,7 @@ namespace functor theorem functor_eq2' {F₁ F₂ : C ⇒ D} {p₁ p₂ : to_fun_ob F₁ = to_fun_ob F₂} (q₁ q₂) (r : p₁ = p₂) : functor_eq' p₁ q₁ = functor_eq' p₂ q₂ := - by cases r; apply (ap (functor_eq' p₂)); apply is_hprop.elim + by cases r; apply (ap (functor_eq' p₂)); apply is_prop.elim theorem functor_eq2 {F₁ F₂ : C ⇒ D} (p q : F₁ = F₂) (r : ap010 to_fun_ob p ~ ap010 to_fun_ob q) : p = q := diff --git a/hott/algebra/category/functor/equivalence.hlean b/hott/algebra/category/functor/equivalence.hlean index 8b7e520ef..ecfb179e3 100644 --- a/hott/algebra/category/functor/equivalence.hlean +++ b/hott/algebra/category/functor/equivalence.hlean @@ -228,8 +228,8 @@ namespace category definition equivalence_of_isomorphism [constructor] (F : C ≅c D) : C ≃c D := equivalence.mk F _ - theorem is_hprop_is_equivalence [instance] {C : Category} {D : Precategory} (F : C ⇒ D) - : is_hprop (is_equivalence F) := + theorem is_prop_is_equivalence [instance] {C : Category} {D : Precategory} (F : C ⇒ D) + : is_prop (is_equivalence F) := begin assert f : is_equivalence F ≃ Σ(H : is_left_adjoint F), is_iso (unit F) × is_iso (counit F), { fapply equiv.MK, @@ -241,7 +241,7 @@ namespace category apply is_trunc_equiv_closed_rev, exact f, end - theorem is_hprop_is_isomorphism [instance] (F : C ⇒ D) : is_hprop (is_isomorphism F) := + theorem is_prop_is_isomorphism [instance] (F : C ⇒ D) : is_prop (is_isomorphism F) := by unfold is_isomorphism; exact _ /- closure properties -/ @@ -332,13 +332,13 @@ namespace category definition equivalence_eq {C : Category} {D : Precategory} {F F' : C ≃c D} (p : equivalence.to_functor F = equivalence.to_functor F') : F = F' := begin - induction F, induction F', exact apd011 equivalence.mk p !is_hprop.elim + induction F, induction F', exact apd011 equivalence.mk p !is_prop.elim end definition isomorphism_eq {F F' : C ≅c D} (p : isomorphism.to_functor F = isomorphism.to_functor F') : F = F' := begin - induction F, induction F', exact apd011 isomorphism.mk p !is_hprop.elim + induction F, induction F', exact apd011 isomorphism.mk p !is_prop.elim end definition is_equiv_isomorphism_of_equivalence [constructor] (C D : Category) diff --git a/hott/algebra/category/functor/yoneda.hlean b/hott/algebra/category/functor/yoneda.hlean index 8d50af170..99f7af386 100644 --- a/hott/algebra/category/functor/yoneda.hlean +++ b/hott/algebra/category/functor/yoneda.hlean @@ -138,12 +138,12 @@ namespace yoneda section set_option apply.class_instance false - definition is_hprop_representable {C : Category} (F : Cᵒᵖ ⇒ cset) - : is_hprop (is_representable F) := + definition is_prop_representable {C : Category} (F : Cᵒᵖ ⇒ cset) + : is_prop (is_representable F) := begin fapply is_trunc_equiv_closed, { exact proof fiber.sigma_char ɏ F qed ⬝e sigma.sigma_equiv_sigma_id (λc, !eq_equiv_iso)}, - { apply function.is_hprop_fiber_of_is_embedding, apply is_embedding_yoneda_embedding} + { apply function.is_prop_fiber_of_is_embedding, apply is_embedding_yoneda_embedding} end end diff --git a/hott/algebra/category/groupoid.hlean b/hott/algebra/category/groupoid.hlean index 815c07ba8..4642a7d9a 100644 --- a/hott/algebra/category/groupoid.hlean +++ b/hott/algebra/category/groupoid.hlean @@ -27,7 +27,7 @@ namespace category begin fapply groupoid.mk, fapply precategory.mk, intros, exact A, - intros, apply (@group.is_hset_carrier A G), + intros, apply (@group.is_set_carrier A G), intros [a, b, c, g, h], exact (@group.mul A G g h), intro a, exact (@group.one A G), intros, exact (@group.mul_assoc A G h g f)⁻¹, @@ -43,7 +43,7 @@ namespace category begin fapply group.mk, intro f g, apply (comp f g), - apply is_hset_hom, + apply is_set_hom, intros f g h, apply (assoc f g h)⁻¹, apply (ID a), intro f, apply id_left, diff --git a/hott/algebra/category/iso.hlean b/hott/algebra/category/iso.hlean index e370c5724..7c52c9f52 100644 --- a/hott/algebra/category/iso.hlean +++ b/hott/algebra/category/iso.hlean @@ -114,16 +114,16 @@ namespace iso [Hf : is_iso f] [Hg : is_iso g] : is_iso (g ∘ f) := !is_iso_of_split_epi_of_split_mono - theorem is_hprop_is_iso [instance] (f : hom a b) : is_hprop (is_iso f) := + theorem is_prop_is_iso [instance] (f : hom a b) : is_prop (is_iso f) := begin - apply is_hprop.mk, intro H H', + apply is_prop.mk, intro H H', cases H with g li ri, cases H' with g' li' ri', fapply (apd0111 (@is_iso.mk ob C a b f)), apply left_inverse_eq_right_inverse, apply li, apply ri', - apply is_hprop.elim, - apply is_hprop.elim, + apply is_prop.elim, + apply is_prop.elim, end end iso open iso @@ -175,7 +175,7 @@ namespace iso definition iso_mk_eq {f f' : a ⟶ b} [H : is_iso f] [H' : is_iso f'] (p : f = f') : iso.mk f _ = iso.mk f' _ := - apd011 iso.mk p !is_hprop.elim + apd011 iso.mk p !is_prop.elim variable {C} definition iso_eq {f f' : a ≅ b} (p : to_hom f = to_hom f') : f = f' := @@ -194,7 +194,7 @@ namespace iso end -- The type of isomorphisms between two objects is a set - definition is_hset_iso [instance] : is_hset (a ≅ b) := + definition is_set_iso [instance] : is_set (a ≅ b) := begin apply is_trunc_is_equiv_closed, apply equiv.to_is_equiv (!iso.sigma_char), diff --git a/hott/algebra/category/limits/colimits.hlean b/hott/algebra/category/limits/colimits.hlean index 38e96450b..5625db6bd 100644 --- a/hott/algebra/category/limits/colimits.hlean +++ b/hott/algebra/category/limits/colimits.hlean @@ -29,15 +29,15 @@ namespace category !center definition hom_initial_eq [H : is_initial c'] (f f' : c' ⟶ c) : f = f' := - !is_hprop.elim + !is_prop.elim definition eq_initial_morphism [H : is_initial c'] (f : c' ⟶ c) : f = initial_morphism c c' := - !is_hprop.elim + !is_prop.elim definition initial_iso_initial {c c' : ob} (H : is_initial c) (K : is_initial c') : c ≅ c' := iso_of_opposite_iso (@terminal_iso_terminal _ (opposite C) _ _ H K) - theorem is_hprop_is_initial [instance] : is_hprop (is_initial c) := _ + theorem is_prop_is_initial [instance] : is_prop (is_initial c) := _ omit C @@ -56,9 +56,9 @@ namespace category initial_iso_initial (@has_initial_object.is_initial D H₁) (@has_initial_object.is_initial D H₂) set_option pp.coercions true - theorem is_hprop_has_initial_object [instance] (D : Category) - : is_hprop (has_initial_object D) := - is_hprop_has_terminal_object (Category_opposite D) + theorem is_prop_has_initial_object [instance] (D : Category) + : is_prop (has_initial_object D) := + is_prop_has_terminal_object (Category_opposite D) variable (D) abbreviation has_colimits_of_shape := has_limits_of_shape Dᵒᵖ Iᵒᵖ @@ -76,12 +76,12 @@ namespace category section open pi - theorem is_hprop_has_colimits_of_shape [instance] (D : Category) (I : Precategory) - : is_hprop (has_colimits_of_shape D I) := - is_hprop_has_limits_of_shape (Category_opposite D) _ + theorem is_prop_has_colimits_of_shape [instance] (D : Category) (I : Precategory) + : is_prop (has_colimits_of_shape D I) := + is_prop_has_limits_of_shape (Category_opposite D) _ - theorem is_hprop_is_cocomplete [instance] (D : Category) : is_hprop (is_cocomplete D) := - is_hprop_is_complete (Category_opposite D) + theorem is_prop_is_cocomplete [instance] (D : Category) : is_prop (is_cocomplete D) := + is_prop_is_complete (Category_opposite D) end variables {D I} (F : I ⇒ D) [H : has_colimits_of_shape D I] {i j : I} diff --git a/hott/algebra/category/limits/limits.hlean b/hott/algebra/category/limits/limits.hlean index 286d13fb9..3a1d5f8fc 100644 --- a/hott/algebra/category/limits/limits.hlean +++ b/hott/algebra/category/limits/limits.hlean @@ -26,17 +26,17 @@ namespace category !center definition hom_terminal_eq [H : is_terminal c'] (f f' : c ⟶ c') : f = f' := - !is_hprop.elim + !is_prop.elim definition eq_terminal_morphism [H : is_terminal c'] (f : c ⟶ c') : f = terminal_morphism c c' := - !is_hprop.elim + !is_prop.elim definition terminal_iso_terminal (c c' : ob) [H : is_terminal c] [K : is_terminal c'] : c ≅ c' := iso.MK !terminal_morphism !terminal_morphism !hom_terminal_eq !hom_terminal_eq local attribute is_terminal [reducible] - theorem is_hprop_is_terminal [instance] : is_hprop (is_terminal c) := + theorem is_prop_is_terminal [instance] : is_prop (is_terminal c) := _ omit C @@ -53,13 +53,13 @@ namespace category : @terminal_object D H₁ ≅ @terminal_object D H₂ := !terminal_iso_terminal - theorem is_hprop_has_terminal_object [instance] (D : Category) - : is_hprop (has_terminal_object D) := + theorem is_prop_has_terminal_object [instance] (D : Category) + : is_prop (has_terminal_object D) := begin - apply is_hprop.mk, intro t₁ t₂, induction t₁ with d₁ H₁, induction t₂ with d₂ H₂, + apply is_prop.mk, intro t₁ t₂, induction t₁ with d₁ H₁, induction t₂ with d₂ H₂, assert p : d₁ = d₂, { apply eq_of_iso, apply terminal_iso_terminal}, - induction p, exact ap _ !is_hprop.elim + induction p, exact ap _ !is_prop.elim end variable (D) @@ -79,12 +79,12 @@ namespace category section open pi - theorem is_hprop_has_limits_of_shape [instance] (D : Category) (I : Precategory) - : is_hprop (has_limits_of_shape D I) := - by apply is_trunc_pi; intro F; exact is_hprop_has_terminal_object (Category_cone F) + theorem is_prop_has_limits_of_shape [instance] (D : Category) (I : Precategory) + : is_prop (has_limits_of_shape D I) := + by apply is_trunc_pi; intro F; exact is_prop_has_terminal_object (Category_cone F) local attribute is_complete [reducible] - theorem is_hprop_is_complete [instance] (D : Category) : is_hprop (is_complete D) := _ + theorem is_prop_is_complete [instance] (D : Category) : is_prop (is_complete D) := _ end variables {D I} diff --git a/hott/algebra/category/limits/set.hlean b/hott/algebra/category/limits/set.hlean index 3d2d2c2ea..deb0f189b 100644 --- a/hott/algebra/category/limits/set.hlean +++ b/hott/algebra/category/limits/set.hlean @@ -49,7 +49,7 @@ namespace category apply eq_of_homotopy, intro x, fapply sigma_eq: esimp, { apply eq_of_homotopy, intro i, exact (ap10 (q i) x)⁻¹}, { with_options [elaborator.ignore_instances true] -- TODO: fix - ( refine is_hprop.elimo _ _ _; + ( refine is_prop.elimo _ _ _; refine is_trunc_pi _ _; intro i; refine is_trunc_pi _ _; intro j; refine is_trunc_pi _ _; intro f; @@ -73,7 +73,7 @@ namespace category fapply cone_obj.mk, { fapply trunctype.mk, { apply set_quotient (is_cocomplete_set_cone_rel.{u v w} I F)}, - { apply is_hset_set_quotient}}, + { apply is_set_set_quotient}}, { fapply nat_trans.mk, { intro i x, esimp, apply class_of, exact ⟨i, x⟩}, { intro i j f, esimp, apply eq_of_homotopy, intro y, apply eq_of_rel, esimp, @@ -99,7 +99,7 @@ namespace category { esimp, intro h, induction h with f q, apply cone_hom_eq, esimp at *, apply eq_of_homotopy, refine set_quotient.rec _ _, { intro v, induction v with i x, esimp, exact (ap10 (q i) x)⁻¹}, - { intro v w r, apply is_hprop.elimo}}}, + { intro v w r, apply is_prop.elimo}}}, end end category diff --git a/hott/algebra/category/nat_trans.hlean b/hott/algebra/category/nat_trans.hlean index e430ab2c1..b7421ff7e 100644 --- a/hott/algebra/category/nat_trans.hlean +++ b/hott/algebra/category/nat_trans.hlean @@ -52,7 +52,7 @@ namespace nat_trans (nat₂ : Π (a b : C) (f : hom a b), G f ∘ η₂ a = η₂ b ∘ F f) (p : η₁ ~ η₂) : nat_trans.mk η₁ nat₁ = nat_trans.mk η₂ nat₂ := - apd011 nat_trans.mk (eq_of_homotopy p) !is_hprop.elim + apd011 nat_trans.mk (eq_of_homotopy p) !is_prop.elim definition nat_trans_eq {η₁ η₂ : F ⟹ G} : natural_map η₁ ~ natural_map η₂ → η₁ = η₂ := by induction η₁; induction η₂; apply nat_trans_mk_eq @@ -82,10 +82,10 @@ namespace nat_trans intro S, fapply sigma_eq, { apply eq_of_homotopy, intro a, apply idp}, - { apply is_hprop.elimo} + { apply is_prop.elimo} end - definition is_hset_nat_trans [instance] : is_hset (F ⟹ G) := + definition is_set_nat_trans [instance] : is_set (F ⟹ G) := by apply is_trunc_is_equiv_closed; apply (equiv.to_is_equiv !nat_trans.sigma_char) definition change_natural_map [constructor] (η : F ⟹ G) (f : Π (a : C), F a ⟶ G a) diff --git a/hott/algebra/category/precategory.hlean b/hott/algebra/category/precategory.hlean index 71652857c..dcf4bdaab 100644 --- a/hott/algebra/category/precategory.hlean +++ b/hott/algebra/category/precategory.hlean @@ -28,10 +28,10 @@ namespace category (id_left : Π ⦃a b : ob⦄ (f : hom a b), comp !ID f = f) (id_right : Π ⦃a b : ob⦄ (f : hom a b), comp f !ID = f) (id_id : Π (a : ob), comp !ID !ID = ID a) - (is_hset_hom : Π(a b : ob), is_hset (hom a b)) + (is_set_hom : Π(a b : ob), is_set (hom a b)) -- attribute precategory [multiple-instances] --this is not used anywhere - attribute precategory.is_hset_hom [instance] + attribute precategory.is_set_hom [instance] infixr ∘ := precategory.comp -- input ⟶ using \--> (this is a different arrow than \-> (→)) @@ -48,15 +48,15 @@ namespace category abbreviation id_left [unfold 2] := @precategory.id_left abbreviation id_right [unfold 2] := @precategory.id_right abbreviation id_id [unfold 2] := @precategory.id_id - abbreviation is_hset_hom [unfold 2] := @precategory.is_hset_hom + abbreviation is_set_hom [unfold 2] := @precategory.is_set_hom - definition is_hprop_hom_eq {ob : Type} [C : precategory ob] {x y : ob} (f g : x ⟶ y) - : is_hprop (f = g) := + definition is_prop_hom_eq {ob : Type} [C : precategory ob] {x y : ob} (f g : x ⟶ y) + : is_prop (f = g) := _ -- the constructor you want to use in practice protected definition precategory.mk [constructor] {ob : Type} (hom : ob → ob → Type) - [hset : Π (a b : ob), is_hset (hom a b)] + [hset : Π (a b : ob), is_set (hom a b)] (comp : Π ⦃a b c : ob⦄, hom b c → hom a b → hom a c) (ID : Π (a : ob), hom a a) (ass : Π ⦃a b c d : ob⦄ (h : hom c d) (g : hom b c) (f : hom a b), comp h (comp g f) = comp (comp h g) f) @@ -179,7 +179,7 @@ namespace category assert K : ID1 = ID2, { apply eq_of_homotopy, intro a, exact !ir'⁻¹ ⬝ !il}, induction K, - apply ap0111111 (precategory.mk' hom1 comp1 ID1): apply is_hprop.elim + apply ap0111111 (precategory.mk' hom1 comp1 ID1): apply is_prop.elim end @@ -211,7 +211,7 @@ namespace category assert K : ID1 = ID2, { apply eq_of_homotopy, intros, apply r}, induction H, induction K, - apply ap0111111 (precategory.mk' hom1 comp1 ID1): apply is_hprop.elim + apply ap0111111 (precategory.mk' hom1 comp1 ID1): apply is_prop.elim end -/ diff --git a/hott/algebra/category/strict.hlean b/hott/algebra/category/strict.hlean index a39a413ca..241fe32d6 100644 --- a/hott/algebra/category/strict.hlean +++ b/hott/algebra/category/strict.hlean @@ -10,12 +10,12 @@ open is_trunc eq namespace category structure strict_precategory [class] (ob : Type) extends precategory ob := - mk' :: (is_hset_ob : is_hset ob) + mk' :: (is_set_ob : is_set ob) - attribute strict_precategory.is_hset_ob [instance] + attribute strict_precategory.is_set_ob [instance] definition strict_precategory.mk [reducible] {ob : Type} (C : precategory ob) - (H : is_hset ob) : strict_precategory ob := + (H : is_set ob) : strict_precategory ob := precategory.rec_on C strict_precategory.mk' H structure Strict_precategory : Type := diff --git a/hott/algebra/group.hlean b/hott/algebra/group.hlean index 0a5d02ce2..f7c3cd08f 100644 --- a/hott/algebra/group.hlean +++ b/hott/algebra/group.hlean @@ -19,10 +19,10 @@ variable {A : Type} namespace algebra structure semigroup [class] (A : Type) extends has_mul A := -(is_hset_carrier : is_hset A) +(is_set_carrier : is_set A) (mul_assoc : Πa b c, mul (mul a b) c = mul a (mul b c)) -attribute semigroup.is_hset_carrier [instance] +attribute semigroup.is_set_carrier [instance] definition mul.assoc [s : semigroup A] (a b c : A) : a * b * c = a * (b * c) := !semigroup.mul_assoc @@ -60,10 +60,10 @@ abbreviation eq_of_mul_eq_mul_right' := @mul.right_cancel /- additive semigroup -/ structure add_semigroup [class] (A : Type) extends has_add A := -(is_hset_carrier : is_hset A) +(is_set_carrier : is_set A) (add_assoc : Πa b c, add (add a b) c = add a (add b c)) -attribute add_semigroup.is_hset_carrier [instance] +attribute add_semigroup.is_set_carrier [instance] definition add.assoc [s : add_semigroup A] (a b c : A) : a + b + c = a + (b + c) := !add_semigroup.add_assoc @@ -128,7 +128,7 @@ definition add_monoid.to_monoid {A : Type} [s : add_monoid A] : monoid A := one := add_monoid.zero A, mul_one := add_monoid.add_zero, one_mul := add_monoid.zero_add, - is_hset_carrier := _ + is_set_carrier := _ ⦄ definition add_comm_monoid.to_comm_monoid {A : Type} [s : add_comm_monoid A] : comm_monoid A := @@ -585,7 +585,7 @@ definition group_of_add_group (A : Type) [G : add_group A] : group A := mul_one := add_zero, inv := has_neg.neg, mul_left_inv := add.left_inv, - is_hset_carrier := _⦄ + is_set_carrier := _⦄ namespace norm_num reveal add.assoc diff --git a/hott/algebra/homotopy_group.hlean b/hott/algebra/homotopy_group.hlean index ce2db14c8..00dce6fea 100644 --- a/hott/algebra/homotopy_group.hlean +++ b/hott/algebra/homotopy_group.hlean @@ -50,12 +50,12 @@ namespace eq prefix `π₁`:95 := fundamental_group open equiv unit - theorem trivial_homotopy_of_is_hset (A : Type*) [H : is_hset A] (n : ℕ) : πG[n+1] A = G0 := + theorem trivial_homotopy_of_is_set (A : Type*) [H : is_set A] (n : ℕ) : πG[n+1] A = G0 := begin apply trivial_group_of_is_contr, apply is_trunc_trunc_of_is_trunc, apply is_contr_loop_of_is_trunc, - apply is_trunc_succ_succ_of_is_hset + apply is_trunc_succ_succ_of_is_set end definition homotopy_group_succ_out (A : Type*) (n : ℕ) : πG[ n +1] A = π₁ Ω[n] A := idp @@ -77,8 +77,8 @@ namespace eq exact ap (Group_homotopy_group n) !loop_space_succ_eq_in⁻¹} end - theorem trivial_homotopy_of_is_hset_loop_space {A : Type*} {n : ℕ} (m : ℕ) (H : is_hset (Ω[n] A)) + theorem trivial_homotopy_of_is_set_loop_space {A : Type*} {n : ℕ} (m : ℕ) (H : is_set (Ω[n] A)) : πG[m+n+1] A = G0 := - !homotopy_group_add ⬝ !trivial_homotopy_of_is_hset + !homotopy_group_add ⬝ !trivial_homotopy_of_is_set end eq diff --git a/hott/algebra/hott.hlean b/hott/algebra/hott.hlean index 53bddbf99..869268c93 100644 --- a/hott/algebra/hott.hlean +++ b/hott/algebra/hott.hlean @@ -50,11 +50,11 @@ namespace algebra ... = Hm G1 (Hi g) : by rewrite Gh4 ... = Hi g : Gh2), cases same_one, cases same_inv, - have ps : Gs = Hs, from !is_hprop.elim, - have ph1 : Gh1 = Hh1, from !is_hprop.elim, - have ph2 : Gh2 = Hh2, from !is_hprop.elim, - have ph3 : Gh3 = Hh3, from !is_hprop.elim, - have ph4 : Gh4 = Hh4, from !is_hprop.elim, + have ps : Gs = Hs, from !is_prop.elim, + have ph1 : Gh1 = Hh1, from !is_prop.elim, + have ph2 : Gh2 = Hh2, from !is_prop.elim, + have ph3 : Gh3 = Hh3, from !is_prop.elim, + have ph4 : Gh4 = Hh4, from !is_prop.elim, cases ps, cases ph1, cases ph2, cases ph3, cases ph4, reflexivity end diff --git a/hott/algebra/trunc_group.hlean b/hott/algebra/trunc_group.hlean index 969961d0a..a3911246d 100644 --- a/hott/algebra/trunc_group.hlean +++ b/hott/algebra/trunc_group.hlean @@ -86,7 +86,7 @@ namespace algebra mul_one := trunc_mul_one, inv := trunc_inv, mul_left_inv := trunc_mul_left_inv, - is_hset_carrier := _⦄ + is_set_carrier := _⦄ definition trunc_comm_group [constructor] (mul_comm : ∀a b, mul a b = mul b a) : comm_group G := diff --git a/hott/choice.hlean b/hott/choice.hlean index e03e1b5b7..bbf2ad871 100644 --- a/hott/choice.hlean +++ b/hott/choice.hlean @@ -7,22 +7,22 @@ namespace choice -- 3.8.1. The axiom of choice. definition AC [reducible] := Π (X : Type.{u}) (A : X -> Type.{u}) (P : Π x, A x -> Type.{u}), - is_hset X -> (Π x, is_hset (A x)) -> (Π x a, is_hprop (P x a)) -> + is_set X -> (Π x, is_set (A x)) -> (Π x a, is_prop (P x a)) -> (Π x, ∥ Σ a, P x a ∥) -> ∥ Σ f, Π x, P x (f x) ∥ -- 3.8.3. Corresponds to the assertion that -- "the cartesian product of a family of nonempty sets is nonempty". definition AC_cart [reducible] := Π (X : Type.{u}) (A : X -> Type.{u}), - is_hset X -> (Π x, is_hset (A x)) -> (Π x, ∥ A x ∥) -> ∥ Π x, A x ∥ + is_set X -> (Π x, is_set (A x)) -> (Π x, ∥ A x ∥) -> ∥ Π x, A x ∥ -- A slight variant of AC with a modified (equivalent) codomain. definition AC' [reducible] := Π (X : Type.{u}) (A : X -> Type.{u}) (P : Π x, A x -> Type.{u}), - is_hset X -> (Π x, is_hset (A x)) -> (Π x a, is_hprop (P x a)) + is_set X -> (Π x, is_set (A x)) -> (Π x a, is_prop (P x a)) -> (Π x, ∥ Σ a, P x a ∥) -> ∥ Π x, Σ a : A x, P x a ∥ -- The equivalence of AC and AC' follows from the equivalence of their codomains. definition AC_equiv_AC' : AC.{u} ≃ AC'.{u} := - equiv_of_is_hprop + equiv_of_is_prop (λ H X A P HX HA HP HI, trunc_functor _ (to_fun !sigma_pi_equiv_pi_sigma) (H X A P HX HA HP HI)) (λ H X A P HX HA HP HI, trunc_functor _ (to_inv !sigma_pi_equiv_pi_sigma) (H X A P HX HA HP HI)) @@ -39,7 +39,7 @@ namespace choice -- Which is enough to show AC' ≃ AC_cart, since both are hprops. definition AC'_equiv_AC_cart : AC'.{u} ≃ AC_cart.{u} := - equiv_of_is_hprop AC_cart_of_AC'.{u} AC'_of_AC_cart.{u} + equiv_of_is_prop AC_cart_of_AC'.{u} AC'_of_AC_cart.{u} -- 3.8.2. AC ≃ AC_cart follows by transitivity. definition AC_equiv_AC_cart : AC.{u} ≃ AC_cart.{u} := @@ -52,21 +52,21 @@ namespace choice definition Y : X -> Type.{1} := λ x, x0 = x - definition not_is_hset_X : ¬ is_hset X := + definition not_is_set_X : ¬ is_set X := begin - intro H, apply not_is_hprop_bool_eq_bool, + intro H, apply not_is_prop_bool_eq_bool, apply @is_trunc_equiv_closed (x0 = x0), apply equiv.symm !equiv_subtype end - definition is_hset_x1 (x : X) : is_hset x.1 := + definition is_set_x1 (x : X) : is_set x.1 := by cases x; induction a_1; cases a_1; exact _ - definition is_hset_Yx (x : X) : is_hset (Y x) := + definition is_set_Yx (x : X) : is_set (Y x) := begin apply @is_trunc_equiv_closed _ _ _ !equiv_subtype, apply @is_trunc_equiv_closed _ _ _ (equiv.symm !eq_equiv_equiv), - apply is_trunc_equiv; repeat (apply is_hset_x1) + apply is_trunc_equiv; repeat (apply is_set_x1) end definition trunc_Yx (x : X) : ∥ Y x ∥ := @@ -81,8 +81,8 @@ namespace choice -- 3.8.5. There exists a type X and a family Y : X → U such that each Y(x) is a set, -- but such that (3.8.3) is false. definition X_must_be_hset : Σ (X : Type.{1}) (Y : X -> Type.{1}) - (HA : Π x : X, is_hset (Y x)), ¬ ((Π x : X, ∥ Y x ∥) -> ∥ Π x : X, Y x ∥) := - ⟨X, Y, is_hset_Yx, λ H, trunc.rec_on (H trunc_Yx) - (λ H0, not_is_hset_X (@is_trunc_of_is_contr _ _ (is_contr.mk x0 H0)))⟩ + (HA : Π x : X, is_set (Y x)), ¬ ((Π x : X, ∥ Y x ∥) -> ∥ Π x : X, Y x ∥) := + ⟨X, Y, is_set_Yx, λ H, trunc.rec_on (H trunc_Yx) + (λ H0, not_is_set_X (@is_trunc_of_is_contr _ _ (is_contr.mk x0 H0)))⟩ end choice diff --git a/hott/cubical/square.hlean b/hott/cubical/square.hlean index 3608f41df..7be7f296e 100644 --- a/hott/cubical/square.hlean +++ b/hott/cubical/square.hlean @@ -48,7 +48,7 @@ namespace eq definition hdeg_square_idp (p : a = a') : hdeg_square (refl p) = hrfl := by cases p; reflexivity - + definition vdeg_square_idp (p : a = a') : vdeg_square (refl p) = vrfl := by cases p; reflexivity @@ -483,8 +483,8 @@ namespace eq by induction s₂;induction s₁;constructor open is_trunc - definition is_hset.elims [H : is_hset A] : square p₁₀ p₁₂ p₀₁ p₂₁ := - square_of_eq !is_hset.elim + definition is_set.elims [H : is_set A] : square p₁₀ p₁₂ p₀₁ p₂₁ := + square_of_eq !is_set.elim -- definition square_of_con_inv_hsquare {p₁ p₂ p₃ p₄ : a₁ = a₂} -- {t : p₁ = p₂} {b : p₃ = p₄} {l : p₁ = p₃} {r : p₂ = p₄} @@ -525,11 +525,11 @@ namespace eq /- Matching eq_hconcat with hconcat etc. -/ -- TODO maybe rename hconcat_eq and the like? variable (s₁₁) - definition ph_eq_pv_h_vp {p : a₀₀ = a₀₂} (r : p = p₀₁) : + definition ph_eq_pv_h_vp {p : a₀₀ = a₀₂} (r : p = p₀₁) : r ⬝ph s₁₁ = !idp_con⁻¹ ⬝pv ((hdeg_square r) ⬝h s₁₁) ⬝vp !idp_con := by cases r; cases s₁₁; esimp - definition hdeg_h_eq_pv_ph_vp {p : a₀₀ = a₀₂} (r : p = p₀₁) : + definition hdeg_h_eq_pv_ph_vp {p : a₀₀ = a₀₂} (r : p = p₀₁) : hdeg_square r ⬝h s₁₁ = !idp_con ⬝pv (r ⬝ph s₁₁) ⬝vp !idp_con⁻¹ := by cases r; cases s₁₁; esimp diff --git a/hott/function.hlean b/hott/function.hlean index 5b60eac26..5e7deafb7 100644 --- a/hott/function.hlean +++ b/hott/function.hlean @@ -57,54 +57,54 @@ namespace function : f a = f a' → a = a' := (ap f)⁻¹ - definition is_embedding_of_is_injective [HA : is_hset A] [HB : is_hset B] + definition is_embedding_of_is_injective [HA : is_set A] [HB : is_set B] (H : Π(a a' : A), f a = f a' → a = a') : is_embedding f := begin intro a a', fapply adjointify, {exact (H a a')}, - {intro p, apply is_hset.elim}, - {intro p, apply is_hset.elim} + {intro p, apply is_set.elim}, + {intro p, apply is_set.elim} end variable (f) - definition is_hprop_is_embedding [instance] : is_hprop (is_embedding f) := + definition is_prop_is_embedding [instance] : is_prop (is_embedding f) := by unfold is_embedding; exact _ - definition is_embedding_equiv_is_injective [HA : is_hset A] [HB : is_hset B] + definition is_embedding_equiv_is_injective [HA : is_set A] [HB : is_set B] : is_embedding f ≃ (Π(a a' : A), f a = f a' → a = a') := begin fapply equiv.MK, { apply @is_injective_of_is_embedding}, { apply is_embedding_of_is_injective}, - { intro H, apply is_hprop.elim}, - { intro H, apply is_hprop.elim, } + { intro H, apply is_prop.elim}, + { intro H, apply is_prop.elim, } end - definition is_hprop_fiber_of_is_embedding [H : is_embedding f] (b : B) : - is_hprop (fiber f b) := + definition is_prop_fiber_of_is_embedding [H : is_embedding f] (b : B) : + is_prop (fiber f b) := begin - apply is_hprop.mk, intro v w, + apply is_prop.mk, intro v w, induction v with a p, induction w with a' q, induction q, fapply fiber_eq, { esimp, apply is_injective_of_is_embedding p}, { esimp [is_injective_of_is_embedding], symmetry, apply right_inv} end - definition is_hprop_fun_of_is_embedding [H : is_embedding f] : is_trunc_fun -1 f := - is_hprop_fiber_of_is_embedding f + definition is_prop_fun_of_is_embedding [H : is_embedding f] : is_trunc_fun -1 f := + is_prop_fiber_of_is_embedding f - definition is_embedding_of_is_hprop_fun [constructor] [H : is_trunc_fun -1 f] : is_embedding f := + definition is_embedding_of_is_prop_fun [constructor] [H : is_trunc_fun -1 f] : is_embedding f := begin intro a a', fapply adjointify, - { intro p, exact ap point (@is_hprop.elim (fiber f (f a')) _ (fiber.mk a p) (fiber.mk a' idp))}, + { intro p, exact ap point (@is_prop.elim (fiber f (f a')) _ (fiber.mk a p) (fiber.mk a' idp))}, { intro p, rewrite [-ap_compose], esimp, apply ap_con_eq (@point_eq _ _ f (f a'))}, - { intro p, induction p, apply ap (ap point), apply is_hprop_elim_self} + { intro p, induction p, apply ap (ap point), apply is_prop_elim_self} end variable {f} - definition is_surjective_rec_on {P : Type} (H : is_surjective f) (b : B) [Pt : is_hprop P] + definition is_surjective_rec_on {P : Type} (H : is_surjective f) (b : B) [Pt : is_prop P] (IH : fiber f b → P) : P := trunc.rec_on (H b) IH variable (f) @@ -113,7 +113,7 @@ namespace function : is_surjective f := λb, tr (H b) - definition is_hprop_is_surjective [instance] : is_hprop (is_surjective f) := + definition is_prop_is_surjective [instance] : is_prop (is_surjective f) := by unfold is_surjective; exact _ definition is_weakly_constant_ap [instance] [H : is_weakly_constant f] (a a' : A) : @@ -184,8 +184,8 @@ namespace function : is_constant (f ∘ point : fiber f b → B) := is_constant.mk b (λv, by induction v with a p;exact p) - definition is_embedding_of_is_hprop_fiber [H : Π(b : B), is_hprop (fiber f b)] : is_embedding f := - is_embedding_of_is_hprop_fun _ + definition is_embedding_of_is_prop_fiber [H : Π(b : B), is_prop (fiber f b)] : is_embedding f := + is_embedding_of_is_prop_fun _ definition is_retraction_of_is_equiv [instance] [H : is_equiv f] : is_retraction f := is_retraction.mk f⁻¹ (right_inv f) @@ -208,9 +208,9 @@ namespace function local attribute is_equiv_of_is_section_of_is_retraction [instance] [priority 10000] local attribute trunctype.struct [instance] [priority 1] -- remove after #842 is closed variable (f) - definition is_hprop_is_retraction_prod_is_section : is_hprop (is_retraction f × is_section f) := + definition is_prop_is_retraction_prod_is_section : is_prop (is_retraction f × is_section f) := begin - apply is_hprop_of_imp_is_contr, intro H, induction H with H1 H2, + apply is_prop_of_imp_is_contr, intro H, induction H with H1 H2, exact _, end end @@ -233,11 +233,11 @@ namespace function exact ap r (center_eq (is_retraction.sect r b)) ⬝ (is_retraction.right_inverse r b) end - local attribute is_hprop_is_retraction_prod_is_section [instance] + local attribute is_prop_is_retraction_prod_is_section [instance] definition is_retraction_prod_is_section_equiv_is_equiv [constructor] : (is_retraction f × is_section f) ≃ is_equiv f := begin - apply equiv_of_is_hprop, + apply equiv_of_is_prop, intro H, induction H, apply is_equiv_of_is_section_of_is_retraction, intro H, split, repeat exact _ end diff --git a/hott/hit/coeq.hlean b/hott/hit/coeq.hlean index 0cb79870e..27a057e19 100644 --- a/hott/hit/coeq.hlean +++ b/hott/hit/coeq.hlean @@ -74,12 +74,12 @@ parameters {A B : Type.{u}} (f g : A → B) (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 - protected definition rec_hprop {P : coeq → Type} [H : Πx, is_hprop (P x)] + protected definition rec_hprop {P : coeq → Type} [H : Πx, is_prop (P x)] (P_i : Π(x : B), P (coeq_i x)) (y : coeq) : P y := - rec P_i (λa, !is_hprop.elimo) y + rec P_i (λa, !is_prop.elimo) y - protected definition elim_hprop {P : Type} [H : is_hprop P] (P_i : B → P) (y : coeq) : P := - elim P_i (λa, !is_hprop.elim) y + protected definition elim_hprop {P : Type} [H : is_prop P] (P_i : B → P) (y : coeq) : P := + elim P_i (λa, !is_prop.elim) y end diff --git a/hott/hit/colimit.hlean b/hott/hit/colimit.hlean index 93a938e16..4b142b955 100644 --- a/hott/hit/colimit.hlean +++ b/hott/hit/colimit.hlean @@ -85,13 +85,13 @@ section {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 - protected definition rec_hprop {P : colimit → Type} [H : Πx, is_hprop (P x)] + protected definition rec_hprop {P : colimit → Type} [H : Πx, is_prop (P x)] (Pincl : Π⦃i : I⦄ (x : A i), P (ι x)) (y : colimit) : P y := - rec Pincl (λa b, !is_hprop.elimo) y + rec Pincl (λa b, !is_prop.elimo) y - protected definition elim_hprop {P : Type} [H : is_hprop P] (Pincl : Π⦃i : I⦄ (x : A i), P) + protected definition elim_hprop {P : Type} [H : is_prop P] (Pincl : Π⦃i : I⦄ (x : A i), P) (y : colimit) : P := - elim Pincl (λa b, !is_hprop.elim) y + elim Pincl (λa b, !is_prop.elim) y end end colimit @@ -175,13 +175,13 @@ section : transport (elim_type Pincl Pglue) (glue a) = Pglue a := by rewrite [tr_eq_cast_ap_fn,↑elim_type,elim_glue];apply cast_ua_fn - protected definition rec_hprop {P : seq_colim → Type} [H : Πx, is_hprop (P x)] + protected definition rec_hprop {P : seq_colim → Type} [H : Πx, is_prop (P x)] (Pincl : Π⦃n : ℕ⦄ (a : A n), P (sι a)) (aa : seq_colim) : P aa := - rec Pincl (λa b, !is_hprop.elimo) aa + rec Pincl (λa b, !is_prop.elimo) aa - protected definition elim_hprop {P : Type} [H : is_hprop P] (Pincl : Π⦃n : ℕ⦄ (a : A n), P) + protected definition elim_hprop {P : Type} [H : is_prop P] (Pincl : Π⦃n : ℕ⦄ (a : A n), P) : seq_colim → P := - elim Pincl (λa b, !is_hprop.elim) + elim Pincl (λa b, !is_prop.elim) end diff --git a/hott/hit/pushout.hlean b/hott/hit/pushout.hlean index 66b1d263a..478b1b0e0 100644 --- a/hott/hit/pushout.hlean +++ b/hott/hit/pushout.hlean @@ -83,13 +83,13 @@ parameters {TL BL TR : Type} (f : TL → BL) (g : TL → TR) : 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 - protected definition rec_hprop {P : pushout → Type} [H : Πx, is_hprop (P x)] + protected definition rec_hprop {P : pushout → Type} [H : Πx, is_prop (P x)] (Pinl : Π(x : BL), P (inl x)) (Pinr : Π(x : TR), P (inr x)) (y : pushout) := - rec Pinl Pinr (λx, !is_hprop.elimo) y + rec Pinl Pinr (λx, !is_prop.elimo) y - protected definition elim_hprop {P : Type} [H : is_hprop P] (Pinl : BL → P) (Pinr : TR → P) + protected definition elim_hprop {P : Type} [H : is_prop P] (Pinl : BL → P) (Pinr : TR → P) (y : pushout) : P := - elim Pinl Pinr (λa, !is_hprop.elim) y + elim Pinl Pinr (λa, !is_prop.elim) y end end pushout @@ -214,7 +214,7 @@ namespace pushout pushout.transpose g f (pushout.transpose f g x) = x := begin induction x, apply idp, apply idp, - apply eq_pathover, refine _ ⬝hp !ap_id⁻¹, + apply eq_pathover, refine _ ⬝hp !ap_id⁻¹, refine !(ap_compose (pushout.transpose _ _)) ⬝ph _, esimp[pushout.transpose], krewrite [elim_glue, ap_inv, elim_glue, inv_inv], apply hrfl end diff --git a/hott/hit/quotient.hlean b/hott/hit/quotient.hlean index a2bada60f..1a412ec0d 100644 --- a/hott/hit/quotient.hlean +++ b/hott/hit/quotient.hlean @@ -39,11 +39,11 @@ namespace quotient end protected definition rec_hprop {A : Type} {R : A → A → Type} {P : quotient R → Type} - [H : Πx, is_hprop (P x)] (Pc : Π(a : A), P (class_of R a)) (x : quotient R) : P x := - quotient.rec Pc (λa a' H, !is_hprop.elimo) x + [H : Πx, is_prop (P x)] (Pc : Π(a : A), P (class_of R a)) (x : quotient R) : P x := + quotient.rec Pc (λa a' H, !is_prop.elimo) x - protected definition elim_hprop {P : Type} [H : is_hprop P] (Pc : A → P) (x : quotient R) : P := - quotient.elim Pc (λa a' H, !is_hprop.elim) x + protected definition elim_hprop {P : Type} [H : is_prop P] (Pc : A → P) (x : quotient R) : P := + quotient.elim Pc (λa a' H, !is_prop.elim) x protected definition elim_type (Pc : A → Type) (Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a ≃ Pc a') : quotient R → Type := diff --git a/hott/hit/set_quotient.hlean b/hott/hit/set_quotient.hlean index 46bc6cb25..dc6b1ac6d 100644 --- a/hott/hit/set_quotient.hlean +++ b/hott/hit/set_quotient.hlean @@ -23,10 +23,10 @@ section definition eq_of_rel {a a' : A} (H : R a a') : class_of a = class_of a' := ap tr (eq_of_rel _ H) - theorem is_hset_set_quotient [instance] : is_hset set_quotient := + theorem is_set_set_quotient [instance] : is_set set_quotient := begin unfold set_quotient, exact _ end - protected definition rec {P : set_quotient → Type} [Pt : Πaa, is_hset (P aa)] + protected definition rec {P : set_quotient → Type} [Pt : Πaa, is_set (P aa)] (Pc : Π(a : A), P (class_of a)) (Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a =[eq_of_rel H] Pc a') (x : set_quotient) : P x := begin @@ -38,24 +38,24 @@ section end protected definition rec_on [reducible] {P : set_quotient → Type} (x : set_quotient) - [Pt : Πaa, is_hset (P aa)] (Pc : Π(a : A), P (class_of a)) + [Pt : Πaa, is_set (P aa)] (Pc : Π(a : A), P (class_of a)) (Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a =[eq_of_rel H] Pc a') : P x := rec Pc Pp x - theorem rec_eq_of_rel {P : set_quotient → Type} [Pt : Πaa, is_hset (P aa)] + theorem rec_eq_of_rel {P : set_quotient → Type} [Pt : Πaa, is_set (P aa)] (Pc : Π(a : A), P (class_of a)) (Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a =[eq_of_rel H] Pc a') {a a' : A} (H : R a a') : apdo (rec Pc Pp) (eq_of_rel H) = Pp H := - !is_hset.elimo + !is_set.elimo - protected definition elim {P : Type} [Pt : is_hset P] (Pc : A → P) + protected definition elim {P : Type} [Pt : is_set P] (Pc : A → P) (Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a = Pc a') (x : set_quotient) : P := rec Pc (λa a' H, pathover_of_eq (Pp H)) x - protected definition elim_on [reducible] {P : Type} (x : set_quotient) [Pt : is_hset P] + protected definition elim_on [reducible] {P : Type} (x : set_quotient) [Pt : is_set P] (Pc : A → P) (Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a = Pc a') : P := elim Pc Pp x - theorem elim_eq_of_rel {P : Type} [Pt : is_hset P] (Pc : A → P) + theorem elim_eq_of_rel {P : Type} [Pt : is_set 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) = Pp H := begin @@ -63,13 +63,13 @@ section rewrite [▸*,-apdo_eq_pathover_of_eq_ap,↑elim,rec_eq_of_rel], end - protected definition rec_hprop {P : set_quotient → Type} [Pt : Πaa, is_hprop (P aa)] + protected definition rec_hprop {P : set_quotient → Type} [Pt : Πaa, is_prop (P aa)] (Pc : Π(a : A), P (class_of a)) (x : set_quotient) : P x := - rec Pc (λa a' H, !is_hprop.elimo) x + rec Pc (λa a' H, !is_prop.elimo) x - protected definition elim_hprop {P : Type} [Pt : is_hprop P] (Pc : A → P) (x : set_quotient) + protected definition elim_hprop {P : Type} [Pt : is_prop P] (Pc : A → P) (x : set_quotient) : P := - elim Pc (λa a' H, !is_hprop.elim) x + elim Pc (λa a' H, !is_prop.elim) x end end set_quotient @@ -84,11 +84,11 @@ namespace set_quotient variables {A B C : Type} (R : A → A → hprop) (S : B → B → hprop) (T : C → C → hprop) definition is_surjective_class_of : is_surjective (class_of : A → set_quotient R) := - λx, set_quotient.rec_on x (λa, tr (fiber.mk a idp)) (λa a' r, !is_hprop.elimo) + λx, set_quotient.rec_on x (λa, tr (fiber.mk a idp)) (λa a' r, !is_prop.elimo) /- non-dependent universal property -/ - definition set_quotient_arrow_equiv (B : Type) [H : is_hset B] : + definition set_quotient_arrow_equiv (B : Type) [H : is_set B] : (set_quotient R → B) ≃ (Σ(f : A → B), Π(a a' : A), R a a' → f a = f a') := begin fapply equiv.MK, @@ -108,7 +108,7 @@ namespace set_quotient intros a' a'' H1, refine to_inv !trunctype_eq_equiv _, esimp, apply ua, - apply equiv_of_is_hprop, + apply equiv_of_is_prop, { intro H2, exact is_transitive.trans R H2 H1}, { intro H2, apply is_transitive.trans R H2, exact is_symmetric.symm R H1} end @@ -139,7 +139,7 @@ namespace set_quotient { intro b b' s, apply eq_of_rel, apply H, apply is_reflexive.refl R, exact s}}, { intro a a' r, apply eq_of_homotopy, refine set_quotient.rec _ _, { intro b, esimp, apply eq_of_rel, apply H, exact r, apply is_reflexive.refl S}, - { intro b b' s, apply eq_pathover, esimp, apply is_hset.elims}} + { intro b b' s, apply eq_pathover, esimp, apply is_set.elims}} end end set_quotient diff --git a/hott/hit/trunc.hlean b/hott/hit/trunc.hlean index e340a8def..62dcf84c5 100644 --- a/hott/hit/trunc.hlean +++ b/hott/hit/trunc.hlean @@ -117,7 +117,7 @@ namespace trunc definition or.intro_left [reducible] [constructor] (x : X) : X ∨ Y := tr (inl x) definition or.intro_right [reducible] [constructor] (y : Y) : X ∨ Y := tr (inr y) - definition is_contr_of_merely_hprop [H : is_hprop A] (aa : merely A) : is_contr A := + definition is_contr_of_merely_hprop [H : is_prop A] (aa : merely A) : is_contr A := is_contr_of_inhabited_hprop (trunc.rec_on aa id) section diff --git a/hott/homotopy/circle.hlean b/hott/homotopy/circle.hlean index 11bbf1d30..57841b5e8 100644 --- a/hott/homotopy/circle.hlean +++ b/hott/homotopy/circle.hlean @@ -219,7 +219,7 @@ namespace circle exact ap succ p}, { intros n p, rewrite [↑circle.encode, nat_succ_eq_int_succ, neg_succ, -power_con_inv, @con_tr _ circle.code, transport_code_loop_inv, ↑[circle.encode] at p, p, -neg_succ] }}, - { apply pathover_of_tr_eq, apply eq_of_homotopy, intro a, apply @is_hset.elim, + { apply pathover_of_tr_eq, apply eq_of_homotopy, intro a, apply @is_set.elim, esimp, exact _} end end}, { intro p, cases p, exact idp}, end @@ -254,7 +254,7 @@ namespace circle open nat definition homotopy_group_of_circle (n : ℕ) : πG[n+1 +1] S¹. = G0 := begin - refine @trivial_homotopy_of_is_hset_loop_space S¹. 1 n _, + refine @trivial_homotopy_of_is_set_loop_space S¹. 1 n _, apply is_trunc_equiv_closed_rev, apply base_eq_base_equiv end diff --git a/hott/homotopy/connectedness.hlean b/hott/homotopy/connectedness.hlean index bf572a6d9..e6e8355b7 100644 --- a/hott/homotopy/connectedness.hlean +++ b/hott/homotopy/connectedness.hlean @@ -231,7 +231,7 @@ namespace homotopy -- Corollary 7.5.5 definition is_conn_homotopy (n : trunc_index) {A B : Type} {f g : A → B} (p : f ~ g) (H : is_conn_map n f) : is_conn_map n g := - @retract_of_conn_is_conn _ _ (arrow.arrow_hom_of_homotopy p) (arrow.is_retraction_arrow_hom_of_homotopy p) n H + @retract_of_conn_is_conn _ _ (arrow.arrow_hom_of_homotopy p) (arrow.is_retraction_arrow_hom_of_homotopy p) n H -- all types are -2-connected definition minus_two_conn [instance] (A : Type) : is_conn -2 A := @@ -255,7 +255,7 @@ namespace homotopy apply pathover_of_tr_eq, rewrite [transport_eq_Fr,idp_con], revert H, induction n with [n, IH], - { intro H, apply is_hprop.elim }, + { intro H, apply is_prop.elim }, { intros H, change ap (@tr n .+2 (susp A)) (merid a) = ap tr (merid a'), generalize a', diff --git a/hott/homotopy/sphere.hlean b/hott/homotopy/sphere.hlean index 0c612909e..d98af7d79 100644 --- a/hott/homotopy/sphere.hlean +++ b/hott/homotopy/sphere.hlean @@ -190,7 +190,7 @@ namespace is_trunc let H' := iff.elim_left (is_trunc_iff_is_contr_loop n A) H a, 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, + apply is_prop.elim, exact ap10 (ap pmap.to_fun p) x end diff --git a/hott/hprop_trunc.hlean b/hott/hprop_trunc.hlean index 6112166c0..52b44412b 100644 --- a/hott/hprop_trunc.hlean +++ b/hott/hprop_trunc.hlean @@ -35,16 +35,16 @@ namespace is_trunc induction (P a b), apply idp}, end - definition is_hprop_is_trunc [instance] (n : trunc_index) : - Π (A : Type), is_hprop (is_trunc n A) := + definition is_prop_is_trunc [instance] (n : trunc_index) : + Π (A : Type), is_prop (is_trunc n A) := begin induction n, { intro A, apply is_trunc_is_equiv_closed, { apply equiv.to_is_equiv, apply is_contr.sigma_char}, - apply is_hprop.mk, intros, + apply is_prop.mk, intros, fapply sigma_eq, apply x.2, - apply is_hprop.elimo}, + apply is_prop.elimo}, { intro A, apply is_trunc_is_equiv_closed, apply equiv.to_is_equiv, diff --git a/hott/init/hedberg.hlean b/hott/init/hedberg.hlean index 603f23797..ead176120 100644 --- a/hott/init/hedberg.hlean +++ b/hott/init/hedberg.hlean @@ -37,11 +37,11 @@ section eq.rec_on (f (refl x)) rfl, eq.rec_on p aux - definition is_hset_of_decidable_eq : is_hset A := - is_hset.mk A (λ x y p q, calc + definition is_set_of_decidable_eq : is_set A := + is_set.mk A (λ x y p q, calc p = (f (refl x))⁻¹ ⬝ (f p) : aux ... = (f (refl x))⁻¹ ⬝ (f q) : f_const ... = q : aux) end -attribute is_hset_of_decidable_eq [instance] [priority 600] +attribute is_set_of_decidable_eq [instance] [priority 600] diff --git a/hott/init/trunc.hlean b/hott/init/trunc.hlean index efa75fe9f..555e25971 100644 --- a/hott/init/trunc.hlean +++ b/hott/init/trunc.hlean @@ -108,8 +108,8 @@ open nat num is_trunc.trunc_index namespace is_trunc abbreviation is_contr := is_trunc -2 - abbreviation is_hprop := is_trunc -1 - abbreviation is_hset := is_trunc 0 + abbreviation is_prop := is_trunc -1 + abbreviation is_set := is_trunc 0 variables {A B : Type} @@ -184,41 +184,41 @@ namespace is_trunc definition is_trunc_of_is_contr (A : Type) (n : trunc_index) [H : is_contr A] : is_trunc n A := trunc_index.rec_on n H (λn H, _) - definition is_trunc_succ_of_is_hprop (A : Type) (n : trunc_index) [H : is_hprop A] + definition is_trunc_succ_of_is_prop (A : Type) (n : trunc_index) [H : is_prop A] : is_trunc (n.+1) A := is_trunc_of_leq A (show -1 ≤ n.+1, from star) - definition is_trunc_succ_succ_of_is_hset (A : Type) (n : trunc_index) [H : is_hset A] + definition is_trunc_succ_succ_of_is_set (A : Type) (n : trunc_index) [H : is_set A] : is_trunc (n.+2) A := @(is_trunc_of_leq A (show 0 ≤ n.+2, from proof star qed)) H /- hprops -/ - definition is_hprop.elim [H : is_hprop A] (x y : A) : x = y := + definition is_prop.elim [H : is_prop A] (x y : A) : x = y := !center - definition is_contr_of_inhabited_hprop {A : Type} [H : is_hprop A] (x : A) : is_contr A := - is_contr.mk x (λy, !is_hprop.elim) + definition is_contr_of_inhabited_hprop {A : Type} [H : is_prop A] (x : A) : is_contr A := + is_contr.mk x (λy, !is_prop.elim) - theorem is_hprop_of_imp_is_contr {A : Type} (H : A → is_contr A) : is_hprop A := + theorem is_prop_of_imp_is_contr {A : Type} (H : A → is_contr A) : is_prop A := @is_trunc_succ_intro A -2 (λx y, have H2 [visible] : is_contr A, from H x, !is_contr_eq) - theorem is_hprop.mk {A : Type} (H : ∀x y : A, x = y) : is_hprop A := - is_hprop_of_imp_is_contr (λ x, is_contr.mk x (H x)) + theorem is_prop.mk {A : Type} (H : ∀x y : A, x = y) : is_prop A := + is_prop_of_imp_is_contr (λ x, is_contr.mk x (H x)) - theorem is_hprop_elim_self {A : Type} {H : is_hprop A} (x : A) : is_hprop.elim x x = idp := - !is_hprop.elim + theorem is_prop_elim_self {A : Type} {H : is_prop A} (x : A) : is_prop.elim x x = idp := + !is_prop.elim /- hsets -/ - theorem is_hset.mk (A : Type) (H : ∀(x y : A) (p q : x = y), p = q) : is_hset A := - @is_trunc_succ_intro _ _ (λ x y, is_hprop.mk (H x y)) + theorem is_set.mk (A : Type) (H : ∀(x y : A) (p q : x = y), p = q) : is_set A := + @is_trunc_succ_intro _ _ (λ x y, is_prop.mk (H x y)) - definition is_hset.elim [H : is_hset A] ⦃x y : A⦄ (p q : x = y) : p = q := - !is_hprop.elim + definition is_set.elim [H : is_set A] ⦃x y : A⦄ (p q : x = y) : p = q := + !is_prop.elim /- instances -/ @@ -241,16 +241,16 @@ namespace is_trunc definition is_contr_unit : is_contr unit := is_contr.mk star (λp, unit.rec_on p idp) - definition is_hprop_empty : is_hprop empty := - is_hprop.mk (λx, !empty.elim x) + definition is_prop_empty : is_prop empty := + is_prop.mk (λx, !empty.elim x) - local attribute is_contr_unit is_hprop_empty [instance] + local attribute is_contr_unit is_prop_empty [instance] definition is_trunc_unit [instance] (n : trunc_index) : is_trunc n unit := !is_trunc_of_is_contr definition is_trunc_empty [instance] (n : trunc_index) : is_trunc (n.+1) empty := - !is_trunc_succ_of_is_hprop + !is_trunc_succ_of_is_prop /- interaction with equivalences -/ @@ -289,16 +289,16 @@ namespace is_trunc : is_trunc n A := is_trunc_is_equiv_closed n (to_inv f) - definition is_equiv_of_is_hprop [constructor] [HA : is_hprop A] [HB : is_hprop B] + definition is_equiv_of_is_prop [constructor] [HA : is_prop A] [HB : is_prop B] (f : A → B) (g : B → A) : is_equiv f := - is_equiv.mk f g (λb, !is_hprop.elim) (λa, !is_hprop.elim) (λa, !is_hset.elim) + is_equiv.mk f g (λb, !is_prop.elim) (λa, !is_prop.elim) (λa, !is_set.elim) - definition equiv_of_is_hprop [constructor] [HA : is_hprop A] [HB : is_hprop B] + definition equiv_of_is_prop [constructor] [HA : is_prop A] [HB : is_prop B] (f : A → B) (g : B → A) : A ≃ B := - equiv.mk f (is_equiv_of_is_hprop f g) + equiv.mk f (is_equiv_of_is_prop f g) - definition equiv_of_iff_of_is_hprop [unfold 5] [HA : is_hprop A] [HB : is_hprop B] (H : A ↔ B) : A ≃ B := - equiv_of_is_hprop (iff.elim_left H) (iff.elim_right H) + definition equiv_of_iff_of_is_prop [unfold 5] [HA : is_prop A] [HB : is_prop B] (H : A ↔ B) : A ≃ B := + equiv_of_is_prop (iff.elim_left H) (iff.elim_right H) /- truncatedness of lift -/ definition is_trunc_lift [instance] [priority 1450] (A : Type) (n : trunc_index) @@ -324,16 +324,16 @@ namespace is_trunc {a a₂ : A} (p : a = a₂) (c : C a) (c₂ : C a₂) - definition is_hprop.elimo [H : is_hprop (C a)] : c =[p] c₂ := - pathover_of_eq_tr !is_hprop.elim + definition is_prop.elimo [H : is_prop (C a)] : c =[p] c₂ := + pathover_of_eq_tr !is_prop.elim definition is_trunc_pathover [instance] (n : trunc_index) [H : is_trunc (n.+1) (C a)] : is_trunc n (c =[p] c₂) := is_trunc_equiv_closed_rev n !pathover_equiv_eq_tr variables {p c c₂} - theorem is_hset.elimo (q q' : c =[p] c₂) [H : is_hset (C a)] : q = q' := - !is_hprop.elim + theorem is_set.elimo (q q' : c =[p] c₂) [H : is_set (C a)] : q = q' := + !is_prop.elim -- TODO: port "Truncated morphisms" diff --git a/hott/init/util.hlean b/hott/init/util.hlean index 4d5055af6..cf5c8d203 100644 --- a/hott/init/util.hlean +++ b/hott/init/util.hlean @@ -11,6 +11,6 @@ import init.trunc open is_trunc -definition eq_rec_eq.{l₁ l₂} {A : Type.{l₁}} {B : A → Type.{l₂}} [h : is_hset A] {a : A} (b : B a) (p : a = a) : +definition eq_rec_eq.{l₁ l₂} {A : Type.{l₁}} {B : A → Type.{l₂}} [h : is_set A] {a : A} (b : B a) (p : a = a) : b = @eq.rec.{l₂ l₁} A a (λ (a' : A) (h : a = a'), B a') b a p := -eq.rec_on (is_hset.elim (eq.refl a) p) (eq.refl (eq.rec_on (eq.refl a) b)) +eq.rec_on (is_set.elim (eq.refl a) p) (eq.refl (eq.rec_on (eq.refl a) b)) diff --git a/hott/logic.hlean b/hott/logic.hlean index 662148113..ad53a46b4 100644 --- a/hott/logic.hlean +++ b/hott/logic.hlean @@ -9,10 +9,10 @@ import types.pi open eq is_trunc decidable -theorem dif_pos {c : Type} [H : decidable c] [P : is_hprop c] (Hc : c) +theorem dif_pos {c : Type} [H : decidable c] [P : is_prop c] (Hc : c) {A : Type} {t : c → A} {e : ¬ c → A} : dite c t e = t Hc := -by induction H with Hc Hnc; apply ap t; apply is_hprop.elim; apply absurd Hc Hnc +by induction H with Hc Hnc; apply ap t; apply is_prop.elim; apply absurd Hc Hnc theorem dif_neg {c : Type} [H : decidable c] (Hnc : ¬c) {A : Type} {t : c → A} {e : ¬ c → A} : dite c t e = e Hnc := -by induction H with Hc Hnc; apply absurd Hc Hnc; apply ap e; apply is_hprop.elim +by induction H with Hc Hnc; apply absurd Hc Hnc; apply ap e; apply is_prop.elim diff --git a/hott/types/bool.hlean b/hott/types/bool.hlean index 7a316329e..4bef259d6 100644 --- a/hott/types/bool.hlean +++ b/hott/types/bool.hlean @@ -155,9 +155,9 @@ namespace bool assert H2 : bnot = id, from !cast_ua_fn⁻¹ ⬝ ap cast H, absurd (ap10 H2 tt) ff_ne_tt - theorem is_hset_bool : is_hset bool := _ - theorem not_is_hprop_bool_eq_bool : ¬ is_hprop (bool = bool) := - λ H, eq_bnot_ne_idp !is_hprop.elim + theorem is_set_bool : is_set bool := _ + theorem not_is_prop_bool_eq_bool : ¬ is_prop (bool = bool) := + λ H, eq_bnot_ne_idp !is_prop.elim definition bool_equiv_option_unit [constructor] : bool ≃ option unit := begin diff --git a/hott/types/eq.hlean b/hott/types/eq.hlean index 06c47fbc1..b2c0c688a 100644 --- a/hott/types/eq.hlean +++ b/hott/types/eq.hlean @@ -460,7 +460,7 @@ namespace eq (p ⬝ q) ▸ (center (Σa, code a)).2 definition decode' {a : A} (c : code a) : a₀ = a := - (is_hprop.elim ⟨a₀, encode idp⟩ ⟨a, c⟩)..1 + (is_prop.elim ⟨a₀, encode idp⟩ ⟨a, c⟩)..1 definition decode {a : A} (c : code a) : a₀ = a := (decode' (encode idp))⁻¹ ⬝ decode' c @@ -472,8 +472,8 @@ namespace eq { exact decode}, { intro c, unfold [encode, decode, decode'], - induction p, esimp, rewrite [is_hprop_elim_self,▸*,+idp_con], apply tr_eq_of_pathover, - eapply @sigma.rec_on _ _ (λx, x.2 =[(is_hprop.elim ⟨x.1, x.2⟩ ⟨a, c⟩)..1] c) + induction p, esimp, rewrite [is_prop_elim_self,▸*,+idp_con], apply tr_eq_of_pathover, + eapply @sigma.rec_on _ _ (λx, x.2 =[(is_prop.elim ⟨x.1, x.2⟩ ⟨a, c⟩)..1] c) (center (sigma code)), -- BUG(?): induction fails intro a c, apply eq_pr2}, { intro q, induction q, esimp, apply con.left_inv, }, diff --git a/hott/types/equiv.hlean b/hott/types/equiv.hlean index 60d48e3ae..f69e725be 100644 --- a/hott/types/equiv.hlean +++ b/hott/types/equiv.hlean @@ -75,19 +75,19 @@ namespace is_equiv local attribute is_contr_right_inverse [instance] [priority 1600] local attribute is_contr_right_coherence [instance] [priority 1600] - theorem is_hprop_is_equiv [instance] : is_hprop (is_equiv f) := - is_hprop_of_imp_is_contr + theorem is_prop_is_equiv [instance] : is_prop (is_equiv f) := + is_prop_of_imp_is_contr (λ(H : is_equiv f), is_trunc_equiv_closed -2 (equiv.symm !is_equiv.sigma_char')) definition inv_eq_inv {A B : Type} {f f' : A → B} {Hf : is_equiv f} {Hf' : is_equiv f'} (p : f = f') : f⁻¹ = f'⁻¹ := - apd011 inv p !is_hprop.elim + apd011 inv p !is_prop.elim /- contractible fibers -/ definition is_contr_fun_of_is_equiv [H : is_equiv f] : is_contr_fun f := is_contr_fiber_of_is_equiv f - definition is_hprop_is_contr_fun (f : A → B) : is_hprop (is_contr_fun f) := _ + definition is_prop_is_contr_fun (f : A → B) : is_prop (is_contr_fun f) := _ definition is_equiv_of_is_contr_fun [H : is_contr_fun f] : is_equiv f := adjointify _ (λb, point (center (fiber f b))) @@ -98,7 +98,7 @@ namespace is_equiv @is_equiv_of_is_contr_fun _ _ f (λb, @is_contr_fiber_of_is_equiv _ _ _ (H b) _) definition is_equiv_equiv_is_contr_fun : is_equiv f ≃ is_contr_fun f := - equiv_of_is_hprop _ (λH, !is_equiv_of_is_contr_fun) + equiv_of_is_prop _ (λH, !is_equiv_of_is_contr_fun) end is_equiv @@ -129,7 +129,7 @@ namespace equiv definition equiv_mk_eq {f f' : A → B} [H : is_equiv f] [H' : is_equiv f'] (p : f = f') : equiv.mk f H = equiv.mk f' H' := - apd011 equiv.mk p !is_hprop.elim + apd011 equiv.mk p !is_prop.elim definition equiv_eq {f f' : A ≃ B} (p : to_fun f = to_fun f') : f = f' := by (cases f; cases f'; apply (equiv_mk_eq p)) @@ -164,11 +164,11 @@ namespace equiv : is_equiv (ap to_fun : f = f' → to_fun f = to_fun f') := begin fapply adjointify, - {intro p, cases f with f H, cases f' with f' H', cases p, apply ap (mk f'), apply is_hprop.elim}, + {intro p, cases f with f H, cases f' with f' H', cases p, apply ap (mk f'), apply is_prop.elim}, {intro p, cases f with f H, cases f' with f' H', cases p, - apply @concat _ _ (ap to_fun (ap (equiv.mk f') (is_hprop.elim H H'))), {apply idp}, - generalize is_hprop.elim H H', intro q, cases q, apply idp}, - {intro p, cases p, cases f with f H, apply ap (ap (equiv.mk f)), apply is_hset.elim} + apply @concat _ _ (ap to_fun (ap (equiv.mk f') (is_prop.elim H H'))), {apply idp}, + generalize is_prop.elim H H', intro q, cases q, apply idp}, + {intro p, cases p, cases f with f H, apply ap (ap (equiv.mk f)), apply is_set.elim} end definition equiv_pathover {A : Type} {a a' : A} (p : a = a') @@ -179,24 +179,24 @@ namespace equiv { intro a, apply equiv.sigma_char}, { fapply sigma_pathover, esimp, apply arrow_pathover, exact r, - apply is_hprop.elimo} + apply is_prop.elimo} end definition is_contr_equiv (A B : Type) [HA : is_contr A] [HB : is_contr B] : is_contr (A ≃ B) := - begin - apply @is_contr_of_inhabited_hprop, apply is_hprop.mk, - intro x y, cases x with fx Hx, cases y with fy Hy, generalize Hy, - apply (eq_of_homotopy (λ a, !eq_of_is_contr)) ▸ (λ Hy, !is_hprop.elim ▸ rfl), - apply equiv_of_is_contr_of_is_contr + begin + apply @is_contr_of_inhabited_hprop, apply is_prop.mk, + intro x y, cases x with fx Hx, cases y with fy Hy, generalize Hy, + apply (eq_of_homotopy (λ a, !eq_of_is_contr)) ▸ (λ Hy, !is_prop.elim ▸ rfl), + apply equiv_of_is_contr_of_is_contr end - + definition is_trunc_succ_equiv (n : trunc_index) (A B : Type) [HA : is_trunc n.+1 A] [HB : is_trunc n.+1 B] : is_trunc n.+1 (A ≃ B) := @is_trunc_equiv_closed _ _ n.+1 (equiv.symm !equiv.sigma_char) - (@is_trunc_sigma _ _ _ _ (λ f, !is_trunc_succ_of_is_hprop)) - - definition is_trunc_equiv (n : trunc_index) (A B : Type) + (@is_trunc_sigma _ _ _ _ (λ f, !is_trunc_succ_of_is_prop)) + + definition is_trunc_equiv (n : trunc_index) (A B : Type) [HA : is_trunc n A] [HB : is_trunc n B] : is_trunc n (A ≃ B) := - by cases n; apply !is_contr_equiv; apply !is_trunc_succ_equiv + by cases n; apply !is_contr_equiv; apply !is_trunc_succ_equiv end equiv diff --git a/hott/types/fiber.hlean b/hott/types/fiber.hlean index 18a429a48..8375eda73 100644 --- a/hott/types/fiber.hlean +++ b/hott/types/fiber.hlean @@ -105,7 +105,7 @@ namespace fiber { intro a, apply fiber.mk a, reflexivity }, { intro a, reflexivity }, { intro f, cases f with a H, change fiber.mk a (refl star) = fiber.mk a H, - rewrite [is_hset.elim H (refl star)] } + rewrite [is_set.elim H (refl star)] } end definition fiber_const_equiv (A : Type) (a₀ : A) (a : A) diff --git a/hott/types/fin.hlean b/hott/types/fin.hlean index 46dc6a07e..d7fa99e8d 100644 --- a/hott/types/fin.hlean +++ b/hott/types/fin.hlean @@ -28,7 +28,7 @@ begin intro i, cases i with i ilt, reflexivity end -definition is_hset_fin [instance] : is_hset (fin n) := +definition is_set_fin [instance] : is_set (fin n) := begin apply is_trunc_equiv_closed, apply equiv.symm, apply sigma_char, end @@ -36,11 +36,11 @@ end definition eq_of_veq : Π {i j : fin n}, (val i) = j → i = j := begin intro i j, cases i with i ilt, cases j with j jlt, esimp, - intro p, induction p, apply ap (mk i), apply !is_hprop.elim + intro p, induction p, apply ap (mk i), apply !is_prop.elim end definition eq_of_veq_refl (i : fin n) : eq_of_veq (refl (val i)) = idp := -!is_hprop.elim +!is_prop.elim definition veq_of_eq : Π {i j : fin n}, i = j → (val i) = j := by intro i j P; apply ap val; exact P @@ -379,9 +379,9 @@ begin apply decidable.rec, { intro ilt', esimp[val_inj], apply concat, apply ap (λ x, eq.rec_on x _), esimp[eq_of_veq, rfl], reflexivity, - assert H : ilt = ilt', apply is_hprop.elim, cases H, - assert H' : is_hprop.elim (lt_add_of_lt_right ilt 1) (lt_add_of_lt_right ilt 1) = idp, - apply is_hprop.elim, + assert H : ilt = ilt', apply is_prop.elim, cases H, + assert H' : is_prop.elim (lt_add_of_lt_right ilt 1) (lt_add_of_lt_right ilt 1) = idp, + apply is_prop.elim, krewrite H' }, { intro a, contradiction }, end @@ -395,7 +395,7 @@ begin { intro a, apply absurd a !nat.lt_irrefl }, { intro a, esimp[val_inj], apply concat, assert H : (le.antisymm (le_of_lt_succ (lt_succ_self n)) (le_of_not_gt a))⁻¹ = idp, - apply is_hprop.elim, + apply is_prop.elim, apply ap _ H, krewrite eq_of_veq_refl }, end diff --git a/hott/types/int/basic.hlean b/hott/types/int/basic.hlean index 142f3f32d..eb0782041 100644 --- a/hott/types/int/basic.hlean +++ b/hott/types/int/basic.hlean @@ -573,7 +573,7 @@ protected definition integral_domain [reducible] [trans_instance] : integral_dom mul_comm := int.mul_comm, zero_ne_one := int.zero_ne_one, eq_zero_sum_eq_zero_of_mul_eq_zero := @int.eq_zero_sum_eq_zero_of_mul_eq_zero, - is_hset_carrier := is_hset_of_decidable_eq⦄ + is_set_carrier := is_set_of_decidable_eq⦄ definition int_has_sub [reducible] [instance] [priority int.prio] : has_sub int := has_sub.mk has_sub.sub diff --git a/hott/types/list.hlean b/hott/types/list.hlean index 585bb5690..8158114f3 100644 --- a/hott/types/list.hlean +++ b/hott/types/list.hlean @@ -137,7 +137,7 @@ rfl theorem last_congr {l₁ l₂ : list T} (h₁ : l₁ ≠ []) (h₂ : l₂ ≠ []) (h₃ : l₁ = l₂) : last l₁ h₁ = last l₂ h₂ := -apd011 last h₃ !is_hprop.elim +apd011 last h₃ !is_prop.elim theorem last_concat {x : T} : ∀ {l : list T} (h : concat x l ≠ []), last (concat x l) h = x | [] h := rfl diff --git a/hott/types/nat/basic.hlean b/hott/types/nat/basic.hlean index baac4f210..40cfdece1 100644 --- a/hott/types/nat/basic.hlean +++ b/hott/types/nat/basic.hlean @@ -305,7 +305,7 @@ protected definition comm_semiring [reducible] [trans_instance] : comm_semiring zero_mul := nat.zero_mul, mul_zero := nat.mul_zero, mul_comm := nat.mul_comm, - is_hset_carrier:= _⦄ + is_set_carrier:= _⦄ end nat section diff --git a/hott/types/nat/hott.hlean b/hott/types/nat/hott.hlean index bdeaaaee9..8ca4d0476 100644 --- a/hott/types/nat/hott.hlean +++ b/hott/types/nat/hott.hlean @@ -11,32 +11,32 @@ import .order open is_trunc unit empty eq equiv algebra namespace nat - definition is_hprop_le [instance] (n m : ℕ) : is_hprop (n ≤ m) := + definition is_prop_le [instance] (n m : ℕ) : is_prop (n ≤ m) := begin assert lem : Π{n m : ℕ} (p : n ≤ m) (q : n = m), p = q ▸ le.refl n, { intros, cases p, - { assert H' : q = idp, apply is_hset.elim, + { assert H' : q = idp, apply is_set.elim, cases H', reflexivity}, { cases q, exfalso, apply not_succ_le_self a}}, - apply is_hprop.mk, intro H1 H2, induction H2, + apply is_prop.mk, intro H1 H2, induction H2, { apply lem}, { cases H1, { exfalso, apply not_succ_le_self a}, { exact ap le.step !v_0}}, end - definition is_hprop_lt [instance] (n m : ℕ) : is_hprop (n < m) := !is_hprop_le + definition is_prop_lt [instance] (n m : ℕ) : is_prop (n < m) := !is_prop_le definition le_equiv_succ_le_succ (n m : ℕ) : (n ≤ m) ≃ (succ n ≤ succ m) := - equiv_of_is_hprop succ_le_succ le_of_succ_le_succ + equiv_of_is_prop succ_le_succ le_of_succ_le_succ definition le_succ_equiv_pred_le (n m : ℕ) : (n ≤ succ m) ≃ (pred n ≤ m) := - equiv_of_is_hprop pred_le_pred le_succ_of_pred_le + equiv_of_is_prop pred_le_pred le_succ_of_pred_le theorem lt_by_cases_lt {a b : ℕ} {P : Type} (H1 : a < b → P) (H2 : a = b → P) (H3 : a > b → P) (H : a < b) : lt.by_cases H1 H2 H3 = H1 H := begin unfold lt.by_cases, induction (lt.trichotomy a b) with H' H', - { esimp, exact ap H1 !is_hprop.elim}, + { esimp, exact ap H1 !is_prop.elim}, { exfalso, cases H' with H' H', apply lt.irrefl, exact H' ▸ H, exact lt.asymm H H'} end @@ -45,7 +45,7 @@ namespace nat begin unfold lt.by_cases, induction (lt.trichotomy a b) with H' H', { exfalso, apply lt.irrefl, exact H ▸ H'}, - { cases H' with H' H', esimp, exact ap H2 !is_hprop.elim, exfalso, apply lt.irrefl, exact H ▸ H'} + { cases H' with H' H', esimp, exact ap H2 !is_prop.elim, exfalso, apply lt.irrefl, exact H ▸ H'} end theorem lt_by_cases_ge {a b : ℕ} {P : Type} (H1 : a < b → P) (H2 : a = b → P) @@ -53,7 +53,7 @@ namespace nat begin unfold lt.by_cases, induction (lt.trichotomy a b) with H' H', { exfalso, exact lt.asymm H H'}, - { cases H' with H' H', exfalso, apply lt.irrefl, exact H' ▸ H, esimp, exact ap H3 !is_hprop.elim} + { cases H' with H' H', exfalso, apply lt.irrefl, exact H' ▸ H, esimp, exact ap H3 !is_prop.elim} end theorem lt_ge_by_cases_lt {n m : ℕ} {P : Type} (H1 : n < m → P) (H2 : n ≥ m → P) @@ -65,7 +65,7 @@ namespace nat begin unfold [lt_ge_by_cases,lt.by_cases], induction (lt.trichotomy n m) with H' H', { exfalso, apply lt.irrefl, exact lt_of_le_of_lt H H'}, - { cases H' with H' H'; all_goals (esimp; apply ap H2 !is_hprop.elim)} + { cases H' with H' H'; all_goals (esimp; apply ap H2 !is_prop.elim)} end theorem lt_ge_by_cases_le {n m : ℕ} {P : Type} {H1 : n ≤ m → P} {H2 : n ≥ m → P} @@ -73,10 +73,10 @@ namespace nat : lt_ge_by_cases (λH', H1 (le_of_lt H')) H2 = H1 H := begin unfold [lt_ge_by_cases,lt.by_cases], induction (lt.trichotomy n m) with H' H', - { esimp, apply ap H1 !is_hprop.elim}, + { esimp, apply ap H1 !is_prop.elim}, { cases H' with H' H', { esimp, induction H', esimp, symmetry, - exact ap H1 !is_hprop.elim ⬝ Heq idp ⬝ ap H2 !is_hprop.elim}, + exact ap H1 !is_prop.elim ⬝ Heq idp ⬝ ap H2 !is_prop.elim}, { exfalso, apply lt.irrefl, apply lt_of_le_of_lt H H'}} end diff --git a/hott/types/pi.hlean b/hott/types/pi.hlean index 32affc086..9cc874341 100644 --- a/hott/types/pi.hlean +++ b/hott/types/pi.hlean @@ -238,7 +238,7 @@ namespace pi { intro f, exact star}, { intro u a, exact !center}, { intro u, induction u, reflexivity}, - { intro f, apply eq_of_homotopy, intro a, apply is_hprop.elim} + { intro f, apply eq_of_homotopy, intro a, apply is_prop.elim} end /- Interaction with other type constructors -/ @@ -298,15 +298,15 @@ namespace pi theorem is_trunc_not [instance] (n : trunc_index) (A : Type) : is_trunc (n.+1) ¬A := by unfold not;exact _ - theorem is_hprop_pi_eq [instance] [priority 490] (a : A) : is_hprop (Π(a' : A), a = a') := - is_hprop_of_imp_is_contr + theorem is_prop_pi_eq [instance] [priority 490] (a : A) : is_prop (Π(a' : A), a = a') := + is_prop_of_imp_is_contr ( assume (f : Πa', a = a'), assert is_contr A, from is_contr.mk a f, by exact _) /- force type clas resolution -/ - theorem is_hprop_neg (A : Type) : is_hprop (¬A) := _ + theorem is_prop_neg (A : Type) : is_prop (¬A) := _ local attribute ne [reducible] - theorem is_hprop_ne [instance] {A : Type} (a b : A) : is_hprop (a ≠ b) := _ + theorem is_prop_ne [instance] {A : Type} (a b : A) : is_prop (a ≠ b) := _ /- Symmetry of Π -/ definition is_equiv_flip [instance] {P : A → A' → Type} diff --git a/hott/types/pointed2.hlean b/hott/types/pointed2.hlean index 3ff51e5a3..969057aad 100644 --- a/hott/types/pointed2.hlean +++ b/hott/types/pointed2.hlean @@ -87,7 +87,7 @@ namespace pointed 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 + exact apd011 pequiv_of_pmap H !is_prop.elim end definition loop_space_pequiv_rfl diff --git a/hott/types/pullback.hlean b/hott/types/pullback.hlean index 2273fb8c7..bbf0c86ed 100644 --- a/hott/types/pullback.hlean +++ b/hott/types/pullback.hlean @@ -58,7 +58,7 @@ namespace pullback { intro v, induction v with x y p, exact (x, y)}, { intro v, induction v with x y, exact pullback.mk x y idp}, { intro v, induction v, reflexivity}, - { intro v, induction v, esimp, apply ap _ !is_hprop.elim}, + { intro v, induction v, esimp, apply ap _ !is_prop.elim}, end definition pullback_along {f : A₂₀ → A₂₂} (g : A₀₂ → A₂₂) : pullback f g → A₂₀ := diff --git a/hott/types/sigma.hlean b/hott/types/sigma.hlean index 82eed52e5..282b1b2f1 100644 --- a/hott/types/sigma.hlean +++ b/hott/types/sigma.hlean @@ -423,28 +423,28 @@ namespace sigma /- Subtypes (sigma types whose second components are hprops) -/ - definition subtype [reducible] {A : Type} (P : A → Type) [H : Πa, is_hprop (P a)] := + definition subtype [reducible] {A : Type} (P : A → Type) [H : Πa, is_prop (P a)] := Σ(a : A), P a notation [parsing_only] `{` binder `|` r:(scoped:1 P, subtype P) `}` := r /- To prove equality in a subtype, we only need equality of the first component. -/ - definition subtype_eq [H : Πa, is_hprop (B a)] {u v : {a | B a}} : u.1 = v.1 → u = v := + definition subtype_eq [H : Πa, is_prop (B a)] {u v : {a | B a}} : u.1 = v.1 → u = v := sigma_eq_unc ∘ inv pr1 - definition is_equiv_subtype_eq [H : Πa, is_hprop (B a)] (u v : {a | B a}) + definition is_equiv_subtype_eq [H : Πa, is_prop (B a)] (u v : {a | B a}) : is_equiv (subtype_eq : u.1 = v.1 → u = v) := !is_equiv_compose local attribute is_equiv_subtype_eq [instance] - definition equiv_subtype [H : Πa, is_hprop (B a)] (u v : {a | B a}) : (u.1 = v.1) ≃ (u = v) := + definition equiv_subtype [H : Πa, is_prop (B a)] (u v : {a | B a}) : (u.1 = v.1) ≃ (u = v) := equiv.mk !subtype_eq _ - definition subtype_eq_inv {A : Type} {B : A → Type} [H : Πa, is_hprop (B a)] (u v : Σa, B a) + definition subtype_eq_inv {A : Type} {B : A → Type} [H : Πa, is_prop (B a)] (u v : Σa, B a) : u = v → u.1 = v.1 := subtype_eq⁻¹ᶠ local attribute subtype_eq_inv [reducible] - definition is_equiv_subtype_eq_inv {A : Type} {B : A → Type} [H : Πa, is_hprop (B a)] + definition is_equiv_subtype_eq_inv {A : Type} {B : A → Type} [H : Πa, is_prop (B a)] (u v : Σa, B a) : is_equiv (subtype_eq_inv u v) := _ @@ -463,7 +463,7 @@ namespace sigma theorem is_trunc_subtype (B : A → hprop) (n : trunc_index) [HA : is_trunc (n.+1) A] : is_trunc (n.+1) (Σa, B a) := - @(is_trunc_sigma B (n.+1)) _ (λa, !is_trunc_succ_of_is_hprop) + @(is_trunc_sigma B (n.+1)) _ (λa, !is_trunc_succ_of_is_prop) end sigma diff --git a/hott/types/sum.hlean b/hott/types/sum.hlean index b163158b9..7b627676b 100644 --- a/hott/types/sum.hlean +++ b/hott/types/sum.hlean @@ -189,7 +189,7 @@ namespace sum begin fapply equiv.MK, { intro x, cases x with ab c, cases ab with a b, exact inl (a, c), exact inr (b, c) }, - { intro x, cases x with ac bc, cases ac with a c, exact (inl a, c), + { intro x, cases x with ac bc, cases ac with a c, exact (inl a, c), cases bc with b c, exact (inr b, c) }, { intro x, cases x with ac bc, cases ac with a c, reflexivity, cases bc, reflexivity }, { intro x, cases x with ab c, cases ab with a b, do 2 reflexivity } @@ -204,7 +204,7 @@ namespace sum section variables (H : unit + A ≃ unit + B) - include H + include H open unit decidable sigma.ops @@ -215,7 +215,7 @@ namespace sum cases u' with u' Hu', exfalso, apply empty_of_inl_eq_inr, calc inl ⋆ = H⁻¹ (H (inl ⋆)) : (to_left_inv H (inl ⋆))⁻¹ ... = H⁻¹ (inl u') : {Hu'} - ... = H⁻¹ (inl u) : is_hprop.elim + ... = H⁻¹ (inl u) : is_prop.elim ... = H⁻¹ (H (inr a)) : {Hu⁻¹} ... = inr a : to_left_inv H (inr a) end @@ -229,7 +229,7 @@ namespace sum { intro x, exfalso, cases x with u' Hu', apply empty_of_inl_eq_inr, calc inl ⋆ = H⁻¹ (H (inl ⋆)) : (to_left_inv H (inl ⋆))⁻¹ ... = H⁻¹ (inl u') : ap H⁻¹ Hu' - ... = H⁻¹ (inl u) : {!is_hprop.elim} + ... = H⁻¹ (inl u) : {!is_prop.elim} ... = H⁻¹ (H (inr _)) : {Hu⁻¹} ... = inr _ : to_left_inv H }, { intro x, cases x with b' Hb', esimp, cases sum.mem_cases (H⁻¹ (inr b)) with x x, @@ -244,26 +244,26 @@ namespace sum apply sum.rec, intro x, exfalso, apply empty_of_inl_eq_inr, apply concat, exact x.2⁻¹, apply Ha, intro x, cases x with a' Ha', esimp, apply eq_of_inr_eq_inr, apply Ha'⁻¹ ⬝ Ha } } }, - { intro x, cases x with b' Hb', esimp, apply eq_of_inr_eq_inr, refine Hb'⁻¹ ⬝ _, + { intro x, cases x with b' Hb', esimp, apply eq_of_inr_eq_inr, refine Hb'⁻¹ ⬝ _, cases sum.mem_cases (to_fun H⁻¹ (inr b)) with x x, - { cases x with u Hu, esimp, cases sum.mem_cases (to_fun H⁻¹ (inl ⋆)) with x x, - { cases x with u' Hu', exfalso, apply empty_of_inl_eq_inr, + { cases x with u Hu, esimp, cases sum.mem_cases (to_fun H⁻¹ (inl ⋆)) with x x, + { cases x with u' Hu', exfalso, apply empty_of_inl_eq_inr, calc inl ⋆ = H (H⁻¹ (inl ⋆)) : (to_right_inv H (inl ⋆))⁻¹ ... = H (inl u') : {ap H Hu'} - ... = H (inl u) : {!is_hprop.elim} + ... = H (inl u) : {!is_prop.elim} ... = H (H⁻¹ (inr b)) : {ap H Hu⁻¹} ... = inr b : to_right_inv H (inr b) }, - { cases x with a Ha, exfalso, apply empty_of_inl_eq_inr, + { cases x with a Ha, exfalso, apply empty_of_inl_eq_inr, apply concat, rotate 1, exact Hb', krewrite HH at Ha, - assert Ha' : inl ⋆ = H (inr a), apply !(to_right_inv H)⁻¹ ⬝ ap H Ha, + assert Ha' : inl ⋆ = H (inr a), apply !(to_right_inv H)⁻¹ ⬝ ap H Ha, apply concat Ha', apply ap H, apply ap inr, apply sum.rec, intro x, cases x with u' Hu', esimp, apply sum.rec, intro x, cases x with u'' Hu'', esimp, apply empty.rec, intro x, cases x with a'' Ha'', esimp, krewrite Ha' at Ha'', apply eq_of_inr_eq_inr, - apply !(to_left_inv H)⁻¹ ⬝ Ha'', + apply !(to_left_inv H)⁻¹ ⬝ Ha'', intro x, exfalso, cases x with a'' Ha'', apply empty_of_inl_eq_inr, apply Hu⁻¹ ⬝ Ha'', } }, - { cases x with a' Ha', esimp, refine _ ⬝ !(to_right_inv H), apply ap H, + { cases x with a' Ha', esimp, refine _ ⬝ !(to_right_inv H), apply ap H, rewrite -HH, apply Ha'⁻¹ } } end @@ -272,7 +272,7 @@ namespace sum fapply equiv.MK, apply unit_sum_equiv_cancel_map H, apply unit_sum_equiv_cancel_map H⁻¹, intro b, apply unit_sum_equiv_cancel_inv, - { intro a, have H = (H⁻¹)⁻¹, from !equiv.symm_symm⁻¹, rewrite this at {2}, + { intro a, have H = (H⁻¹)⁻¹, from !equiv.symm_symm⁻¹, rewrite this at {2}, apply unit_sum_equiv_cancel_inv } end @@ -318,9 +318,9 @@ namespace sum induction n with n IH, { exfalso, exact H !center !center}, { clear IH, induction n with n IH, - { apply is_hprop.mk, intros x y, + { apply is_prop.mk, intros x y, induction x, all_goals induction y, all_goals esimp, - all_goals try (exfalso;apply H;assumption;assumption), all_goals apply ap _ !is_hprop.elim}, + all_goals try (exfalso;apply H;assumption;assumption), all_goals apply ap _ !is_prop.elim}, { apply is_trunc_sum}} end diff --git a/hott/types/trunc.hlean b/hott/types/trunc.hlean index 89d6d0e30..9928b2b21 100644 --- a/hott/types/trunc.hlean +++ b/hott/types/trunc.hlean @@ -87,13 +87,13 @@ namespace is_trunc /- theorems about decidable equality and axiom K -/ - theorem is_hset_of_axiom_K {A : Type} (K : Π{a : A} (p : a = a), p = idp) : is_hset A := - is_hset.mk _ (λa b p q, eq.rec_on q K p) + theorem is_set_of_axiom_K {A : Type} (K : Π{a : A} (p : a = a), p = idp) : is_set A := + is_set.mk _ (λa b p q, eq.rec_on q K p) - theorem is_hset_of_relation.{u} {A : Type.{u}} (R : A → A → Type.{u}) - (mere : Π(a b : A), is_hprop (R a b)) (refl : Π(a : A), R a a) - (imp : Π{a b : A}, R a b → a = b) : is_hset A := - is_hset_of_axiom_K + theorem is_set_of_relation.{u} {A : Type.{u}} (R : A → A → Type.{u}) + (mere : Π(a b : A), is_prop (R a b)) (refl : Π(a : A), R a a) + (imp : Π{a b : A}, R a b → a = b) : is_set A := + is_set_of_axiom_K (λa p, have H2 : transport (λx, R a x → a = x) p (@imp a a) = @imp a a, from !apd, have H3 : Π(r : R a a), transport (λx, a = x) p (imp r) @@ -103,27 +103,27 @@ namespace is_trunc calc imp (refl a) ⬝ p = transport (λx, a = x) p (imp (refl a)) : transport_eq_r ... = imp (transport (λx, R a x) p (refl a)) : H3 - ... = imp (refl a) : is_hprop.elim, + ... = imp (refl a) : is_prop.elim, cancel_left (imp (refl a)) H4) definition relation_equiv_eq {A : Type} (R : A → A → Type) - (mere : Π(a b : A), is_hprop (R a b)) (refl : Π(a : A), R a a) + (mere : Π(a b : A), is_prop (R a b)) (refl : Π(a : A), R a a) (imp : Π{a b : A}, R a b → a = b) (a b : A) : R a b ≃ a = b := - @equiv_of_is_hprop _ _ _ - (@is_trunc_eq _ _ (is_hset_of_relation R mere refl @imp) a b) + @equiv_of_is_prop _ _ _ + (@is_trunc_eq _ _ (is_set_of_relation R mere refl @imp) a b) imp (λp, p ▸ refl a) local attribute not [reducible] - theorem is_hset_of_double_neg_elim {A : Type} (H : Π(a b : A), ¬¬a = b → a = b) - : is_hset A := - is_hset_of_relation (λa b, ¬¬a = b) _ (λa n, n idp) H + theorem is_set_of_double_neg_elim {A : Type} (H : Π(a b : A), ¬¬a = b → a = b) + : is_set A := + is_set_of_relation (λa b, ¬¬a = b) _ (λa n, n idp) H section open decidable --this is proven differently in init.hedberg - theorem is_hset_of_decidable_eq (A : Type) [H : decidable_eq A] : is_hset A := - is_hset_of_double_neg_elim (λa b, by_contradiction) + theorem is_set_of_decidable_eq (A : Type) [H : decidable_eq A] : is_set A := + is_set_of_double_neg_elim (λa b, by_contradiction) end theorem is_trunc_of_axiom_K_of_leq {A : Type} (n : trunc_index) (H : -1 ≤ n) @@ -138,9 +138,9 @@ namespace is_trunc induction p, apply Hp end - theorem is_hprop_iff_is_contr {A : Type} (a : A) : - is_hprop A ↔ is_contr A := - iff.intro (λH, is_contr.mk a (is_hprop.elim a)) _ + theorem is_prop_iff_is_contr {A : Type} (a : A) : + is_prop A ↔ is_contr A := + iff.intro (λH, is_contr.mk a (is_prop.elim a)) _ theorem is_trunc_succ_iff_is_trunc_loop (A : Type) (Hn : -1 ≤ n) : is_trunc (n.+1) A ↔ Π(a : A), is_trunc n (a = a) := @@ -152,7 +152,7 @@ namespace is_trunc revert A, induction n with n IH, { intro A, esimp [Iterated_loop_space], transitivity _, { apply is_trunc_succ_iff_is_trunc_loop, apply le.refl}, - { apply pi_iff_pi, intro a, esimp, apply is_hprop_iff_is_contr, reflexivity}}, + { apply pi_iff_pi, intro a, esimp, apply is_prop_iff_is_contr, reflexivity}}, { intro A, esimp [Iterated_loop_space], transitivity _, apply @is_trunc_succ_iff_is_trunc_loop @n, esimp, constructor, apply pi_iff_pi, intro a, transitivity _, apply IH, @@ -167,7 +167,7 @@ namespace is_trunc induction n with n, { esimp [sub_two,Iterated_loop_space], apply iff.intro, intro H a, exact is_contr_of_inhabited_hprop a, - intro H, apply is_hprop_of_imp_is_contr, exact H}, + intro H, apply is_prop_of_imp_is_contr, exact H}, { apply is_trunc_iff_is_contr_loop_succ}, end @@ -225,15 +225,15 @@ namespace trunc { clear n, intro n IH A m H, induction m with m, { apply (@is_trunc_of_leq _ -2), exact unit.star}, { apply is_trunc_succ_intro, intro aa aa', - apply (@trunc.rec_on _ _ _ aa (λy, !is_trunc_succ_of_is_hprop)), - eapply (@trunc.rec_on _ _ _ aa' (λy, !is_trunc_succ_of_is_hprop)), + apply (@trunc.rec_on _ _ _ aa (λy, !is_trunc_succ_of_is_prop)), + eapply (@trunc.rec_on _ _ _ aa' (λy, !is_trunc_succ_of_is_prop)), intro a a', apply (is_trunc_equiv_closed_rev), { apply tr_eq_tr_equiv}, { exact (IH _ _ _)}}} end open equiv.ops - definition unique_choice {P : A → Type} [H : Πa, is_hprop (P a)] (f : Πa, ∥ P a ∥) (a : A) + definition unique_choice {P : A → Type} [H : Πa, is_prop (P a)] (f : Πa, ∥ P a ∥) (a : A) : P a := !trunc_equiv (f a) @@ -262,7 +262,7 @@ namespace function definition is_equiv_equiv_is_embedding_times_is_surjective [constructor] (f : A → B) : is_equiv f ≃ (is_embedding f × is_surjective f) := - equiv_of_is_hprop (λH, (_, _)) + equiv_of_is_prop (λH, (_, _)) (λP, prod.rec_on P (λH₁ H₂, !is_equiv_of_is_surjective_of_is_embedding)) end function diff --git a/hott/types/univ.hlean b/hott/types/univ.hlean index ff554d914..1f0ef729c 100644 --- a/hott/types/univ.hlean +++ b/hott/types/univ.hlean @@ -39,13 +39,13 @@ namespace univ /- Properties which can be disproven for the universe -/ - definition not_is_hset_type0 : ¬is_hset Type₀ := - assume H : is_hset Type₀, - absurd !is_hset.elim eq_bnot_ne_idp + definition not_is_set_type0 : ¬is_set Type₀ := + assume H : is_set Type₀, + absurd !is_set.elim eq_bnot_ne_idp - definition not_is_hset_type : ¬is_hset Type.{u} := - assume H : is_hset Type, - absurd (is_trunc_is_embedding_closed lift star) not_is_hset_type0 + definition not_is_set_type : ¬is_set Type.{u} := + assume H : is_set Type, + absurd (is_trunc_is_embedding_closed lift star) not_is_set_type0 definition not_double_negation_elimination0 : ¬Π(A : Type₀), ¬¬A → A := begin @@ -53,7 +53,7 @@ namespace univ have u : ¬¬bool, by exact (λg, g tt), let H1 := apdo f eq_bnot, note H2 := apo10 H1 u, - have p : eq_bnot ▸ u = u, from !is_hprop.elim, + have p : eq_bnot ▸ u = u, from !is_prop.elim, rewrite p at H2, note H3 := eq_of_pathover_ua H2, esimp at H3, --TODO: use apply ... at after #700 exact absurd H3 (bnot_ne (f bool u)), diff --git a/src/library/class_instance_resolution.cpp b/src/library/class_instance_resolution.cpp index cc0fe3340..6643a8609 100644 --- a/src/library/class_instance_resolution.cpp +++ b/src/library/class_instance_resolution.cpp @@ -189,10 +189,10 @@ optional mk_class_instance(environment const & env, old_local_context cons return mk_class_instance(env, ctx.get_data(), type, nullptr); } -optional mk_hset_instance(type_checker & tc, options const & o, list const & ctx, expr const & type) { +optional mk_set_instance(type_checker & tc, options const & o, list const & ctx, expr const & type) { level lvl = sort_level(tc.ensure_type(type).first); - expr is_hset = tc.whnf(mk_app(mk_constant(get_is_trunc_is_hset_name(), {lvl}), type)).first; - return mk_class_instance(tc.env(), o, ctx, is_hset); + expr is_set = tc.whnf(mk_app(mk_constant(get_is_trunc_is_set_name(), {lvl}), type)).first; + return mk_class_instance(tc.env(), o, ctx, is_set); } optional mk_subsingleton_instance(environment const & env, options const & o, list const & ctx, expr const & type) { diff --git a/src/library/class_instance_resolution.h b/src/library/class_instance_resolution.h index b097b1a98..834ce6e82 100644 --- a/src/library/class_instance_resolution.h +++ b/src/library/class_instance_resolution.h @@ -39,7 +39,7 @@ pair mk_class_instance_elaborator( optional mk_class_instance(environment const & env, io_state const & ios, old_local_context const & ctx, expr const & type, bool use_local_instances); optional mk_class_instance(environment const & env, old_local_context const & ctx, expr const & type); -optional mk_hset_instance(type_checker & tc, options const & o, list const & ctx, expr const & type); +optional mk_set_instance(type_checker & tc, options const & o, list const & ctx, expr const & type); optional mk_subsingleton_instance(environment const & env, options const & o, list const & ctx, expr const & type); diff --git a/src/library/constants.cpp b/src/library/constants.cpp index 153de75d6..e76d46d37 100644 --- a/src/library/constants.cpp +++ b/src/library/constants.cpp @@ -84,9 +84,9 @@ name const * g_implies = nullptr; name const * g_implies_of_if_neg = nullptr; name const * g_implies_of_if_pos = nullptr; name const * g_implies_resolve = nullptr; -name const * g_is_trunc_is_hprop = nullptr; -name const * g_is_trunc_is_hprop_elim = nullptr; -name const * g_is_trunc_is_hset = nullptr; +name const * g_is_trunc_is_prop = nullptr; +name const * g_is_trunc_is_prop_elim = nullptr; +name const * g_is_trunc_is_set = nullptr; name const * g_ite = nullptr; name const * g_left_distrib = nullptr; name const * g_le_refl = nullptr; @@ -359,9 +359,9 @@ void initialize_constants() { g_implies_of_if_neg = new name{"implies_of_if_neg"}; g_implies_of_if_pos = new name{"implies_of_if_pos"}; g_implies_resolve = new name{"implies", "resolve"}; - g_is_trunc_is_hprop = new name{"is_trunc", "is_hprop"}; - g_is_trunc_is_hprop_elim = new name{"is_trunc", "is_hprop", "elim"}; - g_is_trunc_is_hset = new name{"is_trunc", "is_hset"}; + g_is_trunc_is_prop = new name{"is_trunc", "is_prop"}; + g_is_trunc_is_prop_elim = new name{"is_trunc", "is_prop", "elim"}; + g_is_trunc_is_set = new name{"is_trunc", "is_set"}; g_ite = new name{"ite"}; g_left_distrib = new name{"left_distrib"}; g_le_refl = new name{"le", "refl"}; @@ -635,9 +635,9 @@ void finalize_constants() { delete g_implies_of_if_neg; delete g_implies_of_if_pos; delete g_implies_resolve; - delete g_is_trunc_is_hprop; - delete g_is_trunc_is_hprop_elim; - delete g_is_trunc_is_hset; + delete g_is_trunc_is_prop; + delete g_is_trunc_is_prop_elim; + delete g_is_trunc_is_set; delete g_ite; delete g_left_distrib; delete g_le_refl; @@ -910,9 +910,9 @@ name const & get_implies_name() { return *g_implies; } name const & get_implies_of_if_neg_name() { return *g_implies_of_if_neg; } name const & get_implies_of_if_pos_name() { return *g_implies_of_if_pos; } name const & get_implies_resolve_name() { return *g_implies_resolve; } -name const & get_is_trunc_is_hprop_name() { return *g_is_trunc_is_hprop; } -name const & get_is_trunc_is_hprop_elim_name() { return *g_is_trunc_is_hprop_elim; } -name const & get_is_trunc_is_hset_name() { return *g_is_trunc_is_hset; } +name const & get_is_trunc_is_prop_name() { return *g_is_trunc_is_prop; } +name const & get_is_trunc_is_prop_elim_name() { return *g_is_trunc_is_prop_elim; } +name const & get_is_trunc_is_set_name() { return *g_is_trunc_is_set; } name const & get_ite_name() { return *g_ite; } name const & get_left_distrib_name() { return *g_left_distrib; } name const & get_le_refl_name() { return *g_le_refl; } diff --git a/src/library/constants.h b/src/library/constants.h index 5f926c1e9..67994cf1b 100644 --- a/src/library/constants.h +++ b/src/library/constants.h @@ -86,9 +86,9 @@ name const & get_implies_name(); name const & get_implies_of_if_neg_name(); name const & get_implies_of_if_pos_name(); name const & get_implies_resolve_name(); -name const & get_is_trunc_is_hprop_name(); -name const & get_is_trunc_is_hprop_elim_name(); -name const & get_is_trunc_is_hset_name(); +name const & get_is_trunc_is_prop_name(); +name const & get_is_trunc_is_prop_elim_name(); +name const & get_is_trunc_is_set_name(); name const & get_ite_name(); name const & get_left_distrib_name(); name const & get_le_refl_name(); diff --git a/src/library/constants.txt b/src/library/constants.txt index 2b234a4f8..4634d2d21 100644 --- a/src/library/constants.txt +++ b/src/library/constants.txt @@ -79,9 +79,9 @@ implies implies_of_if_neg implies_of_if_pos implies.resolve -is_trunc.is_hprop -is_trunc.is_hprop.elim -is_trunc.is_hset +is_trunc.is_prop +is_trunc.is_prop.elim +is_trunc.is_set ite left_distrib le.refl diff --git a/src/library/tactic/inversion_tactic.cpp b/src/library/tactic/inversion_tactic.cpp index 8f7a1f419..f6335c9eb 100644 --- a/src/library/tactic/inversion_tactic.cpp +++ b/src/library/tactic/inversion_tactic.cpp @@ -43,7 +43,7 @@ result::result(list const & gs, list> const & args, list apply_eq_rec_eq(type_checker & tc, io_state const & ios, list apply_eq_rec_eq(type_checker & tc, io_state const & ios, list type_context::mk_subsingleton_instance(expr const & type) { if (is_standard(m_env)) subsingleton = mk_app(mk_constant(get_subsingleton_name(), {lvl}), type); else - subsingleton = whnf(mk_app(mk_constant(get_is_trunc_is_hprop_name(), {lvl}), type)); + subsingleton = whnf(mk_app(mk_constant(get_is_trunc_is_prop_name(), {lvl}), type)); auto r = mk_class_instance(subsingleton); m_ss_cache.insert(mk_pair(type, r)); return r; diff --git a/src/library/util.cpp b/src/library/util.cpp index 4f82c0ba0..1acccfb06 100644 --- a/src/library/util.cpp +++ b/src/library/util.cpp @@ -632,7 +632,7 @@ expr mk_subsingleton_elim(type_checker & tc, expr const & h, expr const & x, exp if (is_standard(tc.env())) { r = mk_constant(get_subsingleton_elim_name(), {l}); } else { - r = mk_constant(get_is_trunc_is_hprop_elim_name(), {l}); + r = mk_constant(get_is_trunc_is_prop_elim_name(), {l}); } return mk_app({r, A, h, x, y}); } diff --git a/src/library/util.h b/src/library/util.h index 8b9cac788..85ec1b2b7 100644 --- a/src/library/util.h +++ b/src/library/util.h @@ -170,7 +170,7 @@ expr mk_symm(type_checker & tc, expr const & H); expr mk_trans(type_checker & tc, expr const & H1, expr const & H2); expr mk_subst(type_checker & tc, expr const & motive, expr const & x, expr const & y, expr const & xeqy, expr const & h); expr mk_subst(type_checker & tc, expr const & motive, expr const & xeqy, expr const & h); -/** \brief Create an proof for x = y using subsingleton.elim (in standard mode) and is_trunc.is_hprop.elim (in HoTT mode) */ +/** \brief Create an proof for x = y using subsingleton.elim (in standard mode) and is_trunc.is_prop.elim (in HoTT mode) */ expr mk_subsingleton_elim(type_checker & tc, expr const & h, expr const & x, expr const & y); /** \brief Return true iff \c e is a term of the form (eq.rec ....) */ diff --git a/tests/lean/simplifier1.hlean b/tests/lean/simplifier1.hlean index 10a757094..6abc46c1d 100644 --- a/tests/lean/simplifier1.hlean +++ b/tests/lean/simplifier1.hlean @@ -21,7 +21,7 @@ constants H₁ : a ≠ b constants H₂ : a = c namespace tst attribute H₂ [simp] end tst -definition ne_is_hprop [instance] (a b : nat) : is_hprop (a ≠ b) := +definition ne_is_prop [instance] (a b : nat) : is_prop (a ≠ b) := sorry -- TODO(Daniel): simplifier seems to have applied unnecessary step (see: (eq.nrec ... (eq.refl ..))) #simplify eq tst 0 (g a b H₁)