restoring compilation in Rocq 9.4alpha

.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"

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.
 

TypeTheory/Bsystems/S_St.v

@@ -184,35 +184,35 @@ 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.
 
 
 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.
 

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 ) . 
 

TypeTheory/Bsystems/T_Tt.v

@@ -230,34 +230,34 @@ 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.
 
 
 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.
 

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 _ ) . 

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.
 

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 :=

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,15 +199,15 @@ Proof.
               morphism_from_z_iso _ _ (idtoiso p2)).
   apply maponpaths.
   apply maponpaths.
-  apply is.
+  apply iss.
   cbn.
   etrans.
   { apply maponpaths. exact Hyp. }
   apply cancel_postcomposition.
   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.