feat(hott): add types.sum, greatly expand types.prod, minor changes in types.sigma and types.pi

2015-08-06 22:37:52 +02:00 · 2015-08-06 22:37:52 +02:00 · e51ba09a27
commit e51ba09a27
parent 3d2a6a08a4
12 changed files with 361 additions and 48 deletions
--- a/hott/book.md
+++ b/hott/book.md
@ -16,7 +16,7 @@ The rows indicate the chapters, the columns the sections.
 |       | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9 | 10 | 11 | 12 | 13 | 14 | 15 |
 |-------|---|---|---|---|---|---|---|---|---|----|----|----|----|----|----|
 | Ch 1  | . | . | . | . | + | + | + | + | + | .  | +  | +  |    |    |    |
-| Ch 2  | + | + | + | + | . | + | + | + | + | +  | +  | -  | +  | +  | +  |
+| Ch 2  | + | + | + | + | . | + | + | + | + | +  | +  | +  | +  | +  | +  |
 | Ch 3  | + | - | + | + | ½ | + | + | - | ½ | .  | +  |    |    |    |    |
 | Ch 4  | - | + | - | + | . | + | - | - | + |    |    |    |    |    |    |
 | Ch 5  | - | . | - | - | - | . | . | ½ |   |    |    |    |    |    |    |
@ -61,7 +61,7 @@ Chapter 2: Homotopy type theory
 - 2.9 (Π-types and the function extensionality axiom): [init.funext](init/funext.hlean) and [types.pi](types/pi.hlean)
 - 2.10 (Universes and the univalence axiom): [init.ua](init/ua.hlean)
 - 2.11 (Identity type): [init.equiv](init/equiv.hlean) (ap is equivalence), [types.eq](types/eq.hlean) and [types.cubical.square](types/cubical/square.hlean) (characterization of pathovers in equality types)
- 2.12 (Coproducts): not formalized
+- 2.12 (Coproducts): [types.sum](types/sum.hlean)
 - 2.13 (Natural numbers): [types.nat.hott](types/nat/hott.hlean)
 - 2.14 (Example: equality of structures): algebra formalized in [algebra.group](algebra/group.hlean).
 - 2.15 (Universal properties): in the corresponding file in the [types](types/types.md) folder.
--- a/hott/init/trunc.hlean
+++ b/hott/init/trunc.hlean
@ -189,12 +189,20 @@ namespace is_trunc
    : is_contr (Σ(x : A), a = x) :=
  is_contr.mk (sigma.mk a idp) (λp, sigma.rec_on p (λ b q, eq.rec_on q idp))

-  definition is_contr_unit [instance] : is_contr unit :=
+  definition is_contr_unit : is_contr unit :=
  is_contr.mk star (λp, unit.rec_on p idp)

-  definition is_hprop_empty [instance] : is_hprop empty :=
+  definition is_hprop_empty : is_hprop empty :=
  is_hprop.mk (λx, !empty.elim x)

+  local attribute is_contr_unit is_hprop_empty [instance]
+
+  definition is_trunc_unit [instance] (n : trunc_index) : is_trunc n unit :=
+  !is_trunc_of_is_contr
+
+  definition is_trunc_empty [instance] (n : trunc_index) : is_trunc (n.+1) empty :=
+  !is_trunc_succ_of_is_hprop
+
  /- truncated universe -/

  -- TODO: move to root namespace?
@ -292,6 +300,11 @@ namespace is_trunc
  theorem is_hset.elimo (q q' : c =[p] c₂) [H : is_hset (C a)] : q = q' :=
  !is_hprop.elim

+  /- truncatedness of lift -/
+  definition is_trunc_lift [instance] (A : Type) (n : trunc_index) [H : is_trunc n A]
+    : is_trunc n (lift A) :=
+  is_trunc_equiv_closed _ !equiv_lift
+
  -- TODO: port "Truncated morphisms"

 end is_trunc
--- a/hott/init/types.hlean
+++ b/hott/init/types.hlean
@ -85,7 +85,7 @@ namespace prod
  infixr × := prod

  namespace ops
-  infixr * := prod
+  infixr [parsing-only] * := prod
  postfix `.1`:(max+1) := pr1
  postfix `.2`:(max+1) := pr2
  abbreviation pr₁ := @pr1
--- a/hott/types/bool.hlean
+++ b/hott/types/bool.hlean
@ -17,11 +17,8 @@ namespace bool
  begin
    fapply is_equiv.mk,
      exact bnot,
-      do 3 focus (intro b;cases b;all_goals (exact idp))
-      --should information be propagated with all_goals?
-      -- all_goals (intro b;cases b),
-      -- all_goals (exact idp)
--      all_goals (focus (intro b;cases b;all_goals (exact idp))),
+      all_goals (intro b;cases b), do 6 reflexivity
+--      all_goals (focus (intro b;cases b;all_goals reflexivity)),
  end

  definition equiv_bnot : bool ≃ bool := equiv.mk bnot _
--- a/hott/types/fiber.hlean
+++ b/hott/types/fiber.hlean
@ -31,9 +31,9 @@ namespace fiber
    : (x = y) ≃ (Σ(p : point x = point y), point_eq x = ap f p ⬝ point_eq y) :=
  begin
    apply equiv.trans,
-      {apply eq_equiv_fn_eq_of_equiv, apply sigma_char},
+      apply eq_equiv_fn_eq_of_equiv, apply sigma_char,
    apply equiv.trans,
-      {apply equiv.symm, apply equiv_sigma_eq},
+      apply sigma_eq_equiv,
    apply sigma_equiv_sigma_id,
    intro p,
    apply pathover_eq_equiv_Fl,
--- a/hott/types/nat/hott.hlean
+++ b/hott/types/nat/hott.hlean
@ -77,38 +77,38 @@ namespace nat
        exfalso, apply lt.irrefl, apply lt_of_le_of_lt H H'}
  end

-  definition code [reducible] [unfold 1 2] : ℕ → ℕ → Type₀
-  | code 0 0               := unit
+  protected definition code [reducible] [unfold 1 2] : ℕ → ℕ → Type₀
+  | code 0        0        := unit
+  | code 0        (succ m) := empty
  | code (succ n) 0        := empty
-  | code 0 (succ m)        := empty
  | code (succ n) (succ m) := code n m

-  definition refl : Πn, code n n
-  | refl 0 := star
+  protected definition refl : Πn, nat.code n n
+  | refl 0        := star
  | refl (succ n) := refl n

-  definition encode [unfold 3] {n m : ℕ} (p : n = m) : code n m :=
-  p ▸ refl n
+  protected definition encode [unfold 3] {n m : ℕ} (p : n = m) : nat.code n m :=
+  p ▸ nat.refl n

-  definition decode : Π(n m : ℕ), code n m → n = m
-  | decode 0 0               := λc, idp
-  | decode 0 (succ l)        := λc, empty.elim c _
+  protected definition decode : Π(n m : ℕ), nat.code n m → n = m
+  | decode 0        0        := λc, idp
+  | decode 0        (succ l) := λc, empty.elim c _
  | decode (succ k) 0        := λc, empty.elim c _
  | decode (succ k) (succ l) := λc, ap succ (decode k l c)

-  definition nat_eq_equiv (n m : ℕ) : (n = m) ≃ code n m :=
-  equiv.MK encode
-           !decode
+  definition nat_eq_equiv (n m : ℕ) : (n = m) ≃ nat.code n m :=
+  equiv.MK nat.encode
+           !nat.decode
           begin
             revert m, induction n, all_goals (intro m;induction m;all_goals intro c),
               all_goals try contradiction,
               induction c, reflexivity,
-               xrewrite [↑decode,-tr_compose,v_0],
+               xrewrite [↑nat.decode,-tr_compose,v_0],
           end
           begin
             intro p, induction p, esimp, induction n,
               reflexivity,
-               rewrite [↑decode,↑refl,v_0]
+               rewrite [↑nat.decode,↑nat.refl,v_0]
           end

 end nat
--- a/hott/types/pi.hlean
+++ b/hott/types/pi.hlean
@ -45,6 +45,8 @@ namespace pi
  definition eq_equiv_homotopy (f g : Πx, B x) : (f = g) ≃ (f ~ g) :=
  equiv.mk apd10 _

+  definition pi_eq_equiv (f g : Πx, B x) : (f = g) ≃ (f ~ g) := !eq_equiv_homotopy
+
  definition is_equiv_eq_of_homotopy (f g : Πx, B x) : is_equiv (@eq_of_homotopy _ _ f g) :=
  _

--- a/hott/types/prod.hlean
+++ b/hott/types/prod.hlean
@ -7,7 +7,7 @@ Ported from Coq HoTT
 Theorems about products
 -/

-open eq equiv is_equiv is_trunc prod prod.ops unit
+open eq equiv is_equiv is_trunc prod prod.ops unit equiv.ops

 variables {A A' B B' C D : Type}
          {a a' a'' : A} {b b₁ b₂ b' b'' : B} {u v w : A × B}
@ -17,12 +17,106 @@ namespace prod
  protected definition eta (u : A × B) : (pr₁ u, pr₂ u) = u :=
  by cases u; apply idp

-  definition pair_eq (pa : a = a') (pb : b = b') : (a, b) = (a', b') :=
+  definition pair_eq [unfold 7 8] (pa : a = a') (pb : b = b') : (a, b) = (a', b') :=
  by cases pa; cases pb; apply idp

-  definition prod_eq (H₁ : pr₁ u = pr₁ v) (H₂ : pr₂ u = pr₂ v) : u = v :=
+  definition prod_eq [unfold 3 4 5 6] (H₁ : u.1 = v.1) (H₂ : u.2 = v.2) : u = v :=
  by cases u; cases v; exact pair_eq H₁ H₂

+  /- Projections of paths from a total space -/
+
+  definition eq_pr1 (p : u = v) : u.1 = v.1 :=
+  ap pr1 p
+
+  definition eq_pr2 (p : u = v) : u.2 = v.2 :=
+  ap pr2 p
+
+  namespace ops
+    postfix `..1`:(max+1) := eq_pr1
+    postfix `..2`:(max+1) := eq_pr2
+  end ops
+  open ops
+
+  definition pair_prod_eq (p : u.1 = v.1) (q : u.2 = v.2)
+    : ((prod_eq p q)..1, (prod_eq p q)..2) = (p, q) :=
+  by induction u; induction v;esimp at *;induction p;induction q;reflexivity
+
+  definition prod_eq_pr1 (p : u.1 = v.1) (q : u.2 = v.2) : (prod_eq p q)..1 = p :=
+  (pair_prod_eq p q)..1
+
+  definition prod_eq_pr2 (p : u.1 = v.1) (q : u.2 = v.2) : (prod_eq p q)..2 = q :=
+  (pair_prod_eq p q)..2
+
+  definition prod_eq_eta (p : u = v) : prod_eq (p..1) (p..2) = p :=
+  by induction p; induction u; reflexivity
+
+  /- the uncurried version of prod_eq. We will prove that this is an equivalence -/
+
+  definition prod_eq_unc (H : u.1 = v.1 × u.2 = v.2) : u = v :=
+  by cases H with H₁ H₂;exact prod_eq H₁ H₂
+
+  definition pair_prod_eq_unc : Π(pq : u.1 = v.1 × u.2 = v.2),
+    ((prod_eq_unc pq)..1, (prod_eq_unc pq)..2) = pq
+  | pair_prod_eq_unc (pq₁, pq₂) := pair_prod_eq pq₁ pq₂
+
+  definition prod_eq_unc_pr1 (pq : u.1 = v.1 × u.2 = v.2) : (prod_eq_unc pq)..1 = pq.1 :=
+  (pair_prod_eq_unc pq)..1
+
+  definition prod_eq_unc_pr2 (pq : u.1 = v.1 × u.2 = v.2) : (prod_eq_unc pq)..2 = pq.2 :=
+  (pair_prod_eq_unc pq)..2
+
+  definition prod_eq_unc_eta (p : u = v) : prod_eq_unc (p..1, p..2) = p :=
+  prod_eq_eta p
+
+  definition is_equiv_prod_eq [instance] (u v : A × B)
+    : is_equiv (prod_eq_unc : u.1 = v.1 × u.2 = v.2 → u = v) :=
+  adjointify prod_eq_unc
+             (λp, (p..1, p..2))
+             prod_eq_unc_eta
+             pair_prod_eq_unc
+
+  definition prod_eq_equiv (u v : A × B) : (u = v) ≃ (u.1 = v.1 × u.2 = v.2) :=
+  (equiv.mk prod_eq_unc _)⁻¹ᵉ
+
+  /- Transport -/
+
+  definition prod_transport {P Q : A → Type} {a a' : A} (p : a = a') (u : P a × Q a)
+    : p ▸ u = (p ▸ u.1, p ▸ u.2) :=
+  by induction p; induction u; reflexivity
+
+  /- Functorial action -/
+
+  variables (f : A → A') (g : B → B')
+  definition prod_functor [unfold 7] (u : A × B) : A' × B' :=
+  (f u.1, g u.2)
+
+  definition ap_prod_functor (p : u.1 = v.1) (q : u.2 = v.2)
+    : ap (prod_functor f g) (prod_eq p q) = prod_eq (ap f p) (ap g q) :=
+  by induction u; induction v; esimp at *; induction p; induction q; reflexivity
+
+  /- Equivalences -/
+
+  definition is_equiv_prod_functor [instance] [H : is_equiv f] [H : is_equiv g]
+    : is_equiv (prod_functor f g) :=
+  begin
+    apply adjointify _ (prod_functor f⁻¹ g⁻¹),
+      intro u, induction u, rewrite [▸*,right_inv f,right_inv g],
+      intro u, induction u, rewrite [▸*,left_inv f,left_inv g],
+  end
+
+  definition prod_equiv_prod_of_is_equiv [H : is_equiv f] [H : is_equiv g]
+    : A × B ≃ A' × B' :=
+  equiv.mk (prod_functor f g) _
+
+  definition prod_equiv_prod (f : A ≃ A') (g : B ≃ B') : A × B ≃ A' × B' :=
+  equiv.mk (prod_functor f g) _
+
+  definition prod_equiv_prod_left (g : B ≃ B') : A × B ≃ A × B' :=
+  prod_equiv_prod equiv.refl g
+
+  definition prod_equiv_prod_right (f : A ≃ A') : A × B ≃ A' × B :=
+  prod_equiv_prod f equiv.refl
+
  /- Symmetry -/

  definition is_equiv_flip [instance] (A B : Type) : is_equiv (@flip A B) :=
@ -34,6 +128,17 @@ namespace prod
  definition prod_comm_equiv (A B : Type) : A × B ≃ B × A :=
  equiv.mk flip _

+  /- Associativity -/
+
+  definition prod_assoc_equiv (A B C : Type) : A × (B × C) ≃ (A × B) × C :=
+  begin
+    fapply equiv.MK,
+    { intro z, induction z with a z, induction z with b c, exact (a, b, c)},
+    { intro z, induction z with z c, induction z with a b, exact (a, (b, c))},
+    { intro z, induction z with z c, induction z with a b, reflexivity},
+    { intro z, induction z with a z, induction z with b c, reflexivity},
+  end
+
  definition prod_contr_equiv (A B : Type) [H : is_contr B] : A × B ≃ A :=
  equiv.MK pr1
           (λx, (x, !center))
@ -43,6 +148,49 @@ namespace prod
  definition prod_unit_equiv (A : Type) : A × unit ≃ A :=
  !prod_contr_equiv

-  -- is_trunc_prod is defined in sigma
+  /- Universal mapping properties -/
+  definition is_equiv_prod_rec [instance] (P : A × B → Type)
+    : is_equiv (prod.rec : (Πa b, P (a, b)) → Πu, P u) :=
+  adjointify _
+             (λg a b, g (a, b))
+             (λg, eq_of_homotopy (λu, by induction u;reflexivity))
+             (λf, idp)
+
+  definition equiv_prod_rec (P : A × B → Type) : (Πa b, P (a, b)) ≃ (Πu, P u) :=
+  equiv.mk prod.rec _
+
+  definition imp_imp_equiv_prod_imp (A B C : Type) : (A → B → C) ≃ (A × B → C) :=
+  !equiv_prod_rec
+
+  definition prod_corec_unc [unfold 4] {P Q : A → Type} (u : (Πa, P a) × (Πa, Q a)) (a : A)
+    : P a × Q a :=
+  (u.1 a, u.2 a)
+
+  definition is_equiv_prod_corec (P Q : A → Type)
+    : is_equiv (prod_corec_unc : (Πa, P a) × (Πa, Q a) → Πa, P a × Q a) :=
+  adjointify _
+             (λg, (λa, (g a).1, λa, (g a).2))
+             (by intro g; apply eq_of_homotopy; intro a; esimp; induction (g a); reflexivity)
+             (by intro h; induction h with f g; reflexivity)
+
+  definition equiv_prod_corec (P Q : A → Type) : ((Πa, P a) × (Πa, Q a)) ≃ (Πa, P a × Q a) :=
+  equiv.mk _ !is_equiv_prod_corec
+
+  definition imp_prod_imp_equiv_imp_prod (A B C : Type) : (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]
+    : is_trunc n (A × B) :=
+  begin
+    revert A B HA HB, induction n with n IH, all_goals intro A B HA HB,
+    { fapply is_contr.mk,
+        exact (!center, !center),
+        intro u, apply prod_eq, all_goals apply center_eq},
+    { apply is_trunc_succ_intro, intro u v,
+      apply is_trunc_equiv_closed_rev, apply prod_eq_equiv,
+      exact IH _ _ _ _}
+  end

 end prod
+
+attribute prod.is_trunc_prod [instance] [priority 1505]
--- a/hott/types/sigma.hlean
+++ b/hott/types/sigma.hlean
@ -95,8 +95,8 @@ namespace sigma
             sigma_eq_eta_unc
             dpair_sigma_eq_unc

-  definition equiv_sigma_eq (u v : Σa, B a) : (Σ(p : u.1 = v.1),  u.2 =[p] v.2) ≃ (u = v) :=
-  equiv.mk sigma_eq_unc !is_equiv_sigma_eq
+  definition sigma_eq_equiv (u v : Σa, B a) : (u = v) ≃ (Σ(p : u.1 = v.1),  u.2 =[p] v.2) :=
+  (equiv.mk sigma_eq_unc _)⁻¹ᵉ

  definition dpair_eq_dpair_con (p1 : a  = a' ) (q1 : b  =[p1] b' )
                                (p2 : a' = a'') (q2 : b' =[p2] b'') :
@ -157,18 +157,18 @@ namespace sigma

  In particular, this indicates why `transport` alone cannot be fully defined by induction on the structure of types, although Id-elim/transportD can be (cf. Observational Type Theory).  A more thorough set of lemmas, along the lines of the present ones but dealing with Id-elim rather than just transport, might be nice to have eventually? -/

-  definition transport_eq (p : a = a') (bc : Σ(b : B a), C a b)
+  definition sigma_transport (p : a = a') (bc : Σ(b : B a), C a b)
    : p ▸ bc = ⟨p ▸ bc.1, p ▸D bc.2⟩ :=
  by induction p; induction bc; reflexivity

  /- The special case when the second variable doesn't depend on the first is simpler. -/
-  definition tr_eq_nondep {B : Type} {C : A → B → Type} (p : a = a') (bc : Σ(b : B), C a b)
+  definition sigma_transport_nondep {B : Type} {C : A → B → Type} (p : a = a') (bc : Σ(b : B), C a b)
      : p ▸ bc = ⟨bc.1, p ▸ bc.2⟩ :=
  by induction p; induction bc; reflexivity

  /- Or if the second variable contains a first component that doesn't depend on the first. -/

-  definition tr_eq2_nondep {C : A → Type} {D : Π a:A, B a → C a → Type} (p : a = a')
+  definition sigma_transport2_nondep {C : A → Type} {D : Π a:A, B a → C a → Type} (p : a = a')
      (bcd : Σ(b : B a) (c : C a), D a b c) : p ▸ bcd = ⟨p ▸ bcd.1, p ▸ bcd.2.1, p ▸D2 bcd.2.2⟩ :=
  begin
    induction p, induction bcd with b cd, induction cd, reflexivity
@ -362,17 +362,11 @@ namespace sigma
  induction n with n IH,
  { intro A B HA HB, fapply is_trunc_equiv_closed_rev, apply sigma_equiv_of_is_contr_pr1},
  { intro A B HA HB, apply is_trunc_succ_intro, intro u v,
-    apply is_trunc_equiv_closed,
-      apply equiv_sigma_eq,
+    apply is_trunc_equiv_closed_rev,
+      apply sigma_eq_equiv,
      exact IH _ _ _ _}
  end

 end sigma

-attribute sigma.is_trunc_sigma [instance] [priority 1505]
-
-open is_trunc sigma prod
-/- truncatedness -/
-definition prod.is_trunc_prod [instance] [priority 1490] (A B : Type) (n : trunc_index)
-  [HA : is_trunc n A] [HB : is_trunc n B] : is_trunc n (A × B) :=
-is_trunc.is_trunc_equiv_closed n !equiv_prod
+attribute sigma.is_trunc_sigma [instance] [priority 1490]
--- a/hott/types/sum.hlean
+++ b/hott/types/sum.hlean
@ -0,0 +1,159 @@
+/-
+Copyright (c) 2015 Floris van Doorn. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Floris van Doorn
+
+Theorems about sums/coproducts/disjoint unions
+-/
+
+open lift eq is_equiv equiv equiv.ops prod prod.ops is_trunc sigma bool
+
+namespace sum
+  universe variables u v
+  variables {A : Type.{u}} {B : Type.{v}} (z z' : A + B)
+
+  protected definition eta : sum.rec inl inr z = z :=
+  by induction z; all_goals reflexivity
+
+  protected definition code [unfold 3 4] : A + B → A + B → Type.{max u v}
+  | code (inl a) (inl a') := lift.{u v} (a = a')
+  | code (inr b) (inr b') := lift.{v u} (b = b')
+  | code _       _        := lift empty
+
+  protected definition decode [unfold 3 4] : Π(z z' : A + B), sum.code z z' → z = z'
+  | decode (inl a) (inl a') := λc, ap inl (down c)
+  | decode (inl a) (inr b') := λc, empty.elim (down c) _
+  | decode (inr b) (inl a') := λc, empty.elim (down c) _
+  | decode (inr b) (inr b') := λc, ap inr (down c)
+
+  variables {z z'}
+  protected definition encode [unfold 3 4 5] (p : z = z') : sum.code z z' :=
+  by induction p; induction z; all_goals exact up idp
+
+  variables (z z')
+  definition sum_eq_equiv : (z = z') ≃ sum.code z z' :=
+  equiv.MK sum.encode
+           !sum.decode
+           abstract begin
+             intro c, induction z with a b, all_goals induction z' with a' b',
+             all_goals (esimp at *; induction c with c),
+             all_goals induction c, -- c either has type empty or a path
+             all_goals reflexivity
+           end end
+           abstract begin
+             intro p, induction p, induction z, all_goals reflexivity
+           end end
+
+  section
+  variables {a a' : A} {b b' : B}
+  definition eq_of_inl_eq_inl [unfold 5] (p : inl a = inl a' :> A + B) : a = a' :=
+  down (sum.encode p)
+  definition eq_of_inr_eq_inr [unfold 5] (p : inr b = inr b' :> A + B) : b = b' :=
+  down (sum.encode p)
+  definition empty_of_inl_eq_inr (p : inl a = inr b) : empty := down (sum.encode p)
+  definition empty_of_inr_eq_inl (p : inr b = inl a) : empty := down (sum.encode p)
+
+  definition sum_transport {P Q : A → Type} (p : a = a') (z : P a + Q a)
+    : p ▸ z = sum.rec (λa, inl (p ▸ a)) (λb, inr (p ▸ b)) z :=
+  by induction p; induction z; all_goals reflexivity
+  end
+
+  variables {A' B' : Type} (f : A → A') (g : B → B')
+  definition sum_functor [unfold 7] : A + B → A' + B'
+  | sum_functor (inl a) := inl (f a)
+  | sum_functor (inr b) := inr (g b)
+
+  definition is_equiv_sum_functor [Hf : is_equiv f] [Hg : is_equiv g] : is_equiv (sum_functor f g) :=
+  adjointify (sum_functor f   g)
+             (sum_functor f⁻¹ g⁻¹)
+             abstract begin
+               intro z, induction z,
+               all_goals (esimp; (apply ap inl | apply ap inr); apply right_inv)
+             end end
+             abstract begin
+               intro z, induction z,
+               all_goals (esimp; (apply ap inl | apply ap inr); apply right_inv)
+             end end
+
+  definition sum_equiv_sum_of_is_equiv [Hf : is_equiv f] [Hg : is_equiv g] : A + B ≃ A' + B' :=
+  equiv.mk _ (is_equiv_sum_functor f g)
+
+  definition sum_equiv_sum (f : A ≃ A') (g : B ≃ B') : A + B ≃ A' + B' :=
+  equiv.mk _ (is_equiv_sum_functor f g)
+
+  definition sum_equiv_sum_left (g : B ≃ B') : A + B ≃ A + B' :=
+  sum_equiv_sum equiv.refl g
+
+  definition sum_equiv_sum_right (f : A ≃ A') : A + B ≃ A' + B :=
+  sum_equiv_sum f equiv.refl
+
+  definition flip : A + B → B + A
+  | flip (inl a) := inr a
+  | flip (inr b) := inl b
+
+  definition sum_comm_equiv (A B : Type) : A + B ≃ B + A :=
+  begin
+    fapply equiv.MK,
+      exact flip,
+      exact flip,
+      all_goals (intro z; induction z; all_goals reflexivity)
+  end
+
+  -- definition sum_assoc_equiv (A B C : Type) : A + (B + C) ≃ (A + B) + C :=
+  -- begin
+  --   fapply equiv.MK,
+  --     all_goals try (intro z; induction z with u v;
+  --                    all_goals try induction u; all_goals try induction v),
+  --     all_goals try (repeat (apply inl | apply inr | assumption); now),
+  -- end
+
+  definition sum_empty_equiv (A : Type) : A + empty ≃ A :=
+  begin
+    fapply equiv.MK,
+      intro z, induction z, assumption, contradiction,
+      exact inl,
+      intro a, reflexivity,
+      intro z, induction z, reflexivity, contradiction
+  end
+
+  definition sum_rec_unc {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 (P : A + B → Type)
+    : is_equiv (sum_rec_unc : (Πa, P (inl a)) × (Πb, P (inr b)) → Πz, P z) :=
+  begin
+     apply adjointify sum_rec_unc (λf, (λa, f (inl a), λb, f (inr b))),
+       intro f, apply eq_of_homotopy, intro z, focus (induction z; all_goals reflexivity),
+       intro h, induction h with f g, reflexivity
+  end
+
+  definition equiv_sum_rec (P : A + B → Type) : (Πa, P (inl a)) × (Πb, P (inr b)) ≃ Πz, P z :=
+  equiv.mk _ !is_equiv_sum_rec
+
+  definition imp_prod_imp_equiv_sum_imp (A B C : Type) : (A → C) × (B → C) ≃ (A + B → C) :=
+  !equiv_sum_rec
+
+  definition 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',
+    apply is_trunc_equiv_closed_rev, apply sum_eq_equiv,
+    induction z with a b, all_goals induction z' with a' b', all_goals esimp,
+    all_goals exact _,
+  end
+
+  /- Sums are equivalent to dependent sigmas where the first component is a bool. -/
+
+  definition sum_of_sigma_bool {A B : Type} (v : Σ(b : bool), bool.rec A B b) : A + B :=
+  by induction v with b x; induction b; exact inl x; exact inr x
+
+  definition sigma_bool_of_sum {A B : Type} (z : A + B) : Σ(b : bool), bool.rec A B b :=
+  by induction z with a b; exact ⟨ff, a⟩; exact ⟨tt, b⟩
+
+  definition sum_equiv_sigma_bool (A B : Type) : A + B ≃ Σ(b : bool), bool.rec A B b :=
+  equiv.MK sigma_bool_of_sum
+           sum_of_sigma_bool
+           begin intro v, induction v with b x, induction b, all_goals reflexivity end
+           begin intro z, induction z with a b, all_goals reflexivity end
+
+end sum
--- a/hott/types/types.md
+++ b/hott/types/types.md
@ -9,6 +9,7 @@ Types (not necessarily HoTT-related):
 * [int](int/int.md) (subfolder)
 * [prod](prod.hlean)
 * [sigma](sigma.hlean)
+* [sum](sum.hlean)
 * [pi](pi.hlean)
 * [arrow](arrow.hlean)
 * [W](W.hlean): W-types (not loaded by default)
--- a/library/init/prod.lean
+++ b/library/init/prod.lean
@ -12,10 +12,9 @@ notation A × B := prod A B
 notation `(` h `,` t:(foldl `,` (e r, prod.mk r e) h) `)` := t

 namespace prod
-  notation A * B := prod A B
-  notation A × B := prod A B  -- repeat, so this takes precedence
+  notation [parsing-only] A * B := prod A B
  namespace low_precedence_times
-    reserve infixr `*`:30     -- conflicts with notation for multiplication
+    reserve infixr [parsing-only] `*`:30     -- conflicts with notation for multiplication
    infixr `*` := prod
  end low_precedence_times