From facd94a1b4c32bd901a4870cdf341492b57070fb Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpv@andrew.cmu.edu>
Date: Mon, 15 Feb 2016 20:59:38 -0500
Subject: [PATCH] feat(hott): various changes

more about pointed truncated types, including pointed sets.
also increase the priority of some basic instances that nat/num/pos_num/trunc_index have 0, 1 and + (in both libraries)
also move the notation + for sum into the namespace sum, to (sometimes) avoid overloading with add
---
 hott/algebra/homotopy_group.hlean   | 32 ++++++------
 hott/homotopy/connectedness.hlean   |  2 +-
 hott/init/default.hlean             |  2 +-
 hott/init/equiv.hlean               |  9 ++--
 hott/init/logic.hlean               |  1 -
 hott/init/reserved_notation.hlean   |  5 +-
 hott/init/trunc.hlean               | 36 +++++++-------
 hott/init/types.hlean               |  1 +
 hott/types/pointed.hlean            | 76 ++++++++++++++++++++++++-----
 hott/types/pointed2.hlean           |  5 --
 hott/types/trunc.hlean              | 10 ++--
 library/init/reserved_notation.lean |  3 ++
 src/emacs/lean-syntax.el            |  4 +-
 13 files changed, 123 insertions(+), 63 deletions(-)

diff --git a/hott/algebra/homotopy_group.hlean b/hott/algebra/homotopy_group.hlean
index e97dabcd5a..272bbab796 100644
--- a/hott/algebra/homotopy_group.hlean
+++ b/hott/algebra/homotopy_group.hlean
@@ -12,15 +12,15 @@ open nat eq pointed trunc is_trunc algebra
 
 namespace eq
 
+  definition phomotopy_group [constructor] (n : ℕ) (A : Type*) : Set* :=
+  ptrunc 0 (Ω[n] A)
+
   definition homotopy_group [reducible] (n : ℕ) (A : Type*) : Type :=
-  trunc 0 (Ω[n] A)
+  phomotopy_group n A
 
+  notation `π*[`:95  n:0    `] `:0 A:95 := phomotopy_group n A
   notation `π[`:95 n:0 `] `:0 A:95 := homotopy_group n A
 
-  definition pointed_homotopy_group [instance] [constructor] (n : ℕ) (A : Type*)
-    : pointed (π[n] A) :=
-  pointed.mk (tr rfln)
-
   definition group_homotopy_group [instance] [constructor] (n : ℕ) (A : Type*)
     : group (π[succ n] A) :=
   trunc_group concat inverse idp con.assoc idp_con con_idp con.left_inv
@@ -31,21 +31,17 @@ namespace eq
 
   local attribute comm_group_homotopy_group [instance]
 
-  definition pType_homotopy_group [constructor] (n : ℕ) (A : Type*) : Type* :=
-  pointed.Mk (π[n] A)
-
-  definition Group_homotopy_group [constructor] (n : ℕ) (A : Type*) : Group :=
+  definition ghomotopy_group [constructor] (n : ℕ) (A : Type*) : Group :=
   Group.mk (π[succ n] A) _
 
-  definition CommGroup_homotopy_group [constructor] (n : ℕ) (A : Type*) : CommGroup :=
+  definition cghomotopy_group [constructor] (n : ℕ) (A : Type*) : CommGroup :=
   CommGroup.mk (π[succ (succ n)] A) _
 
   definition fundamental_group [constructor] (A : Type*) : Group :=
-  Group_homotopy_group zero A
+  ghomotopy_group zero A
 
-  notation `πP[`:95  n:0    `] `:0 A:95 := pType_homotopy_group n A
-  notation `πG[`:95  n:0 ` +1] `:0 A:95 := Group_homotopy_group n A
-  notation `πaG[`:95 n:0 ` +2] `:0 A:95 := CommGroup_homotopy_group n A
+  notation `πG[`:95  n:0 ` +1] `:0 A:95 := ghomotopy_group n A
+  notation `πaG[`:95 n:0 ` +2] `:0 A:95 := cghomotopy_group n A
 
   prefix `π₁`:95 := fundamental_group
 
@@ -74,11 +70,17 @@ namespace eq
     revert A, induction m with m IH: intro A,
     { reflexivity},
     { esimp [iterated_ploop_space, nat.add], refine !homotopy_group_succ_in ⬝ _, refine !IH ⬝ _,
-      exact ap (Group_homotopy_group n) !loop_space_succ_eq_in⁻¹}
+      exact ap (ghomotopy_group n) !loop_space_succ_eq_in⁻¹}
   end
 
   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_set
 
+  definition phomotopy_group_functor [constructor] (n : ℕ) {A B : Type*} (f : A →* B)
+    : π*[n] A →* π*[n] B :=
+  ptrunc_functor 0 (apn n f)
+
+  notation `π→*[`:95  n:0    `] `:0 f:95 := phomotopy_group_functor n f
+
 end eq
diff --git a/hott/homotopy/connectedness.hlean b/hott/homotopy/connectedness.hlean
index 2c6b5dba9c..6c270fe512 100644
--- a/hott/homotopy/connectedness.hlean
+++ b/hott/homotopy/connectedness.hlean
@@ -111,7 +111,7 @@ namespace homotopy
     begin
       intro b,
       apply is_contr.mk (@is_retraction.sect _ _ _ s (λa, tr (fiber.mk a idp)) b),
-      apply trunc.rec, apply fiber.rec, intros a p,
+      esimp, apply trunc.rec, apply fiber.rec, intros a p,
       apply transport
                (λz : (Σy, h a = y), @sect _ _ _ s (λa, tr (mk a idp)) (sigma.pr1 z) =
                                     tr (fiber.mk a (sigma.pr2 z)))
diff --git a/hott/init/default.hlean b/hott/init/default.hlean
index 1882be93ae..8d3e80475e 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 (Prop.mk Set.mk)
+  export [abbreviation] is_trunc
 end core
diff --git a/hott/init/equiv.hlean b/hott/init/equiv.hlean
index 993c24c2d1..5fc445c8ae 100644
--- a/hott/init/equiv.hlean
+++ b/hott/init/equiv.hlean
@@ -68,7 +68,7 @@ namespace is_equiv
   parameters {A B : Type} (f : A → B) (g : B → A)
             (ret : Πb, f (g b) = b) (sec : Πa, g (f a) = a)
 
-  private abbreviation adjointify_left_inv' (a : A) : g (f a) = a :=
+  private definition adjointify_left_inv' (a : A) : g (f a) = a :=
   ap g (ap f (inverse (sec a))) ⬝ ap g (ret (f a)) ⬝ sec a
 
   private theorem adjointify_adj' (a : A) : ret (f a) = ap f (adjointify_left_inv' a) :=
@@ -97,12 +97,11 @@ namespace is_equiv
       ... = retrfa⁻¹ ⬝ ap f (ap g (ap f (sec a)⁻¹) ⬝ ap g (ret (f a))) ⬝ ap f (sec a)   : by rewrite ap_con
       ... = retrfa⁻¹ ⬝ (ap f (ap g (ap f (sec a)⁻¹) ⬝ ap g (ret (f a))) ⬝ ap f (sec a)) : by rewrite con.assoc'
       ... = retrfa⁻¹ ⬝ ap f ((ap g (ap f (sec a)⁻¹) ⬝ ap g (ret (f a))) ⬝ sec a)        : by rewrite -ap_con,
-  have eq4 : ret (f a) = ap f ((ap g (ap f (sec a)⁻¹) ⬝ ap g (ret (f a))) ⬝ sec a),
-    from eq_of_idp_eq_inv_con eq3,
-  eq4
+  show ret (f a) = ap f ((ap g (ap f (sec a)⁻¹) ⬝ ap g (ret (f a))) ⬝ sec a),
+    from eq_of_idp_eq_inv_con eq3
 
   definition adjointify [constructor] : is_equiv f :=
-  is_equiv.mk f g ret abstract adjointify_left_inv' end adjointify_adj'
+  is_equiv.mk f g ret adjointify_left_inv' adjointify_adj'
   end
 
   -- Any function pointwise equal to an equivalence is an equivalence as well.
diff --git a/hott/init/logic.hlean b/hott/init/logic.hlean
index 3214923bec..e7ec11291a 100644
--- a/hott/init/logic.hlean
+++ b/hott/init/logic.hlean
@@ -167,7 +167,6 @@ prod.rec (λHa Hb, prod.mk Hb Ha)
 /- sum -/
 
 infixr ⊎ := sum
-infixr + := sum
 
 attribute sum.rec [elim]
 
diff --git a/hott/init/reserved_notation.hlean b/hott/init/reserved_notation.hlean
index caac2d23e2..ee2cabbef2 100644
--- a/hott/init/reserved_notation.hlean
+++ b/hott/init/reserved_notation.hlean
@@ -41,7 +41,7 @@ definition bit0 [reducible] {A : Type} [s  : has_add A] (a  : A)
 definition bit1 [reducible] {A : Type} [s₁ : has_one A] [s₂ : has_add A] (a : A) : A :=
 add (bit0 a) one
 
-definition num_has_zero [reducible] [instance] : has_zero num :=
+definition num_has_zero [reducible] [instance]  : has_zero num :=
 has_zero.mk num.zero
 
 definition num_has_one [reducible] [instance] : has_one num :=
@@ -102,6 +102,9 @@ namespace nat
     (λ n, pos_num.rec (succ zero) (λ n r, nat.add (nat.add r r) (succ zero)) (λ n r, nat.add r r) n) n
 end nat
 
+attribute pos_num_has_add pos_num_has_one num_has_zero num_has_one num_has_add
+          [instance] [priority nat.prio]
+
 definition nat_has_zero [reducible] [instance] [priority nat.prio] : has_zero nat :=
 has_zero.mk nat.zero
 
diff --git a/hott/init/trunc.hlean b/hott/init/trunc.hlean
index 617853edf9..e0bf90ad8e 100644
--- a/hott/init/trunc.hlean
+++ b/hott/init/trunc.hlean
@@ -23,10 +23,10 @@ namespace is_trunc
 
   open trunc_index
 
-  definition has_zero_trunc_index [instance] [reducible] : has_zero trunc_index :=
+  definition has_zero_trunc_index [instance] [priority 2000] [reducible] : has_zero trunc_index :=
   has_zero.mk (succ (succ minus_two))
 
-  definition has_one_trunc_index [instance] [reducible] : has_one trunc_index :=
+  definition has_one_trunc_index [instance] [priority 2000] [reducible] : has_one trunc_index :=
   has_one.mk (succ (succ (succ minus_two)))
 
   /-
@@ -55,14 +55,14 @@ namespace is_trunc
   definition leq [reducible] (n m : trunc_index) : Type₀ :=
   trunc_index.rec_on n (λm, unit) (λ n p m, trunc_index.rec_on m (λ p, empty) (λ m q p, p m) p) m
 
-  definition has_le_trunc_index [instance] [reducible] : has_le trunc_index :=
+  definition has_le_trunc_index [instance] [priority 2000] [reducible] : has_le trunc_index :=
   has_le.mk leq
 
   end trunc_index
 
   attribute trunc_index.tr_add [reducible]
   infix `+2+`:65 := trunc_index.add_plus_two
-  definition has_add_trunc_index [instance] [reducible] : has_add ℕ₋₂ :=
+  definition has_add_trunc_index [instance] [priority 2000] [reducible] : has_add ℕ₋₂ :=
   has_add.mk trunc_index.tr_add
 
   namespace trunc_index
@@ -343,22 +343,22 @@ structure trunctype (n : trunc_index) :=
   (carrier : Type)
   (struct : is_trunc n carrier)
 
+notation n `-Type` := trunctype n
+abbreviation Prop := -1-Type
+abbreviation Set  := 0-Type
+
+attribute trunctype.carrier [coercion]
+attribute trunctype.struct [instance] [priority 1400]
+
+protected abbreviation Prop.mk := @trunctype.mk -1
+protected abbreviation Set.mk := @trunctype.mk (-1.+1)
+
+protected definition trunctype.mk' [constructor] (n : trunc_index) (A : Type) [H : is_trunc n A]
+  : n-Type :=
+trunctype.mk A H
+
 namespace is_trunc
 
-  attribute trunctype.carrier [coercion]
-  attribute trunctype.struct [instance] [priority 1400]
-
-  notation n `-Type` := trunctype n
-  abbreviation Prop := -1-Type
-  abbreviation Set  := 0-Type
-
-  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 :=
-  trunctype.mk A H
-
   definition tlift.{u v} [constructor] {n : trunc_index} (A : trunctype.{u} n)
     : trunctype.{max u v} n :=
   trunctype.mk (lift A) !is_trunc_lift
diff --git a/hott/init/types.hlean b/hott/init/types.hlean
index bac36fc19b..7080922718 100644
--- a/hott/init/types.hlean
+++ b/hott/init/types.hlean
@@ -43,6 +43,7 @@ end sigma
 -- --------
 
 namespace sum
+  infixr + := sum
   namespace low_precedence_plus
     reserve infixr ` + `:25  -- conflicts with notation for addition
     infixr ` + ` := sum
diff --git a/hott/types/pointed.hlean b/hott/types/pointed.hlean
index ea710e7d47..78830d21de 100644
--- a/hott/types/pointed.hlean
+++ b/hott/types/pointed.hlean
@@ -6,7 +6,7 @@ Authors: Jakob von Raumer, Floris van Doorn
 Ported from Coq HoTT
 -/
 
-import arity .eq .bool .unit .sigma .nat.basic
+import arity .eq .bool .unit .sigma .nat.basic prop_trunc
 open is_trunc eq prod sigma nat equiv option is_equiv bool unit algebra equiv.ops
 
 structure pointed [class] (A : Type) :=
@@ -18,13 +18,22 @@ structure pType :=
 
 notation `Type*` := pType
 
+section
+  universe variable u
+  structure ptrunctype (n : trunc_index) extends trunctype.{u} n, pType.{u}
+end
+
+notation n `-Type*` := ptrunctype n
+abbreviation pSet  [parsing_only] := 0-Type*
+notation `Set*` := pSet
+
 namespace pointed
   attribute pType.carrier [coercion]
   variables {A B : Type}
 
   definition pt [unfold 2] [H : pointed A] := point A
   definition Point [unfold 1] (A : Type*) := pType.Point A
-  definition carrier [unfold 1] (A : Type*) := pType.carrier A
+  abbreviation carrier [unfold 1] (A : Type*) := pType.carrier A
   protected definition Mk [constructor] {A : Type} (a : A) := pType.mk A a
   protected definition MK [constructor] (A : Type) (a : A) := pType.mk A a
   protected definition mk' [constructor] (A : Type) [H : pointed A] : Type* :=
@@ -62,12 +71,6 @@ namespace pointed
 
   infixr ` ×* `:35 := pprod
 
-  definition pbool [constructor] : Type* :=
-  pointed.mk' bool
-
-  definition punit [constructor] : Type* :=
-  pointed.Mk unit.star
-
   definition pointed_fun_closed [constructor] (f : A → B) [H : pointed A] : pointed B :=
   pointed.mk (f pt)
 
@@ -97,6 +100,10 @@ namespace pointed
     { rewrite [cast_ua,p]},
   end
 
+  definition pType_eq_elim {A B : Type*} (p : A = B :> Type*)
+    : Σ(p : carrier A = carrier B :> Type), cast p pt = pt :=
+  by induction p; exact ⟨idp, idp⟩
+
   protected definition pType.sigma_char.{u} : pType.{u} ≃ Σ(X : Type.{u}), X :=
   begin
     fapply equiv.MK,
@@ -111,9 +118,56 @@ namespace pointed
   postfix `₊`:(max+1) := add_point
   -- the inclusion A → A₊ is called "some", the extra point "pt" or "none" ("@none A")
 
-end pointed
+end pointed open pointed
+
+protected definition ptrunctype.mk' [constructor] (n : trunc_index)
+  (A : Type) [pointed A] [is_trunc n A] : n-Type* :=
+ptrunctype.mk A _ pt
+
+protected definition pSet.mk [constructor] := @ptrunctype.mk (-1.+1)
+protected definition pSet.mk' [constructor] := ptrunctype.mk' (-1.+1)
+
+definition ptrunctype_of_trunctype [constructor] {n : trunc_index} (A : n-Type) (a : A) : n-Type* :=
+ptrunctype.mk A _ a
+
+definition ptrunctype_of_pType [constructor] {n : trunc_index} (A : Type*) (H : is_trunc n A)
+  : n-Type* :=
+ptrunctype.mk A _ pt
+
+definition pSet_of_Set [constructor] (A : Set) (a : A) : Set* :=
+ptrunctype.mk A _ a
+
+definition pSet_of_pType [constructor] (A : Type*) (H : is_set A) : Set* :=
+ptrunctype.mk A _ pt
+
+attribute pType._trans_to_carrier ptrunctype.to_pType ptrunctype.to_trunctype [unfold 2]
+
+definition ptrunctype_eq {n : trunc_index} {A B : n-Type*} (p : A = B :> Type) (q : cast p pt = pt)
+  : A = B :=
+begin
+  induction A with A HA a, induction B with B HB b, esimp at *,
+  induction p, induction q,
+  esimp,
+  refine ap010 (ptrunctype.mk A) _ a,
+  exact !is_prop.elim
+end
+
+definition ptrunctype_eq_of_pType_eq {n : trunc_index} {A B : n-Type*} (p : A = B :> Type*)
+  : A = B :=
+begin
+  cases pType_eq_elim p with q r,
+  exact ptrunctype_eq q r
+end
+
 
 namespace pointed
+
+  definition pbool [constructor] : Set* :=
+  pSet.mk' bool
+
+  definition punit [constructor] : Set* :=
+  pSet.mk' unit
+
   /- properties of iterated loop space -/
   variable (A : Type*)
   definition loop_space_succ_eq_in (n : ℕ) : Ω[succ n] A = Ω[n] (Ω A) :=
@@ -249,7 +303,7 @@ namespace pointed
 
   -- set_option pp.notation false
   -- definition pmap_equiv_right (A : Type*) (B : Type)
-  --   : (Σ(b : B), map₊ A (pointed.Mk b)) ≃ (A → B) :=
+  --   : (Σ(b : B), A →* (pointed.Mk b)) ≃ (A → B) :=
   -- begin
   --   fapply equiv.MK,
   --   { intro u a, cases u with b f, cases f with f p, esimp at f, exact f a},
@@ -262,7 +316,7 @@ namespace pointed
   --     }
   -- end
 
-  definition pmap_bool_equiv (B : Type*) : map₊ pbool B ≃ B :=
+  definition pmap_bool_equiv (B : Type*) : (pbool →* B) ≃ B :=
   begin
     fapply equiv.MK,
     { intro f, cases f with f p, exact f tt},
diff --git a/hott/types/pointed2.hlean b/hott/types/pointed2.hlean
index a3a93cee9c..c9ae953620 100644
--- a/hott/types/pointed2.hlean
+++ b/hott/types/pointed2.hlean
@@ -17,11 +17,6 @@ open eq is_equiv equiv equiv.ops pointed is_trunc
 
 structure pequiv (A B : Type*) extends equiv A B, pmap A B
 
-section
-  universe variable u
-  structure ptrunctype (n : trunc_index) extends trunctype.{u} n, pType.{u}
-end
-
 namespace pointed
 
   variables {A B C : Type*}
diff --git a/hott/types/trunc.hlean b/hott/types/trunc.hlean
index f1d6bd9bfd..b48f689a0b 100644
--- a/hott/types/trunc.hlean
+++ b/hott/types/trunc.hlean
@@ -242,11 +242,15 @@ 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) : Prop := ∥ fiber f b ∥
+  definition image [constructor] {A B : Type} (f : A → B) (b : B) : Prop := ∥ fiber f b ∥
+
+  definition image.mk [constructor] {A B : Type} {f : A → B} {b : B} (a : A) (p : f a = b)
+    : image f b :=
+  tr (fiber.mk a p)
 
   -- truncation of pointed types
-  definition ptrunc [constructor] (n : trunc_index) (X : Type*) : Type* :=
-  pointed.MK (trunc n X) (tr pt)
+  definition ptrunc [constructor] (n : trunc_index) (X : Type*) : n-Type* :=
+  ptrunctype.mk (trunc n X) _ (tr pt)
 
   definition ptrunc_functor [constructor] {X Y : Type*} (n : ℕ₋₂) (f : X →* Y)
     : ptrunc n X →* ptrunc n Y :=
diff --git a/library/init/reserved_notation.lean b/library/init/reserved_notation.lean
index 8a744c2dd4..8317a69bf3 100644
--- a/library/init/reserved_notation.lean
+++ b/library/init/reserved_notation.lean
@@ -101,6 +101,9 @@ namespace nat
     (λ n, pos_num.rec (succ zero) (λ n r, nat.add (nat.add r r) (succ zero)) (λ n r, nat.add r r) n) n
 end nat
 
+attribute pos_num_has_add pos_num_has_one num_has_zero num_has_one num_has_add
+          [instance] [priority nat.prio]
+
 definition nat_has_zero [reducible] [instance] [priority nat.prio] : has_zero nat :=
 has_zero.mk nat.zero
 
diff --git a/src/emacs/lean-syntax.el b/src/emacs/lean-syntax.el
index 4970bf1e5b..c46c25e1f6 100644
--- a/src/emacs/lean-syntax.el
+++ b/src/emacs/lean-syntax.el
@@ -175,8 +175,8 @@
      (,(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*" "pType" "Set") symbol-end) . 'font-lock-type-face)
-     (,(rx word-start (group (or "Prop" "Type" "Set" "pType")) ".") (1 'font-lock-type-face))
+     (,(rx word-start (or "Prop" "Type" "Type'" "Type₊" "Type₀" "Type₁" "Type₂" "Type₃" "Type*" "pType" "Set" "pSet" "Set*") symbol-end) . 'font-lock-type-face)
+     (,(rx word-start (group (or "Prop" "Type" "Set" "pType" "pSet")) ".") (1 'font-lock-type-face))
      ;; String
      ("\"[^\"]*\"" . 'font-lock-string-face)
      ;; ;; Constants