diff --git a/.github/workflows/build-typetheory.yml b/.github/workflows/build-typetheory.yml
index 01fc47d5..b7108cf7 100644
--- a/.github/workflows/build-typetheory.yml
+++ b/.github/workflows/build-typetheory.yml
@@ -5,6 +5,11 @@ on:
     branches: [master]
   pull_request:
     branches: [master]
+    types:
+      - ready_for_review
+      - opened
+      - reopened
+      - synchronize
   # Allows you to run this workflow manually from the Actions tab
   workflow_dispatch:
   schedule:
@@ -20,7 +25,8 @@ jobs:
     strategy:
       fail-fast: false
       matrix:
-        coq-version: [dev, latest, 8.16]
+        coq-version: [dev, latest]
+        # '8.20' does not work since Corelib is not known (the apostrophes are needed to interpret it as version 20 instead of 2)
         ocaml-version: [4.14-flambda]
     name: Build with ${{ matrix.coq-version }}
     runs-on: ubuntu-22.04
@@ -58,7 +64,11 @@ jobs:
           ocaml_version: ${{ matrix.ocaml-version }}
           custom_script: |
             startGroup "Workaround permission issue"
-            sudo chown -R coq:coq . || sudo chown -R rocq:rocq .
+            sudo chown -R 1000:1000 .
+            endGroup
+
+            startGroup "Install the coq shim if need be"
+            command -v coqc || opam install --confirm-level=unsafe-yes -j 2 coq-core
             endGroup
 
             startGroup "Print versions"
diff --git a/TypeTheory/Auxiliary/Auxiliary.v b/TypeTheory/Auxiliary/Auxiliary.v
index 9fa884fc..0646da5e 100644
--- a/TypeTheory/Auxiliary/Auxiliary.v
+++ b/TypeTheory/Auxiliary/Auxiliary.v
@@ -608,12 +608,12 @@ Proof.
   - intros bp. use total2_paths_f. apply idpath. apply wv.
 Qed.
 
-Definition truncation_weq (A : UU) (is : isaprop A) : A ≃ ∥ A ∥.
+Definition truncation_weq (A : UU) (isa : isaprop A) : A ≃ ∥ A ∥.
 Proof.
   apply weqimplimpl.
   - apply hinhpr.
   - intro a. unsquash a; assumption.
-  - apply is.
+  - apply isa.
   - apply propproperty. 
 Defined.
 
diff --git a/TypeTheory/Bsystems/S_St.v b/TypeTheory/Bsystems/S_St.v
index 04859e17..b9159831 100644
--- a/TypeTheory/Bsystems/S_St.v
+++ b/TypeTheory/Bsystems/S_St.v
@@ -184,18 +184,18 @@ Defined.
 Lemma isover_S_S_2 { BB : lBsystem_carrier }
       { S : S_ops_type BB } ( ax0 :  S_ax0_type S ) ( ax1a : S_ax1a_type S )
       { r : Tilde BB } { Y Y' : BB } ( inn : S_dom r Y ) ( inn' : S_dom r Y' )
-      ( is : isover Y Y' ) : isover ( S r Y inn ) ( S r Y' inn' ) .
+      ( iso : isover Y Y' ) : isover ( S r Y inn ) ( S r Y' inn' ) .
 Proof .
   unfold isover in * .
   do 2 rewrite ax0 .
   simpl .
   assert ( isab : isabove ( ftn ( ll Y - ll Y') Y ) ( dd r ) ) .
-  rewrite <- is . 
+  rewrite <- iso . 
   exact inn' . 
 
   rewrite ( natmiusmius1mminus1 ( S_dom_gt0 inn ) ( S_dom_gt0 inn' ) ) . 
   rewrite ( ftn_S ax1a _ isab inn ) .
-  exact ( S_equals_2 _ is _ _ ) . 
+  exact ( S_equals_2 _ iso _ _ ) . 
 
 Defined.
 
@@ -203,16 +203,16 @@ Defined.
 Lemma isabove_S_S_2 { BB : lBsystem_carrier }
       { S : S_ops_type BB } ( ax0 :  S_ax0_type S ) ( ax1a : S_ax1a_type S )
       { r : Tilde BB } { Y Y' : BB } ( inn : S_dom r Y ) ( inn' : S_dom r Y' )
-      ( is : isabove Y Y' ) : isabove ( S r Y inn ) ( S r Y' inn' ) .
+      ( isa : isabove Y Y' ) : isabove ( S r Y inn ) ( S r Y' inn' ) .
 Proof .
   use isabove_constr.
   do 2 rewrite ax0 .
   use natgthandminusinvr.
-  exact ( isabove_gth is ) .
+  exact ( isabove_gth isa ) .
 
   exact ( S_dom_ge1 inn' ) . 
 
-  exact ( isover_S_S_2 ax0 ax1a _ _ is ) . 
+  exact ( isover_S_S_2 ax0 ax1a _ _ isa ) . 
 
 Defined.
 
diff --git a/TypeTheory/Bsystems/S_fun.v b/TypeTheory/Bsystems/S_fun.v
index d7eb356b..27c1fc1d 100644
--- a/TypeTheory/Bsystems/S_fun.v
+++ b/TypeTheory/Bsystems/S_fun.v
@@ -56,17 +56,17 @@ Defined.
 Lemma isover_S_ext_S_ext_2 { BB : lBsystem_carrier }
       { S : S_ops_type BB } ( ax0 :  S_ax0_type S ) ( ax1a : S_ax1a_type S ) ( ax1b : S_ax1b_type S )
       { r : Tilde BB } { X2 X2' : BB } ( inn : S_ext_dom r X2 ) ( inn' : S_ext_dom r X2' )
-      ( is : isover X2 X2' ) : isover ( S_ext S inn ) ( S_ext S inn' ) .
+      ( iso : isover X2 X2' ) : isover ( S_ext S inn ) ( S_ext S inn' ) .
 Proof .
   unfold S_ext .
   destruct ( ovab_choice inn ) as [ isab | eq ] .
   + destruct ( ovab_choice inn' ) as [ isab' | eq' ] .
-    * apply ( isover_S_S_2 ax0 ax1a _ _ is ) . 
+    * apply ( isover_S_S_2 ax0 ax1a _ _ iso ) . 
     * exact ( ax1b _ _ _ ) . 
   + destruct ( ovab_choice inn' ) as [ isab' | eq' ] .
     * assert ( absd : empty ) .
-      rewrite eq in is . 
-      assert ( ge := isover_geh is ) .  
+      rewrite eq in iso . 
+      assert ( ge := isover_geh iso ) .  
       assert ( gt := isabove_gth isab' ) . 
       exact ( natgthnegleh gt ge ) . 
 
diff --git a/TypeTheory/Bsystems/T_Tt.v b/TypeTheory/Bsystems/T_Tt.v
index c0952872..ec94141c 100644
--- a/TypeTheory/Bsystems/T_Tt.v
+++ b/TypeTheory/Bsystems/T_Tt.v
@@ -230,20 +230,20 @@ Defined.
 Lemma isover_T_T_2 { BB : lBsystem_carrier }
       { T : T_ops_type BB } ( ax0 :  T_ax0_type T ) ( ax1a : T_ax1a_type T )
       { X1 X2 X2' : BB } ( inn : T_dom X1 X2 ) ( inn' : T_dom X1 X2' )
-      ( is : isover X2 X2' ) : isover ( T X1 X2 inn ) ( T X1 X2' inn' ) .
+      ( iso : isover X2 X2' ) : isover ( T X1 X2 inn ) ( T X1 X2' inn' ) .
 Proof .
   unfold isover in * .
   do 2 rewrite ax0 .
   simpl .
   assert ( isab : isabove ( ftn ( ll X2 - ll X2') X2 ) ( ft X1 ) ) .
-  rewrite <- is .
+  rewrite <- iso .
 
 (*  Set Printing All . *)
   
   exact ( T_dom_isabove inn' ) . 
 
   rewrite ( ftn_T ax1a _ isab inn ) .
-  exact ( T_equals_T _ is _ _ ) . 
+  exact ( T_equals_T _ iso _ _ ) . 
 
 Defined.
 
@@ -251,13 +251,13 @@ Defined.
 Lemma isabove_T_T_2 { BB : lBsystem_carrier }
       { T : T_ops_type BB } ( ax0 :  T_ax0_type T ) ( ax1a : T_ax1a_type T )
       { X1 X2 X2' : BB } ( inn : T_dom X1 X2 ) ( inn' : T_dom X1 X2' )
-      ( is : isabove X2 X2' ) : isabove ( T X1 X2 inn ) ( T X1 X2' inn' ) .
+      ( isa : isabove X2 X2' ) : isabove ( T X1 X2 inn ) ( T X1 X2' inn' ) .
 Proof .
   use isabove_constr.
   do 2 rewrite ax0 . 
-  exact ( isabove_gth is ) . 
+  exact ( isabove_gth isa ) . 
 
-  exact ( isover_T_T_2 ax0 ax1a _ _ is ) . 
+  exact ( isover_T_T_2 ax0 ax1a _ _ isa ) . 
   
 Defined.
 
diff --git a/TypeTheory/Bsystems/T_fun.v b/TypeTheory/Bsystems/T_fun.v
index a6a59fe6..ff894c03 100644
--- a/TypeTheory/Bsystems/T_fun.v
+++ b/TypeTheory/Bsystems/T_fun.v
@@ -63,17 +63,17 @@ Defined.
 Lemma isover_T_ext_T_ext_2 { BB : lBsystem_carrier }
       { T : T_ops_type BB } ( ax0 :  T_ax0_type T ) ( ax1a : T_ax1a_type T ) ( ax1b : T_ax1b_type T )
       { X1 X2 X2' : BB } ( inn : T_ext_dom X1 X2 ) ( inn' : T_ext_dom X1 X2' )
-      ( is : isover X2 X2' ) : isover ( T_ext T inn ) ( T_ext T inn' ) .
+      ( iso : isover X2 X2' ) : isover ( T_ext T inn ) ( T_ext T inn' ) .
 Proof .
   unfold T_ext .
   destruct ( ovab_choice (pr2 inn) ) as [ isab | eq ] .
   + destruct ( ovab_choice (pr2 inn') ) as [ isab' | eq' ] .
-    * apply ( isover_T_T_2 ax0 ax1a _ _ is ) . 
+    * apply ( isover_T_T_2 ax0 ax1a _ _ iso ) . 
     * exact ( ax1b _ _ _ ) . 
   + destruct ( ovab_choice (pr2 inn') ) as [ isab' | eq' ] .
     * apply fromempty. 
-      rewrite eq in is . 
-      assert ( ge := isover_geh is ) .  
+      rewrite eq in iso . 
+      assert ( ge := isover_geh iso ) .  
       assert ( gt := isabove_gth isab' ) . 
       exact ( natgthnegleh gt ge ) . 
     * exact ( isover_XX _ ) . 
diff --git a/TypeTheory/Bsystems/lB_carriers.v b/TypeTheory/Bsystems/lB_carriers.v
index aacfb2ea..12b82b16 100644
--- a/TypeTheory/Bsystems/lB_carriers.v
+++ b/TypeTheory/Bsystems/lB_carriers.v
@@ -24,13 +24,13 @@ hold. *)
 
 
 Definition lBsystem_carrier_constr { B : hSet_pltower } { TildeB : hSet }
-           ( dd : TildeB -> B ) ( is : forall r : TildeB, ll ( dd r ) > 0 ) : lBsystem_carrier .
+           ( dd : TildeB -> B ) ( hyp : forall r : TildeB, ll ( dd r ) > 0 ) : lBsystem_carrier .
 Proof .
   split with B . 
 
   split with TildeB . 
 
-  exact ( tpair _ dd is ) .
+  exact ( tpair _ dd hyp ) .
 
 Defined.
 
diff --git a/TypeTheory/Csystems/hSet_ltowers.v b/TypeTheory/Csystems/hSet_ltowers.v
index 16a2ab27..3c7497a8 100644
--- a/TypeTheory/Csystems/hSet_ltowers.v
+++ b/TypeTheory/Csystems/hSet_ltowers.v
@@ -8,8 +8,8 @@ Require Export TypeTheory.Csystems.ltowers_over.
 
 Definition hSet_ltower := ∑ T : ltower, isaset T.
 
-Definition hSet_ltower_constr ( T : ltower ) ( is : isaset T ):
-  hSet_ltower := T ,, is. 
+Definition hSet_ltower_constr ( T : ltower ) ( isa : isaset T ):
+  hSet_ltower := T ,, isa. 
 
 Definition hSet_ltower_pr1: hSet_ltower -> ltower := pr1. 
 Coercion hSet_ltower_pr1: hSet_ltower >-> ltower.
@@ -30,8 +30,8 @@ Defined.
 
 Definition hSet_pltower := ∑ T : hSet_ltower, ispointed_type T.
 
-Definition hSet_pltower_constr ( T : hSet_ltower ) ( is : ispointed_type T ):
-  hSet_pltower := T ,, is. 
+Definition hSet_pltower_constr ( T : hSet_ltower ) ( isp : ispointed_type T ):
+  hSet_pltower := T ,, isp. 
 
 
 Definition hSet_pltowers_to_pltowers: hSet_pltower -> pltower :=
diff --git a/TypeTheory/Csystems/lC0systems.v b/TypeTheory/Csystems/lC0systems.v
index 6f9c68d9..0f30bad8 100644
--- a/TypeTheory/Csystems/lC0systems.v
+++ b/TypeTheory/Csystems/lC0systems.v
@@ -179,18 +179,18 @@ Proof.
 Defined.
 
 (* not needed later! *)
-Lemma eq_parameterized_equation {S T: UU}(is: isaset S)
+Lemma eq_parameterized_equation {S T: UU}(iss: isaset S)
       (l r: T -> S)(pequ: forall h: T, l h = r h)(chk: T -> T -> UU)
       (l_ok: forall {g g'}, chk g g' -> l g = l g')
       (r_ok: forall {g g'}, chk g g' -> r g = r g')
       { g g': T }(H: chk g g'):
   pequ g = l_ok H @ pequ g' @ (! r_ok H).
 Proof.
-  apply is.
+  apply iss.
 Qed.
 
 
-Lemma cancelidtoiso_left {CC: precategory}(is: isaset (ob CC)) {a b c: CC}
+Lemma cancelidtoiso_left {CC: precategory}(iss: isaset (ob CC)) {a b c: CC}
       (p1 p2: a = b)(m1 m2: b --> c):
   m1 = m2 -> idtoiso p1 · m1  = idtoiso p2 · m2.
 Proof.
@@ -199,7 +199,7 @@ Proof.
               morphism_from_z_iso _ _ (idtoiso p2)).
   apply maponpaths.
   apply maponpaths.
-  apply is.
+  apply iss.
   cbn.
   etrans.
   { apply maponpaths. exact Hyp. }
@@ -207,7 +207,7 @@ Proof.
   assumption.
 Qed.
 
-Lemma cancelidtoiso_left_cor {CC: precategory}(is: isaset (ob CC)) {a b: CC}
+Lemma cancelidtoiso_left_cor {CC: precategory}(iss: isaset (ob CC)) {a b: CC}
       (p: a = a)(m1 m2: a --> b):
   m1 = m2 -> m1  = idtoiso p · m2.
 Proof.
@@ -218,7 +218,7 @@ Proof.
 Qed.
 
 
-Lemma cancelidtoiso_right {CC: precategory}(is: isaset (ob CC)) {a b c: CC}
+Lemma cancelidtoiso_right {CC: precategory}(iss: isaset (ob CC)) {a b c: CC}
       (m1 m2: a --> b)(q1 q2: b = c):
   m1 = m2 -> m1 · idtoiso q1  =  m2 · idtoiso q2.
 Proof.
@@ -227,14 +227,14 @@ Proof.
               morphism_from_z_iso _ _ (idtoiso q2)).
   apply maponpaths.
   apply maponpaths.
-  apply is.
+  apply iss.
   etrans.
   { apply maponpaths. exact H1. }
   apply cancel_postcomposition.
   assumption.
 Qed.
 
-Lemma cancelidtoiso_right_cor {CC: precategory}(is: isaset (ob CC)) {a b: CC}
+Lemma cancelidtoiso_right_cor {CC: precategory}(iss: isaset (ob CC)) {a b: CC}
       (m1 m2: a --> b)(q: b = b):
   m1 = m2 -> m1 =  m2 · idtoiso q.
 Proof.
@@ -244,7 +244,7 @@ Proof.
   apply cancelidtoiso_right; assumption.
 Qed.
 
-Corollary eq_par_arrow_cor_objirr {CC: precategory}(is: isaset (ob CC)){T: UU}
+Corollary eq_par_arrow_cor_objirr {CC: precategory}(iss: isaset (ob CC)){T: UU}
       ( s t: T -> ob CC )
       ( par: forall h: T, CC ⟦ s h , t h ⟧)
       { g g': T}(e : g = g')(p: s g = s g')(q: t g' = t g):
@@ -253,14 +253,14 @@ Proof.
   rewrite (eq_par_arrow_cor _ _ _ e).
   do 2 rewrite <- assoc.
   apply cancelidtoiso_left.
-  { apply is. }
+  { apply iss. }
   etrans.
   { apply cancel_precomposition.
     apply pathsinv0.
     apply idtoiso_inv0.
   }
   apply cancelidtoiso_right.
-  { apply is. }
+  { apply iss. }
   apply idpath.
 Qed.
 
diff --git a/TypeTheory/Csystems/lTowers.v b/TypeTheory/Csystems/lTowers.v
index 13efc6c4..3f736d23 100644
--- a/TypeTheory/Csystems/lTowers.v
+++ b/TypeTheory/Csystems/lTowers.v
@@ -220,11 +220,11 @@ Defined.
 Definition isover { BB : ltower } ( X A : BB ):= ( A = ftn ( ll X - ll A ) X ).
 
 
-Lemma isover_geh { BB : ltower } { X A : BB } ( is : isover X A ):
+Lemma isover_geh { BB : ltower } { X A : BB } ( iso : isover X A ):
   ll X >= ll A.
 Proof.
-  unfold isover in is. 
-  assert ( int : ll A = ll ( ftn (ll X - ll A) X ) ) by exact ( maponpaths ll is ).
+  unfold isover in iso. 
+  assert ( int : ll A = ll ( ftn (ll X - ll A) X ) ) by exact ( maponpaths ll iso ).
   rewrite int.
   rewrite ll_ftn.
   use natminuslehn.
@@ -284,36 +284,36 @@ Defined.
 
   
 Lemma isover_X_ftA { BB : ltower } { X A : BB }
-      ( is : isover X A ): isover X ( ft A ).
+      ( iso : isover X A ): isover X ( ft A ).
 Proof.
-  exact ( isover_trans is ( isover_X_ftX _ ) ). 
+  exact ( isover_trans iso ( isover_X_ftX _ ) ). 
 Defined.
 
 
 Lemma isover_ft { BB : ltower } { X A : BB }
-      ( is : isover X A ) ( gt : ll X > ll A ): isover ( ft X ) A.
+      ( iso : isover X A ) ( gt : ll X > ll A ): isover ( ft X ) A.
 Proof.
   unfold isover in *. 
   rewrite ftn_ft.
   rewrite ll_ft.
   rewrite <- lB_2014_12_07_l1.
-  - exact is.
+  - exact iso.
   - exact gt.
 Defined.
 
 
 Lemma isover_ftn { BB : ltower } { n : nat } { X A : BB } 
-      ( is : isover X A ) ( gte : ll X - ll A >= n ): isover ( ftn n X ) A.
+      ( iso : isover X A ) ( gte : ll X - ll A >= n ): isover ( ftn n X ) A.
 Proof.
-  revert X A is gte.
+  revert X A iso gte.
   induction n as [ | n IHn ].
   - intros.
-    exact is.
-  - intros X A is gte.
+    exact iso.
+  - intros X A iso gte.
     simpl.
     use isover_ft.
     + use IHn.
-      * exact is.
+      * exact iso.
       * exact ( istransnatgeh _ _ _ gte ( natgehsnn n ) ).
     + rewrite ll_ftn. 
       use natgthleftminus.
@@ -325,14 +325,14 @@ Defined.
 
 
 Lemma isover_choice { BB : ltower } { X A : BB }
-      ( is : isover X A ): ( isover ( ft X ) A ) ⨿ ( A = X ).
+      ( iso : isover X A ): ( isover ( ft X ) A ) ⨿ ( A = X ).
 Proof.
-  destruct ( natgehchoice _ _ ( isover_geh is ) ) as [ gt | eq ]. 
-  - exact ( ii1 ( isover_ft is gt ) ). 
-  - unfold isover in is. 
-    rewrite eq in is. 
-    rewrite natminusnn in is. 
-    exact ( ii2 is ).
+  destruct ( natgehchoice _ _ ( isover_geh iso ) ) as [ gt | eq ]. 
+  - exact ( ii1 ( isover_ft iso gt ) ). 
+  - unfold isover in iso. 
+    rewrite eq in iso. 
+    rewrite natminusnn in iso. 
+    exact ( ii2 iso ).
 Defined.
 
 
@@ -347,12 +347,12 @@ Definition isabove { BB : ltower } ( X A : BB ):=
 Definition isabove_constr { BB : ltower } { X A : BB }
   ( gt : ll X > ll A ) ( isov : isover X A ): isabove X A := gt ,, isov. 
 
-Definition isabove_gth { BB : ltower } { X A : BB } ( is : isabove X A ):
-  ll X > ll A := pr1 is.
+Definition isabove_gth { BB : ltower } { X A : BB } ( isa : isabove X A ):
+  ll X > ll A := pr1 isa.
 
-Lemma isabove_gt0 { BB : ltower } { X A : BB } ( is : isabove X A ): ll X > 0.
+Lemma isabove_gt0 { BB : ltower } { X A : BB } ( isa : isabove X A ): ll X > 0.
 Proof.
-  exact ( natgthgehtrans _ _ _ ( isabove_gth is ) ( natgehn0 _ ) ).
+  exact ( natgthgehtrans _ _ _ ( isabove_gth isa ) ( natgehn0 _ ) ).
 Defined.
 
   
@@ -385,68 +385,68 @@ Defined.
 
   
 Lemma isabove_X_ftA { BB : ltower } { X A : BB }
-      ( is : isabove X A ) : isabove X ( ft A ).
+      ( isa : isabove X A ) : isabove X ( ft A ).
 Proof.
   use isabove_constr.
   - rewrite ll_ft. 
-    exact ( natgthgehtrans _ _ _ ( isabove_gth is ) ( natminuslehn _ 1 ) ). 
-  - exact (isover_X_ftA is ).
+    exact ( natgthgehtrans _ _ _ ( isabove_gth isa ) ( natminuslehn _ 1 ) ). 
+  - exact (isover_X_ftA isa ).
 Defined.
 
 
 Lemma isabove_X_ftA' { BB : ltower } { X A : BB }
-      ( is : isover X A ) ( gt0 : ll A > 0 ): isabove X ( ft A ).
+      ( iso : isover X A ) ( gt0 : ll A > 0 ): isabove X ( ft A ).
 Proof.
   use isabove_constr.
   - rewrite ll_ft.
-    use ( natgehgthtrans _ _ _ ( isover_geh is ) ).
+    use ( natgehgthtrans _ _ _ ( isover_geh iso ) ).
     exact ( natgthnnmius1 gt0 ). 
-  - exact ( isover_X_ftA is ). 
+  - exact ( isover_X_ftA iso ). 
 Defined.
 
 
 Lemma isabove_trans { BB : ltower } { X A A' : BB }:
   isabove X A -> isabove A A' -> isabove X A'.
 Proof.
-  intros is is'.
+  intros isa isa'.
   use isabove_constr.
-  - exact ( istransnatgth _ _ _ ( isabove_gth is ) ( isabove_gth is' ) ).
-  - exact ( isover_trans is is' ).
+  - exact ( istransnatgth _ _ _ ( isabove_gth isa ) ( isabove_gth isa' ) ).
+  - exact ( isover_trans isa isa' ).
 Defined.
 
 
 Lemma isabov_trans { BB : ltower } { X A A' : BB }:
   isabove X A -> isover A A' -> isabove X A'.
 Proof.
-  intros is is'.
+  intros isa iso.
   use isabove_constr.
-  - exact ( natgthgehtrans _ _ _ ( isabove_gth is ) ( isover_geh is' ) ).
-  - exact ( isover_trans is is' ).
+  - exact ( natgthgehtrans _ _ _ ( isabove_gth isa ) ( isover_geh iso ) ).
+  - exact ( isover_trans isa iso ).
 Defined.
 
 
 Lemma isovab_trans { BB : ltower } { X A A' : BB }:
   isover X A -> isabove A A' -> isabove X A'.
 Proof.
-  intros is is'.
+  intros iso isa.
   use isabove_constr.
-  - exact ( natgehgthtrans _ _ _ ( isover_geh is ) ( isabove_gth is' ) ).
-  - exact ( isover_trans is is' ).
+  - exact ( natgehgthtrans _ _ _ ( isover_geh iso ) ( isabove_gth isa ) ).
+  - exact ( isover_trans iso isa ).
 Defined.
 
 
 
-Lemma isover_ft' { BB : ltower } { X A : BB } ( is : isabove X A ):
+Lemma isover_ft' { BB : ltower } { X A : BB } ( isa : isabove X A ):
   isover ( ft X ) A.
 Proof.
-  exact ( isover_ft is ( isabove_gth is ) ). 
+  exact ( isover_ft isa ( isabove_gth isa ) ). 
 Defined.
 
 
-Lemma isabove_ft_inv { BB : ltower } { X A : BB } ( is : isabove ( ft X ) A ):
+Lemma isabove_ft_inv { BB : ltower } { X A : BB } ( isa : isabove ( ft X ) A ):
   isabove X A.
 Proof.
-  exact ( isovab_trans ( isover_X_ftX _ ) is ).  
+  exact ( isovab_trans ( isover_X_ftX _ ) isa ).  
 Defined.
 
 
@@ -509,8 +509,8 @@ Definition ovmonot_fun ( T1 T2 : ltower ):=
   ∑ f : T1 -> T2, isovmonot f. 
 
 Definition ovmonot_fun_constr { T1 T2 : ltower }
-           ( f : T1 -> T2 ) ( is : forall ( X Y : T1 ), isover X Y -> isover ( f X ) ( f Y ) ):
-  ovmonot_fun T1 T2 := f ,, is.
+           ( f : T1 -> T2 ) ( hyp : forall ( X Y : T1 ), isover X Y -> isover ( f X ) ( f Y ) ):
+  ovmonot_fun T1 T2 := f ,, hyp.
 
 
 Definition ovmonot_fun_pr1 ( T1 T2 : ltower ): ovmonot_fun T1 T2 -> ( T1 -> T2 ):= pr1. 
@@ -524,10 +524,10 @@ Definition isovmonot_funcomp { T1 T2 T3 : ltower } { f : T1 -> T2 } { g : T2 ->
            ( isf : isovmonot f ) ( isg : isovmonot g ): isovmonot ( funcomp f g ).
 Proof.
   unfold isovmonot.  
-  intros X Y is. 
+  intros X Y iso. 
   apply isg. 
   apply isf. 
-  apply is. 
+  apply iso. 
 Defined.
 
 
@@ -656,7 +656,7 @@ Definition ispointed_type ( T : ltower ) := iscontr ( ∑ X : T, ll X = 0 ).
 
 Definition pltower := ∑ T : ltower, ispointed_type T.
 
-Definition pltower_constr { T : ltower } ( is : ispointed_type T ) : pltower := tpair _ _ is. 
+Definition pltower_constr { T : ltower } ( isp : ispointed_type T ) : pltower := tpair _ _ isp. 
 
 Definition pltower_pr1 : pltower -> ltower := pr1.
 Coercion pltower_pr1 : pltower >-> ltower.
@@ -679,7 +679,7 @@ Defined.
 Lemma isoverll0 { T : pltower } { X1 : T }
   ( eq0 : ll X1 = 0 ) ( X2 : T ) : isover X2 X1.
 Proof.
-  set ( is := pr2 T ). 
+  set ( isp := pr2 T ). 
   unfold isover. 
   assert ( eq0' : ll ( ftn ( ll X2 - ll X1 ) X2 ) = 0 ). 
   { rewrite ll_ftn. 
@@ -687,7 +687,7 @@ Proof.
     rewrite natminuseqn.
     exact ( natminusnn _ ).
   }
-  assert ( eq : tpair ( fun X : T => ll X = 0 ) _ eq0 = tpair ( fun X : T => ll X = 0 ) _ eq0' ) by use ( proofirrelevancecontr is ).
+  assert ( eq : tpair ( fun X : T => ll X = 0 ) _ eq0 = tpair ( fun X : T => ll X = 0 ) _ eq0' ) by use ( proofirrelevancecontr isp ).
   exact ( maponpaths ( @pr1 _ ( fun X : T => ll X = 0 ) ) eq ). 
 Defined.
 
@@ -698,8 +698,8 @@ Definition isover_cntr { T : pltower } ( X : T ): isover X ( cntr T ) :=
 Lemma noparts_ispointed { T : pltower } { X Y : T }
   ( eqX : ll X = 0 ) ( eqY : ll Y = 0 ) : X = Y.
 Proof.
-  set ( is := pr2 T ). 
-  set ( int := proofirrelevancecontr is ( tpair _ _ eqX ) ( tpair _ _ eqY ) ). 
+  set ( isp := pr2 T ). 
+  set ( int := proofirrelevancecontr isp ( tpair _ _ eqX ) ( tpair _ _ eqY ) ). 
   apply ( maponpaths pr1 int ). 
 Defined.
 
@@ -741,4 +741,4 @@ Defined.
 
   
   
-(* End of the file ltowers.v *)
\ No newline at end of file
+(* End of the file ltowers.v *)
diff --git a/TypeTheory/Csystems/prelim.v b/TypeTheory/Csystems/prelim.v
index 944fea1e..260ca65e 100644
--- a/TypeTheory/Csystems/prelim.v
+++ b/TypeTheory/Csystems/prelim.v
@@ -235,10 +235,10 @@ Definition nateqandplusl ( n m k : nat ): n = m -> k + n = k + m :=
 
 (** **** Cancellation properties of minus on nat *)
 
-Lemma natminusrcan { n m k : nat } ( ge1 : n >= k ) ( ge2 : m >= k ) ( is : n - k = m - k ):
+Lemma natminusrcan { n m k : nat } ( ge1 : n >= k ) ( ge2 : m >= k ) ( ise : n - k = m - k ):
   n = m.
 Proof.
-  assert ( is' := nateqandplusr _ _ k is ).
+  assert ( is' := nateqandplusr _ _ k ise ).
   rewrite ( minusplusnmm _ _ ge1 ) in is'.
   rewrite ( minusplusnmm _ _ ge2 ) in is'.
   exact is'.
@@ -351,20 +351,20 @@ Defined.
 
 (* Two-sided minus and greater *)
 
-Definition natgthandminusinvr { n m k : nat } ( is : n > m ) ( is' : m >= k ):
+Definition natgthandminusinvr { n m k : nat } ( isgt : n > m ) ( is' : m >= k ):
   n - k > m - k.
 Proof.
-  revert m k is is'.
+  revert m k isgt is'.
   induction n as [ | n IHn ].
   - intros.
-    destruct ( negnatgth0n _ is ).
+    destruct ( negnatgth0n _ isgt ).
   - intro m.
     induction k as [ | k ]; intros.
     + do 2 rewrite natminuseqn.
-      exact is.
+      exact isgt.
     + induction m as [ | m ].
       * destruct ( negnatgeh0sn _ is' ).
-      * exact ( IHn m k is is' ).
+      * exact ( IHn m k isgt is' ).
 Defined.
 
 
@@ -382,10 +382,10 @@ Proof.
       induction k as [ | k ].
       * apply natminuslehn.
       * apply natminuslehn.
-    + induction k as [ | k ]; intro is.
+    + induction k as [ | k ]; intro isge.
       * apply isreflnatleh.
       * apply ( IHn m k ).
-        apply is.
+        apply isge.
 Defined.
 
 
diff --git a/TypeTheory/Initiality/SyntacticCategory.v b/TypeTheory/Initiality/SyntacticCategory.v
index 0108237e..9a25b71f 100644
--- a/TypeTheory/Initiality/SyntacticCategory.v
+++ b/TypeTheory/Initiality/SyntacticCategory.v
@@ -394,14 +394,27 @@ Section Context_Maps.
     intros H Γ Δ.
     unsquash H as [Γ' [Δ' d_fg]].
     unsquash from Γ Γ' Δ Δ' d_fg
-             (cxteq_context_representatives Γ Γ')
-             (cxteq_context_representatives Δ Δ')
-      as ? d_Γ' ? d_Δ' [? [? ?]] ? ?. apply hinhpr.
+      (cxteq_context_representatives Γ Γ')
+      (cxteq_context_representatives Δ Δ')
+      as X d_Γ' X0 d_Δ' [pr1 [pr0 pr2]] X1 X2. (* names Xi and pri assigned for later exact command *) apply hinhpr.
+    exact (derive_mapeq_conv_cxteq_dom d_Γ' X (derive_flat_cxteq_sym X d_Γ' X1) X0
+             (derive_map_conv_cxteq_cod d_Γ' d_Δ' X0 (derive_flat_cxteq_sym X0 d_Δ' X2) pr1)
+             (derive_map_conv_cxteq_cod d_Γ' d_Δ' X0 (derive_flat_cxteq_sym X0 d_Δ' X2) pr0)
+             (derive_mapeq_conv_cxteq_cod d_Γ' d_Δ' X0 (derive_flat_cxteq_sym X0 d_Δ' X2) pr1 pr0 pr2)).
+  (* a less monolithic try to prove the goal:
+    unsquash from Γ Γ' Δ Δ' d_fg
+      (cxteq_context_representatives Γ Γ')
+      (cxteq_context_representatives Δ Δ')
+      as ? d_Γ' X0 d_Δ' [pr1 [pr0 pr2]] ? X2. (* names Xi and pri assigned for later exact command *) apply hinhpr.
     apply (derive_mapeq_conv_cxteq_dom d_Γ');
       auto using derive_flat_cxt_from_strat, derive_flat_cxteq_sym,
-         (derive_map_conv_cxteq_cod d_Γ' d_Δ').
-    use (derive_mapeq_conv_cxteq_cod _ d_Δ');
-      auto using derive_flat_cxt_from_strat, derive_flat_cxteq_sym.
+      (derive_map_conv_cxteq_cod d_Γ' d_Δ').
+    exact (derive_mapeq_conv_cxteq_cod d_Γ' d_Δ' X0 (derive_flat_cxteq_sym X0 d_Δ' X2) pr1 pr0 pr2).
+    Rocq 9.4alpha complains that the type of this expression does not match the goal
+   *)
+  (* prior to Rocq 9.4alpha the latter exact replaced with tactics:
+       use (derive_mapeq_conv_cxteq_cod _ d_Δ');
+       auto using derive_flat_cxt_from_strat, derive_flat_cxteq_sym. *)
   Qed.
 
   Lemma mapeq_for_some_rep
@@ -453,13 +466,13 @@ Section Context_Map_Operations.
     revert ff gg. use setquotfun2'; [ | split].
     - (* construction of the composite *)
       intros f g. exists (comp_raw_context f g).
-      abstract (intros Γ Θ;
+      abstract ( intros Γ Θ;
         apply (take_context_representative ΔΔ);
         [ apply isapropishinh |
           intros Δ;
           unsquash from Δ (map_derivable f Γ Δ) (map_derivable g Δ Θ)
             as d_Δ d_f d_g; apply hinhpr;
-          eauto using (derive_comp d_f) ]).
+          exact (derive_comp d_f d_g) ]).
     - (* respecting equality in [f] *)
       abstract ( intros f f' g e_f Γ Θ; cbn;
         apply (take_context_representative ΔΔ);
@@ -794,7 +807,8 @@ Section Split_Typecat.
         try apply derive_extend_flat_cxteq, (substeq_derivation [! Γ |- A !]);
         try refine (derive_flat_extend_context _ d_A);
         try refine (derive_weaken_raw_context_map _ _ _ d_f);
-        auto using derive_flat_cxt_from_strat, (@derive_flat_cxteq_refl Γ').
+        auto using derive_flat_cxt_from_strat, (@derive_flat_cxteq_refl Γ');
+        try exact (derive_flat_cxteq_refl d_Γ').
     + refine (derive_weaken_raw_context_map _ _ _ d_g);
         auto using derive_flat_cxt_from_strat.
     + refine (derive_weaken_raw_context_mapeq _ _ _ _ _ d_fg);
diff --git a/TypeTheory/RelUniv/RelativeUniverses.v b/TypeTheory/RelUniv/RelativeUniverses.v
index 38d6d609..45642f24 100644
--- a/TypeTheory/RelUniv/RelativeUniverses.v
+++ b/TypeTheory/RelUniv/RelativeUniverses.v
@@ -731,7 +731,7 @@ Variables (U tU : D) (pp : tU --> U).
 
 Section map_on_is_universe_relativ_to.
 
-Hypothesis is : is_universe_relative_to J pp.
+Hypothesis isu : is_universe_relative_to J pp.
 
 
 Lemma mere_fpullback_transfer {X' : C'} (g : D' ⟦ J' X', S U ⟧)
@@ -741,7 +741,7 @@ Proof.
   unsquash from (R_es X') as [X i]; clear R_es.
   set (f' := (α X ;; #J' i ;; g) : D' ⟦ S (J X), S U ⟧).
   unsquash from (S_full _ _ f') as [f e_Sf_f']; clear S_full.
-  unsquash from (is _ f) as [[Xf [p q]] [e isPb]].
+  unsquash from (isu _ f) as [[Xf [p q]] [e isPb]].
   assert (Sfp := S_pb _ _ _ _ _ _ _ _ _ isPb); clear S_pb.
   set (HSfp := functor_on_square D D' S e) in *; clearbody HSfp.
   apply hinhpr.