feat(hott.circle): prove that the fundamental group of the circle is equal to the integers, as groups

Also many minor fixes at various places

hott/algebra/binary.hlean

@@ -8,7 +8,7 @@ Authors: Leonardo de Moura, Jeremy Avigad
 General properties of binary operations.
 -/
 
-open eq.ops function
+open eq.ops function equiv
 
 namespace binary
   section
@@ -82,3 +82,34 @@ namespace binary
     {A B : Type} (f : A → A → A) (g : B → A) (lcomm : left_commutative f) : left_commutative (compose_left f g) :=
   λ a b₁ b₂, !lcomm
 end binary
+
+open eq
+namespace is_equiv
+  definition inv_preserve_binary {A B : Type} (f : A → B) [H : is_equiv f]
+    (mA : A → A → A) (mB : B → B → B) (H : Π(a a' : A), mB (f a) (f a') = f (mA a a'))
+    (b b' : B) : f⁻¹ (mB b b') = mA (f⁻¹ b) (f⁻¹ b') :=
+  begin
+  have H2 : f⁻¹ (mB (f (f⁻¹ b)) (f (f⁻¹ b'))) = f⁻¹ (f (mA (f⁻¹ b) (f⁻¹ b'))), from ap f⁻¹ !H,
+  rewrite [+right_inv f at H2,left_inv f at H2,▸* at H2,H2]
+  end
+
+  definition preserve_binary_of_inv_preserve {A B : Type} (f : A → B) [H : is_equiv f]
+    (mA : A → A → A) (mB : B → B → B) (H : Π(b b' : B), mA (f⁻¹ b) (f⁻¹ b') = f⁻¹ (mB b b'))
+    (a a' : A) : f (mA a a') = mB (f a) (f a') :=
+  begin
+  have H2 : f (mA (f⁻¹ (f a)) (f⁻¹ (f a'))) = f (f⁻¹ (mB (f a) (f a'))), from ap f !H,
+  rewrite [right_inv f at H2,+left_inv f at H2,▸* at H2,H2]
+  end
+end is_equiv
+namespace equiv
+  open is_equiv equiv.ops
+  definition inv_preserve_binary {A B : Type} (f : A ≃ B)
+    (mA : A → A → A) (mB : B → B → B) (H : Π(a a' : A), mB (f a) (f a') = f (mA a a'))
+    (b b' : B) : f⁻¹ (mB b b') = mA (f⁻¹ b) (f⁻¹ b') :=
+  inv_preserve_binary f mA mB H b b'
+
+  definition preserve_binary_of_inv_preserve {A B : Type} (f : A ≃ B)
+    (mA : A → A → A) (mB : B → B → B) (H : Π(b b' : B), mA (f⁻¹ b) (f⁻¹ b') = f⁻¹ (mB b b'))
+    (a a' : A) : f (mA a a') = mB (f a) (f a') :=
+  preserve_binary_of_inv_preserve f mA mB H a a'
+end equiv

hott/algebra/category/category.hlean

@@ -15,7 +15,7 @@ open iso is_equiv eq is_trunc
 -- is an equivalecnce.
 namespace category
   definition is_univalent [reducible] {ob : Type} (C : precategory ob) :=
-  Π(a b : ob), is_equiv (@iso_of_eq ob C a b)
+  Π(a b : ob), is_equiv (iso_of_eq : a = b → a ≅ b)
 
   structure category [class] (ob : Type) extends parent : precategory ob :=
   mk' :: (iso_of_path_equiv : is_univalent parent)
@@ -37,7 +37,7 @@ namespace category
   attribute iso_of_path_equiv [instance]
 
   definition eq_of_iso [reducible] {a b : ob} : a ≅ b → a = b :=
-  iso_of_eq⁻¹ᵉ
+  iso_of_eq⁻¹ᶠ
 
   definition is_trunc_1_ob : is_trunc 1 ob :=
   begin

hott/algebra/category/constructions/hset.hlean

@@ -49,7 +49,7 @@ namespace category
     open sigma.ops
     definition subtype_eq_inv {A : Type} {B : A → Type} [H : Πa, is_hprop (B a)] (u v : Σa, B a)
       : u = v → u.1 = v.1 :=
-    (subtype_eq u v)⁻¹ᵉ
+    (subtype_eq u v)⁻¹ᶠ
     local attribute subtype_eq_inv [reducible]
     definition is_equiv_subtype_eq_inv {A : Type} {B : A → Type} [H : Πa, is_hprop (B a)] (u v : Σa, B a)
       : is_equiv (subtype_eq_inv u v) :=
@@ -72,7 +72,7 @@ namespace category
     definition equiv_eq_iso (A B : Precategory_hset) : (A ≃ B) = (A ≅ B) :=
     ua !equiv_equiv_iso
 
-    definition is_univalent_hset (A B : Precategory_hset) : is_equiv (@iso_of_eq _ _ A B) :=
+    definition is_univalent_hset (A B : Precategory_hset) : is_equiv (iso_of_eq : A = B → A ≅ B) :=
     have 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 _ _ _ _ _
@@ -85,7 +85,7 @@ namespace category
     (iso_of_eq_eq_compose A B)⁻¹ ▸ H
   end set
 
-  definition category_hset [reducible] [instance] : category hset :=
+  definition category_hset [instance] : category hset :=
   category.mk precategory_hset set.is_univalent_hset
 
   definition Category_hset [reducible] : Category :=

hott/algebra/fundamental_group.hlean

@@ -0,0 +1,89 @@
+/-
+Copyright (c) 2015 Floris van Doorn. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Module: algebra.fundamental_group
+Authors: Floris van Doorn
+
+fundamental group of a pointed space
+-/
+
+import hit.trunc algebra.group types.pointed
+
+open core eq trunc algebra is_trunc pointed
+
+namespace fundamental_group
+  section
+  parameters {A : Type} (a : A)
+  definition carrier [reducible] : Type :=
+  trunc 0 (a = a)
+
+  local abbreviation G := carrier
+
+  definition mul (g h : G) : G :=
+  begin
+    apply trunc.rec_on g, intro p,
+    apply trunc.rec_on h, intro q,
+    exact tr (p ⬝ q)
+  end
+
+  definition inv (g : G) : G :=
+  begin
+    apply trunc.rec_on g, intro p,
+    exact tr p⁻¹
+  end
+
+  definition one : G :=
+  tr idp
+
+  local notation 1 := one
+  local postfix ⁻¹ := inv
+  local infix * := mul
+
+  definition mul_assoc (g₁ g₂ g₃ : G) : g₁ * g₂ * g₃ = g₁ * (g₂ * g₃) :=
+  begin
+    apply trunc.rec_on g₁, intro p₁,
+    apply trunc.rec_on g₂, intro p₂,
+    apply trunc.rec_on g₃, intro p₃,
+    exact ap tr !con.assoc,
+  end
+
+  definition one_mul (g : G) : 1 * g = g :=
+  begin
+    apply trunc.rec_on g, intro p,
+    exact ap tr !idp_con,
+  end
+
+  definition mul_one (g : G) : g * 1 = g :=
+  begin
+    apply trunc.rec_on g, intro p,
+    exact idp,
+  end
+
+  definition mul_left_inv (g : G) : g⁻¹ * g = 1 :=
+  begin
+    apply trunc.rec_on g, intro p,
+    apply ap tr !con.left_inv
+  end
+
+  definition group : group G :=
+  ⦃group,
+    mul          := mul,
+    mul_assoc    := mul_assoc,
+    one          := one,
+    one_mul      := one_mul,
+    mul_one      := mul_one,
+    inv          := inv,
+    mul_left_inv := mul_left_inv,
+   is_hset_carrier := _⦄
+
+  end
+end fundamental_group
+attribute fundamental_group.group [instance] [constructor] [priority 800]
+
+definition fundamental_group [constructor] (A : Type) [H : pointed A]: Group :=
+Group.mk (fundamental_group.carrier (point A)) _
+
+namespace core
+  prefix `π₁`:95 := fundamental_group
+end core

hott/algebra/group.hlean

@@ -86,8 +86,11 @@ theorem mul.right_cancel [s : right_cancel_semigroup A] {a b c : A} :
 /- additive semigroup -/
 
 structure add_semigroup [class] (A : Type) extends has_add A :=
+(is_hset_carrier : is_hset A)
 (add_assoc : ∀a b c, add (add a b) c = add a (add b c))
 
+attribute add_semigroup.is_hset_carrier [instance]
+
 theorem add.assoc [s : add_semigroup A] (a b c : A) : a + b + c = a + (b + c) :=
 !add_semigroup.add_assoc
 
@@ -476,6 +479,17 @@ section add_comm_group
   !add.comm ▸ add_eq_of_eq_sub H
 end add_comm_group
 
+definition group_of_add_group (A : Type) [G : add_group A] : group A :=
+⦃group,
+  mul             := has_add.add,
+  mul_assoc       := add.assoc,
+  one             := !has_zero.zero,
+  one_mul         := zero_add,
+  mul_one         := add_zero,
+  inv             := has_neg.neg,
+  mul_left_inv    := add.left_inv,
+  is_hset_carrier := !add_group.is_hset_carrier⦄
+
 /- bundled structures -/
 structure Semigroup :=
 (carrier : Type) (struct : semigroup carrier)

hott/algebra/hott.hlean

@@ -0,0 +1,64 @@
+/-
+Copyright (c) 2015 Floris van Doorn. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Module: types.algebra.hott
+Author: Floris van Doorn
+
+Theorems about algebra specific to HoTT
+-/
+
+import .group arity types.pi types.hprop_trunc cubical.pathover
+
+open equiv eq equiv.ops is_trunc cubical
+
+namespace algebra
+  open Group has_mul has_inv
+  -- we prove under which conditions two groups are equal
+  universe variable l
+  variables {A B : Type.{l}}
+  definition group_eq {G H : group A} (same_mul' : Π(g h : A), @mul A G g h = @mul A H g h)
+    : G = H :=
+  begin
+    have foo : Π(g : A), @inv A G g = (@inv A G g * g) * @inv A H g,
+      from λg, !mul_inv_cancel_right⁻¹,
+    cases G with Gm Gs Gh1 G1 Gh2 Gh3 Gi Gh4,
+    cases H with Hm Hs Hh1 H1 Hh2 Hh3 Hi Hh4,
+    rewrite [↑[semigroup.to_has_mul,group.to_has_inv] at (same_mul,foo)] ,
+    have same_mul : Gm = Hm, from eq_of_homotopy2 same_mul',
+    cases same_mul,
+    have same_one : G1 = H1, from calc
+      G1 = Hm G1 H1 : Hh3
+     ... = H1 : Gh2,
+    have same_inv : Gi = Hi, from eq_of_homotopy (take g, calc
+      Gi g = Hm (Hm (Gi g) g) (Hi g) : foo
+       ... = 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,
+    cases ps, cases ph1, cases ph2, cases ph3, cases ph4, reflexivity
+  end
+
+  definition group_pathover {G : group A} {H : group B} (f : A ≃ B) : (Π(g h : A), f (g * h) = f g * f h) → G =[ua f] H :=
+  begin
+    revert H,
+    eapply (rec_on_ua3 f),
+    intros H resp_mul,
+    esimp [equiv.refl] at resp_mul, esimp,
+    apply pathover_idp_of_eq, apply group_eq,
+    exact resp_mul
+  end
+
+  definition Group_eq {G H : Group} (f : carrier G ≃ carrier H)
+    (resp_mul : Π(g h : G), f (g * h) = f g * f h) : G = H :=
+  begin
+    cases G with Gc G, cases H with Hc H,
+    apply (apd011o mk (ua f)),
+    apply group_pathover, exact resp_mul
+  end
+
+end algebra

hott/arity.hlean

@@ -9,12 +9,16 @@ Theorems about functions with multiple arguments
 -/
 
 variables {A U V W X Y Z : Type} {B : A → Type} {C : Πa, B a → Type} {D : Πa b, C a b → Type}
-          {E : Πa b c, D a b c → Type}
+          {E : Πa b c, D a b c → Type} {F : Πa b c d, E a b c d → Type}
+          {G : Πa b c d e, F a b c d e → Type} {H : Πa b c d e f, G a b c d e f → Type}
 variables {a a' : A} {u u' : U} {v v' : V} {w w' : W} {x x' x'' : X} {y y' : Y} {z z' : Z}
           {b : B a} {b' : B a'}
           {c : C a b} {c' : C a' b'}
           {d : D a b c} {d' : D a' b' c'}
           {e : E a b c d} {e' : E a' b' c' d'}
+         {ff : F a b c d e} {f' : F a' b' c' d' e'}
+          {g : G a b c d e ff} {g' : G a' b' c' d' e' f'}
+          {h : H a b c d e ff g} {h' : H a' b' c' d' e' f' g'}
 
 namespace eq
   /-
@@ -79,26 +83,46 @@ namespace eq
   definition ap01000 (f : X → Πa b c, D a b c) (Hx : x = x') : f x ∼3 f x' :=
   by intros; cases Hx; reflexivity
 
-  definition apd011 (f : Πa, B a → Z) (Ha : a = a') (Hb : (Ha ▸ b) = b')
+  definition apd011 (f : Πa, B a → Z) (Ha : a = a') (Hb : transport B Ha b = b')
       : f a b = f a' b' :=
   by cases Ha; cases Hb; reflexivity
 
-  definition apd0111 (f : Πa b, C a b → Z) (Ha : a = a') (Hb : (Ha ▸ b) = b')
+  definition apd0111 (f : Πa b, C a b → Z) (Ha : a = a') (Hb : transport B Ha b = b')
-    (Hc : apd011 C Ha Hb ▸ c = c')
+    (Hc : cast (apd011 C Ha Hb) c = c')
       : f a b c = f a' b' c' :=
   by cases Ha; cases Hb; cases Hc; reflexivity
 
-  definition apd01111 (f : Πa b c, D a b c → Z) (Ha : a = a') (Hb : (Ha ▸ b) = b')
+  definition apd01111 (f : Πa b c, D a b c → Z) (Ha : a = a') (Hb : transport B Ha b = b')
-    (Hc : apd011 C Ha Hb ▸ c = c') (Hd : apd0111 D Ha Hb Hc ▸ d = d')
+    (Hc : cast (apd011 C Ha Hb) c = c') (Hd : cast (apd0111 D Ha Hb Hc) d = d')
       : f a b c d = f a' b' c' d' :=
   by cases Ha; cases Hb; cases Hc; cases Hd; reflexivity
 
-  definition apd011111 (f : Πa b c d, E a b c d → Z) (Ha : a = a') (Hb : (Ha ▸ b) = b')
+  definition apd011111 (f : Πa b c d, E a b c d → Z) (Ha : a = a') (Hb : transport B Ha b = b')
-    (Hc : apd011 C Ha Hb ▸ c = c') (Hd : apd0111 D Ha Hb Hc ▸ d = d')
+    (Hc : cast (apd011 C Ha Hb) c = c') (Hd : cast (apd0111 D Ha Hb Hc) d = d')
-    (He : apd01111 E Ha Hb Hc Hd ▸ e = e')
+    (He : cast (apd01111 E Ha Hb Hc Hd) e = e')
     : f a b c d e = f a' b' c' d' e' :=
   by cases Ha; cases Hb; cases Hc; cases Hd; cases He; reflexivity
 
+  definition apd0111111 (f : Πa b c d e, F a b c d e → Z) (Ha : a = a') (Hb : transport B Ha b = b')
+    (Hc : cast (apd011 C Ha Hb) c = c') (Hd : cast (apd0111 D Ha Hb Hc) d = d')
+    (He : cast (apd01111 E Ha Hb Hc Hd) e = e') (Hf : cast (apd011111 F Ha Hb Hc Hd He) ff = f')
+    : f a b c d e ff = f a' b' c' d' e' f' :=
+  begin cases Ha, cases Hb, cases Hc, cases Hd, cases He, cases Hf, reflexivity end
+
+  -- definition apd0111111 (f : Πa b c d e ff, G a b c d e ff → Z) (Ha : a = a') (Hb : transport B Ha b = b')
+  --   (Hc : cast (apd011 C Ha Hb) c = c') (Hd : cast (apd0111 D Ha Hb Hc) d = d')
+  --   (He : cast (apd01111 E Ha Hb Hc Hd) e = e') (Hf : cast (apd011111 F Ha Hb Hc Hd He) ff = f')
+  --   (Hg : cast (apd0111111 G Ha Hb Hc Hd He Hf) g = g')
+  --   : f a b c d e ff g = f a' b' c' d' e' f' g' :=
+  -- by cases Ha; cases Hb; cases Hc; cases Hd; cases He; cases Hf; cases Hg; reflexivity
+
+  -- definition apd01111111 (f : Πa b c d e ff g, G a b c d e ff g → Z) (Ha : a = a') (Hb : transport B Ha b = b')
+  --   (Hc : cast (apd011 C Ha Hb) c = c') (Hd : cast (apd0111 D Ha Hb Hc) d = d')
+  --   (He : cast (apd01111 E Ha Hb Hc Hd) e = e') (Hf : cast (apd011111 F Ha Hb Hc Hd He) ff = f')
+  --   (Hg : cast (apd0111111 G Ha Hb Hc Hd He Hf) g = g') (Hh : cast (apd01111111 H Ha Hb Hc Hd He Hf Hg) h = h')
+  --   : f a b c d e ff g h = f a' b' c' d' e' f' g' h' :=
+  -- by cases Ha; cases Hb; cases Hc; cases Hd; cases He; cases Hf; cases Hg; cases Hh; reflexivity
+
   definition apd100 {f g : Πa b, C a b} (p : f = g) : f ∼2 g :=
   λa b, apd10 (apd10 p a) b
 

hott/cubical/pathover.hlean

@@ -208,18 +208,18 @@ namespace cubical
 
   end sigma
 
-  definition apD011o (f : Πa, B a → A') (Ha : a = a₂) (Hb : b =[Ha] b₂)
+  definition apd011o (f : Πa, B a → A') (Ha : a = a₂) (Hb : b =[Ha] b₂)
       : f a b = f a₂ b₂ :=
   by cases Hb; exact idp
 
-  definition apD0111o (f : Πa b, C a b → A') (Ha : a = a₂) (Hb : b =[Ha] b₂)
+  definition apd0111o (f : Πa b, C a b → A') (Ha : a = a₂) (Hb : b =[Ha] b₂)
-    (Hc : c =[apD011o C Ha Hb] c₂) : f a b c = f a₂ b₂ c₂ :=
+    (Hc : c =[apd011o C Ha Hb] c₂) : f a b c = f a₂ b₂ c₂ :=
   by cases Hb; apply (idp_rec_on Hc); apply idp
 
   namespace pi
     --the most 'natural' version here needs a notion of "path over a pathover"
     definition pi_pathover {f : Πb, C a b} {g : Πb₂, C a₂ b₂}
-      (r : Π(b : B a) (b₂ : B a₂) (q : b =[p] b₂), f b =[apD011o C p q] g b₂) : f =[p] g :=
+      (r : Π(b : B a) (b₂ : B a₂) (q : b =[p] b₂), f b =[apd011o C p q] g b₂) : f =[p] g :=
     begin
       cases p, apply pathover_idp_of_eq,
       apply eq_of_homotopy, intro b,
@@ -236,15 +236,15 @@ namespace cubical
     end
 
     definition ap11o {f : Πb, C a b} {g : Πb₂, C a₂ b₂} (r : f =[p] g)
-      {b : B a} {b₂ : B a₂} (q : b =[p] b₂) : f b =[apD011o C p q] g b₂ :=
+      {b : B a} {b₂ : B a₂} (q : b =[p] b₂) : f b =[apd011o C p q] g b₂ :=
     by cases r; apply (idp_rec_on q); exact idpo
 
     definition ap10o {f : Πb, C a b} {g : Πb₂, C a₂ b₂} (r : f =[p] g)
-      {b : B a} : f b =[apD011o C p !pathover_transport] g (p ▸ b) :=
+      {b : B a} : f b =[apd011o C p !pathover_transport] g (p ▸ b) :=
     by cases r; exact idpo
 
     -- definition equiv_pi_pathover' (f : Πb, C a b) (g : Πb₂, C a₂ b₂) :
-    --   (f =[p] g) ≃ (Π(b : B a), f b =[apD011o C p !pathover_transport] g (p ▸ b)) :=
+    --   (f =[p] g) ≃ (Π(b : B a), f b =[apd011o C p !pathover_transport] g (p ▸ b)) :=
     -- begin
     --   fapply equiv.MK,
     --   { exact ap10o},
@@ -255,7 +255,7 @@ namespace cubical
 
 
     -- definition equiv_pi_pathover (f : Πb, C a b) (g : Πb₂, C a₂ b₂) :
-    --   (f =[p] g) ≃ (Π(b : B a) (b₂ : B a₂) (q : b =[p] b₂), f b =[apD011o C p q] g b₂) :=
+    --   (f =[p] g) ≃ (Π(b : B a) (b₂ : B a₂) (q : b =[p] b₂), f b =[apd011o C p q] g b₂) :=
     -- begin
     --   fapply equiv.MK,
     --   { exact ap11o},

hott/hit/circle.hlean

@@ -8,14 +8,14 @@ Authors: Floris van Doorn
 Declaration of the circle
 -/
 
-import .sphere types.bool types.eq types.int.hott types.arrow types.equiv
+import .sphere types.bool types.eq types.int.hott types.arrow types.equiv algebra.fundamental_group algebra.hott
 
 open eq suspension bool sphere_index is_equiv equiv equiv.ops is_trunc
 
 definition circle : Type₀ := sphere 1
 
 namespace circle
-
+  notation `S¹` := circle
   definition base1 : circle := !north
   definition base2 : circle := !south
   definition seg1 : base1 = base2 := merid !north
@@ -161,6 +161,9 @@ attribute circle.rec2_on circle.elim2_on [unfold-c 2]
 attribute circle.elim2_type [unfold-c 1]
 
 namespace circle
+  definition pointed_circle [instance] [constructor] : pointed circle :=
+  pointed.mk base
+
   definition loop_neq_idp : loop ≠ idp :=
   assume H : loop = idp,
   have H2 : Π{A : Type₁} {a : A} (p : a = a), p = idp,
@@ -195,33 +198,68 @@ namespace circle
   protected definition encode {x : circle} (p : base = x) : code x :=
   transport code p (of_num 0) -- why is the explicit coercion needed here?
 
+  protected definition decode {x : circle} : code x → base = x :=
+  begin
+    refine circle.rec_on x _ _,
+    { exact power loop},
+    { apply eq_of_homotopy, intro a,
+      refine !arrow.arrow_transport ⬝ !transport_eq_r ⬝ _,
+      rewrite [transport_code_loop_inv,power_con,succ_pred]}
+  end
+
+  --remove this theorem after #484
+  theorem encode_decode {x : circle} : Π(a : code x), encode (decode a) = a :=
+  begin
+    unfold decode, refine circle.rec_on x _ _,
+    { intro a, esimp [base,base1], --simplify after #587
+      apply rec_nat_on a,
+      { exact idp},
+      { intros n p,
+        apply transport (λ(y : base = base), transport code y _ = _), apply power_con,
+        rewrite [▸*,con_tr, transport_code_loop, ↑[encode,code] at p, p]},
+      { intros n p,
+        apply transport (λ(y : base = base), transport code y _ = _),
+        { exact !power_con_inv ⬝ ap (power loop) !neg_succ⁻¹},
+        rewrite [▸*,@con_tr _ code,transport_code_loop_inv, ↑[encode] at p, p, -neg_succ]}},
+    { apply eq_of_homotopy, intro a, apply @is_hset.elim, esimp [code,base,base1], exact _}
+        --simplify after #587
+  end
+
+
   definition circle_eq_equiv (x : circle) : (base = x) ≃ code x :=
   begin
     fapply equiv.MK,
     { exact encode},
-    { refine circle.rec_on x _ _,
+    { exact decode},
-      { exact power loop},
+    { exact encode_decode},
-      { apply eq_of_homotopy, intro a,
-        refine !arrow.arrow_transport ⬝ !transport_eq_r ⬝ _,
-        rewrite [transport_code_loop_inv,power_con,succ_pred]}},
-    { refine circle.rec_on x _ _,
-      { intro a, esimp [base,base1], --simplify after #587
-        apply rec_nat_on a,
-        { exact idp},
-        { intros n p,
-          apply transport (λ(y : base = base), transport code y _ = _), apply power_con,
-          rewrite [▸*,con_tr, transport_code_loop, ↑[encode,code] at p, p]},
-        { intros n p,
-          apply transport (λ(y : base = base), transport code y _ = _),
-          { exact !power_con_inv ⬝ ap (power loop) !neg_succ⁻¹},
-          rewrite [▸*,@con_tr _ code,transport_code_loop_inv, ↑[encode] at p, p, -neg_succ]}},
-      { apply eq_of_homotopy, intro a, apply @is_hset.elim, esimp [code,base,base1], exact _}},
-        --simplify after #587
     { intro p, cases p, exact idp},
   end
 
-  definition base_eq_base_equiv : (base = base) ≃ ℤ :=
+  definition base_eq_base_equiv : base = base ≃ ℤ :=
   circle_eq_equiv base
 
+  definition decode_add (a b : ℤ) :
+    base_eq_base_equiv⁻¹ a ⬝ base_eq_base_equiv⁻¹ b = base_eq_base_equiv⁻¹ (a + b) :=
+  !power_con_power
+
+  definition encode_con (p q : base = base) : encode (p ⬝ q) = encode p + encode q :=
+  preserve_binary_of_inv_preserve base_eq_base_equiv concat add decode_add p q
+
+  --the carrier of π₁(S¹) is the set-truncation of base = base.
+  open core algebra trunc equiv.ops
+  definition fg_carrier_equiv_int : π₁(S¹) ≃ ℤ :=
+  trunc_equiv_trunc 0 base_eq_base_equiv ⬝e !equiv_trunc⁻¹ᵉ
+
+  definition fundamental_group_of_circle : π₁(S¹) = group_integers :=
+  begin
+    apply (Group_eq fg_carrier_equiv_int),
+    intros g h,
+    apply trunc.rec_on g, intro g', apply trunc.rec_on h, intro h',
+    -- esimp at *,
+    -- esimp [fg_carrier_equiv_int,equiv.trans,equiv.symm,equiv_trunc,trunc_equiv_trunc,
+    --   base_eq_base_equiv,circle_eq_equiv,is_equiv_tr,semigroup.to_has_mul,monoid.to_semigroup,
+    --   group.to_monoid,fundamental_group.mul],
+    apply encode_con,
+  end
 
 end circle

hott/hit/hit.md

@@ -1,7 +1,12 @@
 hit
 ===
 
-Declaration and theorems of higher inductive types in Lean. We take two higher inductive types (hits) as primitive notions in Lean. We define all other hits in terms of these two hits. The hits which are primitive are n-truncation and type quotients. These are defined in [init.hit](../init.hit.hlean) and they have definitional computation rules on the point constructors.
+Declaration and theorems of higher inductive types in Lean. We take
+two higher inductive types (hits) as primitive notions in Lean. We
+define all other hits in terms of these two hits. The hits which are
+primitive are n-truncation and type quotients. These are defined in
+[init.hit](../init.hit.hlean) and they have definitional computation
+rules on the point constructors.
 
 Files in this folder:
 

hott/hit/trunc.hlean

@@ -12,7 +12,7 @@ Ported from Coq HoTT
 
 /- The hit n-truncation is primitive, declared in init.hit. -/
 
-import types.sigma
+import types.sigma types.pointed
 
 open is_trunc eq equiv is_equiv function prod sum sigma
 
@@ -53,11 +53,8 @@ namespace trunc
   tr⁻¹
 
   /- Functoriality -/
-  definition trunc_functor (f : X → Y) : trunc n X → trunc n Y :=
+  definition trunc_functor [unfold-c 5] (f : X → Y) : trunc n X → trunc n Y :=
   λxx, trunc.rec_on xx (λx, tr (f x))
---  by intro xx; apply (trunc.rec_on xx); intro x; exact (tr (f x))
---  by intro xx; fapply (trunc.rec_on xx); intro x; exact (tr (f x))
---  by intro xx; exact (trunc.rec_on xx (λx, (tr (f x))))
 
   definition trunc_functor_compose (f : X → Y) (g : Y → Z)
     : trunc_functor n (g ∘ f) ∼ trunc_functor n g ∘ trunc_functor n f :=
@@ -72,10 +69,16 @@ namespace trunc
              (λyy, trunc.rec_on yy (λy, ap tr !right_inv))
              (λxx, trunc.rec_on xx (λx, ap tr !left_inv))
 
+  section
+    open equiv.ops
+    definition trunc_equiv_trunc (f : X ≃ Y) : trunc n X ≃ trunc n Y :=
+    equiv.mk _ (is_equiv_trunc_functor n f)
+  end
+
   section
   open prod.ops
-  definition trunc_prod_equiv : trunc n (X × Y) ≃ trunc n X × trunc n Y :=
+  -- definition trunc_prod_equiv : trunc n (X × Y) ≃ trunc n X × trunc n Y :=
-  sorry
+  -- sorry
   -- equiv.MK (λpp, trunc.rec_on pp (λp, (tr p.1, tr p.2)))
   --          (λp, trunc.rec_on p.1 (λx, trunc.rec_on p.2 (λy, tr (x,y))))
   --          sorry --(λp, trunc.rec_on p.1 (λx, trunc.rec_on p.2 (λy, idp)))

hott/init/default.hlean

@@ -18,9 +18,10 @@ namespace core
   export bool empty unit sum
   export sigma (hiding pr1 pr2)
   export [notations] prod
+  export [notations] nat
   export eq (idp idpath concat inverse transport ap ap10 cast tr_inv homotopy ap11 apd refl)
   export [declarations] function
   export equiv (to_inv to_right_inv to_left_inv)
   export is_equiv (inv right_inv left_inv)
-
+  export [abbreviations] [declarations] is_trunc (trunctype hprop.mk hset.mk)
 end core

hott/init/equiv.hlean

@@ -35,13 +35,13 @@ namespace is_equiv
   /- Some instances and closure properties of equivalences -/
   postfix `⁻¹` := inv
   /- a second notation for the inverse, which is not overloaded -/
-  postfix [parsing-only] `⁻¹ᵉ`:std.prec.max_plus := inv
+  postfix [parsing-only] `⁻¹ᶠ`:std.prec.max_plus := inv
 
   section
   variables {A B C : Type} (f : A → B) (g : B → C) {f' : A → B}
 
   -- The variant of mk' where f is explicit.
-  protected abbreviation mk := @is_equiv.mk' A B f
+  protected abbreviation mk [constructor] := @is_equiv.mk' A B f
 
   -- The identity function is an equivalence.
   definition is_equiv_id (A : Type) : (@is_equiv A A id) :=
@@ -138,7 +138,8 @@ namespace is_equiv
         from eq_of_idp_eq_inv_con eq3,
       eq4)
 
-  definition adjointify : is_equiv f := is_equiv.mk f g ret adjointify_sect' adjointify_adj'
+  definition adjointify [constructor] : is_equiv f :=
+  is_equiv.mk f g ret adjointify_sect' adjointify_adj'
 
   end
 
@@ -242,21 +243,21 @@ namespace equiv
 
   variables {A B C : Type}
 
-  protected definition MK [reducible] (f : A → B) (g : B → A)
+  protected definition MK [reducible] [constructor] (f : A → B) (g : B → A)
     (right_inv : f ∘ g ∼ id) (left_inv : g ∘ f ∼ id) : A ≃ B :=
   equiv.mk f (adjointify f g right_inv left_inv)
 
-  definition to_inv [reducible] (f : A ≃ B) : B → A := f⁻¹
+  definition to_inv [reducible] [unfold-c 3] (f : A ≃ B) : B → A := f⁻¹
-  definition to_right_inv [reducible] (f : A ≃ B) : f ∘ f⁻¹ ∼ id := right_inv f
+  definition to_right_inv [reducible] [unfold-c 3] (f : A ≃ B) : f ∘ f⁻¹ ∼ id := right_inv f
-  definition to_left_inv [reducible] (f : A ≃ B) : f⁻¹ ∘ f ∼ id := left_inv f
+  definition to_left_inv [reducible] [unfold-c 3] (f : A ≃ B) : f⁻¹ ∘ f ∼ id := left_inv f
 
-  protected definition refl : A ≃ A :=
+  protected definition refl [refl] : A ≃ A :=
   equiv.mk id !is_equiv_id
 
-  protected definition symm (f : A ≃ B) : B ≃ A :=
+  protected definition symm [symm] (f : A ≃ B) : B ≃ A :=
   equiv.mk f⁻¹ !is_equiv_inv
 
-  protected definition trans (f : A ≃ B) (g: B ≃ C) : A ≃ C :=
+  protected definition trans [trans] (f : A ≃ B) (g: B ≃ C) : A ≃ C :=
   equiv.mk (g ∘ f) !is_equiv_compose
 
   definition equiv_of_eq_fn_of_equiv (f : A ≃ B) {f' : A → B} (Heq : f = f') : A ≃ B :=
@@ -275,18 +276,13 @@ namespace equiv
   theorem inv_eq {A B : Type} (eqf eqg : A ≃ B) (p : eqf = eqg) : (to_fun eqf)⁻¹ = (to_fun eqg)⁻¹ :=
   eq.rec_on p idp
 
-  -- calc enviroment
-  -- Note: Calculating with substitutions needs univalence
   definition equiv_of_equiv_of_eq {A B C : Type} (p : A = B) (q : B ≃ C) : A ≃ C := p⁻¹ ▸ q
   definition equiv_of_eq_of_equiv {A B C : Type} (p : A ≃ B) (q : B = C) : A ≃ C := q   ▸ p
 
-  attribute equiv.trans [trans]
-  attribute equiv.refl [refl]
-  attribute equiv.symm [symm]
-
   namespace ops
     infixl `⬝e`:75 := equiv.trans
-    postfix `⁻¹e`:(max + 1) := equiv.symm
+    postfix `⁻¹` := equiv.symm -- overloaded notation for inverse
+    postfix `⁻¹ᵉ`:(max + 1) := equiv.symm -- notation for inverse which is not overloaded
     abbreviation erfl := @equiv.refl
   end ops
 end equiv

hott/init/num.hlean

@@ -132,4 +132,4 @@ namespace nat
   num.rec zero
     (λ n, pos_num.rec (succ zero) (λ n r, r + r + (succ zero)) (λ n r, r + r) n) n
 end nat
-attribute nat.of_num [reducible] -- of_num is also reducible if namespace "nat" is not opened
+attribute nat.of_num [reducible] [constructor] -- of_num is also reducible if namespace "nat" is not opened

hott/init/trunc.hlean

@@ -72,9 +72,7 @@ namespace is_trunc
       (λA, contr_internal A)
       (λn trunc_n A, (Π(x y : A), trunc_n (x = y)))
 
-end is_trunc
+end is_trunc open is_trunc
-
-open is_trunc
 structure is_trunc [class] (n : trunc_index) (A : Type) :=
   (to_internal : is_trunc_internal n A)
 open nat num is_trunc.trunc_index
@@ -195,6 +193,7 @@ namespace is_trunc
 
   /- truncated universe -/
 
+  -- TODO: move to root namespace?
   structure trunctype (n : trunc_index) :=
   (carrier : Type) (struct : is_trunc n carrier)
   attribute trunctype.carrier [coercion]

hott/init/ua.hlean

@@ -49,18 +49,27 @@ definition ua_equiv_of_eq [reducible] {A B : Type} (p : A = B) : ua (equiv_of_eq
 left_inv equiv_of_eq p
 
 
--- One consequence of UA is that we can transport along equivalencies of types
-namespace equiv
-  universe variable l
 
-  protected definition transport_of_equiv [subst] (P : Type → Type) {A B : Type.{l}} (H : A ≃ B)
+namespace equiv
+  -- One consequence of UA is that we can transport along equivalencies of types
+  -- We can use this for calculation evironments
+  protected definition transport_of_equiv [subst] (P : Type → Type) {A B : Type} (H : A ≃ B)
     : P A → P B :=
   eq.transport P (ua H)
 
-  -- We can use this for calculation evironments
+  -- we can "recurse" on equivalences, by replacing them by (equiv_of_eq _)
+  definition rec_on_ua {A B : Type} {P : A ≃ B → Type}
+    (f : A ≃ B) (H : Π(q : A = B), P (equiv_of_eq q)) : P f :=
+  right_inv equiv_of_eq f ▸ H (ua f)
 
-  definition rec_on_of_equiv_of_eq {A B : Type} {P : (A ≃ B) → Type}
+  -- a variant where (equiv_of_eq (ua f)) will be replaced by f in the new goal
-    (p : A ≃ B) (H : Π(q : A = B), P (equiv_of_eq q)) : P p :=
+  definition rec_on_ua2 {A B : Type} {P : A ≃ B → A = B → Type}
-  right_inv equiv_of_eq p ▸ H (ua p)
+    (f : A ≃ B) (H : Π(q : A = B), P (equiv_of_eq q) q) : P f (ua f) :=
+  right_inv equiv_of_eq f ▸ H (ua f)
+
+  -- a variant where we immediately recurse on the equality in the new goal
+  definition rec_on_ua3 {A : Type} {P : Π{B}, A ≃ B → A = B → Type} {B : Type}
+    (f : A ≃ B) (H : P equiv.refl idp) : P f (ua f) :=
+  rec_on_ua2 f (λq, eq.rec_on q H)
 
 end equiv

hott/types/function.hlean

@@ -16,7 +16,7 @@ open equiv sigma sigma.ops eq trunc is_trunc pi is_equiv fiber prod
 variables {A B : Type} {f : A → B} {b : B}
 
 structure is_embedding [class] (f : A → B) :=
-(elim : Π(a a' : A), is_equiv (@ap A B f a a'))
+(elim : Π(a a' : A), is_equiv (ap f : a = a' → f a = f a'))
 
 structure is_surjective [class] (f : A → B) :=
 (elim : Π(b : B), ∥ fiber f b ∥)

hott/types/int/basic.hlean

@@ -40,7 +40,8 @@ inductive int : Type :=
 
 notation `ℤ` := int
 attribute int.of_nat [coercion]
-definition int.of_num [coercion] [reducible] (n : num) : ℤ := int.of_nat (nat.of_num n)
+definition int.of_num [coercion] [reducible] [constructor] (n : num) : ℤ :=
+int.of_nat (nat.of_num n)
 
 namespace int
 
@@ -146,16 +147,6 @@ int.cases_on a
   (take m, assume H : nat_abs (of_nat m) = 0, ap of_nat H)
   (take m', assume H : nat_abs (neg_succ_of_nat m') = 0, absurd H (succ_ne_zero _))
 
-definition rec_nat_on {P : ℤ → Type} (z : ℤ) (H0 : P 0) (Hsucc : Π⦃n : ℕ⦄, P n → P (succ n))
-  (Hpred : Π⦃n : ℕ⦄, P (- n) → P (-succ n)) : P z :=
-int.rec_on z (λn, nat.rec_on n H0 Hsucc) (λn, nat.rec_on n (Hpred H0) (λm H, Hpred H))
-
---the only computation rule of rec_nat_on which is not definitional
-definition rec_nat_on_neg {P : ℤ → Type} (n : nat) (H0 : P zero)
-  (Hsucc : Π⦃n : nat⦄, P n → P (succ n)) (Hpred : Π⦃n : nat⦄, P (- n) → P (-succ n))
-  : rec_nat_on (-succ n) H0 Hsucc Hpred = Hpred (rec_nat_on (-n) H0 Hsucc Hpred) :=
-nat.rec_on n rfl (λn H, rfl)
-
 /- int is a quotient of ordered pairs of natural numbers -/
 
 definition int_equiv (p q : ℕ × ℕ) : Type₀ :=  pr1 p + pr2 q = pr2 p + pr1 q
@@ -791,4 +782,31 @@ sub_eq_of_eq_add H2
 definition neg_succ_of_nat_eq' (m : ℕ) : -[m +1] = -m - 1 :=
 by rewrite [neg_succ_of_nat_eq, -of_nat_add_of_nat, neg_add]
 
+definition succ (a : ℤ) := a + (nat.succ zero)
+definition pred (a : ℤ) := a - (nat.succ zero)
+definition pred_succ (a : ℤ) : pred (succ a) = a := !sub_add_cancel
+definition succ_pred (a : ℤ) : succ (pred a) = a := !add_sub_cancel
+definition neg_succ (a : ℤ) : -succ a = pred (-a) :=
+by rewrite [↑succ,neg_add]
+definition succ_neg_succ (a : ℤ) : succ (-succ a) = -a :=
+by rewrite [neg_succ,succ_pred]
+definition neg_pred (a : ℤ) : -pred a = succ (-a) :=
+by rewrite [↑pred,neg_sub,sub_eq_add_neg,add.comm]
+definition pred_neg_pred (a : ℤ) : pred (-pred a) = -a :=
+by rewrite [neg_pred,pred_succ]
+
+definition pred_nat_succ (n : ℕ) : pred (nat.succ n) = n := pred_succ n
+definition neg_nat_succ (n : ℕ) : -nat.succ n = pred (-n) := !neg_succ
+definition succ_neg_nat_succ (n : ℕ) : succ (-nat.succ n) = -n := !succ_neg_succ
+
+definition rec_nat_on [unfold-c 2] {P : ℤ → Type} (z : ℤ) (H0 : P 0)
+  (Hsucc : Π⦃n : ℕ⦄, P n → P (succ n)) (Hpred : Π⦃n : ℕ⦄, P (-n) → P (-nat.succ n)) : P z :=
+int.rec_on z (λn, nat.rec_on n H0 Hsucc) (λn, nat.rec_on n (Hpred H0) (λm H, Hpred H))
+
+--the only computation rule of rec_nat_on which is not definitional
+definition rec_nat_on_neg {P : ℤ → Type} (n : nat) (H0 : P zero)
+  (Hsucc : Π⦃n : nat⦄, P n → P (succ n)) (Hpred : Π⦃n : nat⦄, P (-n) → P (-nat.succ n))
+  : rec_nat_on (-nat.succ n) H0 Hsucc Hpred = Hpred (rec_nat_on (-n) H0 Hsucc Hpred) :=
+nat.rec_on n rfl (λn H, rfl)
+
 end int

hott/types/int/hott.hlean

@@ -8,25 +8,16 @@ Author: Floris van Doorn
 Theorems about the integers specific to HoTT
 -/
 
-import .basic types.eq
+import .basic types.eq arity
-open core is_equiv equiv equiv.ops
+open core eq is_equiv equiv equiv.ops
 open nat (hiding pred)
 
 namespace int
-
+  section
-  definition succ (a : ℤ) := a + (nat.succ zero)
+  open algebra
-  definition pred (a : ℤ) := a - (nat.succ zero)
+  definition group_integers : Group :=
-  definition pred_succ (a : ℤ) : pred (succ a) = a := !sub_add_cancel
+  Group.mk ℤ (group_of_add_group _)
-  definition pred_nat_succ (n : ℕ) : pred (nat.succ n) = n := pred_succ n
+  end
-  definition succ_pred (a : ℤ) : succ (pred a) = a := !add_sub_cancel
-  definition neg_succ (a : ℤ) : -succ a = pred (-a) :=
-  by rewrite [↑succ,neg_add]
-  definition succ_neg_succ (a : ℤ) : succ (-succ a) = -a :=
-  by rewrite [neg_succ,succ_pred]
-  definition neg_pred (a : ℤ) : -pred a = succ (-a) :=
-  by rewrite [↑pred,neg_sub,sub_eq_add_neg,add.comm]
-  definition pred_neg_pred (a : ℤ) : pred (-pred a) = -a :=
-  by rewrite [neg_pred,pred_succ]
 
   definition is_equiv_succ [instance] : is_equiv succ :=
   adjointify succ pred (λa, !add_sub_cancel) (λa, !sub_add_cancel)
@@ -39,7 +30,7 @@ namespace int
   definition iterate {A : Type} (f : A ≃ A) (a : ℤ) : A ≃ A :=
   rec_nat_on a erfl
                (λb g, f ⬝e g)
-               (λb g, g ⬝e f⁻¹e)
+               (λb g, g ⬝e f⁻¹ᵉ)
 
   -- definition iterate_trans {A : Type} (f : A ≃ A) (a : ℤ)
   --   : iterate f a ⬝e f = iterate f (a + 1) :=
@@ -84,7 +75,7 @@ end int open int
 
 
 namespace eq
-  variables {A : Type} {a : A} (p : a = a) (b : ℤ) (n : ℕ)
+  variables {A : Type} {a : A} (p : a = a) (b c : ℤ) (n : ℕ)
   definition power : a = a :=
   rec_nat_on b idp
                (λc q, q ⬝ p)
@@ -94,33 +85,16 @@ namespace eq
   -- definition power_neg_succ (n : ℕ) : power p (-succ n) = power p (-n) ⬝ p⁻¹ :=
   -- !rec_nat_on_neg
 
-
+  -- local attribute nat.add int.add int.of_num nat.of_num int.succ [constructor]
-  set_option pp.coercions true
-  -- attribute nat.add int.add int.of_num nat.of_num int.succ [constructor]
-  attribute rec_nat_on [unfold-c 2]
 
   definition power_con : power p b ⬝ p = power p (succ b) :=
   rec_nat_on b
     idp
     (λn IH, idp)
     (λn IH, calc
-      power p (-succ n) ⬝ p = (power p (-n) ⬝ p⁻¹) ⬝ p : by rewrite [↑power,rec_nat_on_neg]
+      power p (-succ n) ⬝ p = (power p (-n) ⬝ p⁻¹) ⬝ p : by rewrite [↑power,-rec_nat_on_neg]
         ... = power p (-n) : inv_con_cancel_right
-        ... = power p (succ (-succ n)) : {(succ_neg_succ n)⁻¹})
+        ... = power p (succ (-succ n)) : by rewrite -succ_neg_succ)
-
-  -- definition con_power : p ⬝ power p b = power p (succ b) :=
-  -- rec_nat_on b
-  --   (by rewrite ↑[power];exact !idp_con⁻¹)
-  --   (λn IH, calc
-  --     p ⬝ power p (succ n) = (p ⬝ power p n) ⬝ p : con.assoc
-  --       ... = power p (succ (succ n)) : by rewrite IH)
-  --   (λn IH, calc
-  --     p ⬝ power p (-succ n) = p ⬝ (power p (-n) ⬝ p⁻¹) : by rewrite [↑power,rec_nat_on_neg]
-  --       ... = (p ⬝ power p (-n)) ⬝ p⁻¹ : con.assoc
-  --       ... = power p (succ (-n)) ⬝ p⁻¹ : by rewrite IH
-  --       ... = power p (-pred n) ⬝ p⁻¹ : {(neg_pred n)⁻¹}
-  --       ... = power p (-succ (pred n)) : sorry
-  --       ... = power p (succ (-succ n)) : sorry)
 
   definition power_con_inv : power p b ⬝ p⁻¹ = power p (pred b) :=
   rec_nat_on b
@@ -132,9 +106,41 @@ namespace eq
       power p (-succ n) ⬝ p⁻¹ = power p (-succ (succ n)) : by rewrite [↑power,-rec_nat_on_neg]
         ... = power p (pred (-succ n)) : by rewrite -neg_succ)
 
-  -- definition inv_con_power : p⁻¹ ⬝ power p b = power p (pred b) :=
+  definition con_power : p ⬝ power p b = power p (succ b) :=
-  -- rec_nat_on b sorry
+  rec_nat_on b
-  --              sorry
+  ( by rewrite ↑[power];exact !idp_con⁻¹)
-  --              sorry
+  ( λn IH, proof calc
+    p ⬝ power p (succ n) = (p ⬝ power p n) ⬝ p : con.assoc p _ p
+      ... = power p (succ (succ n)) : by rewrite IH qed)
+  ( λn IH, calc
+          p ⬝ power p (-succ n)
+                = p ⬝ (power p (-n) ⬝ p⁻¹) : by rewrite [↑power,rec_nat_on_neg]
+            ... = (p ⬝ power p (-n)) ⬝ p⁻¹ : con.assoc
+            ... = power p (succ (-n)) ⬝ p⁻¹ : by rewrite IH
+            ... = power p (pred (succ (-n))) : power_con_inv
+            ... = power p (succ (-succ n)) : by rewrite [succ_neg_nat_succ,int.pred_succ])
+
+  definition inv_con_power : p⁻¹ ⬝ power p b = power p (pred b) :=
+  rec_nat_on b
+  ( by rewrite ↑[power];exact !idp_con⁻¹)
+  (λn IH, calc
+    p⁻¹ ⬝ power p (succ n) = p⁻¹ ⬝ power p n ⬝ p : con.assoc
+      ... = power p (pred n) ⬝ p : by rewrite IH
+      ... = power p (succ (pred n)) : power_con
+      ... = power p (pred (succ n)) : by rewrite [succ_pred,-int.pred_succ n])
+  ( λn IH, calc
+    p⁻¹ ⬝ power p (-succ n) = p⁻¹ ⬝ (power p (-n) ⬝ p⁻¹) : by rewrite [↑power,rec_nat_on_neg]
+      ... = (p⁻¹ ⬝ power p (-n)) ⬝ p⁻¹ : con.assoc
+      ... = power p (pred (-n)) ⬝ p⁻¹ : by rewrite IH
+      ... = power p (-succ n) ⬝ p⁻¹ : by rewrite -neg_succ
+      ... = power p (-succ (succ n)) : by rewrite [↑power,-rec_nat_on_neg]
+      ... = power p (pred (-succ n)) : by rewrite -neg_succ)
+
+  definition power_con_power : Π(b : ℤ), power p b ⬝ power p c = power p (b + c) :=
+  rec_nat_on c
+    (λb, by rewrite int.add_zero)
+    (λn IH b, by rewrite [-con_power,-con.assoc,power_con,IH,↑succ,int.add.assoc,int.add.comm 1 n])
+    (λn IH b, by rewrite [neg_nat_succ,-inv_con_power,-con.assoc,power_con_inv,IH,↑pred,
+                          +sub_eq_add_neg,int.add.assoc,int.add.comm (-1) (-n)])
 
 end eq

hott/types/pointed.hlean

@@ -3,38 +3,76 @@ Copyright (c) 2014 Jakob von Raumer. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 
 Module: types.pointed
-Author: Jakob von Raumer
+Authors: Jakob von Raumer, Floris van Doorn
 
 Ported from Coq HoTT
 -/
 
-open eq prod is_trunc sigma
+open core is_trunc
 
-structure is_pointed [class] (A : Type) :=
+structure pointed [class] (A : Type) :=
   (point : A)
 
-namespace is_pointed
+namespace pointed
-  variables {A B : Type} (f : A → B)
+  variables {A B : Type}
+  definition pt [H : pointed A] := point A
 
   -- Any contractible type is pointed
-  definition is_pointed_of_is_contr [instance] [H : is_contr A] : is_pointed A :=
+  definition pointed_of_is_contr [instance] (A : Type) [H : is_contr A] : pointed A :=
-    is_pointed.mk !center
+  pointed.mk !center
 
   -- A pi type with a pointed target is pointed
-  definition is_pointed_pi [instance] {P : A → Type} [H : Πx, is_pointed (P x)]
+  definition pointed_pi [instance] (P : A → Type) [H : Πx, pointed (P x)]
-      : is_pointed (Πx, P x) :=
+      : pointed (Πx, P x) :=
-    is_pointed.mk (λx, point (P x))
+  pointed.mk (λx, pt)
 
   -- A sigma type of pointed components is pointed
-  definition is_pointed_sigma [instance] {P : A → Type} [G : is_pointed A]
+  definition pointed_sigma [instance] (P : A → Type) [G : pointed A]
-      [H : is_pointed (P !point)] : is_pointed (Σx, P x) :=
+      [H : pointed (P pt)] : pointed (Σx, P x) :=
-    is_pointed.mk ⟨!point,!point⟩
+  pointed.mk ⟨pt,pt⟩
 
-  definition is_pointed_prod [H1 : is_pointed A] [H2 : is_pointed B]
+  definition pointed_prod [instance] (A B : Type) [H1 : pointed A] [H2 : pointed B]
-      : is_pointed (A × B) :=
+      : pointed (A × B) :=
-    is_pointed.mk (!point,!point)
+  pointed.mk (pt,pt)
 
-  definition is_pointed_loop_space (a : A) : is_pointed (a = a) :=
+  definition pointed_loop [instance] (a : A) : pointed (a = a) :=
-    is_pointed.mk idp
+  pointed.mk idp
 
-end is_pointed
+  definition pointed_fun_closed (f : A → B) [H : pointed A] : pointed B :=
+  pointed.mk (f pt)
+
+end pointed
+
+structure Pointed :=
+  {carrier : Type}
+  (Point   : carrier)
+
+open pointed Pointed
+
+namespace Pointed
+  attribute carrier [coercion]
+  protected definition mk' (A : Type) [H : pointed A] : Pointed := Pointed.mk (point A)
+  definition pointed_carrier [instance] (A : Pointed) : pointed (carrier A) :=
+  pointed.mk (Point A)
+
+  definition Loop_space [reducible] (A : Pointed) : Pointed :=
+  Pointed.mk' (point A = point A)
+
+  definition Iterated_loop_space (A : Pointed) (n : ℕ) : Pointed :=
+  nat.rec_on n A (λn X, Loop_space X)
+
+  prefix `Ω`:95 := Loop_space
+  notation `Ω[`:95 n:0 `]`:0 A:95 := Iterated_loop_space A n
+
+end Pointed
+
+namespace pointed
+  export Pointed (hiding cases_on destruct mk)
+  abbreviation Cases_on := @Pointed.cases_on
+  abbreviation Destruct := @Pointed.destruct
+  abbreviation Mk := @Pointed.mk
+
+  definition iterated_loop_space (A : Type) [H : pointed A] (n : ℕ) : Type :=
+  carrier (Iterated_loop_space (Pointed.mk' A) n)
+
+end pointed

library/algebra/group.lean

@@ -487,4 +487,14 @@ section add_comm_group
   !add.comm ▸ add_eq_of_eq_sub H
 end add_comm_group
 
+definition group_of_add_group (A : Type) [G : add_group A] : group A :=
+⦃group,
+  mul             := has_add.add,
+  mul_assoc       := add.assoc,
+  one             := !has_zero.zero,
+  one_mul         := zero_add,
+  mul_one         := add_zero,
+  inv             := has_neg.neg,
+  mul_left_inv    := add.left_inv⦄
+
 end algebra

library/data/int/basic.lean

@@ -40,7 +40,8 @@ inductive int : Type :=
 
 notation `ℤ` := int
 attribute int.of_nat [coercion]
-definition int.of_num [coercion] [reducible] (n : num) : ℤ := int.of_nat (nat.of_num n)
+definition int.of_num [coercion] [reducible] [constructor] (n : num) : ℤ :=
+int.of_nat (nat.of_num n)
 
 namespace int
 
@@ -146,7 +147,7 @@ int.cases_on a
   (take m, assume H : nat_abs (of_nat m) = 0, congr_arg of_nat H)
   (take m', assume H : nat_abs (neg_succ_of_nat m') = 0, absurd H (succ_ne_zero _))
 
-definition rec_nat_on {P : ℤ → Type} (z : ℤ) (H0 : P 0) (Hsucc : Π⦃n : ℕ⦄, P n → P (succ n))
+definition rec_nat_on [unfold-c 2] {P : ℤ → Type} (z : ℤ) (H0 : P 0) (Hsucc : Π⦃n : ℕ⦄, P n → P (succ n))
   (Hpred : Π⦃n : ℕ⦄, P (- n) → P (-succ n)) : P z :=
 int.rec_on z (λn, nat.rec_on n H0 Hsucc) (λn, nat.rec_on n (Hpred H0) (λm H, Hpred H))
 

library/init/num.lean

@@ -129,4 +129,4 @@ namespace nat
   num.rec zero
     (λ n, pos_num.rec (succ zero) (λ n r, r + r + (succ zero)) (λ n r, r + r) n) n
 end nat
-attribute nat.of_num [reducible] -- of_num is also reducible if namespace "nat" is not opened
+attribute nat.of_num [reducible] [constructor] -- of_num is also reducible if namespace "nat" is not opened

src/emacs/lean-input.el

@@ -337,6 +337,7 @@ order for the change to take effect."
   ("-1"        . ("⁻¹"))
   ("-1p"       . ("⁻¹ᵖ"))
   ("-1e"       . ("⁻¹ᵉ"))
+  ("-1f"       . ("⁻¹ᶠ"))
   ("-1h"       . ("⁻¹ʰ"))
   ("-1g"       . ("⁻¹ᵍ"))
   ("-1o"       . ("⁻¹ᵒ"))