fix(types): change some definitions to theorems

hott/types/pi.hlean

@@ -249,7 +249,7 @@ namespace pi
 
   /- Truncatedness: any dependent product of n-types is an n-type -/
 
-  definition is_trunc_pi (B : A → Type) (n : trunc_index)
+  theorem is_trunc_pi (B : A → Type) (n : trunc_index)
       [H : ∀a, is_trunc n (B a)] : is_trunc n (Πa, B a) :=
   begin
     revert B H,
@@ -269,23 +269,23 @@ namespace pi
               is_trunc_eq n (f a) (g a)}
   end
   local attribute is_trunc_pi [instance]
-  definition is_trunc_pi_eq [instance] [priority 500] (n : trunc_index) (f g : Πa, B a)
+  theorem is_trunc_pi_eq [instance] [priority 500] (n : trunc_index) (f g : Πa, B a)
       [H : ∀a, is_trunc n (f a = g a)] : is_trunc n (f = g) :=
   begin
     apply is_trunc_equiv_closed_rev,
     apply eq_equiv_homotopy
   end
 
-  definition is_trunc_not [instance] (n : trunc_index) (A : Type) : is_trunc (n.+1) ¬A :=
+  theorem is_trunc_not [instance] (n : trunc_index) (A : Type) : is_trunc (n.+1) ¬A :=
   by unfold not;exact _
 
-  definition is_hprop_pi_eq [instance] [priority 490] (a : A) : is_hprop (Π(a' : A), a = a') :=
+  theorem is_hprop_pi_eq [instance] [priority 490] (a : A) : is_hprop (Π(a' : A), a = a') :=
   is_hprop_of_imp_is_contr
   ( assume (f : Πa', a = a'),
     assert H : is_contr A, from is_contr.mk a f,
     _)
 
-  definition is_hprop_neg (A : Type) : is_hprop (¬A) := _
+  theorem is_hprop_neg (A : Type) : is_hprop (¬A) := _
 
   /- Symmetry of Π -/
   definition is_equiv_flip [instance] {P : A → A' → Type}

hott/types/prod.hlean

@@ -200,7 +200,7 @@ namespace prod
     : (A → B) × (A → C) ≃ (A → (B × C)) :=
   !equiv_prod_corec
 
-  definition is_trunc_prod (A B : Type) (n : trunc_index) [HA : is_trunc n A] [HB : is_trunc n B]
+  theorem is_trunc_prod (A B : Type) (n : trunc_index) [HA : is_trunc n A] [HB : is_trunc n B]
     : is_trunc n (A × B) :=
   begin
     revert A B HA HB, induction n with n IH, all_goals intro A B HA HB,

hott/types/sigma.hlean

@@ -410,7 +410,7 @@ namespace sigma
   equiv.mk !subtype_eq _
 
   /- truncatedness -/
-  definition is_trunc_sigma (B : A → Type) (n : trunc_index)
+  theorem is_trunc_sigma (B : A → Type) (n : trunc_index)
       [HA : is_trunc n A] [HB : Πa, is_trunc n (B a)] : is_trunc n (Σa, B a) :=
   begin
   revert A B HA HB,

hott/types/sum.hlean

@@ -147,7 +147,7 @@ namespace sum
       all_goals (intro z; induction z; all_goals reflexivity)
   end
 
-  definition sum_assoc_equiv (A B C : Type) : A + (B + C) ≃ (A + B) + C :=
+  definition sum_assoc_equiv [constructor] (A B C : Type) : A + (B + C) ≃ (A + B) + C :=
   begin
     fapply equiv.MK,
       all_goals try (intro z; induction z with u v;
@@ -170,7 +170,8 @@ namespace sum
 
   /- universal property -/
 
-  definition sum_rec_unc {P : A + B → Type} (fg : (Πa, P (inl a)) × (Πb, P (inr b))) : Πz, P z :=
+  definition sum_rec_unc [unfold 5] {P : A + B → Type} (fg : (Πa, P (inl a)) × (Πb, P (inr b)))
+    : Πz, P z :=
   sum.rec fg.1 fg.2
 
   definition is_equiv_sum_rec [constructor] (P : A + B → Type)
@@ -192,7 +193,7 @@ namespace sum
   /- truncatedness -/
 
   variables (A B)
-  definition is_trunc_sum (n : trunc_index) [HA : is_trunc (n.+2) A]  [HB : is_trunc (n.+2) B]
+  theorem is_trunc_sum (n : trunc_index) [HA : is_trunc (n.+2) A]  [HB : is_trunc (n.+2) B]
     : is_trunc (n.+2) (A + B) :=
   begin
     apply is_trunc_succ_intro, intro z z',
@@ -201,7 +202,7 @@ namespace sum
     all_goals exact _,
   end
 
-  definition is_trunc_sum_excluded (n : trunc_index) [HA : is_trunc n A]  [HB : is_trunc n B]
+  theorem is_trunc_sum_excluded (n : trunc_index) [HA : is_trunc n A]  [HB : is_trunc n B]
     (H : A → B → empty) : is_trunc n (A + B) :=
   begin
     induction n with n IH,
@@ -243,13 +244,13 @@ end sum
 namespace decidable
   open sum pi
 
-  definition decidable_equiv (A : Type) : decidable A ≃ A + ¬A :=
+  definition decidable_equiv [constructor] (A : Type) : decidable A ≃ A + ¬A :=
   begin
     fapply equiv.MK:intro a;induction a:try (constructor;assumption;now),
     all_goals reflexivity
   end
 
-  definition is_trunc_decidable (A : Type) (n : trunc_index) [H : is_trunc n A] :
+  definition is_trunc_decidable [constructor] (A : Type) (n : trunc_index) [H : is_trunc n A] :
     is_trunc n (decidable A) :=
   begin
     apply is_trunc_equiv_closed_rev,

src/emacs/lean-input.el

@@ -678,13 +678,15 @@ order for the change to take effect."
   ;; \omicron \Omicron
   ;; \pi \Pi
   ("Gr"  . ("ρ"))  ("GR"  . ("Ρ"))
-  ("Gs"  . ("σ"))  ("GS"  . ("Σ")) ("S"  . ("Σ"))
+  ("Gs"  . ("σ"))  ("GS"  . ("Σ")) 
   ("Gt"  . ("τ"))  ("GT"  . ("Τ"))
   ("Gu"  . ("υ"))  ("GU"  . ("Υ"))
   ("Gf"  . ("φ"))  ("GF"  . ("Φ"))
   ("Gc"  . ("χ"))  ("GC"  . ("Χ"))
   ("Gp"  . ("ψ"))  ("GP"  . ("Ψ"))
   ("Go"  . ("ω"))  ("GO"  . ("Ω"))
+  ;; even shorter versions for central type constructors
+  ("S"   . ("Σ"))  ("P"   . ("Π")) 
 
   ;; Mathematical characters