style(hott/types): some style fixes in prod and sigma

library/hott/types/sigma.lean

@@ -11,7 +11,6 @@ import ..trunc .prod
 open path sigma sigma.ops equiv is_equiv
 
 namespace sigma
-  -- remove the ₁'s (globally)
   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}
@@ -51,9 +50,9 @@ namespace sigma
   definition dpair_path_sigma (p : u.1 ≈ v.1) (q : p ▹ u.2 ≈ v.2)
       :  dpair (path_sigma p q)..1 (path_sigma 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
@@ -75,7 +74,7 @@ namespace sigma
   definition transport_pr1_path_sigma {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 :=
   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),
@@ -121,7 +120,7 @@ namespace sigma
       path_sigma_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 :=
   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,
@@ -133,7 +132,7 @@ namespace sigma
       path_sigma (p1 ⬝ p2) (transport_pp B p1 p2 u.2 ⬝ ap (transport B p2) q1 ⬝ q2)
     ≈ path_sigma p1 q1 ⬝ path_sigma 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,
@@ -143,7 +142,7 @@ namespace sigma
   definition path_sigma_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 :=
   begin
-    generalize q, generalize b',
+    reverts (b', q),
     apply (path.rec_on p), intros (b', q),
     apply (path.rec_on q), apply idp
   end
@@ -172,7 +171,7 @@ namespace sigma
               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
@@ -181,7 +180,7 @@ namespace sigma
   /- 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 :=
   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,
@@ -189,7 +188,6 @@ namespace sigma
     apply (path_path_sigma_path_sigma 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}
       (rs : Σ(r : p..1 ≈ q..1), transport (λx, transport B x u.2 ≈ v.2) r p..2 ≈ q..2) : p ≈ q :=
@@ -223,7 +221,7 @@ namespace sigma
   definition transport_sigma_' {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),
@@ -236,15 +234,35 @@ namespace sigma
   definition functor_sigma (u : Σa, B a) : Σa', B' a' :=
   ⟨f u.1, g u.1 u.2⟩
 
-  /- Equivalences -/
+  -- variables {A A' : Type} {B : A → Type} {B' : A' → Type} (f : A → A') (g : Πa, B a → B' (f a))
+  --           (H1 : is_equiv f) (H2 : Π (a : A), is_equiv (g a)) (u' : Σ (a' : A'), B' a')
+  --           (a' : A') (b' : B' a')
+  -- check retr f a' ▹ (g (f⁻¹ a') (g (f⁻¹ a')⁻¹ ((retr f a')⁻¹ ▹ b'))) ≈ b'
+  -- check retr f a' ▹ (g (f⁻¹ a') (g (f⁻¹ a')⁻¹ ((retr f a')⁻¹ ▹ b')))
+  -- check (g (f⁻¹ a') (g (f⁻¹ a')⁻¹ ((retr f a')⁻¹ ▹ b')))
+  -- check retr f a'
 
-  --remove explicit arguments of IsEquiv
+  /- Equivalences -/
+  irreducible inv --function.compose
+  --TODO: remove explicit arguments of IsEquiv
   definition isequiv_functor_sigma [H1 : is_equiv f] [H2 : Π a, @is_equiv (B a) (B' (f a)) (g a)]
       : is_equiv (functor_sigma f g) :=
-  /-adjointify (functor_sigma f g)
+  adjointify (functor_sigma f g)
-             (functor_sigma (f⁻¹) (λ(x : A') (y : B' x), ((g (f⁻¹ x))⁻¹ ((retr f x)⁻¹ ▹ y))))
+             (functor_sigma (f⁻¹) (λ(x : A') (y : B' x),
-             sorry-/
+               ((g (f⁻¹ x))⁻¹ (transport B' (retr f x)⁻¹ y))))
-             sorry
+  -- begin
+  --   intro u',
+  --   apply (destruct u'), intros (a', b'),
+  --   apply (path_sigma (retr f a')),
+  --   -- show retr f a' ▹ (g (f⁻¹ a') (g (f⁻¹ a')⁻¹ ((retr f a')⁻¹ ▹ b'))) ≈ b',
+  --   -- from sorry
+  --   -- exact (calc
+  --   --   retr f a' ▹ g (f⁻¹ a') (g (f⁻¹ a')⁻¹ ((retr f a')⁻¹ ▹ b'))
+  --   --          ≈ retr f a' ▹ ((retr f a')⁻¹ ▹ b') : {retr (g (f⁻¹ a')) _}
+  --   --      ... ≈ b' : transport_pV)
+  -- end
+             proof (λu', sorry) qed
+             proof (λu, sorry) qed
 
   definition equiv_functor_sigma [H1 : is_equiv f] [H2 : Π a, is_equiv (g a)] : (Σa, B a) ≃ (Σa', B' a') :=
   equiv.mk (functor_sigma f g) !isequiv_functor_sigma
@@ -333,25 +351,25 @@ namespace sigma
               ... ≃ Σ(b : B), A : equiv_sigma0_prod
 
   /- truncatedness -/
-  definition sigma_trunc (n : trunc_index) [HA : is_trunc n A] [HB : Πa, is_trunc n (B a)]
+  definition trunc_sigma [instance] (B : A → Type) (n : trunc_index)
-      : is_trunc n (Σa, B a) :=
+      [HA : is_trunc n A] [HB : Πa, is_trunc n (B a)] : is_trunc n (Σa, B a) :=
 begin
-  generalize HB, generalize HA, generalize B, generalize A,
+  reverts (A, B, HA, HB),
   apply (truncation.trunc_index.rec_on n),
     intros (A, B, HA, HB),
-      apply trunc_equiv',
+      fapply trunc_equiv',
         apply equiv.symm,
-          apply equiv_contr_sigma, apply HA,
+          apply equiv_contr_sigma, apply HA, --should be solved by term synthesis
         apply HB,
      intros (n, IH, A, B, HA, HB),
-       apply is_trunc_succ, intros (u, v),
+       fapply is_trunc_succ, intros (u, v),
-       apply trunc_equiv',
+      fapply trunc_equiv',
          apply equiv_path_sigma,
          apply IH,
            apply succ_is_trunc,
-           intro aa,
+           intro p,
-             show is_trunc n (aa ▹ u .2 ≈ v .2), from
+             show is_trunc n (p ▹ u .2 ≈ v .2), from
-             succ_is_trunc (aa ▹ u.2) (v.2),
+             succ_is_trunc (p ▹ u.2) (v.2),
 end
 
 end sigma