diff --git a/src/Bool.agda b/src/Bool.agda
index 25a0a7f..ff7c092 100644
--- a/src/Bool.agda
+++ b/src/Bool.agda
@@ -86,7 +86,7 @@ not≡↔≡not {false} {false} =

 -- Some lemmas related to T.

-T↔≡true : ∀ {b} → T b ↔ b ≡ true
+T↔≡true : {b : Bool} → T b ↔ b ≡ true
 T↔≡true {false} =   $⟨ Bool.true≢false ⟩
   true ≢ false      ↝⟨ (_∘ sym) ⟩
   false ≢ true      ↝⟨ Bijection.⊥↔uninhabited ⟩□
diff --git a/src/Equality.agda b/src/Equality.agda
index d45e369..8b74c2d 100644
--- a/src/Equality.agda
+++ b/src/Equality.agda
@@ -1590,7 +1590,7 @@ module Derived-definitions-and-properties
          trans (f≡g x px) (cong g (refl x))   ∎)
       _
       where
-      T-irr : ∀ b → Proof-irrelevant (T b)
+      T-irr : (b : Bool) → Proof-irrelevant (T b)
       T-irr true  _ _ = refl _
       T-irr false ()

diff --git a/src/H-level/Closure.agda b/src/H-level/Closure.agda
index 82ad340..8428906 100644
--- a/src/H-level/Closure.agda
+++ b/src/H-level/Closure.agda
@@ -625,7 +625,7 @@ abstract
     to : A ⊎ B → (∃ λ x → if x then ↑ b A else ↑ a B)
     to = [ _,_ true ∘ lift , _,_ false ∘ lift ]

-    from : (∃ λ x → if x then ↑ b A else ↑ a B) → A ⊎ B
+    from : (∃ {A = Bool} λ x → if x then ↑ b A else ↑ a B) → A ⊎ B
     from (true  , x) = inj₁ $ lower x
     from (false , y) = inj₂ $ lower y

@@ -665,7 +665,7 @@ abstract
     Bool-2+n : H-level (2 + n) Bool
     Bool-2+n = mono (m≤m+n 2 n) Bool-set

-    if-2+n : ∀ x → H-level (2 + n) (if x then ↑ b A else ↑ a B)
+    if-2+n : (x : Bool) → H-level (2 + n) (if x then ↑ b A else ↑ a B)
     if-2+n true  = respects-surjection
                      (_↔_.surjection $ Bijection.inverse ↑↔)
                      (2 + n) hA
diff --git a/src/Quotient.agda b/src/Quotient.agda
index a85dc73..4e1c09a 100644
--- a/src/Quotient.agda
+++ b/src/Quotient.agda
@@ -694,7 +694,8 @@ module _ {a} {A : Set a} {R : A → A → Set a} where
                                                                      inverse currying) (λ _ →
                                                              F.id) ⟩
     (∃ λ (f : (x : A) → (∃ λ P → R x ≡ P) → B) →
-       ∀ P → Constant (λ { (x , eq) → f x (P , eq) }))    ↝⟨ inverse $
+       ∀ P → Constant {A = ∃ λ x → R x ≡ P} (λ { (x , eq) → f x (P , eq) }))
+                                                          ↝⟨ inverse $
                                                              Σ-cong (Bij.inverse $
                                                                      ∀-cong (lower-extensionality _ _ ext) λ _ →
                                                                      drop-⊤-left-Π (lower-extensionality _ _ ext) $
diff --git a/src/Univalence-axiom/Isomorphism-is-equality/Simple.agda b/src/Univalence-axiom/Isomorphism-is-equality/Simple.agda
index d0a5eca..44b0377 100644
--- a/src/Univalence-axiom/Isomorphism-is-equality/Simple.agda
+++ b/src/Univalence-axiom/Isomorphism-is-equality/Simple.agda
@@ -291,7 +291,8 @@ module Class (Univ : Universe) where
                      eq)

         (Σ-map ≡⇒≃ f (Σ-≡,≡←≡ (proj₁ (Σ-≡,≡←≡ {A = ∃ (El a)}
-                        (cong (λ { (C , (x , p)) → (C , x) , p })
+                        (cong {A = ∃ λ _ → ∃ _}
+                              (λ { (C , (x , p)) → (C , x) , p })
                               (refl (C , x , p))))))               ≡⟨ cong (Σ-map ≡⇒≃ f ∘ Σ-≡,≡←≡ ∘ proj₁ ∘ Σ-≡,≡←≡) $
                                                                         cong-refl {A = Instance (a , P)}
                                                                                   (λ { (C , (x , p)) → (C , x) , p }) ⟩
@@ -1273,7 +1274,7 @@ private
                      +-comm *-comm *+ +0 *1 +- 0≢1 =
     _⇔_.from propositional⇔irrelevant irr
     where
-    irr : ∀ x y → x ≡ y
+    irr : (x y : ∃ λ _ → ∃ _) → x ≡ y
     irr (inv , inv₁ , inv₂) (inv′ , inv₁′ , inv₂′) =
       _↔_.to (ignore-propositional-component
                 (×-closure 1 (Π-closure ext 1 λ _ →

diff --git a/src/Lambda/Partiality-monad/Inductive/Interpreter.agda b/src/Lambda/Partiality-monad/Inductive/Interpreter.agda
index 441d226..47e589b 100644
--- a/src/Lambda/Partiality-monad/Inductive/Interpreter.agda
+++ b/src/Lambda/Partiality-monad/Inductive/Interpreter.agda
@@ -136,7 +136,7 @@ module Interpreter₂ where

   ⟦_⟧ : ∀ {n} → Tm n → Env n → M Value
   run (⟦ t ⟧ ρ) =
-    fixP (λ { (_ , t , ρ) → run (⟦ t ⟧′ ρ) }) (_ , t , ρ)
+    fixP {A = ∃ λ _ → ∃ _} (λ { (_ , t , ρ) → run (⟦ t ⟧′ ρ) }) (_ , t , ρ)

 ------------------------------------------------------------------------
 -- The two interpreters are pointwise equal

diff --git a/src/Bisimilarity/Classical.agda b/src/Bisimilarity/Classical.agda
index 98f9ec6..907cd71 100644
--- a/src/Bisimilarity/Classical.agda
+++ b/src/Bisimilarity/Classical.agda
@@ -175,15 +175,16 @@ transitive-∼ p∼q q∼r with _⇔_.to (Bisimilarity↔ _) p∼q
                         | _⇔_.to (Bisimilarity↔ _) q∼r
 ... | R₁ , R-is₁ , pR₁q | R₂ , R-is₂ , qR₂r =
   ⟨ R₁ ⊙ R₂
-  , ⟪ (λ { (q , pR₁q , qR₂r) p⟶p′ →
+  , ⟪_,_⟫
+      {R = λ _ → ∃ λ _ → ∃ _}
+      (λ { (q , pR₁q , qR₂r) p⟶p′ →
            let q′ , q⟶q′ , p′R₁q′ = left-to-right R-is₁ pR₁q p⟶p′
                r′ , r⟶r′ , q′R₂r′ = left-to-right R-is₂ qR₂r q⟶q′
            in r′ , r⟶r′ , (q′ , p′R₁q′ , q′R₂r′) })
-    , (λ { (q , pR₁q , qR₂r) r⟶r′ →
+      (λ { (q , pR₁q , qR₂r) r⟶r′ →
          let q′ , q⟶q′ , q′R₂r′ = right-to-left R-is₂ qR₂r r⟶r′
              p′ , p⟶p′ , p′R₁q′ = right-to-left R-is₁ pR₁q q⟶q′
          in p′ , p⟶p′ , (q′ , p′R₁q′ , q′R₂r′) })
-    ⟫
   , (_ , pR₁q , qR₂r)
   ⟩

@@ -240,7 +241,9 @@ bisimulation-up-to-∼⇒bisimulation :
   Bisimulation-up-to-bisimilarity R →
   Bisimulation (Bisimilarity ⊙ R ⊙ Bisimilarity)
 bisimulation-up-to-∼⇒bisimulation R-is =
-  ⟪ (λ { (q , p∼q , r , qRr , r∼s) p⟶p′ →
+  ⟪_,_⟫
+    {R = λ _ → ∃ λ _ → ∃ λ _ → ∃ λ _ → ∃ _}
+    (λ { (q , p∼q , r , qRr , r∼s) p⟶p′ →
        let q′ , q⟶q′ , p′∼q′ =
              left-to-right bisimilarity-is-a-bisimulation p∼q p⟶p′
            r′ , r⟶r′ , (q″ , q′∼q″ , r″ , q″Rr″ , r″∼r′) =
@@ -252,7 +255,7 @@ bisimulation-up-to-∼⇒bisimulation R-is =
        , transitive-∼ p′∼q′ q′∼q″
        , r″ , q″Rr″
        , transitive-∼ r″∼r′ r′∼s′ })
-  , (λ { (q , p∼q , r , qRr , r∼s) s⟶s′ →
+    (λ { (q , p∼q , r , qRr , r∼s) s⟶s′ →
        let r′ , r⟶r′ , r′∼s′ =
              right-to-left bisimilarity-is-a-bisimulation r∼s s⟶s′
            q′ , q⟶q′ , (q″ , q′∼q″ , r″ , q″Rr″ , r″∼r′) =
@@ -264,7 +267,6 @@ bisimulation-up-to-∼⇒bisimulation R-is =
        , transitive-∼ p′∼q′ q′∼q″
        , r″ , q″Rr″
        , transitive-∼ r″∼r′ r′∼s′ })
-  ⟫

 -- If R is a bisimulation up to bisimilarity, then R is contained in
 -- bisimilarity.

diff --git a/src/Free-variables.agda b/src/Free-variables.agda
index ffdd957..57b701a 100644
--- a/src/Free-variables.agda
+++ b/src/Free-variables.agda
@@ -117,7 +117,7 @@ mutual
   subst-∈FV x (lambda y e)  (lambda x′≢y p)        | yes x≡y = inj₁ (lambda x′≢y p , x′≢y ∘ flip trans x≡y)
   subst-∈FV x (lambda y e)  (lambda x′≢y p)        | no  _   = ⊎-map (Σ-map (lambda x′≢y) id) id (subst-∈FV x e p)
   subst-∈FV x (case e bs)   (case-head p)          = ⊎-map (Σ-map case-head id) id (subst-∈FV x e p)
-  subst-∈FV x (case e bs)   (case-body p ps x′∉xs) = ⊎-map (Σ-map (λ p → let _ , _ , _ , ps , p , ∉ = p in
+  subst-∈FV x (case e bs)   (case-body p ps x′∉xs) = ⊎-map (Σ-map (λ (p : ∃ λ _ → ∃ λ _ → ∃ λ _ → ∃ λ _ → ∃ _) → let _ , _ , _ , ps , p , ∉ = p in
                                                                          case-body p ps ∉)
                                                                   id)
                                                            id

diff -rN -u old-dependent-lenses/src/Lens/Non-dependent/Alternative.agda new-dependent-lenses/src/Lens/Non-dependent/Alternative.agda
--- old-dependent-lenses/src/Lens/Non-dependent/Alternative.agda	2018-01-05 11:39:25.769594364 +0100
+++ new-dependent-lenses/src/Lens/Non-dependent/Alternative.agda	2018-01-05 11:39:25.769594364 +0100
@@ -953,7 +953,7 @@

       (∥ B ∥ ×
        (∃ λ (f : B → R) → Constant f) ×
-       (∃ λ (g : B → B) → B → ∀ b → b ≡ g b))                     ↔⟨ (∃-cong λ ∥b∥ → ∃-cong λ { (f , _) → ∃-cong λ _ → inverse $
+       (∃ λ (g : B → B) → B → ∀ b → b ≡ g b))                     ↔⟨ (∃-cong λ ∥b∥ → ∃-cong {A = ∃ _} λ { (f , _) → ∃-cong λ _ → inverse $
                                                                         →-intro ext (λ _ → B-set f ∥b∥ _ _) }) ⟩
       (∥ B ∥ ×
        (∃ λ (f : B → R) → Constant f) ×