fix(hott): abstract some equivalence proofs

Note: this is important. I proved a quite complicated equivalence with calc, by chaining these
equivalences. Now if I want to know the underlying function of this composite equivalence, I have to
unfold all these instances. Without the abstracts, this took 14 seconds, and afterwards, it took 2
seconds.

hott/init/equiv.hlean

@@ -48,16 +48,15 @@ namespace is_equiv
   definition is_equiv_compose [constructor] [Hf : is_equiv f] [Hg : is_equiv g]
     : is_equiv (g ∘ f) :=
   is_equiv.mk (g ∘ f) (f⁻¹ ∘ g⁻¹)
-             (λc, ap g (right_inv f (g⁻¹ c)) ⬝ right_inv g c)
+             abstract (λc, ap g (right_inv f (g⁻¹ c)) ⬝ right_inv g c) end
-             (λa, ap (inv f) (left_inv g (f a)) ⬝ left_inv f a)
+             abstract (λa, ap (inv f) (left_inv g (f a)) ⬝ left_inv f a) end
-             (λa, (whisker_left _ (adj g (f a))) ⬝
+             abstract (λa, (whisker_left _ (adj g (f a))) ⬝
                   (ap_con g _ _)⁻¹ ⬝
                   ap02 g ((ap_con_eq_con (right_inv f) (left_inv g (f a)))⁻¹ ⬝
                           (ap_compose f (inv f) _ ◾  adj f a) ⬝
                           (ap_con f _ _)⁻¹
                          ) ⬝
-                  (ap_compose g f _)⁻¹
+                  (ap_compose g f _)⁻¹) end
-             )
 
   -- Any function equal to an equivalence is an equivlance as well.
   variable {f}
@@ -103,7 +102,7 @@ namespace is_equiv
   eq4
 
   definition adjointify [constructor] : is_equiv f :=
-  is_equiv.mk f g ret adjointify_left_inv' adjointify_adj'
+  is_equiv.mk f g ret abstract adjointify_left_inv' end adjointify_adj'
   end
 
   -- Any function pointwise equal to an equivalence is an equivalence as well.

hott/types/eq.hlean

@@ -233,7 +233,7 @@ namespace eq
   is_equiv.mk (concat p) (concat p⁻¹)
               (con_inv_cancel_left p)
               (inv_con_cancel_left p)
-              (λq, by induction p;induction q;reflexivity)
+              abstract (λq, by induction p;induction q;reflexivity) end
   local attribute is_equiv_concat_left [instance]
 
   definition equiv_eq_closed_left [constructor] (a₃ : A) (p : a₁ = a₂) : (a₁ = a₃) ≃ (a₂ = a₃) :=

hott/types/fiber.hlean

@@ -24,8 +24,8 @@ namespace fiber
   fapply equiv.MK,
     {intro x, exact ⟨point x, point_eq x⟩},
     {intro x, exact (fiber.mk x.1 x.2)},
-    {intro x, cases x, apply idp},
+    {intro x, exact abstract begin cases x, apply idp end end},
-    {intro x, cases x, apply idp},
+    {intro x, exact abstract begin cases x, apply idp end end},
   end
 
   definition fiber_eq_equiv (x y : fiber f b)

hott/types/sigma.hlean

@@ -219,20 +219,20 @@ namespace sigma
   adjointify (sigma_functor f g)
              (sigma_functor f⁻¹ (λ(a' : A') (b' : B' a'),
                ((g (f⁻¹ a'))⁻¹ (transport B' (right_inv f a')⁻¹ b'))))
-  begin
+  abstract begin
     intro u', induction u' with a' b',
     apply sigma_eq (right_inv f a'),
     rewrite [▸*,right_inv (g (f⁻¹ a')),▸*],
     apply tr_pathover
-  end
+  end end
-  begin
+  abstract begin
     intro u,
     induction u with a b,
     apply (sigma_eq (left_inv f a)),
     apply pathover_of_tr_eq,
     rewrite [▸*,adj f,-(fn_tr_eq_tr_fn (left_inv f a) (λ a, (g a)⁻¹)),
              ▸*,tr_compose B' f,tr_inv_tr,left_inv]
-  end
+  end end
 
   definition sigma_equiv_sigma_of_is_equiv [constructor]
     [H1 : is_equiv f] [H2 : Π a, is_equiv (g a)] : (Σa, B a) ≃ (Σa', B' a') :=
@@ -280,8 +280,8 @@ namespace sigma
   equiv.MK
     (λu, (center_eq u.1)⁻¹ ▸ u.2)
     (λb, ⟨!center, b⟩)
-    (λb, ap (λx, x ▸ b) !hprop_eq_of_is_contr)
+    abstract (λb, ap (λx, x ▸ b) !hprop_eq_of_is_contr) end
-    (λu, sigma_eq !center_eq !tr_pathover)
+    abstract (λu, sigma_eq !center_eq !tr_pathover) end
 
   /- Associativity -/
 
@@ -291,16 +291,16 @@ namespace sigma
   equiv.mk _ (adjointify
     (λav, ⟨⟨av.1, av.2.1⟩, av.2.2⟩)
     (λuc, ⟨uc.1.1, uc.1.2, !sigma.eta⁻¹ ▸ uc.2⟩)
-    begin intro uc, induction uc with u c, induction u, reflexivity end
+    abstract begin intro uc, induction uc with u c, induction u, reflexivity end end
-    begin intro av, induction av with a v, induction v, reflexivity end)
+    abstract begin intro av, induction av with a v, induction v, reflexivity end end)
 
   open prod prod.ops
   definition assoc_equiv_prod [constructor] (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), !prod.eta⁻¹ ▸ uc.2⟩)
-    proof (λuc, destruct uc (λu, prod.destruct u (λa b c, idp))) qed
+    abstract proof (λuc, destruct uc (λu, prod.destruct u (λa b c, idp))) qed end
-    proof (λav, destruct av (λa v, destruct v (λb c, idp))) qed)
+    abstract proof (λav, destruct av (λa v, destruct v (λb c, idp))) qed end)
 
   /- Symmetry -/