uses Context consistenly (UniMath#1841)

This is nothing but beautification.

UniMath/SubstitutionSystems/BinProductOfSignatures.v

@@ -39,15 +39,14 @@ Section construction.
 
 Local Notation "'PCD'" := (BinProducts_functor_precat C D PD : BinProducts [C, D]).
 
-Variables H1 H2 : functor [C, D'] [C, D].
+Context (H1 H2 : functor [C, D'] [C, D])
+        (θ1 : θ_source H1 ⟹ θ_target H1)
+        (θ2 : θ_source H2 ⟹ θ_target H2).
 
-Variable θ1 : θ_source H1 ⟹ θ_target H1.
-Variable θ2 : θ_source H2 ⟹ θ_target H2.
-
-Variable S11 : θ_Strength1 θ1.
-Variable S12 : θ_Strength2 θ1.
-Variable S21 : θ_Strength1 θ2.
-Variable S22 : θ_Strength2 θ2.
+Context (S11 : θ_Strength1 θ1)
+        (S12 : θ_Strength2 θ1)
+        (S21 : θ_Strength1 θ2)
+        (S22 : θ_Strength2 θ2).
 
 (** * Definition of the data of the product of two signatures *)
 
@@ -136,10 +135,10 @@ Proof.
     apply (nat_trans_eq_pointwise Ha x).
 Qed.
 
-Variable S11' : θ_Strength1_int θ1.
-Variable S12' : θ_Strength2_int θ1.
-Variable S21' : θ_Strength1_int θ2.
-Variable S22' : θ_Strength2_int θ2.
+Context (S11' : θ_Strength1_int θ1)
+        (S12' : θ_Strength2_int θ1)
+        (S21' : θ_Strength1_int θ2)
+        (S22' : θ_Strength2_int θ2).
 
 Lemma ProductStrength1' : θ_Strength1_int θ.
 Proof.

UniMath/SubstitutionSystems/BinSumOfSignatures.v

@@ -41,24 +41,20 @@ Local Open Scope cat.
 
 Section binsum_of_signatures.
 
-Variable C : category.
-Variable D : category.
-Variable D' : category.
-Variable CD : BinCoproducts D.
+Context  (C D D' : category) (CD : BinCoproducts D).
 
 Section construction.
 
 Local Notation "'CCD'" := (BinCoproducts_functor_precat C D CD : BinCoproducts [C, D]).
 
-Variables H1 H2 : functor [C, D'] [C, D].
+Context (H1 H2 : functor [C, D'] [C, D])
+        (θ1 : θ_source H1 ⟹ θ_target H1)
+        (θ2 : θ_source H2 ⟹ θ_target H2).
 
-Variable θ1 : θ_source H1 ⟹ θ_target H1.
-Variable θ2 : θ_source H2 ⟹ θ_target H2.
-
-Variable S11 : θ_Strength1 θ1.
-Variable S12 : θ_Strength2 θ1.
-Variable S21 : θ_Strength1 θ2.
-Variable S22 : θ_Strength2 θ2.
+Context (S11 : θ_Strength1 θ1)
+        (S12 : θ_Strength2 θ1)
+        (S21 : θ_Strength1 θ2)
+        (S22 : θ_Strength2 θ2).
 
 (** * Definition of the data of the sum of two signatures *)
 
@@ -169,10 +165,11 @@ Proof.
     apply Ha_x.
 Qed.
 
-Variable S11' : θ_Strength1_int θ1.
-Variable S12' : θ_Strength2_int θ1.
-Variable S21' : θ_Strength1_int θ2.
-Variable S22' : θ_Strength2_int θ2.
+
+Context (S11' : θ_Strength1_int θ1)
+        (S12' : θ_Strength2_int θ1)
+        (S21' : θ_Strength1_int θ2)
+        (S22' : θ_Strength2_int θ2).
 
 Lemma SumStrength1' : θ_Strength1_int θ.
 Proof.

UniMath/SubstitutionSystems/ContinuitySignature/CommutingOfOmegaLimitsAndCoproducts.v

@@ -48,7 +48,7 @@ Section OmegaLimitsCommutingWithCoproducts.
   Context {I : UU} (Iset : isaset I).
   Context (coproducts_given : Coproducts I C).
 
-  Variable (ind : I → cochain C).
+  Context (ind : I → cochain C).
 
   Let coproduct_n (n : nat) := coproducts_given (λ i, pr1 (ind i) n).
   Definition coproduct_n_cochain : cochain C.

UniMath/SubstitutionSystems/ContinuitySignature/ContinuityOfMultiSortedSigToFunctor.v

@@ -47,8 +47,8 @@ Local Open Scope cat.
 
 Section FixTheContext.
 
-  Variables (sort : UU) (Hsort : isofhlevel 3 sort) (C : category).
-  Variables (TC : Terminal C) (IC : Initial C)
+  Context (sort : UU) (Hsort : isofhlevel 3 sort) (C : category)
+          (TC : Terminal C) (IC : Initial C)
           (BP : BinProducts C) (BC : BinCoproducts C)
           (PC : forall (I : UU), Products I C) (CC : forall (I : UU), isaset I → Coproducts I C).
 
@@ -220,8 +220,8 @@ Section FixTheContext.
 
   Section OmegaContinuityOfMultiSortedSigToFunctorPrime.
 
-  Variable (LC : Lims_of_shape conat_graph C).
-  Variable (distr : ∏ I : HSET, ω_limits_distribute_over_I_coproducts C I LC (CC (pr1 I) (pr2 I))).
+  Context (LC : Lims_of_shape conat_graph C)
+          (distr : ∏ I : HSET, ω_limits_distribute_over_I_coproducts C I LC (CC (pr1 I) (pr2 I))).
 
   (* Should also be split up into multiple definitions/lemmas *)
   Lemma post_comp_with_pr_and_hat_is_omega_cont (s t : sort)

UniMath/SubstitutionSystems/ContinuitySignature/MultiSortedSignatureFunctorEquivalence.v

@@ -335,8 +335,8 @@ End A.
 
 Section EquivalenceBetweenDifferentCharacterizationsOfMultiSortedSignatureToFunctor.
 
-  Variables (sort : UU) (Hsort_set : isaset sort) (C : category).
-  Variables (TC : Terminal C) (IC : Initial C)
+  Context (sort : UU) (Hsort_set : isaset sort) (C : category)
+          (TC : Terminal C) (IC : Initial C)
           (BP : BinProducts C) (BC : BinCoproducts C)
           (PC : forall (I : UU), Products I C) (CC : forall (I : UU), isaset I → Coproducts I C).
 

UniMath/SubstitutionSystems/GenMendlerIteration.v

@@ -64,7 +64,7 @@ Defined.
 Notation "⟨ A , α ⟩" := (AlgConstr A α).
 (* \<  , \> *)
 
-Variable μF_Initial : Initial AF.
+Context (μF_Initial : Initial AF).
 
 Let μF : C := alg_carrier _ (InitialObject μF_Initial).
 Let inF : F μF --> μF := alg_map _ (InitialObject μF_Initial).
@@ -76,13 +76,12 @@ Context (C' : category).
 
 Section the_iteration_principle.
 
-Variable X : C'.
+Context (X : C').
 
 Let Yon : functor C'^op HSET := yoneda_objects C' X.
 
-Variable L : functor C C'.
-
-Variable is_left_adj_L : is_left_adjoint L.
+Context (L : functor C C')
+        (is_left_adj_L : is_left_adjoint L).
 
 Let φ := @φ_adj _ _ _ _ (pr2 is_left_adj_L).
 Let φ_inv := @φ_adj_inv _ _ _ _ (pr2 is_left_adj_L).
@@ -103,7 +102,7 @@ Definition ψ_target : functor C^op HSET := functor_composite (functor_opp F) ψ
 
 Section general_case.
 
-Variable ψ : ψ_source ⟹ ψ_target.
+Context (ψ : ψ_source ⟹ ψ_target).
 
 Definition preIt : L μF --> X := φ_inv (iter (φ (ψ (R X) (ε X)))).
 
@@ -214,9 +213,9 @@ End general_case.
 
 Section special_case.
 
-  Variable G : functor C' C'.
-  Variable ρ : G X --> X.
-  Variable θ : functor_composite F L ⟹ functor_composite L G.
+  Context (G : functor C' C')
+          (ρ : G X --> X)
+          (θ : functor_composite F L ⟹ functor_composite L G).
 
 
   Lemma is_nat_trans_ψ_from_comps
@@ -258,21 +257,21 @@ End the_iteration_principle.
 
 (** * Fusion law for Generalized Iteration in Mendler-style *)
 
-Variable X X': C'.
+Context (X X': C').
 Let Yon : functor C'^op HSET := yoneda_objects C' X.
 Let Yon' : functor C'^op HSET := yoneda_objects C' X'.
-Variable L : functor C C'.
-Variable is_left_adj_L : is_left_adjoint L.
-Variable ψ : ψ_source X L ⟹ ψ_target X L.
-Variable L' : functor C C'.
-Variable is_left_adj_L' : is_left_adjoint L'.
-Variable ψ' : ψ_source X' L' ⟹ ψ_target X' L'.
+Context (L : functor C C')
+        (is_left_adj_L : is_left_adjoint L)
+        (ψ : ψ_source X L ⟹ ψ_target X L)
+        (L' : functor C C')
+        (is_left_adj_L' : is_left_adjoint L')
+        (ψ' : ψ_source X' L' ⟹ ψ_target X' L')
 
-Variable Φ : functor_composite (functor_opp L) Yon ⟹ functor_composite (functor_opp L') Yon'.
+        (Φ : functor_composite (functor_opp L) Yon ⟹ functor_composite (functor_opp L') Yon').
 
 Section fusion_law.
 
-  Variable H : ψ μF · Φ (F μF) = Φ μF · ψ' μF.
+  Context (H : ψ μF · Φ (F μF) = Φ μF · ψ' μF).
 
   Theorem fusion_law : Φ μF (It X L is_left_adj_L ψ) = It X' L' is_left_adj_L' ψ'.
   Proof.

UniMath/SubstitutionSystems/GenMendlerIteration_alt.v

@@ -75,7 +75,7 @@ Context {D : category}.
 
 Section the_iteration_principle.
 
-Variables (X : D) (L : functor C D) (IL : isInitial D (L 0)) (HL : is_omega_cocont L).
+Context (X : D) (L : functor C D) (IL : isInitial D (L 0)) (HL : is_omega_cocont L).
 
 Let ILD : Initial D := tpair _ _ IL.
 Local Notation "'L0'" := (InitialObject ILD).
@@ -87,7 +87,7 @@ Definition ψ_target : functor C^op HSET := functor_composite (functor_opp F) ψ
 
 Section general_case.
 
-Variable (ψ : ψ_source ⟹ ψ_target).
+Context (ψ : ψ_source ⟹ ψ_target).
 
 Let LchnF : chain D := mapchain L chnF.
 Let z : D⟦L0,X⟧ := InitialArrow ILD X.
@@ -221,8 +221,8 @@ End general_case.
 (** * Specialized Mendler Iteration *)
 Section special_case.
 
-Variables (G : functor D D) (ρ : G X --> X).
-Variables (θ : functor_composite F L ⟹ functor_composite L G).
+Context (G : functor D D) (ρ : G X --> X)
+        (θ : functor_composite F L ⟹ functor_composite L G).
 
 Lemma is_nat_trans_ψ_from_comps :
         is_nat_trans ψ_source ψ_target
@@ -252,20 +252,20 @@ End the_iteration_principle.
 (** * Fusion law for Generalized Iteration in Mendler-style *)
 Section fusion_law.
 
-Variables (X X' : D).
+Context (X X' : D).
 
 Let Yon : functor D^op HSET := yoneda_objects D X.
 Let Yon' : functor D^op HSET := yoneda_objects D X'.
 
-Variables (L : functor C D) (HL : is_omega_cocont L) (IL : isInitial D (L 0)).
-Variables (ψ : ψ_source X L ⟹ ψ_target X L).
+Context (L : functor C D) (HL : is_omega_cocont L) (IL : isInitial D (L 0))
+        (ψ : ψ_source X L ⟹ ψ_target X L).
 
-Variables (L' : functor C D) (HL' : is_omega_cocont L') (IL' : isInitial D (L' 0)).
-Variables (ψ' : ψ_source X' L' ⟹ ψ_target X' L').
+Context (L' : functor C D) (HL' : is_omega_cocont L') (IL' : isInitial D (L' 0))
+        (ψ' : ψ_source X' L' ⟹ ψ_target X' L').
 
-Variables (Φ : functor_composite (functor_opp L) Yon ⟹ functor_composite (functor_opp L') Yon').
+Context (Φ : functor_composite (functor_opp L) Yon ⟹ functor_composite (functor_opp L') Yon').
 
-Variables (H : ψ μF · Φ (F μF) = Φ μF · ψ' μF).
+Context (H : ψ μF · Φ (F μF) = Φ μF · ψ' μF).
 
 Theorem fusion_law : Φ μF (It X L IL HL ψ) = It X' L' IL' HL' ψ'.
 Proof.

UniMath/SubstitutionSystems/Lam.v

@@ -58,10 +58,9 @@ Context (C : category).
 (** The category of endofunctors on [C] *)
 Local Notation "'EndC'":= ([C, C]) .
 
-Variable terminal : Terminal C.
-
-Variable CC : BinCoproducts C.
-Variable CP : BinProducts C.
+Context (terminal : Terminal C)
+        (CC : BinCoproducts C)
+        (CP : BinProducts C).
 
 Local Notation "'Ptd'" := (category_Ptd C).
 
@@ -74,18 +73,18 @@ Let CPEndEndC:= BinCoproducts_functor_precat _ _ CPEndC: BinCoproducts EndEndC.
 
 Let one : C :=  @TerminalObject C terminal.
 
-Variable KanExt : ∏ Z : precategory_Ptd C,
+Context (KanExt : ∏ Z : precategory_Ptd C,
    RightKanExtension.GlobalRightKanExtensionExists C C
-     (U Z) C.
+     (U Z) C).
 
 
 Let Lam_S : Signature _ _ _ := Lam_Sig C terminal CC CP.
 Let LamE_S : Signature _ _ _ := LamE_Sig C terminal CC CP.
 
 (* assume initial algebra for signature Lam *)
 
-Variable Lam_Initial : Initial
-     (@category_FunctorAlg [C, C] (Id_H C CC Lam_S)).
+Context (Lam_Initial : Initial
+     (@category_FunctorAlg [C, C] (Id_H C CC Lam_S))).
 
 Let Lam := InitialObject Lam_Initial.
 
@@ -508,9 +507,9 @@ Defined.
 
 (* assume initial algebra for signature LamE *)
 
-Variable  LamE_Initial : Initial
+Context (LamE_Initial : Initial
      (@category_FunctorAlg [C, C]
-        (Id_H C CC LamE_S)).
+        (Id_H C CC LamE_S))).
 
 
 Definition LamEHSS_Initial : Initial (hss_category CC LamE_S).

UniMath/SubstitutionSystems/LamSignature.v

@@ -52,25 +52,22 @@ Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits.
 
 Section Preparations.
 
-Variable C : category.
-Variable CP : BinProducts C.
-Variable CC : BinCoproducts C.
+Context (C : category) (CP : BinProducts C) (CC : BinCoproducts C).
 
 Definition square_functor := BinProduct_of_functors C C CP (functor_identity C) (functor_identity C).
 
 End Preparations.
 
 Section Lambda.
 
-Variable C : category.
+Context (C : category).
 
 (** The category of endofunctors on [C] *)
 Local Notation "'EndC'":= ([C, C]) .
 
-Variable terminal : Terminal C.
-
-Variable CC : BinCoproducts C.
-Variable CP : BinProducts C.
+Context (terminal : Terminal C)
+        (CC : BinCoproducts C)
+        (CP : BinProducts C).
 
 Let one : C :=  @TerminalObject C terminal.
 

UniMath/SubstitutionSystems/LiftingInitial.v

@@ -70,9 +70,9 @@ Let EndEndC := [EndC, EndC].
 Let CPEndEndC:= BinCoproducts_functor_precat _ _ CPEndC: BinCoproducts EndEndC.
 
 
-Variable KanExt : ∏ Z : Ptd, GlobalRightKanExtensionExists _ _ (U Z) C.
+Context (KanExt : ∏ Z : Ptd, GlobalRightKanExtensionExists _ _ (U Z) C).
 
-Variable H : Presignature C C C.
+Context (H : Presignature C C C).
 Let θ := theta H.
 
 Definition Const_plus_H (X : EndC) : functor EndC EndC
@@ -85,7 +85,8 @@ Definition Id_H :  functor [C, C] [C, C]
 Let Alg : category := FunctorAlg Id_H.
 
 
-Variable IA : Initial Alg.
+Context (IA : Initial Alg).
+
 Definition SpecializedGMIt (Z : Ptd) (X : EndC)
   :  ∏ (G : functor [C, C] [C, C])
        (ρ : [C, C] ⟦ G X, X ⟧)

UniMath/SubstitutionSystems/LiftingInitial_alt.v

@@ -50,8 +50,8 @@ Local Coercion alg_carrier : algebra_ob >-> ob.
 
 Section category_Algebra.
 
-Variables (C : category) (CP : BinCoproducts C).
-Variables (IC : Initial C) (CC : Colims_of_shape nat_graph C).
+Context (C : category) (CP : BinCoproducts C)
+        (IC : Initial C) (CC : Colims_of_shape nat_graph C).
 
 Local Notation "'EndC'":= ([C, C]) .
 Local Notation "'Ptd'" := (category_Ptd C).