feat(library/hott): multiple changes in the HoTT library

Jakob accidentally undid some of my changes in commit aad4592, reverted that;
made style changes in multiple files;
in types/sigma: finished porting Coq-HoTT, and finished unfinished proof;
in axioms/funext: rename path_forall, make arguments implicit and make instance visible

library/hott/algebra/precategory/constructions.lean

@@ -6,7 +6,7 @@
 
 
 import .natural_transformation hott.path
-import data.unit data.sigma data.prod data.empty data.bool hott.types.prod
+import data.unit data.sigma data.prod data.empty data.bool hott.types.prod hott.types.sigma
 
 open path prod eq eq.ops
 
@@ -94,7 +94,7 @@ namespace precategory
   definition prod_precategory {obC obD : Type} (C : precategory obC) (D : precategory obD)
       : precategory (obC × obD) :=
   mk (λ a b, hom (pr1 a) (pr1 b) × hom (pr2 a) (pr2 b))
-     (λ a b, trunc_prod nat.zero (!homH) (!homH))
+     (λ a b, !trunc_prod)
      (λ a b c g f, (pr1 g ∘ pr1 f , pr2 g ∘ pr2 f) )
      (λ a, (id, id))
      (λ a b c d h g f, pair_path  !assoc    !assoc   )

library/hott/axioms/funext.lean

@@ -16,20 +16,19 @@ inductive funext [class] : Type  :=
 
 namespace funext
 
-  context
+  universe variables l k
-    universe variables l k
+  variables [F : funext.{l k}] {A : Type.{l}} {P : A → Type.{k}}
-    parameters [F : funext.{l k}] {A : Type.{l}} {P : A → Type.{k}} (f g : Π x, P x)
 
-    protected definition ap [instance] : is_equiv (@apD10 A P f g) :=
+  include F
-      rec_on F (λ (H : Π A P f g, _), !H)
+  protected definition ap [instance] (f g : Π x, P x) : is_equiv (@apD10 A P f g) :=
+    rec_on F (λ(H : Π A P f g, _), !H)
 
-    definition path_forall : f ∼ g → f ≈ g :=
+  definition path_pi {f g : Π x, P x} : f ∼ g → f ≈ g :=
-      @is_equiv.inv _ _ (@apD10 A P f g) ap
+  is_equiv.inv (@apD10 A P f g)
 
-  end
+  omit F
-
+  definition path_pi2 [F : funext] {A B : Type} {P : A → B → Type}
-  definition path_forall2 [F : funext] {A B : Type} {P : A → B → Type}
       (f g : Πx y, P x y) : (Πx y, f x y ≈ g x y) → f ≈ g :=
-    λ E, path_forall f g (λx, path_forall (f x) (g x) (E x))
+    λ E, path_pi (λx, path_pi (E x))
 
 end funext

library/hott/equiv.lean

@@ -30,7 +30,7 @@ namespace is_equiv
   variables {A B C : Type} (f : A → B) (g : B → C) {f' : A → B}
 
   -- The identity function is an equivalence.
-  protected definition id_is_equiv : (@is_equiv A A id) := is_equiv.mk id (λa, idp) (λa, idp) (λa, idp)
+  definition id_is_equiv : (@is_equiv A A id) := is_equiv.mk id (λa, idp) (λa, idp) (λa, idp)
 
   -- The composition of two equivalences is, again, an equivalence.
   protected definition compose [Hf : is_equiv f] [Hg : is_equiv g] : (is_equiv (g ∘ f)) :=

library/hott/equiv_precomp.lean

@@ -18,15 +18,15 @@ namespace is_equiv
   definition precomp_closed [instance] {A B : Type} (f : A → B) [F : funext] [Hf : is_equiv f] (C : Type)
       : is_equiv (precomp f C) :=
     adjointify (precomp f C) (λh, h ∘ f⁻¹)
-      (λh, path_forall _ _ (λx, ap h (sect f x)))
+      (λh, path_pi (λx, ap h (sect f x)))
-      (λg, path_forall _ _ (λy, ap g (retr f y)))
+      (λg, path_pi (λy, ap g (retr f y)))
 
   --Postcomposing with an equivalence is an equivalence
   definition postcomp_closed [instance] {A B : Type} (f : A → B) [F : funext] [Hf : is_equiv f] (C : Type)
       : is_equiv (postcomp f C) :=
     adjointify (postcomp f C) (λl, f⁻¹ ∘ l)
-      (λh, path_forall _ _ (λx, retr f (h x)))
+      (λh, path_pi (λx, retr f (h x)))
-      (λg, path_forall _ _ (λy, sect f (g y)))
+      (λg, path_pi (λy, sect f (g y)))
 
   --Conversely, if pre- or post-composing with a function is always an equivalence,
   --then that function is also an equivalence.  It's convenient to know

library/hott/trunc.lean

@@ -78,12 +78,12 @@ namespace truncation
 
   variables {A B : Type}
 
-  -- maybe rename to is_trunc_succ.mk
+  -- TODO: rename to is_trunc_succ
   definition is_trunc_succ (A : Type) (n : trunc_index) [H : ∀x y : A, is_trunc n (x ≈ y)]
     : is_trunc n.+1 A :=
   is_trunc.mk (λ x y, !is_trunc.to_internal)
 
-  -- maybe rename to is_trunc_succ.elim
+  -- TODO: rename to is_trunc_path
   definition succ_is_trunc (n : trunc_index) [H : is_trunc (n.+1) A] (x y : A) : is_trunc n (x ≈ y) :=
   is_trunc.mk (!is_trunc.to_internal x y)
 

library/hott/types/W.lean

@@ -10,30 +10,30 @@ import .sigma .pi
 open path sigma sigma.ops equiv is_equiv
 
 
-inductive W {A : Type} (B : A → Type) :=
+inductive Wtype {A : Type} (B : A → Type) :=
-sup : Π(a : A), (B a → W B) → W B
+sup : Π(a : A), (B a → Wtype B) → Wtype B
 
-namespace W
+namespace Wtype
-  notation `WW` binders `,` r:(scoped B, W B) := r
+  notation `W` binders `,` r:(scoped B, Wtype B) := r
 
-  universe variables l k
+  universe variables u v
-  variables {A A' : Type.{l}} {B B' : A → Type.{k}} {C : Π(a : A), B a → Type}
+  variables {A A' : Type.{u}} {B B' : A → Type.{v}} {C : Π(a : A), B a → Type}
-            {a a' : A} {f : B a → W B} {f' : B a' → W B} {w w' : WW(a : A), B a}
+            {a a' : A} {f : B a → W a, B a} {f' : B a' → W a, B a} {w w' : W(a : A), B a}
 
-  definition pr1 (w : WW(a : A), B a) : A :=
+  definition pr1 (w : W(a : A), B a) : A :=
-  W.rec_on w (λa f IH, a)
+  Wtype.rec_on w (λa f IH, a)
 
-  definition pr2 (w : WW(a : A), B a) : B (pr1 w) → WW(a : A), B a :=
+  definition pr2 (w : W(a : A), B a) : B (pr1 w) → W(a : A), B a :=
-  W.rec_on w (λa f IH, f)
+  Wtype.rec_on w (λa f IH, f)
 
   namespace ops
-  postfix `.1`:(max+1) := W.pr1
+  postfix `.1`:(max+1) := Wtype.pr1
-  postfix `.2`:(max+1) := W.pr2
+  postfix `.2`:(max+1) := Wtype.pr2
-  notation `⟨` a `,` f `⟩`:0 := W.sup a f --input ⟨ ⟩ as \< \>
+  notation `⟨` a `,` f `⟩`:0 := Wtype.sup a f --input ⟨ ⟩ as \< \>
   end ops
   open ops
 
-  protected definition eta (w : WW a, B a) : ⟨w.1 , w.2⟩ ≈ w :=
+  protected definition eta (w : W a, B a) : ⟨w.1 , w.2⟩ ≈ w :=
   cases_on w (λa f, idp)
 
   definition path_W_sup (p : a ≈ a') (q : p ▹ f ≈ f') : ⟨a, f⟩ ≈ ⟨a', f'⟩ :=
@@ -112,18 +112,18 @@ namespace W
       : transport (λx, B' x.1) (@path_W_uncurried A B w w' pq) ≈ transport B' pq.1 :=
     destruct pq transport_pr1_path_W
 
-  definition isequiv_path_W /-[instance]-/ (w w' : W B)
+  definition isequiv_path_W /-[instance]-/ (w w' : W a, B a)
       : is_equiv (@path_W_uncurried A B w w') :=
   adjointify path_W_uncurried
              (λp, dpair (p..1) (p..2))
              eta_path_W_uncurried
              sup_path_W_uncurried
 
-  definition equiv_path_W (w w' : W B) : (Σ(p : w.1 ≈ w'.1),  p ▹ w.2 ≈ w'.2) ≃ (w ≈ w') :=
+  definition equiv_path_W (w w' : W a, B a) : (Σ(p : w.1 ≈ w'.1),  p ▹ w.2 ≈ w'.2) ≃ (w ≈ w') :=
   equiv.mk path_W_uncurried !isequiv_path_W
 
-  definition double_induction_on {P : W B → W B → Type} (w w' : W B)
+  definition double_induction_on {P : (W a, B a) → (W a, B a) → Type} (w w' : W a, B a)
-    (H : ∀ (a a' : A) (f : B a → W B) (f' : B a' → W B),
+    (H : ∀ (a a' : A) (f : B a → W a, B a) (f' : B a' → W a, B a),
       (∀ (b : B a) (b' : B a'), P (f b) (f' b')) → P (sup a f) (sup a' f')) : P w w' :=
   begin
     revert w',
@@ -135,8 +135,8 @@ namespace W
 
   /- truncatedness -/
   open truncation
-  definition trunc_W [FUN : funext.{k (max 1 l k)}] (n : trunc_index) [HA : is_trunc (n.+1) A]
+  definition trunc_W [FUN : funext.{v (max 1 u v)}] (n : trunc_index) [HA : is_trunc (n.+1) A]
-    : is_trunc (n.+1) (WW a, B a) :=
+    : is_trunc (n.+1) (W a, B a) :=
   begin
   fapply is_trunc_succ, intros (w, w'),
   apply (double_induction_on w w'), intros (a, a', f, f', IH),
@@ -146,8 +146,8 @@ namespace W
       fapply (succ_is_trunc n),
       intro p, revert IH, generalize f', --change to revert after simpl
       apply (path.rec_on p), intros (f', IH),
-      apply (@pi.trunc_path_pi FUN (B a) (λx, W B) n f f'), intro b,
+      apply pi.trunc_path_pi, intro b,
       apply IH
   end
 
-end W
+end Wtype

library/hott/types/pi.lean

@@ -7,52 +7,116 @@ Ported from Coq HoTT
 Theorems about pi-types (dependent function spaces)
 -/
 
-import ..trunc ..axioms.funext
+import ..trunc ..axioms.funext .sigma
 open path equiv is_equiv funext
 
 namespace pi
   universe variables l k
-  variables [H : funext.{l k}] {A : Type.{l}} {B : A → Type.{k}} {C : Πa, B a → Type}
+  variables {A A' : Type.{l}} {B : A → Type.{k}} {C : Πa, B a → Type}
             {D : Πa b, C a b → Type}
-            {a a' a'' : A} {b b₁ b₂ : B a} {b' : B a'} {b'' : B a''} {f g h : Πa, B a}
+            {a a' a'' : A} {b b₁ b₂ : B a} {b' : B a'} {b'' : B a''} {f g : Πa, B a}
-  include H
+
   /- Paths -/
 
-  /- Paths [p : f ≈ g] in a function type [Πx:X, P x] are equivalent to functions taking values in path types, [H : Πx:X, f x ≈ g x], or concisely, [H : f == g].
+  /- Paths [p : f ≈ g] in a function type [Πx:X, P x] are equivalent to functions taking values in path types, [H : Πx:X, f x ≈ g x], or concisely, [H : f ∼ g].
 
   This equivalence, however, is just the combination of [apD10] and function extensionality [funext], and as such, [path_forall], et seq. are given in axioms.funext and path:  -/
 
   /- Now we show how these things compute. -/
 
-  definition equiv_apD10 : (f ≈ g) ≃ (f ∼ g) :=
+  definition apD10_path_pi [H : funext] (h : f ∼ g) : apD10 (path_pi h) ∼ h :=
+  apD10 (retr apD10 h)
+
+  definition path_pi_eta [H : funext] (p : f ≈ g) : path_pi (apD10 p) ≈ p :=
+  sect apD10 p
+
+  definition path_pi_idp [H : funext] : path_pi (λx : A, idpath (f x)) ≈ idpath f :=
+  !path_pi_eta
+
+  /- The identification of the path space of a dependent function space, up to equivalence, is of course just funext. -/
+
+  definition path_equiv_homotopy [H : funext] (f g : Πx, B x) : (f ≈ g) ≃ (f ∼ g) :=
   equiv.mk _ !funext.ap
 
+  definition is_equiv_path_pi [instance] [H : funext] (f g : Πx, B x)
+      : is_equiv (@path_pi _ _ _ f g) :=
+  inv_closed apD10
+
+  definition homotopy_equiv_path [H : funext] (f g : Πx, B x) : (f ∼ g) ≃ (f ≈ g) :=
+  equiv.mk _ !is_equiv_path_pi
+
+
+  /- Transport -/
+
+  protected definition transport (p : a ≈ a') (f : Π(b : B a), C a b)
+    : (transport (λa, Π(b : B a), C a b) p f)
+      ∼ (λb, transport (C a') !transport_pV (transportD _ _ p _ (f (p⁻¹ ▹ b)))) :=
+  path.rec_on p (λx, idp)
+
+  /- A special case of [transport_pi] where the type [B] does not depend on [A],
+      and so it is just a fixed type [B]. -/
+  definition transport_constant {C : A → A' → Type} (p : a ≈ a') (f : Π(b : A'), C a b)
+    : (path.transport (λa, Π(b : A'), C a b) p f) ∼ (λb, path.transport (λa, C a b) p (f b)) :=
+  path.rec_on p (λx, idp)
+
+  /- Maps on paths -/
+
+  /- The action of maps given by lambda. -/
+  definition ap_lambdaD [H : funext] {C : A' → Type} (p : a ≈ a') (f : Πa b, C b) :
+    ap (λa b, f a b) p ≈ path_pi (λb, ap (λa, f a b) p) :=
+  begin
+    apply (path.rec_on p),
+    apply inverse,
+    apply path_pi_idp
+  end
+
+  /- Dependent paths -/
+
+  /- with more implicit arguments the conclusion of the following theorem is
+     (Π(b : B a), transportD B C p b (f b) ≈ g (path.transport B p b)) ≃
+     (path.transport (λa, Π(b : B a), C a b) p f ≈ g) -/
+  definition dpath_pi [H : funext] (p : a ≈ a') (f : Π(b : B a), C a b) (g : Π(b' : B a'), C a' b')
+    : (Π(b : B a), p ▹D (f b) ≈ g (p ▹ b)) ≃ (p ▹ f ≈ g) :=
+  path.rec_on p (λg, !homotopy_equiv_path) g
+
+  section open sigma.ops
+  /- more implicit arguments:
+  (Π(b : B a), path.transport C (sigma.path p idp) (f b) ≈ g (p ▹ b)) ≃
+  (Π(b : B a), transportD B (λ(a : A) (b : B a), C ⟨a, b⟩) p b (f b) ≈ g (path.transport B p b)) -/
+  definition dpath_pi_sigma {C : (Σa, B a) → Type} (p : a ≈ a')
+    (f : Π(b : B a), C ⟨a, b⟩) (g : Π(b' : B a'), C ⟨a', b'⟩) :
+    (Π(b : B a), (sigma.path p idp) ▹ (f b) ≈ g (p ▹ b)) ≃ (Π(b : B a), p ▹D (f b) ≈ g (p ▹ b)) :=
+  path.rec_on p (λg, !equiv.refl) g
+  end
+
+  /- truncation -/
+
   open truncation
-  definition trunc_pi [instance] (B : A → Type.{k}) (n : trunc_index)
+  definition trunc_pi [instance] [H : funext.{l k}] (B : A → Type.{k}) (n : trunc_index)
-      [H : Πa, is_trunc n (B a)] : is_trunc n (Πa, B a) :=
+      [H : ∀a, is_trunc n (B a)] : is_trunc n (Πa, B a) :=
   begin
     reverts (B, H),
-    apply (truncation.trunc_index.rec_on n),
+    apply (trunc_index.rec_on n),
       intros (B, H),
         fapply is_contr.mk,
           intro a, apply center, apply H, --remove "apply H" when term synthesis works correctly
-          intro f, apply path_forall,
+          intro f, apply path_pi,
             intro x, apply (contr (f x)),
       intros (n, IH, B, H),
         fapply is_trunc_succ, intros (f, g),
           fapply trunc_equiv',
-            apply equiv.symm, apply equiv_apD10,
+            apply equiv.symm, apply path_equiv_homotopy,
             apply IH,
               intro a,
               show is_trunc n (f a ≈ g a), from
               succ_is_trunc n (f a) (g a)
   end
 
-  definition trunc_path_pi [instance] (n : trunc_index) (f g : Πa, B a)
+  definition trunc_path_pi [instance] [H : funext.{l k}] (n : trunc_index) (f g : Πa, B a)
       [H : ∀a, is_trunc n (f a ≈ g a)] : is_trunc n (f ≈ g) :=
   begin
     apply trunc_equiv', apply equiv.symm,
-    apply equiv_apD10,
+    apply path_equiv_homotopy,
     apply trunc_pi, exact H,
   end
 

library/hott/types/prod.lean

@@ -15,7 +15,8 @@ variables {A A' B B' C D : Type}
 
 namespace prod
 
-  definition eta_prod (u : A × B) : (pr₁ u , pr₂ u) ≈ u :=
+  -- prod.eta is already used for the eta rule for strict equality
+  protected definition peta (u : A × B) : (pr₁ u , pr₂ u) ≈ u :=
   destruct u (λu1 u2, idp)
 
   definition pair_path (pa : a ≈ a') (pb : b ≈ b') : (a , b) ≈ (a' , b') :=
@@ -25,25 +26,22 @@ namespace prod
   begin
     apply (prod.rec_on u), intros (a₁, b₁),
     apply (prod.rec_on v), intros (a₂, b₂, H₁, H₂),
-    apply (transport _ (eta_prod (a₁, b₁))),
+    apply (transport _ (peta (a₁, b₁))),
-    apply (transport _ (eta_prod (a₂, b₂))),
+    apply (transport _ (peta (a₂, b₂))),
     apply (pair_path H₁ H₂),
   end
 
   /- Symmetry -/
 
-  definition isequiv_prod_symm [instance] (A B : Type) : is_equiv (@flip A B) :=
+  definition isequiv_flip [instance] (A B : Type) : is_equiv (@flip A B) :=
   adjointify flip
              flip
              (λu, destruct u (λb a, idp))
              (λu, destruct u (λa b, idp))
 
-  definition equiv_prod_symm (A B : Type) : A × B ≃ B × A :=
+  definition symm_equiv (A B : Type) : A × B ≃ B × A :=
   equiv.mk flip _
 
-  -- Pairs preserve truncatedness
+  -- trunc_prod is defined in sigma
-  definition trunc_prod [instance] {A B : Type} (n : trunc_index) :
-      (is_trunc n A) → (is_trunc n B) → is_trunc n (A × B)
-    := sorry --Assignment for Floris
 
 end prod

library/hott/types/sigma.lean

@@ -7,193 +7,194 @@ Ported from Coq HoTT
 Theorems about sigma-types (dependent sums)
 -/
 
-import ..trunc .prod
+import ..trunc .prod ..axioms.funext
 open path sigma sigma.ops equiv is_equiv
 
 namespace sigma
-  -- remove the ₁'s (globally)
+  infixr [local] ∘ := function.compose --remove
   variables {A A' : Type} {B : A → Type} {B' : A' → Type} {C : Πa, B a → Type}
             {D : Πa b, C a b → Type}
             {a a' a'' : A} {b b₁ b₂ : B a} {b' : B a'} {b'' : B a''} {u v w : Σa, B a}
 
-  definition eta_sigma (u : Σa, B a) : ⟨u.1 , u.2⟩ ≈ u :=
+  -- sigma.eta is already used for the eta rule for strict equality
+  protected definition peta (u : Σa, B a) : ⟨u.1 , u.2⟩ ≈ u :=
   destruct u (λu1 u2, idp)
 
-  definition eta2_sigma (u : Σa b, C a b) : ⟨u.1, u.2.1, u.2.2⟩ ≈ u :=
+  definition eta2 (u : Σa b, C a b) : ⟨u.1, u.2.1, u.2.2⟩ ≈ u :=
   destruct u (λu1 u2, destruct u2 (λu21 u22, idp))
 
-  definition eta3_sigma (u : Σa b c, D a b c) : ⟨u.1, u.2.1, u.2.2.1, u.2.2.2⟩ ≈ u :=
+  definition eta3 (u : Σa b c, D a b c) : ⟨u.1, u.2.1, u.2.2.1, u.2.2.2⟩ ≈ u :=
   destruct u (λu1 u2, destruct u2 (λu21 u22, destruct u22 (λu221 u222, idp)))
 
-  definition path_sigma_dpair (p : a ≈ a') (q : p ▹ b ≈ b') : dpair a b ≈ dpair a' b' :=
+  definition dpair_eq_dpair (p : a ≈ a') (q : p ▹ b ≈ b') : dpair a b ≈ dpair a' b' :=
   path.rec_on p (λb b' q, path.rec_on q idp) b b' q
 
   /- In Coq they often have to give u and v explicitly -/
-  definition path_sigma (p : u.1 ≈ v.1) (q : p ▹ u.2 ≈ v.2) : u ≈ v :=
+  protected definition path (p : u.1 ≈ v.1) (q : p ▹ u.2 ≈ v.2) : u ≈ v :=
   destruct u
-           (λu1 u2, destruct v (λ v1 v2, path_sigma_dpair))
+           (λu1 u2, destruct v (λ v1 v2, dpair_eq_dpair))
            p q
 
   /- Projections of paths from a total space -/
 
-  definition pr1_path (p : u ≈ v) : u.1 ≈ v.1 :=
+  definition path_pr1 (p : u ≈ v) : u.1 ≈ v.1 :=
   ap dpr1 p
 
-  postfix `..1`:(max+1) := pr1_path
+  postfix `..1`:(max+1) := path_pr1
 
-  definition pr2_path (p : u ≈ v) : p..1 ▹ u.2 ≈ v.2 :=
+  definition path_pr2 (p : u ≈ v) : p..1 ▹ u.2 ≈ v.2 :=
   path.rec_on p idp
   --Coq uses the following proof, which only computes if u,v are dpairs AND p is idp
   --(transport_compose B dpr1 p u.2)⁻¹ ⬝ apD dpr2 p
 
-  postfix `..2`:(max+1) := pr2_path
+  postfix `..2`:(max+1) := path_pr2
 
-  definition dpair_path_sigma (p : u.1 ≈ v.1) (q : p ▹ u.2 ≈ v.2)
+  definition dpair_sigma_path (p : u.1 ≈ v.1) (q : p ▹ u.2 ≈ v.2)
-      :  dpair (path_sigma p q)..1 (path_sigma p q)..2 ≈ ⟨p, q⟩ :=
+      :  dpair (sigma.path p q)..1 (sigma.path p q)..2 ≈ ⟨p, q⟩ :=
   begin
-    generalize q, generalize p,
+    reverts (p, q),
     apply (destruct u), intros (u1, u2),
-    apply (destruct v), intros (v1, v2, p), generalize v2,
+    apply (destruct v), intros (v1, v2, p), generalize v2, --change to revert
     apply (path.rec_on p), intros (v2, q),
     apply (path.rec_on q), apply idp
   end
 
-  definition pr1_path_sigma (p : u.1 ≈ v.1) (q : p ▹ u.2 ≈ v.2) : (path_sigma p q)..1 ≈ p :=
+  definition sigma_path_pr1 (p : u.1 ≈ v.1) (q : p ▹ u.2 ≈ v.2) : (sigma.path p q)..1 ≈ p :=
-  (!dpair_path_sigma)..1
+  (!dpair_sigma_path)..1
 
-  definition pr2_path_sigma (p : u.1 ≈ v.1) (q : p ▹ u.2 ≈ v.2)
+  definition sigma_path_pr2 (p : u.1 ≈ v.1) (q : p ▹ u.2 ≈ v.2)
-      : pr1_path_sigma p q ▹ (path_sigma p q)..2 ≈ q :=
+      : sigma_path_pr1 p q ▹ (sigma.path p q)..2 ≈ q :=
-  (!dpair_path_sigma)..2
+  (!dpair_sigma_path)..2
 
-  definition eta_path_sigma (p : u ≈ v) : path_sigma (p..1) (p..2) ≈ p :=
+  definition sigma_path_eta (p : u ≈ v) : sigma.path (p..1) (p..2) ≈ p :=
   begin
     apply (path.rec_on p),
     apply (destruct u), intros (u1, u2),
     apply idp
   end
 
-  definition transport_pr1_path_sigma {B' : A → Type} (p : u.1 ≈ v.1) (q : p ▹ u.2 ≈ v.2)
+  definition transport_dpr1_sigma_path {B' : A → Type} (p : u.1 ≈ v.1) (q : p ▹ u.2 ≈ v.2)
-      : transport (λx, B' x.1) (path_sigma p q) ≈ transport B' p :=
+      : transport (λx, B' x.1) (sigma.path p q) ≈ transport B' p :=
   begin
-    generalize q, generalize p,
+    reverts (p, q),
     apply (destruct u), intros (u1, u2),
     apply (destruct v), intros (v1, v2, p), generalize v2,
     apply (path.rec_on p), intros (v2, q),
     apply (path.rec_on q), apply idp
   end
 
-  /- the uncurried version of path_sigma. We will prove that this is an equivalence -/
+  /- the uncurried version of sigma_path. We will prove that this is an equivalence -/
 
-  definition path_sigma_uncurried (pq : Σ(p : dpr1 u ≈ dpr1 v), p ▹ (dpr2 u) ≈ dpr2 v) : u ≈ v :=
+  definition sigma_path_uncurried (pq : Σ(p : dpr1 u ≈ dpr1 v), p ▹ (dpr2 u) ≈ dpr2 v) : u ≈ v :=
-  destruct pq path_sigma
+  destruct pq sigma.path
 
-  definition dpair_path_sigma_uncurried (pq : Σ(p : u.1 ≈ v.1), p ▹ u.2 ≈ v.2)
+  definition dpair_sigma_path_uncurried (pq : Σ(p : u.1 ≈ v.1), p ▹ u.2 ≈ v.2)
-      :  dpair (path_sigma_uncurried pq)..1 (path_sigma_uncurried pq)..2 ≈ pq :=
+      :  dpair (sigma_path_uncurried pq)..1 (sigma_path_uncurried pq)..2 ≈ pq :=
-  destruct pq dpair_path_sigma
+  destruct pq dpair_sigma_path
 
-  definition pr1_path_sigma_uncurried (pq : Σ(p : u.1 ≈ v.1), p ▹ u.2 ≈ v.2)
+  definition sigma_path_pr1_uncurried (pq : Σ(p : u.1 ≈ v.1), p ▹ u.2 ≈ v.2)
-      : (path_sigma_uncurried pq)..1 ≈ pq.1 :=
+      : (sigma_path_uncurried pq)..1 ≈ pq.1 :=
-  (!dpair_path_sigma_uncurried)..1
+  (!dpair_sigma_path_uncurried)..1
 
-  definition pr2_path_sigma_uncurried (pq : Σ(p : u.1 ≈ v.1), p ▹ u.2 ≈ v.2)
+  definition sigma_path_pr2_uncurried (pq : Σ(p : u.1 ≈ v.1), p ▹ u.2 ≈ v.2)
-      : (pr1_path_sigma_uncurried pq) ▹ (path_sigma_uncurried pq)..2 ≈ pq.2 :=
+      : (sigma_path_pr1_uncurried pq) ▹ (sigma_path_uncurried pq)..2 ≈ pq.2 :=
-  (!dpair_path_sigma_uncurried)..2
+  (!dpair_sigma_path_uncurried)..2
 
-  definition eta_path_sigma_uncurried (p : u ≈ v) : path_sigma_uncurried (dpair p..1 p..2) ≈ p :=
+  definition sigma_path_eta_uncurried (p : u ≈ v) : sigma_path_uncurried (dpair p..1 p..2) ≈ p :=
-  !eta_path_sigma
+  !sigma_path_eta
 
-  definition transport_pr1_path_sigma_uncurried {B' : A → Type} (pq : Σ(p : u.1 ≈ v.1), p ▹ u.2 ≈ v.2)
+  definition transport_sigma_path_dpr1_uncurried {B' : A → Type}
-      : transport (λx, B' x.1) (@path_sigma_uncurried A B u v pq) ≈ transport B' pq.1 :=
+    (pq : Σ(p : u.1 ≈ v.1), p ▹ u.2 ≈ v.2)
-    destruct pq transport_pr1_path_sigma
+      : transport (λx, B' x.1) (@sigma_path_uncurried A B u v pq) ≈ transport B' pq.1 :=
+  destruct pq transport_dpr1_sigma_path
 
-  definition isequiv_path_sigma /-[instance]-/ (u v : Σa, B a)
+  definition is_equiv_sigma_path [instance] (u v : Σa, B a)
-      : is_equiv (@path_sigma_uncurried A B u v) :=
+      : is_equiv (@sigma_path_uncurried A B u v) :=
-  adjointify path_sigma_uncurried
+  adjointify sigma_path_uncurried
              (λp, ⟨p..1, p..2⟩)
-             eta_path_sigma_uncurried
+             sigma_path_eta_uncurried
-             dpair_path_sigma_uncurried
+             dpair_sigma_path_uncurried
 
-  definition equiv_path_sigma (u v : Σa, B a) : (Σ(p : u.1 ≈ v.1),  p ▹ u.2 ≈ v.2) ≃ (u ≈ v) :=
+  definition equiv_sigma_path (u v : Σa, B a) : (Σ(p : u.1 ≈ v.1),  p ▹ u.2 ≈ v.2) ≃ (u ≈ v) :=
-    equiv.mk path_sigma_uncurried !isequiv_path_sigma
+  equiv.mk sigma_path_uncurried !is_equiv_sigma_path
 
-  definition path_sigma_dpair_pp_pp (p1 : a  ≈ a' ) (q1 : p1 ▹ b  ≈ b' )
+  definition dpair_eq_dpair_pp_pp (p1 : a  ≈ a' ) (q1 : p1 ▹ b  ≈ b' )
-                                    (p2 : a' ≈ a'') (q2 : p2 ▹ b' ≈ b'') :
+                                  (p2 : a' ≈ a'') (q2 : p2 ▹ b' ≈ b'') :
-      path_sigma_dpair (p1 ⬝ p2) (transport_pp B p1 p2 b ⬝ ap (transport B p2) q1 ⬝ q2)
+      dpair_eq_dpair (p1 ⬝ p2) (transport_pp B p1 p2 b ⬝ ap (transport B p2) q1 ⬝ q2)
-    ≈ path_sigma_dpair p1 q1 ⬝ path_sigma_dpair  p2 q2 :=
+    ≈ dpair_eq_dpair p1 q1 ⬝ dpair_eq_dpair  p2 q2 :=
   begin
-    generalize q2, generalize q1, generalize b'', generalize p2, generalize b',
+    reverts (b', p2, b'', q1, q2),
     apply (path.rec_on p1), intros (b', p2),
     apply (path.rec_on p2), intros (b'', q1),
     apply (path.rec_on q1), intro q2,
     apply (path.rec_on q2), apply idp
   end
 
-  definition path_sigma_pp_pp (p1 : u.1 ≈ v.1) (q1 : p1 ▹ u.2 ≈ v.2)
+  definition sigma_path_pp_pp (p1 : u.1 ≈ v.1) (q1 : p1 ▹ u.2 ≈ v.2)
                               (p2 : v.1 ≈ w.1) (q2 : p2 ▹ v.2 ≈ w.2) :
-      path_sigma (p1 ⬝ p2) (transport_pp B p1 p2 u.2 ⬝ ap (transport B p2) q1 ⬝ q2)
+      sigma.path (p1 ⬝ p2) (transport_pp B p1 p2 u.2 ⬝ ap (transport B p2) q1 ⬝ q2)
-    ≈ path_sigma p1 q1 ⬝ path_sigma p2 q2 :=
+    ≈ sigma.path p1 q1 ⬝ sigma.path p2 q2 :=
   begin
-    generalize q2, generalize p2, generalize q1, generalize p1,
+    reverts (p1, q1, p2, q2),
     apply (destruct u), intros (u1, u2),
     apply (destruct v), intros (v1, v2),
     apply (destruct w), intros,
-    apply path_sigma_dpair_pp_pp
+    apply dpair_eq_dpair_pp_pp
   end
 
-  definition path_sigma_dpair_p1_1p (p : a ≈ a') (q : p ▹ b ≈ b') :
+  definition dpair_eq_dpair_p1_1p (p : a ≈ a') (q : p ▹ b ≈ b') :
-      path_sigma_dpair p q ≈ path_sigma_dpair p idp ⬝ path_sigma_dpair idp q :=
+      dpair_eq_dpair p q ≈ dpair_eq_dpair p idp ⬝ dpair_eq_dpair idp q :=
   begin
-    generalize q, generalize b',
+    reverts (b', q),
     apply (path.rec_on p), intros (b', q),
     apply (path.rec_on q), apply idp
   end
 
-  /- pr1_path commutes with the groupoid structure. -/
+  /- path_pr1 commutes with the groupoid structure. -/
 
-  definition pr1_path_1  (u : Σa, B a)           : (idpath u)..1 ≈ idpath (u.1)    := idp
+  definition path_pr1_idp (u : Σa, B a)           : (idpath u)..1 ≈ idpath (u.1)    := idp
-  definition pr1_path_pp (p : u ≈ v) (q : v ≈ w) : (p ⬝ q)   ..1 ≈ (p..1) ⬝ (q..1) := !ap_pp
+  definition path_pr1_pp  (p : u ≈ v) (q : v ≈ w) : (p ⬝ q)   ..1 ≈ (p..1) ⬝ (q..1) := !ap_pp
-  definition pr1_path_V  (p : u ≈ v)             : p⁻¹       ..1 ≈ (p..1)⁻¹        := !ap_V
+  definition path_pr1_V   (p : u ≈ v)             : p⁻¹       ..1 ≈ (p..1)⁻¹        := !ap_V
 
-  /- Applying dpair to one argument is the same as path_sigma_dpair with reflexivity in the first place. -/
+  /- Applying dpair to one argument is the same as dpair_eq_dpair with reflexivity in the first place. -/
 
-  definition ap_dpair (q : b₁ ≈ b₂) : ap (dpair a) q ≈ path_sigma_dpair idp q :=
+  definition ap_dpair (q : b₁ ≈ b₂) : ap (dpair a) q ≈ dpair_eq_dpair idp q :=
   path.rec_on q idp
 
-  /- Dependent transport is the same as transport along a path_sigma. -/
+  /- Dependent transport is the same as transport along a sigma_path. -/
 
-  definition transportD_is_transport (p : a ≈ a') (c : C a b) :
+  definition transportD_eq_transport (p : a ≈ a') (c : C a b) :
-      p ▹D c ≈ transport (λu, C (u.1) (u.2)) (path_sigma_dpair p idp) c :=
+      p ▹D c ≈ transport (λu, C (u.1) (u.2)) (dpair_eq_dpair p idp) c :=
   path.rec_on p idp
 
-  definition path_path_sigma_path_sigma {p1 q1 : a ≈ a'} {p2 : p1 ▹ b ≈ b'} {q2 : q1 ▹ b ≈ b'}
+  definition sigma_path_eq_sigma_path {p1 q1 : a ≈ a'} {p2 : p1 ▹ b ≈ b'} {q2 : q1 ▹ b ≈ b'}
-      (r : p1 ≈ q1) (s : r ▹ p2 ≈ q2) : path_sigma p1 p2 ≈ path_sigma q1 q2 :=
+      (r : p1 ≈ q1) (s : r ▹ p2 ≈ q2) : sigma.path p1 p2 ≈ sigma.path q1 q2 :=
   path.rec_on r
               proof (λq2 s, path.rec_on s idp) qed
               q2
               s
   -- begin
-  --   generalize s, generalize q2,
+  --   reverts (q2, s),
   --   apply (path.rec_on r), intros (q2, s),
   --   apply (path.rec_on s), apply idp
   -- end
 
 
   /- A path between paths in a total space is commonly shown component wise. -/
-  definition path_path_sigma {p q : u ≈ v} (r : p..1 ≈ q..1) (s : r ▹ p..2 ≈ q..2) : p ≈ q :=
+  definition path_sigma_path {p q : u ≈ v} (r : p..1 ≈ q..1) (s : r ▹ p..2 ≈ q..2) : p ≈ q :=
   begin
-    generalize s, generalize r, generalize q,
+    reverts (q, r, s),
     apply (path.rec_on p),
     apply (destruct u), intros (u1, u2, q, r, s),
     apply concat, rotate 1,
-    apply eta_path_sigma,
+    apply sigma_path_eta,
-    apply (path_path_sigma_path_sigma r s)
+    apply (sigma_path_eq_sigma_path r s)
   end
 
-
   /- In Coq they often have to give u and v explicitly when using the following definition -/
-  definition path_path_sigma_uncurried {p q : u ≈ v}
+  definition path_sigma_path_uncurried {p q : u ≈ v}
       (rs : Σ(r : p..1 ≈ q..1), transport (λx, transport B x u.2 ≈ v.2) r p..2 ≈ q..2) : p ≈ q :=
-  destruct rs path_path_sigma
+  destruct rs path_sigma_path
 
   /- Transport -/
 
@@ -201,8 +202,8 @@ 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_sigma (p : a ≈ a') (bc : Σ(b : B a), C a b) : p ▹ bc ≈ ⟨p ▹ bc.1, p ▹D bc.2⟩
+  definition transport_eq (p : a ≈ a') (bc : Σ(b : B a), C a b)
-  :=
+      : p ▹ bc ≈ ⟨p ▹ bc.1, p ▹D bc.2⟩ :=
   begin
     apply (path.rec_on p),
     apply (destruct bc), intros (b, c),
@@ -210,7 +211,7 @@ namespace sigma
   end
 
   /- The special case when the second variable doesn't depend on the first is simpler. -/
-  definition transport_sigma' {B : Type} {C : A → B → Type} (p : a ≈ a') (bc : Σ(b : B), C a b)
+  definition transport_eq_deg {B : Type} {C : A → B → Type} (p : a ≈ a') (bc : Σ(b : B), C a b)
       : p ▹ bc ≈ ⟨bc.1, p ▹ bc.2⟩ :=
   begin
     apply (path.rec_on p),
@@ -218,12 +219,12 @@ namespace sigma
     apply idp
   end
 
-  /- Or if the second variable contains a first component that doesn't depend on the first.  Need to think about the naming of these. -/
+  /- Or if the second variable contains a first component that doesn't depend on the first. -/
 
-  definition transport_sigma_' {C : A → Type} {D : Π a:A, B a → C a → Type} (p : a ≈ a')
+  definition transport_eq_4deg {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
-    generalize bcd,
+    revert bcd,
     apply (path.rec_on p), intro bcd,
     apply (destruct bcd), intros (b, cd),
     apply (destruct cd), intros (c, d),
@@ -233,58 +234,117 @@ namespace sigma
   /- Functorial action -/
   variables (f : A → A') (g : Πa, B a → B' (f a))
 
-  definition functor_sigma (u : Σa, B a) : Σa', B' a' :=
+  protected definition functor (u : Σa, B a) : Σa', B' a' :=
   ⟨f u.1, g u.1 u.2⟩
 
   /- Equivalences -/
 
-  --remove explicit arguments of IsEquiv
+  --TODO: remove explicit arguments of is_equiv
-  definition isequiv_functor_sigma [H1 : is_equiv f] [H2 : Π a, @is_equiv (B a) (B' (f a)) (g a)]
+  definition is_equiv_functor [H1 : is_equiv f] [H2 : Π a, is_equiv (g a)]
-      : is_equiv (functor_sigma f g) :=
+      : is_equiv (functor f g) :=
-  /-adjointify (functor_sigma f g)
+  adjointify (functor f g)
-             (functor_sigma (f⁻¹) (λ(x : A') (y : B' x), ((g (f⁻¹ x))⁻¹ ((retr f x)⁻¹ ▹ y))))
+             (functor (f⁻¹) (λ(a' : A') (b' : B' a'),
-             sorry-/
+               ((g (f⁻¹ a'))⁻¹ (transport B' (retr f a'⁻¹) b'))))
-             sorry
+  begin
+    intro u',
+    apply (destruct u'), intros (a', b'),
+    apply (sigma.path (retr f a')),
+    -- "rewrite retr (g (f⁻¹ a'))"
+    apply concat, apply (ap (λx, (transport B' (retr f a') x))), apply (retr (g (f⁻¹ a'))),
+    show retr f a' ▹ (((retr f a') ⁻¹) ▹ b') ≈ b',
+    from transport_pV B' (retr f a') b'
+  end
+  begin
+    intro u,
+    apply (destruct u), intros (a, b),
+    apply (sigma.path (sect f a)),
+    show transport B (sect f a) (g (f⁻¹ (f a))⁻¹ (transport B' (retr f (f a)⁻¹) (g a b))) ≈ b,
+    from calc
+      transport B (sect f a) (g (f⁻¹ (f a))⁻¹ (transport B' (retr f (f a)⁻¹) (g a b)))
+          ≈ g a⁻¹ (transport (B' ∘ f) (sect f a) (transport B' (retr f (f a)⁻¹) (g a b)))
+              : ap_transport (sect f a) (λ a, g a⁻¹)
+      ... ≈ g a⁻¹ (transport B' (ap f (sect f a)) (transport B' (retr f (f a)⁻¹) (g a b)))
+              : ap (g a⁻¹) !transport_compose
+      ... ≈ g a⁻¹ (transport B' (ap f (sect f a)) (transport B' (ap f (sect f a)⁻¹) (g a b)))
+           : ap (λ x, g a⁻¹ (transport B' (ap f (sect f a)) (transport B' (x⁻¹) (g a b)))) (adj f a)
+      ... ≈ g a⁻¹ (g a b) : transport_pV
+      ... ≈ b : sect (g a) b
+  end
+    -- -- "rewrite ap_transport"
+    -- apply concat, apply inverse, apply (ap_transport (sect f a) (λ a, g a⁻¹)),
+    -- apply concat, apply (ap (g a⁻¹)),
+    --   -- "rewrite transport_compose"
+    --   apply concat, apply transport_compose,
+    --   -- "rewrite adj"
+    --   -- "rewrite transport_pV"
+    -- apply sect,
 
-  definition equiv_functor_sigma [H1 : is_equiv f] [H2 : Π a, is_equiv (g a)] : (Σa, B a) ≃ (Σa', B' a') :=
+  definition equiv_functor_of_is_equiv [H1 : is_equiv f] [H2 : Π a, is_equiv (g a)]
-  equiv.mk (functor_sigma f g) !isequiv_functor_sigma
+    : (Σa, B a) ≃ (Σa', B' a') :=
+  equiv.mk (functor f g) !is_equiv_functor
 
   context --remove
   irreducible inv function.compose --remove
-  definition equiv_functor_sigma' (Hf : A ≃ A') (Hg : Π a, B a ≃ B' (to_fun Hf a)) :
+  definition equiv_functor (Hf : A ≃ A') (Hg : Π a, B a ≃ B' (to_fun Hf a)) :
       (Σa, B a) ≃ (Σa', B' a') :=
-  equiv_functor_sigma (to_fun Hf) (λ a, to_fun (Hg a))
+  equiv_functor_of_is_equiv (to_fun Hf) (λ a, to_fun (Hg a))
   end --remove
 
+  definition equiv_functor_id {B' : A → Type} (Hg : Π a, B a ≃ B' a) : (Σa, B a) ≃ Σa, B' a :=
+  equiv_functor equiv.refl Hg
+
+  definition ap_functor_sigma_dpair (p : a ≈ a') (q : p ▹ b ≈ b')
+    : ap (sigma.functor f g) (sigma.path p q)
+    ≈ sigma.path (ap f p)
+                 (transport_compose _ f p (g a b)⁻¹ ⬝ ap_transport p g b⁻¹ ⬝ ap (g a') q) :=
+  begin
+    reverts (b', q),
+    apply (path.rec_on p),
+    intros (b', q), apply (path.rec_on q),
+    apply idp
+  end
+
+  definition ap_functor_sigma (p : u.1 ≈ v.1) (q : p ▹ u.2 ≈ v.2)
+    : ap (sigma.functor f g) (sigma.path p q)
+    ≈ sigma.path (ap f p)
+                 (transport_compose B' f p (g u.1 u.2)⁻¹ ⬝ ap_transport p g u.2⁻¹ ⬝ ap (g v.1) q) :=
+  begin
+    reverts (p, q),
+    apply (destruct u), intros (a, b),
+    apply (destruct v), intros (a', b', p, q),
+    apply ap_functor_sigma_dpair
+  end
+
   /- definition 3.11.9(i): Summing up a contractible family of types does nothing. -/
   open truncation
-  definition isequiv_pr1_contr [instance] (B : A → Type) [H : Π a, is_contr (B a)]
+  definition is_equiv_dpr1 [instance] (B : A → Type) [H : Π a, is_contr (B a)]
       : is_equiv (@dpr1 A B) :=
   adjointify dpr1
              (λa, ⟨a, !center⟩)
              (λa, idp)
-             (λu, path_sigma idp !contr)
+             (λu, sigma.path idp !contr)
 
-  definition equiv_sigma_contr [H : Π a, is_contr (B a)] : (Σa, B a) ≃ A :=
+  definition equiv_of_all_contr [H : Π a, is_contr (B a)] : (Σa, B a) ≃ A :=
   equiv.mk dpr1 _
 
   /- definition 3.11.9(ii): Dually, summing up over a contractible type does nothing. -/
 
-  definition equiv_contr_sigma (B : A → Type) [H : is_contr A] : (Σa, B a) ≃ B (center A) :=
+  definition equiv_center_of_contr (B : A → Type) [H : is_contr A] : (Σa, B a) ≃ B (center A)
+  :=
   equiv.mk _ (adjointify
     (λu, contr u.1⁻¹ ▹ u.2)
     (λb, ⟨!center, b⟩)
     (λb, ap (λx, x ▹ b) !path2_contr)
-    (λu, path_sigma !contr !transport_pV))
+    (λu, sigma.path !contr !transport_pV))
 
   /- Associativity -/
 
-  --this proof is harder here than in Coq because we don't have eta definitionally for sigma
+  --this proof is harder than in Coq because we don't have eta definitionally for sigma
-  definition equiv_sigma_assoc (C : (Σa, B a) → Type) : (Σa b, C ⟨a,b⟩) ≃ (Σu, C u) :=
+  protected definition assoc_equiv (C : (Σa, B a) → Type) : (Σa b, C ⟨a, b⟩) ≃ (Σu, C u) :=
   -- begin
-  --   apply Equiv.mk,
+  --   apply equiv.mk,
   --   apply (adjointify (λav, ⟨⟨av.1, av.2.1⟩, av.2.2⟩)
-  --                     (λuc, ⟨uc.1.1, uc.1.2, !eta_sigma⁻¹ ▹ uc.2⟩)),
+  --                     (λuc, ⟨uc.1.1, uc.1.2, !peta⁻¹ ▹ uc.2⟩)),
   --     intro uc, apply (destruct uc), intro u,
   --               apply (destruct u), intros (a, b, c),
   --               apply idp,
@@ -294,64 +354,121 @@ namespace sigma
   -- end
   equiv.mk _ (adjointify
     (λav, ⟨⟨av.1, av.2.1⟩, av.2.2⟩)
-    (λuc, ⟨uc.1.1, uc.1.2, !eta_sigma⁻¹ ▹ uc.2⟩)
+    (λuc, ⟨uc.1.1, uc.1.2, !peta⁻¹ ▹ uc.2⟩)
     proof (λuc, destruct uc (λu, destruct u (λa b c, idp))) qed
     proof (λav, destruct av (λa v, destruct v (λb c, idp))) qed)
 
   open prod
-  definition equiv_sigma_prod (C : (A × A') → Type) : (Σa a', C (a,a')) ≃ (Σu, C u) :=
+  definition assoc_equiv_prod (C : (A × A') → Type) : (Σa a', C (a,a')) ≃ (Σu, C u) :=
   equiv.mk _ (adjointify
     (λav, ⟨(av.1, av.2.1), av.2.2⟩)
-    (λuc, ⟨pr₁ (uc.1), pr₂ (uc.1), !eta_prod⁻¹ ▹ uc.2⟩)
+    (λuc, ⟨pr₁ (uc.1), pr₂ (uc.1), !prod.peta⁻¹ ▹ uc.2⟩)
     proof (λuc, destruct uc (λu, prod.destruct u (λa b c, idp))) qed
     proof (λav, destruct av (λa v, destruct v (λb c, idp))) qed)
 
-
   /- Symmetry -/
-  -- if this breaks, replace "Equiv.id" by "proof Equiv.id qed"
+  definition symm_equiv_uncurried (C : A × A' → Type) : (Σa a', C (a, a')) ≃ (Σa' a, C (a, a')) :=
-  definition equiv_sigma_symm_prod (C : A × A' → Type) : (Σa a', C (a, a')) ≃ (Σa' a, C (a, a')) :=
   calc
-    (Σa a', C (a, a')) ≃ Σu, C u : equiv_sigma_prod
+    (Σa a', C (a, a')) ≃ Σu, C u : assoc_equiv_prod
-                 ... ≃ Σv, C (flip v) : equiv_functor_sigma' !equiv_prod_symm
+                 ... ≃ Σv, C (flip v) : equiv_functor !prod.symm_equiv
                                           (λu, prod.destruct u (λa a', equiv.refl))
-                 ... ≃ (Σa' a, C (a, a')) : equiv_sigma_prod
+                 ... ≃ (Σa' a, C (a, a')) : assoc_equiv_prod
 
-  definition equiv_sigma_symm (C : A → A' → Type) : (Σa a', C a a') ≃ (Σa' a, C a a') :=
+  definition symm_equiv (C : A → A' → Type) : (Σa a', C a a') ≃ (Σa' a, C a a') :=
-  sigma.equiv_sigma_symm_prod (λu, C (pr1 u) (pr2 u))
+  symm_equiv_uncurried (λu, C (pr1 u) (pr2 u))
 
-  definition equiv_sigma0_prod (A B : Type) : (Σ(a : A), B) ≃ A × B :=
+  definition equiv_prod (A B : Type) : (Σ(a : A), B) ≃ A × B :=
   equiv.mk _ (adjointify
     (λs, (s.1, s.2))
     (λp, ⟨pr₁ p, pr₂ p⟩)
     proof (λp, prod.destruct p (λa b, idp)) qed
     proof (λs, destruct s (λa b, idp)) qed)
 
-  definition equiv_sigma_symm0 (A B : Type) : (Σ(a : A), B) ≃ Σ(b : B), A :=
+  definition symm_equiv_deg (A B : Type) : (Σ(a : A), B) ≃ Σ(b : B), A :=
   calc
-    (Σ(a : A), B) ≃ A × B : equiv_sigma0_prod
+    (Σ(a : A), B) ≃ A × B : equiv_prod
-              ... ≃ B × A : equiv_prod_symm
+              ... ≃ B × A : prod.symm_equiv
-              ... ≃ Σ(b : B), A : equiv_sigma0_prod
+              ... ≃ Σ(b : B), A : equiv_prod
+
+  /- ** Universal mapping properties -/
+  /- *** The positive universal property. -/
+
+  section
+  open funext
+  --in Coq this can be done without function extensionality
+  definition is_equiv_sigma_rec [instance] [FUN : funext] (C : (Σa, B a) → Type)
+    : is_equiv (@sigma.rec _ _ C) :=
+  adjointify _ (λ g a b, g ⟨a, b⟩)
+               (λ g, proof path_pi (λu, destruct u (λa b, idp)) qed)
+               (λ f, idpath f)
+
+  definition equiv_sigma_rec [FUN : funext] (C : (Σa, B a) → Type)
+    : (Π(a : A) (b: B a), C ⟨a, b⟩) ≃ (Πxy, C xy) :=
+  equiv.mk sigma.rec _
+
+  /- *** The negative universal property. -/
+
+  definition coind_uncurried (fg : Σ(f : Πa, B a), Πa, C a (f a)) (a : A) : Σ(b : B a), C a b
+  := ⟨fg.1 a, fg.2 a⟩
+
+  definition coind (f : Π a, B a) (g : Π a, C a (f a)) (a : A) : Σ(b : B a), C a b :=
+  coind_uncurried ⟨f, g⟩ a
+
+  --is the instance below dangerous?
+  --in Coq this can be done without function extensionality
+  definition is_equiv_coind [instance] [FUN : funext] (C : Πa, B a → Type)
+    : is_equiv (@coind_uncurried _ _ C) :=
+  adjointify _ (λ h, ⟨λa, (h a).1, λa, (h a).2⟩)
+               (λ h, proof path_pi (λu, !peta) qed)
+               (λfg, destruct fg (λ(f : Π (a : A), B a) (g : Π (x : A), C x (f x)), proof idp qed))
+
+  definition equiv_coind [FUN : funext] : (Σ(f : Πa, B a), Πa, C a (f a)) ≃ (Πa, Σb, C a b) :=
+  equiv.mk coind_uncurried _
+  end
+
+  /- ** Subtypes (sigma types whose second components are hprops) -/
+
+  /- To prove equality in a subtype, we only need equality of the first component. -/
+  definition path_hprop [H : Πa, is_hprop (B a)] (u v : Σa, B a) : u.1 ≈ v.1 → u ≈ v :=
+  (sigma_path_uncurried ∘ (@inv _ _ dpr1 (@is_equiv_dpr1 _ _ (λp, !succ_is_trunc))))
+
+  definition is_equiv_path_hprop [instance] [H : Πa, is_hprop (B a)] (u v : Σa, B a)
+      : is_equiv (path_hprop u v) :=
+  !is_equiv.compose
+
+  definition equiv_path_hprop [H : Πa, is_hprop (B a)] (u v : Σa, B a) : (u.1 ≈ v.1) ≃ (u ≈ v)
+  :=
+  equiv.mk !path_hprop _
 
   /- truncatedness -/
   definition trunc_sigma [instance] (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
+  begin
   reverts (A, B, HA, HB),
-  apply (truncation.trunc_index.rec_on n),
+  apply (trunc_index.rec_on n),
     intros (A, B, HA, HB),
       fapply trunc_equiv',
         apply equiv.symm,
-          apply equiv_contr_sigma, apply HA, --should be solved by term synthesis
+          apply equiv_center_of_contr, apply HA, --should be solved by term synthesis
         apply HB,
      intros (n, IH, A, B, HA, HB),
        fapply is_trunc_succ, intros (u, v),
       fapply trunc_equiv',
-         apply equiv_path_sigma,
+         apply equiv_sigma_path,
          apply IH,
-           apply (succ_is_trunc n),
+           apply succ_is_trunc, assumption,
            intro p,
              show is_trunc n (p ▹ u .2 ≈ v .2), from
              succ_is_trunc n (p ▹ u.2) (v.2),
-end
+  end
 
 end sigma
+
+open truncation sigma
+
+namespace prod
+  /- truncatedness -/
+  definition trunc_prod [instance] (A B : Type) (n : trunc_index)
+      [HA : is_trunc n A] [HB : is_trunc n B] : is_trunc n (A × B) :=
+  trunc_equiv' n !equiv_prod
+end prod