From 43cf2ad23dd261e7a31cbaf0afd3f5585d2d84cd Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpv@andrew.cmu.edu>
Date: Mon, 15 Feb 2016 15:55:29 -0500
Subject: [PATCH] style(hott): replace all other occurrences of hprop/hset

They are replaced by either Prop/Set or prop/set
---
 hott/algebra/category/constructions/set.hlean | 24 +++++++++----------
 hott/algebra/category/functor/yoneda.hlean    |  2 +-
 hott/algebra/category/limits/set.hlean        |  2 +-
 hott/algebra/category/precategory.hlean       |  8 +++----
 hott/algebra/hott.hlean                       |  2 +-
 hott/book.md                                  |  4 ++--
 hott/choice.hlean                             |  4 ++--
 hott/hit/coeq.hlean                           |  4 ++--
 hott/hit/colimit.hlean                        |  8 +++----
 hott/hit/pushout.hlean                        |  4 ++--
 hott/hit/quotient.hlean                       |  4 ++--
 hott/hit/set_quotient.hlean                   | 10 ++++----
 hott/hit/trunc.hlean                          | 12 +++++-----
 hott/homotopy/cellcomplex.hlean               | 10 ++++----
 hott/homotopy/connectedness.hlean             |  4 ++--
 hott/hott.md                                  |  2 +-
 hott/init/default.hlean                       |  2 +-
 hott/init/funext.hlean                        |  2 +-
 hott/init/hedberg.hlean                       |  2 +-
 hott/init/trunc.hlean                         | 20 +++++++---------
 hott/{hprop_trunc.hlean => prop_trunc.hlean}  |  0
 hott/types/bool.hlean                         |  2 +-
 hott/types/equiv.hlean                        |  4 ++--
 hott/types/pi.hlean                           |  4 ++--
 hott/types/sigma.hlean                        |  6 ++---
 hott/types/trunc.hlean                        |  8 +++----
 src/emacs/lean-syntax.el                      |  5 ++--
 27 files changed, 79 insertions(+), 80 deletions(-)
 rename hott/{hprop_trunc.hlean => prop_trunc.hlean} (100%)

diff --git a/hott/algebra/category/constructions/set.hlean b/hott/algebra/category/constructions/set.hlean
index 04293f864..0e5a2fadc 100644
--- a/hott/algebra/category/constructions/set.hlean
+++ b/hott/algebra/category/constructions/set.hlean
@@ -12,18 +12,18 @@ open eq category equiv iso is_equiv is_trunc function sigma
 
 namespace category
 
-  definition precategory_hset.{u} [reducible] [constructor] : precategory hset.{u} :=
-  precategory.mk (λx y : hset, x → y)
+  definition precategory_Set.{u} [reducible] [constructor] : precategory Set.{u} :=
+  precategory.mk (λx y : Set, x → y)
                  (λx y z g f a, g (f a))
                  (λx a, a)
                  (λx y z w h g f, eq_of_homotopy (λa, idp))
                  (λx y f, eq_of_homotopy (λa, idp))
                  (λx y f, eq_of_homotopy (λa, idp))
 
-  definition Precategory_hset [reducible] [constructor] : Precategory :=
-  Precategory.mk hset precategory_hset
+  definition Precategory_Set [reducible] [constructor] : Precategory :=
+  Precategory.mk Set precategory_Set
 
-  abbreviation set [constructor] := Precategory_hset
+  abbreviation set [constructor] := Precategory_Set
 
   namespace set
     local attribute is_equiv_subtype_eq [instance]
@@ -48,7 +48,7 @@ namespace category
 
     local attribute is_equiv_iso_of_equiv [instance]
 
-    definition iso_of_eq_eq_compose (A B : hset) : @iso_of_eq _ _ A B =
+    definition iso_of_eq_eq_compose (A B : Set) : @iso_of_eq _ _ A B =
       @iso_of_equiv A B ∘ @equiv_of_eq A B ∘ subtype_eq_inv _ _ ∘
       @ap _ _ (to_fun (trunctype.sigma_char 0)) A B :=
     eq_of_homotopy (λp, eq.rec_on p idp)
@@ -65,7 +65,7 @@ namespace category
     definition equiv_eq_iso (A B : set) : (A ≃ B) = (A ≅ B) :=
     ua !equiv_equiv_iso
 
-    definition is_univalent_hset (A B : set) : is_equiv (iso_of_eq : A = B → A ≅ B) :=
+    definition is_univalent_Set (A B : set) : is_equiv (iso_of_eq : A = B → A ≅ B) :=
     assert H₁ : is_equiv (@iso_of_equiv A B ∘ @equiv_of_eq A B ∘ subtype_eq_inv _ _ ∘
                   @ap _ _ (to_fun (trunctype.sigma_char 0)) A B), from
       @is_equiv_compose _ _ _ _ _
@@ -82,13 +82,13 @@ namespace category
     end
   end set
 
-  definition category_hset [instance] [constructor] [reducible] : category hset :=
-  category.mk precategory_hset set.is_univalent_hset
+  definition category_Set [instance] [constructor] [reducible] : category Set :=
+  category.mk precategory_Set set.is_univalent_Set
 
-  definition Category_hset [reducible] [constructor] : Category :=
-  Category.mk hset category_hset
+  definition Category_Set [reducible] [constructor] : Category :=
+  Category.mk Set category_Set
 
-  abbreviation cset [constructor] := Category_hset
+  abbreviation cset [constructor] := Category_Set
 
   open functor lift
   definition functor_lift.{u v} [constructor] : set.{u} ⇒ set.{max u v} :=
diff --git a/hott/algebra/category/functor/yoneda.hlean b/hott/algebra/category/functor/yoneda.hlean
index 99f7af386..bd095193e 100644
--- a/hott/algebra/category/functor/yoneda.hlean
+++ b/hott/algebra/category/functor/yoneda.hlean
@@ -86,7 +86,7 @@ namespace yoneda
 
   -- TODO: Investigate what is the bottleneck to type check the next theorem
 
-  -- attribute yoneda_lemma functor_lift Precategory_hset precategory_hset homset
+  -- attribute yoneda_lemma functor_lift Precategory_Set precategory_Set homset
   --   yoneda_embedding nat_trans.compose functor_nat_trans_compose [reducible]
   -- attribute tlift functor.compose [reducible]
   theorem yoneda_lemma_natural_functor.{u v} {C : Precategory.{u v}} (c : C) (F F' : Cᵒᵖ ⇒ cset)
diff --git a/hott/algebra/category/limits/set.hlean b/hott/algebra/category/limits/set.hlean
index deb0f189b..d99d533cd 100644
--- a/hott/algebra/category/limits/set.hlean
+++ b/hott/algebra/category/limits/set.hlean
@@ -58,7 +58,7 @@ namespace category
 
   definition is_cocomplete_set_cone_rel.{u v w} [unfold 3 4]
     (I : Precategory.{v w}) (F : I ⇒ set.{max u v w}ᵒᵖ) : (Σ(i : I), trunctype.carrier (F i)) →
-    (Σ(i : I), trunctype.carrier (F i)) → hprop.{max u v w} :=
+    (Σ(i : I), trunctype.carrier (F i)) → Prop.{max u v w} :=
   begin
     intro v w, induction v with i x, induction w with j y,
       fapply trunctype.mk,
diff --git a/hott/algebra/category/precategory.hlean b/hott/algebra/category/precategory.hlean
index dcf4bdaab..63001121f 100644
--- a/hott/algebra/category/precategory.hlean
+++ b/hott/algebra/category/precategory.hlean
@@ -56,13 +56,13 @@ namespace category
 
   -- the constructor you want to use in practice
   protected definition precategory.mk [constructor] {ob : Type} (hom : ob → ob → Type)
-    [hset : Π (a b : ob), is_set (hom a b)]
+    [set : Π (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)
     (idl : Π ⦃a b : ob⦄ (f : hom a b), comp (ID b) f = f)
     (idr : Π ⦃a b : ob⦄ (f : hom a b), comp f (ID a) = f) : precategory ob :=
-  precategory.mk' hom comp ID ass (λa b c d h g f, !ass⁻¹) idl idr (λa, !idl) hset
+  precategory.mk' hom comp ID ass (λa b c d h g f, !ass⁻¹) idl idr (λa, !idl) set
 
   section basic_lemmas
     variables {ob : Type} [C : precategory ob]
@@ -83,8 +83,8 @@ namespace category
     calc i = id ∘ i : by rewrite id_left
        ... = id     : by rewrite H
 
-    definition homset [reducible] [constructor] (x y : ob) : hset :=
-    hset.mk (hom x y) _
+    definition homset [reducible] [constructor] (x y : ob) : Set :=
+    Set.mk (hom x y) _
 
   end basic_lemmas
   section squares
diff --git a/hott/algebra/hott.hlean b/hott/algebra/hott.hlean
index 869268c93..2fb73a5a2 100644
--- a/hott/algebra/hott.hlean
+++ b/hott/algebra/hott.hlean
@@ -6,7 +6,7 @@ Author: Floris van Doorn
 Theorems about algebra specific to HoTT
 -/
 
-import .group arity types.pi hprop_trunc types.unit .bundled
+import .group arity types.pi prop_trunc types.unit .bundled
 
 open equiv eq equiv.ops is_trunc unit
 
diff --git a/hott/book.md b/hott/book.md
index 371698ef8..91f859018 100644
--- a/hott/book.md
+++ b/hott/book.md
@@ -73,7 +73,7 @@ Chapter 3: Sets and logic
 
 - 3.1 (Sets and n-types): [init.trunc](init/trunc.hlean). Example 3.1.9 in [types.univ](types/univ.hlean)
 - 3.2 (Propositions as types?): [types.univ](types/univ.hlean)
-- 3.3 (Mere propositions): [init.trunc](init/trunc.hlean) and [hprop_trunc](hprop_trunc.hlean) (Lemma 3.3.5).
+- 3.3 (Mere propositions): [init.trunc](init/trunc.hlean) and [prop_trunc](prop_trunc.hlean) (Lemma 3.3.5).
 - 3.4 (Classical vs. intuitionistic logic): decidable is defined in [init.logic](init/logic.hlean)
 - 3.5 (Subsets and propositional resizing): Lemma 3.5.1 is subtype_eq in [types.sigma](types/sigma.hlean), we don't have propositional resizing as axiom yet.
 - 3.6 (The logic of mere propositions): in the corresponding file in the [types](types/types.md) folder. (is_trunc_prod is defined in [types.sigma](types/sigma.hlean))
@@ -128,7 +128,7 @@ Chapter 6: Higher inductive types
 Chapter 7: Homotopy n-types
 ---------
 
-- 7.1 (Definition of n-types): [init.trunc](init/trunc.hlean), [types.trunc](types/trunc.hlean), [types.sigma](types/sigma.hlean) (Theorem 7.1.8), [types.pi](types/pi.hlean) (Theorem 7.1.9), [hprop_trunc](hprop_trunc.hlean) (Theorem 7.1.10)
+- 7.1 (Definition of n-types): [init.trunc](init/trunc.hlean), [types.trunc](types/trunc.hlean), [types.sigma](types/sigma.hlean) (Theorem 7.1.8), [types.pi](types/pi.hlean) (Theorem 7.1.9), [prop_trunc](prop_trunc.hlean) (Theorem 7.1.10)
 - 7.2 (Uniqueness of identity proofs and Hedberg’s theorem): [init.hedberg](init/hedberg.hlean) and [types.trunc](types/trunc.hlean)
 - 7.3 (Truncations): [init.hit](init/hit.hlean), [hit.trunc](hit/trunc.hlean) and [types.trunc](types/trunc.hlean)
 - 7.4 (Colimits of n-types): not formalized
diff --git a/hott/choice.hlean b/hott/choice.hlean
index bbf2ad871..7ccec2722 100644
--- a/hott/choice.hlean
+++ b/hott/choice.hlean
@@ -37,7 +37,7 @@ namespace choice
   by intro H X A P HX HA HP HI;
   apply H X (λ x, Σ a, P x a) HX (λ x, !is_trunc_sigma) HI
 
-  -- Which is enough to show AC' ≃ AC_cart, since both are hprops.
+  -- Which is enough to show AC' ≃ AC_cart, since both are props.
   definition AC'_equiv_AC_cart : AC'.{u} ≃ AC_cart.{u} :=
   equiv_of_is_prop AC_cart_of_AC'.{u} AC'_of_AC_cart.{u}
 
@@ -80,7 +80,7 @@ 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})
+  definition X_must_be_set : Σ (X : Type.{1}) (Y : X -> Type.{1})
   (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)))⟩
diff --git a/hott/hit/coeq.hlean b/hott/hit/coeq.hlean
index 27a057e19..3a8e38481 100644
--- a/hott/hit/coeq.hlean
+++ b/hott/hit/coeq.hlean
@@ -74,11 +74,11 @@ 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_prop (P x)]
+  protected definition rec_prop {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_prop.elimo) y
 
-  protected definition elim_hprop {P : Type} [H : is_prop P] (P_i : B → P) (y : coeq) : P :=
+  protected definition elim_prop {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 4b142b955..9ab899dd6 100644
--- a/hott/hit/colimit.hlean
+++ b/hott/hit/colimit.hlean
@@ -85,11 +85,11 @@ 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_prop (P x)]
+  protected definition rec_prop {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_prop.elimo) y
 
-  protected definition elim_hprop {P : Type} [H : is_prop P] (Pincl : Π⦃i : I⦄ (x : A i), P)
+  protected definition elim_prop {P : Type} [H : is_prop P] (Pincl : Π⦃i : I⦄ (x : A i), P)
     (y : colimit) : P :=
   elim Pincl (λa b, !is_prop.elim) y
 
@@ -175,11 +175,11 @@ 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_prop (P x)]
+  protected definition rec_prop {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_prop.elimo) aa
 
-  protected definition elim_hprop {P : Type} [H : is_prop P] (Pincl : Π⦃n : ℕ⦄ (a : A n), P)
+  protected definition elim_prop {P : Type} [H : is_prop P] (Pincl : Π⦃n : ℕ⦄ (a : A n), P)
     : seq_colim → P :=
   elim Pincl (λa b, !is_prop.elim)
 
diff --git a/hott/hit/pushout.hlean b/hott/hit/pushout.hlean
index 478b1b0e0..491bbf71c 100644
--- a/hott/hit/pushout.hlean
+++ b/hott/hit/pushout.hlean
@@ -83,11 +83,11 @@ 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_prop (P x)]
+  protected definition rec_prop {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_prop.elimo) y
 
-  protected definition elim_hprop {P : Type} [H : is_prop P] (Pinl : BL → P) (Pinr : TR → P)
+  protected definition elim_prop {P : Type} [H : is_prop P] (Pinl : BL → P) (Pinr : TR → P)
     (y : pushout) : P :=
   elim Pinl Pinr (λa, !is_prop.elim) y
 
diff --git a/hott/hit/quotient.hlean b/hott/hit/quotient.hlean
index 1a412ec0d..f8f53aa31 100644
--- a/hott/hit/quotient.hlean
+++ b/hott/hit/quotient.hlean
@@ -38,11 +38,11 @@ namespace quotient
     rewrite [▸*,-apdo_eq_pathover_of_eq_ap,↑quotient.elim,rec_eq_of_rel],
   end
 
-  protected definition rec_hprop {A : Type} {R : A → A → Type} {P : quotient R → Type}
+  protected definition rec_prop {A : Type} {R : A → A → Type} {P : quotient R → Type}
     [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_prop P] (Pc : A → P) (x : quotient R) : P :=
+  protected definition elim_prop {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)
diff --git a/hott/hit/set_quotient.hlean b/hott/hit/set_quotient.hlean
index dc6b1ac6d..9b75b648e 100644
--- a/hott/hit/set_quotient.hlean
+++ b/hott/hit/set_quotient.hlean
@@ -12,7 +12,7 @@ open eq is_trunc trunc quotient equiv
 
 namespace set_quotient
 section
-  parameters {A : Type} (R : A → A → hprop)
+  parameters {A : Type} (R : A → A → Prop)
   -- set-quotients are just set-truncations of (type) quotients
   definition set_quotient : Type := trunc 0 (quotient R)
 
@@ -63,11 +63,11 @@ 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_prop (P aa)]
+  protected definition rec_prop {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_prop.elimo) x
 
-  protected definition elim_hprop {P : Type} [Pt : is_prop P] (Pc : A → P) (x : set_quotient)
+  protected definition elim_prop {P : Type} [Pt : is_prop P] (Pc : A → P) (x : set_quotient)
     : P :=
   elim Pc (λa a' H, !is_prop.elim) x
 
@@ -81,7 +81,7 @@ attribute set_quotient.rec_on set_quotient.elim_on [unfold 4]
 open sigma relation function
 
 namespace set_quotient
-  variables {A B C : Type} (R : A → A → hprop) (S : B → B → hprop) (T : C → C → hprop)
+  variables {A B C : Type} (R : A → A → Prop) (S : B → B → Prop) (T : C → C → Prop)
 
   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_prop.elimo)
@@ -102,7 +102,7 @@ namespace set_quotient
   end
 
   protected definition code [unfold 4] (a : A) (x : set_quotient R) [H : is_equivalence R]
-    : hprop :=
+    : Prop :=
   set_quotient.elim_on x (R a)
     begin
       intros a' a'' H1,
diff --git a/hott/hit/trunc.hlean b/hott/hit/trunc.hlean
index 62dcf84c5..ea7b3d345 100644
--- a/hott/hit/trunc.hlean
+++ b/hott/hit/trunc.hlean
@@ -98,14 +98,14 @@ namespace trunc
 
   /- Propositional truncation -/
 
-  -- should this live in hprop?
-  definition merely [reducible] [constructor] (A : Type) : hprop := trunctype.mk (trunc -1 A) _
+  -- should this live in Prop?
+  definition merely [reducible] [constructor] (A : Type) : Prop := trunctype.mk (trunc -1 A) _
 
   notation `||`:max A `||`:0 := merely A
   notation `∥`:max A `∥`:0   := merely A
 
-  definition Exists [reducible] [constructor] (P : X → Type) : hprop := ∥ sigma P ∥
-  definition or [reducible] [constructor] (A B : Type) : hprop := ∥ A ⊎ B ∥
+  definition Exists [reducible] [constructor] (P : X → Type) : Prop := ∥ sigma P ∥
+  definition or [reducible] [constructor] (A B : Type) : Prop := ∥ A ⊎ B ∥
 
   notation `exists` binders `,` r:(scoped P, Exists P) := r
   notation `∃` binders `,` r:(scoped P, Exists P) := r
@@ -117,8 +117,8 @@ 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_prop A] (aa : merely A) : is_contr A :=
-  is_contr_of_inhabited_hprop (trunc.rec_on aa id)
+  definition is_contr_of_merely_prop [H : is_prop A] (aa : merely A) : is_contr A :=
+  is_contr_of_inhabited_prop (trunc.rec_on aa id)
 
   section
   open sigma.ops
diff --git a/hott/homotopy/cellcomplex.hlean b/hott/homotopy/cellcomplex.hlean
index 63a45400f..ad21d442b 100644
--- a/hott/homotopy/cellcomplex.hlean
+++ b/hott/homotopy/cellcomplex.hlean
@@ -36,14 +36,14 @@ namespace cellcomplex
 
   definition fdcc_family [reducible] : ℕ → family :=
   nat.rec
-    -- a zero-dimensional cell complex is just an hset
+    -- a zero-dimensional cell complex is just an set
     -- with realization the identity map
-    ⟨hset , λA, trunctype.carrier A⟩
+    ⟨Set , λA, trunctype.carrier A⟩
     (λn fdcc_family_n, -- sigma.rec (λ fdcc_n realize_n,
       /- a (succ n)-dimensional cell complex is a triple of
-         an n-dimensional cell complex X, an hset of (succ n)-cells A,
+         an n-dimensional cell complex X, an set of (succ n)-cells A,
          and an attaching map f : A × sphere n → |X| -/
-      ⟨Σ X : pr1 fdcc_family_n , Σ A : hset, A × sphere n → pr2 fdcc_family_n X ,
+      ⟨Σ X : pr1 fdcc_family_n , Σ A : Set, A × sphere n → pr2 fdcc_family_n X ,
       /- the realization of such is the pushout of f with
          canonical map A × sphere n → unit -/
        sigma.rec (λX , sigma.rec (λA f, pushout (λx , star) f))
@@ -51,7 +51,7 @@ namespace cellcomplex
 
   definition fdcc (n : ℕ) : Type := pr1 (fdcc_family n)
 
-  definition cell : Πn, fdcc n → hset :=
+  definition cell : Πn, fdcc n → Set :=
   nat.cases (λA, A) (λn T, pr1 (pr2 T))
 
 end cellcomplex
diff --git a/hott/homotopy/connectedness.hlean b/hott/homotopy/connectedness.hlean
index e6e8355b7..5738db398 100644
--- a/hott/homotopy/connectedness.hlean
+++ b/hott/homotopy/connectedness.hlean
@@ -196,7 +196,7 @@ namespace homotopy
     : is_surjective f → is_conn_map -1 f :=
   begin
     intro H, intro b,
-    exact @is_contr_of_inhabited_hprop (∥fiber f b∥) (is_trunc_trunc -1 (fiber f b)) (H b),
+    exact @is_contr_of_inhabited_prop (∥fiber f b∥) (is_trunc_trunc -1 (fiber f b)) (H b),
   end
 
   definition is_surjection_of_minus_one_conn {A B : Type} (f : A → B)
@@ -210,7 +210,7 @@ namespace homotopy
   λH, @center (∥A∥) H
 
   definition minus_one_conn_of_merely {A : Type} : ∥A∥ → is_conn -1 A :=
-  @is_contr_of_inhabited_hprop (∥A∥) (is_trunc_trunc -1 A)
+  @is_contr_of_inhabited_prop (∥A∥) (is_trunc_trunc -1 A)
 
   section
     open arrow
diff --git a/hott/hott.md b/hott/hott.md
index 11c9a4229..542e01e75 100644
--- a/hott/hott.md
+++ b/hott/hott.md
@@ -10,7 +10,7 @@ The Lean Homotopy Type Theory library consists of the following directories:
 * [cubical](cubical/cubical.md): cubical types
 
 The following files don't fit in any of the subfolders:
-* [hprop_trunc](hprop_trunc.hlean): in this file we prove that `is_trunc n A` is a mere proposition. We separate this from [types.trunc](types/trunc.hlean) to avoid circularity in imports.
+* [prop_trunc](prop_trunc.hlean): in this file we prove that `is_trunc n A` is a mere proposition. We separate this from [types.trunc](types/trunc.hlean) to avoid circularity in imports.
 * [eq2](eq2.hlean): coherence rules for the higher dimensional structure of equality
 * [function](function.hlean): embeddings, (split) surjections, retractions
 * [arity](arity.hlean) : equality theorems about functions with arity 2 or higher
diff --git a/hott/init/default.hlean b/hott/init/default.hlean
index 4967c126d..1882be93a 100644
--- a/hott/init/default.hlean
+++ b/hott/init/default.hlean
@@ -23,5 +23,5 @@ namespace core
   export [declaration] function
   export equiv (to_inv to_right_inv to_left_inv)
   export is_equiv (inv right_inv left_inv adjointify)
-  export [abbreviation] [declaration] is_trunc (hprop.mk hset.mk)
+  export [abbreviation] [declaration] is_trunc (Prop.mk Set.mk)
 end core
diff --git a/hott/init/funext.hlean b/hott/init/funext.hlean
index 92905c4c4..44af4eff0 100644
--- a/hott/init/funext.hlean
+++ b/hott/init/funext.hlean
@@ -84,7 +84,7 @@ section
   local attribute weak_funext [reducible]
   local attribute homotopy_ind [reducible]
   definition homotopy_ind_comp : homotopy_ind f (homotopy.refl f) = d :=
-    (@hprop_eq_of_is_contr _ _ _ _ !eq_of_is_contr idp)⁻¹ ▸ idp
+    (@prop_eq_of_is_contr _ _ _ _ !eq_of_is_contr idp)⁻¹ ▸ idp
 end
 
 /- Now the proof is fairly easy; we can just use the same induction principle on both sides. -/
diff --git a/hott/init/hedberg.hlean b/hott/init/hedberg.hlean
index ead176120..77a830c67 100644
--- a/hott/init/hedberg.hlean
+++ b/hott/init/hedberg.hlean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 
-Hedberg's Theorem: every type with decidable equality is a hset
+Hedberg's Theorem: every type with decidable equality is a set
 -/
 
 prelude
diff --git a/hott/init/trunc.hlean b/hott/init/trunc.hlean
index 555e25971..617853edf 100644
--- a/hott/init/trunc.hlean
+++ b/hott/init/trunc.hlean
@@ -8,8 +8,6 @@ Definition of is_trunc (n-truncatedness)
 Ported from Coq HoTT.
 -/
 
---TODO: can we replace some definitions with a hprop as codomain by theorems?
-
 prelude
 import .nat .logic .equiv .pathover
 open eq nat sigma unit sigma.ops
@@ -135,12 +133,12 @@ namespace is_trunc
   definition eq_of_is_contr [H : is_contr A] (x y : A) : x = y :=
   (center_eq x)⁻¹ ⬝ (center_eq y)
 
-  definition hprop_eq_of_is_contr {A : Type} [H : is_contr A] {x y : A} (p q : x = y) : p = q :=
+  definition prop_eq_of_is_contr {A : Type} [H : is_contr A] {x y : A} (p q : x = y) : p = q :=
   have K : ∀ (r : x = y), eq_of_is_contr x y = r, from (λ r, eq.rec_on r !con.left_inv),
   (K p)⁻¹ ⬝ K q
 
   theorem is_contr_eq {A : Type} [H : is_contr A] (x y : A) : is_contr (x = y) :=
-  is_contr.mk !eq_of_is_contr (λ p, !hprop_eq_of_is_contr)
+  is_contr.mk !eq_of_is_contr (λ p, !prop_eq_of_is_contr)
   local attribute is_contr_eq [instance]
 
   /- truncation is upward close -/
@@ -192,12 +190,12 @@ namespace is_trunc
       : is_trunc (n.+2) A :=
   @(is_trunc_of_leq A (show 0 ≤ n.+2, from proof star qed)) H
 
-  /- hprops -/
+  /- props -/
 
   definition is_prop.elim [H : is_prop A] (x y : A) : x = y :=
   !center
 
-  definition is_contr_of_inhabited_hprop {A : Type} [H : is_prop A] (x : A) : is_contr A :=
+  definition is_contr_of_inhabited_prop {A : Type} [H : is_prop A] (x : A) : is_contr A :=
   is_contr.mk x (λy, !is_prop.elim)
 
   theorem is_prop_of_imp_is_contr {A : Type} (H : A → is_contr A) : is_prop A :=
@@ -212,7 +210,7 @@ namespace is_trunc
   theorem is_prop_elim_self {A : Type} {H : is_prop A} (x : A) : is_prop.elim x x = idp :=
   !is_prop.elim
 
-  /- hsets -/
+  /- sets -/
 
   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))
@@ -351,11 +349,11 @@ namespace is_trunc
   attribute trunctype.struct [instance] [priority 1400]
 
   notation n `-Type` := trunctype n
-  abbreviation hprop := -1-Type
-  abbreviation hset := 0-Type
+  abbreviation Prop := -1-Type
+  abbreviation Set  := 0-Type
 
-  protected abbreviation hprop.mk := @trunctype.mk -1
-  protected abbreviation hset.mk := @trunctype.mk (-1.+1)
+  protected abbreviation Prop.mk := @trunctype.mk -1
+  protected abbreviation Set.mk := @trunctype.mk (-1.+1)
 
   protected abbreviation trunctype.mk' [parsing_only] (n : trunc_index) (A : Type)
     [H : is_trunc n A] : n-Type :=
diff --git a/hott/hprop_trunc.hlean b/hott/prop_trunc.hlean
similarity index 100%
rename from hott/hprop_trunc.hlean
rename to hott/prop_trunc.hlean
diff --git a/hott/types/bool.hlean b/hott/types/bool.hlean
index 4bef259d6..c25d5f138 100644
--- a/hott/types/bool.hlean
+++ b/hott/types/bool.hlean
@@ -168,6 +168,6 @@ namespace bool
     { intro b, cases b, reflexivity, reflexivity},
   end
 
-  definition tbool [constructor] : hset := trunctype.mk bool _
+  definition tbool [constructor] : Set := trunctype.mk bool _
 
 end bool
diff --git a/hott/types/equiv.hlean b/hott/types/equiv.hlean
index f69e725be..2509b3c0f 100644
--- a/hott/types/equiv.hlean
+++ b/hott/types/equiv.hlean
@@ -7,7 +7,7 @@ Ported from Coq HoTT
 Theorems about the types equiv and is_equiv
 -/
 
-import .fiber .arrow arity ..hprop_trunc
+import .fiber .arrow arity ..prop_trunc
 
 open eq is_trunc sigma sigma.ops pi fiber function equiv equiv.ops
 
@@ -184,7 +184,7 @@ namespace equiv
 
   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_prop.mk,
+    apply @is_contr_of_inhabited_prop, 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
diff --git a/hott/types/pi.hlean b/hott/types/pi.hlean
index 9cc874341..9fc3c6a92 100644
--- a/hott/types/pi.hlean
+++ b/hott/types/pi.hlean
@@ -226,9 +226,9 @@ namespace pi
     fapply equiv.MK,
     { intro f, exact f (center A)},
     { intro b a, exact (center_eq a) ▸ b},
-    { intro b, rewrite [hprop_eq_of_is_contr (center_eq (center A)) idp]},
+    { intro b, rewrite [prop_eq_of_is_contr (center_eq (center A)) idp]},
     { intro f, apply eq_of_homotopy, intro a, induction (center_eq a),
-      rewrite [hprop_eq_of_is_contr (center_eq (center A)) idp]}
+      rewrite [prop_eq_of_is_contr (center_eq (center A)) idp]}
   end
 
   definition pi_equiv_of_is_contr_right [constructor] [H : Πa, is_contr (B a)]
diff --git a/hott/types/sigma.hlean b/hott/types/sigma.hlean
index 282b1b2f1..25ebebfb5 100644
--- a/hott/types/sigma.hlean
+++ b/hott/types/sigma.hlean
@@ -280,7 +280,7 @@ namespace sigma
   equiv.MK
     (λu, (center_eq u.1)⁻¹ ▸ u.2)
     (λb, ⟨!center, b⟩)
-    abstract (λb, ap (λx, x ▸ b) !hprop_eq_of_is_contr) end
+    abstract (λb, ap (λx, x ▸ b) !prop_eq_of_is_contr) end
     abstract (λu, sigma_eq !center_eq !tr_pathover) end
 
   /- Associativity -/
@@ -421,7 +421,7 @@ namespace sigma
   equiv.mk sigma.coind_unc _
   end
 
-  /- Subtypes (sigma types whose second components are hprops) -/
+  /- Subtypes (sigma types whose second components are props) -/
 
   definition subtype [reducible] {A : Type} (P : A → Type) [H : Πa, is_prop (P a)] :=
   Σ(a : A), P a
@@ -461,7 +461,7 @@ namespace sigma
       exact IH _ _ _ _}
   end
 
-  theorem is_trunc_subtype (B : A → hprop) (n : trunc_index)
+  theorem is_trunc_subtype (B : A → Prop) (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_prop)
 
diff --git a/hott/types/trunc.hlean b/hott/types/trunc.hlean
index 9928b2b21..8d1ef9047 100644
--- a/hott/types/trunc.hlean
+++ b/hott/types/trunc.hlean
@@ -6,7 +6,7 @@ Authors: Floris van Doorn
 Properties of is_trunc and trunctype
 -/
 
--- NOTE: the fact that (is_trunc n A) is a mere proposition is proved in .hprop_trunc
+-- NOTE: the fact that (is_trunc n A) is a mere proposition is proved in .prop_trunc
 
 import types.pi types.eq types.equiv ..function
 
@@ -75,7 +75,7 @@ namespace is_trunc
     fapply is_trunc_equiv_closed,
       {apply equiv.symm, apply eq_equiv_equiv},
     induction n,
-      {apply @is_contr_of_inhabited_hprop,
+      {apply @is_contr_of_inhabited_prop,
         {apply is_trunc_is_embedding_closed,
           {apply is_embedding_to_fun} ,
           {exact unit.star}},
@@ -166,7 +166,7 @@ namespace is_trunc
   begin
     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 a, exact is_contr_of_inhabited_prop a,
         intro H, apply is_prop_of_imp_is_contr, exact H},
     { apply is_trunc_iff_is_contr_loop_succ},
   end
@@ -242,7 +242,7 @@ namespace trunc
     : transport (λa, trunc n (P a)) p (tr x) = tr (p ▸ x) :=
   by induction p; reflexivity
 
-  definition image {A B : Type} (f : A → B) (b : B) : hprop := ∥ fiber f b ∥
+  definition image {A B : Type} (f : A → B) (b : B) : Prop := ∥ fiber f b ∥
 
   -- truncation of pointed types
   definition ptrunc [constructor] (n : trunc_index) (X : Type*) : Type* :=
diff --git a/src/emacs/lean-syntax.el b/src/emacs/lean-syntax.el
index 79ff2e6c5..b905f379a 100644
--- a/src/emacs/lean-syntax.el
+++ b/src/emacs/lean-syntax.el
@@ -27,7 +27,7 @@
 (defconst lean-keywords1-regexp
   (eval `(rx word-start (or ,@lean-keywords1) word-end)))
 (defconst lean-keywords2
-  '("by+" "begin+" "example.")
+  '("by+" "begin+")
   "lean keywords ending with 'symbol'")
 (defconst lean-keywords2-regexp
   (eval `(rx word-start (or ,@lean-keywords2) symbol-end)))
@@ -172,10 +172,11 @@
      ("\\(set_option\\)[ \t]*\\([^ \t\n]*\\)" (2 'font-lock-constant-face))
      (,lean-keywords2-regexp . 'font-lock-keyword-face)
      (,lean-keywords1-regexp . 'font-lock-keyword-face)
+     (,(rx word-start (group "example") ".") (1 'font-lock-keyword-face))
      (,(rx (or "∎")) . 'font-lock-keyword-face)
      ;; Types
      (,(rx word-start (or "Prop" "Type" "Type'" "Type₊" "Type₀" "Type₁" "Type₂" "Type₃" "Type*" "Set") symbol-end) . 'font-lock-type-face)
-     (,(rx word-start (group "Type") ".") (1 'font-lock-type-face))
+     (,(rx word-start (group (or "Prop" "Type" "Set")) ".") (1 'font-lock-type-face))
      ;; String
      ("\"[^\"]*\"" . 'font-lock-string-face)
      ;; ;; Constants