diff --git a/TypeTheory/Csystems/hSet_ltowers.v b/TypeTheory/Csystems/hSet_ltowers.v
index 6d00ae76..16a2ab27 100644
--- a/TypeTheory/Csystems/hSet_ltowers.v
+++ b/TypeTheory/Csystems/hSet_ltowers.v
@@ -699,11 +699,11 @@ Proof.
           exact eq.
         }
         clear eq0.
-        remember (transportf (isover X) (! eq) (isover_X_ftnX X (S n))) as H''.
+        set (H'' := transportf (isover X) (! eq) (isover_X_ftnX X (S n))).
         set (H3 := transportf (isover X) (! eq') (isover_XX X)).
         assert (eq'' : H'' = H3) by (apply isaprop_isover).
         rewrite eq''.
-        clear HeqH'' H'' eq'' eq.
+        clear H'' eq'' eq.
         induction eq'.
         cbn in H3.
         unfold H3.
diff --git a/TypeTheory/Initiality/Interpretation.v b/TypeTheory/Initiality/Interpretation.v
index 6239e69e..4693be22 100644
--- a/TypeTheory/Initiality/Interpretation.v
+++ b/TypeTheory/Initiality/Interpretation.v
@@ -1,5 +1,14 @@
 (** This file defines the interpretation function, from the syntax of our toy type theory into any split type-cat with suitable structure. *)
 
+
+(** * TODO NOTE: This file depends on Coq.Init.Logic.
+    Removing the following line causes the error:
+
+    File "./TypeTheory/TypeTheory/Initiality/Interpretation.v", line 366, characters 4-5:
+    Error: [Focus] Wrong bullet -: Current bullet + is not finished.
+ *)
+Require Import Coq.Init.Logic.
+
 Require Import UniMath.MoreFoundations.All.
 Require Import UniMath.CategoryTheory.Core.Prelude.
 
diff --git a/TypeTheory/Initiality/SyntacticCategory.v b/TypeTheory/Initiality/SyntacticCategory.v
index 9e3d40bc..512f218c 100644
--- a/TypeTheory/Initiality/SyntacticCategory.v
+++ b/TypeTheory/Initiality/SyntacticCategory.v
@@ -287,7 +287,7 @@ Section Contexts_Modulo_Equality.
     destruct ΓΓ as [n ΓΓ]. generalize ΓΓ.
     apply setquotunivprop'.
     { intros; apply isapropishinh. }
-    intros Γ; apply hinhpr. exists Γ; auto.
+    intros Γ; apply hinhpr. exists Γ; apply idpath.
   Defined.
 
 End Contexts_Modulo_Equality.
diff --git a/TypeTheory/TypeCat/General.v b/TypeTheory/TypeCat/General.v
index 55bf37e4..1fffe1f3 100644
--- a/TypeTheory/TypeCat/General.v
+++ b/TypeTheory/TypeCat/General.v
@@ -5,6 +5,14 @@ Note: much of this essentially duplicates material given already in the [CwF_Spl
 
 Probably much of this really should belong in a different package. *)
 
+(** * TODO NOTE: This file depends on Coq.Init.Logic.
+    Removing the following line causes the error:
+
+    File "./TypeTheory/TypeTheory/TypeCat/General.v", line 365, characters 6-115:
+    Error: not found in table: core.eq.type
+ *)
+Require Import Coq.Init.Logic.
+
 Require Import UniMath.MoreFoundations.All.
 Require Import TypeTheory.Auxiliary.CategoryTheoryImports.
 
diff --git a/TypeTheory/TypeConstructions/CwF_SplitTypeCat_TypeEquiv.v b/TypeTheory/TypeConstructions/CwF_SplitTypeCat_TypeEquiv.v
index 7119b42c..2aba9af6 100644
--- a/TypeTheory/TypeConstructions/CwF_SplitTypeCat_TypeEquiv.v
+++ b/TypeTheory/TypeConstructions/CwF_SplitTypeCat_TypeEquiv.v
@@ -362,11 +362,11 @@ Lemma unit_equiv_inv1 : ∏ x : unit_structure Sc, unit_equiv_2(unit_equiv_1 x)
 Proof.
   intro Unit.
   apply pair_path_in2.
-  assert (prj : pr2 Unit = pr12 Unit ,, pr22 Unit) by auto.
+  assert (prj : pr2 Unit = pr12 Unit ,, pr22 Unit) by apply idpath.
   apply pathsinv0.
   apply (pathscomp0 prj).
   refine (subtypePairEquality' _ _ ).
-  -  assert (func:  pr12 Unit = λ Γ : C , pr12 Unit Γ) by auto.
+  -  assert (func:  pr12 Unit = λ Γ : C , pr12 Unit Γ) by apply idpath.
      apply (pathscomp0 func).
      apply funextsec2.
      intro Γ.
@@ -378,11 +378,11 @@ Lemma unit_equiv_inv2 : ∏ x : CwF_unit_structure CWF, unit_equiv_1(unit_equiv_
 Proof.
   intro Unit.
   apply pair_path_in2.
-  assert (prj : pr2 Unit = (pr12 Unit ,, pr22 Unit)) by auto.
+  assert (prj : pr2 Unit = (pr12 Unit ,, pr22 Unit)) by apply idpath.
   apply pathsinv0.
   apply (pathscomp0 prj).
   refine (subtypePairEquality' _ _ ).
-  -  assert (func:  pr12 Unit = λ Γ : C , pr12 Unit Γ) by auto.
+  -  assert (func:  pr12 Unit = λ Γ : C , pr12 Unit Γ) by apply idpath.
      apply (pathscomp0 func).
      apply funextsec2.
      intro Γ.
@@ -434,15 +434,15 @@ Lemma universe_equiv_inv1
 Proof.
   intro Universe.
   apply pair_path_in2.
-  assert (prj : pr2 Universe = pr12 Universe ,, pr22 Universe) by auto.
+  assert (prj : pr2 Universe = pr12 Universe ,, pr22 Universe) by apply idpath.
   apply pathsinv0.
   apply (pathscomp0 prj).
   refine (subtypePairEquality' _ _ ).
-  -  assert (func : pr12 Universe = λ Γ : C , pr12 Universe Γ) by auto.
+  -  assert (func : pr12 Universe = λ Γ : C , pr12 Universe Γ) by apply idpath.
      apply (pathscomp0 func).
      apply funextsec2.
      intro Γ.
-     assert (simplman : pr12 Universe Γ  =  λ a : _, pr12 Universe Γ a) by auto.
+     assert (simplman : pr12 Universe Γ  =  λ a : _, pr12 Universe Γ a) by apply idpath.
      rewrite simplman.
      reflexivity.
   -  do 4 (apply impred_isaprop; intro); exact (pr12 Split _ _ _).
@@ -453,15 +453,15 @@ Lemma universe_equiv_inv2
 Proof.
   intro Universe.
   apply pair_path_in2.
-  assert (prj : pr2 Universe = pr12 Universe ,, pr22 Universe) by auto.
+  assert (prj : pr2 Universe = pr12 Universe ,, pr22 Universe) by apply idpath.
   apply pathsinv0.
   apply (pathscomp0 prj).
   refine (subtypePairEquality' _ _ ).
-  -  assert (func : pr12 Universe = λ Γ : C , pr12 Universe Γ) by auto.
+  -  assert (func : pr12 Universe = λ Γ : C , pr12 Universe Γ) by apply idpath.
      apply (pathscomp0 func).
      apply funextsec2.
      intro Γ.
-     assert (simplman : pr12 Universe Γ  =  λ a : _, pr12 Universe Γ a) by auto.
+     assert (simplman : pr12 Universe Γ  =  λ a : _, pr12 Universe Γ a) by apply idpath.
      rewrite simplman.
      cbn; apply funextsec; intro a; rewrite tm_equiv_inter_21; reflexivity.
   -  do 4 (apply impred_isaprop; intro); exact (setproperty (Ty CWF _) _ _).