Merge pull request #149 from rmatthes/propagateremovalofprecategoriesfrommodules

makes this satellite compile again after merging UniMath PR #1728

Author: benediktahrens

Modules/Prelims/DerivationIsFunctorial.v

@@ -87,10 +87,10 @@ MR(X+o)) --------->  NR(X+o)
   Proof.
     split.
     - intro M.
-      apply LModule_Mor_equiv;[exact D|].
+      apply LModule_Mor_equiv.
       apply pre_whisker_identity.
     - intros M N O f g.
-      apply LModule_Mor_equiv;[exact D|].
+      apply LModule_Mor_equiv.
       apply pre_whisker_composition.
   Qed.
 
@@ -149,7 +149,7 @@ f := η ∘ in₁
   Lemma LModule_to_deriv_is_nt : is_nat_trans (functor_identity _) ∂ LModule_to_deriv.
   Proof.
     intros M N f.
-    apply (LModule_Mor_equiv _ D).
+    apply LModule_Mor_equiv.
     apply (nat_trans_eq D).
     intro c.
     cbn.

Modules/Prelims/LModulesBinProducts.v

@@ -137,14 +137,14 @@ Local Notation σ := (lm_mult _).
         (g : LMOD ⟦ S, N ⟧) :
     (LModule_BinProductArrow S f g : LMOD ⟦_ , _⟧) · LModule_binproductPr1 = f.
   Proof.
-    apply LModule_Mor_equiv; [exact C |].
+    apply LModule_Mor_equiv.
     apply (BinProductPr1Commutes _ _ _ bpFunct).
   Qed.
   Lemma LModule_BinProductPr2Commutes (S : LMOD) (f : LMOD ⟦ S, M ⟧)
         (g : LMOD ⟦ S, N ⟧) :
     (LModule_BinProductArrow S f g : LMOD ⟦_ , _⟧) · LModule_binproductPr2 = g.
   Proof.
-    apply LModule_Mor_equiv; [exact C |].
+    apply LModule_Mor_equiv.
     apply (BinProductPr2Commutes _ _ _ bpFunct).
   Qed.
 
@@ -162,10 +162,10 @@ Local Notation σ := (lm_mult _).
     - intro y.
       apply isapropdirprod; apply has_homsets_LModule.
     - intros y [h1 h2].
-      apply LModule_Mor_equiv; [exact C |].
+      apply LModule_Mor_equiv.
       apply (BinProductArrowUnique _ _ _ bpFunct).
-      +  exact ((LModule_Mor_equiv _ C _ _ ) h1).
-      +  exact ((LModule_Mor_equiv _ C _ _ ) h2).
+      +  exact ((LModule_Mor_equiv _ _ _ ) h1).
+      +  exact ((LModule_Mor_equiv _ _ _ ) h2).
   Defined.
   Definition LModule_ProductCone : BinProduct LMOD M N  :=
     make_BinProduct LMOD M N LModule_binproduct
@@ -212,7 +212,7 @@ Section pullback_binprod.
   Defined.
 
   Definition binprod_pbm_to_pbm_iso : iso (C:= precategory_LModule _ _)  binprod_pbm pbm_binprod :=
-    LModule_same_func_iso _ _ binprod_pbm_to_pbm_eq_mult (homset_property _).
+    LModule_same_func_iso _ _ binprod_pbm_to_pbm_eq_mult.
 
   Definition binprod_pbm_to_pbm_binprod : LModule_Mor  _ binprod_pbm pbm_binprod :=
     morphism_from_iso binprod_pbm_to_pbm_iso.

Modules/Prelims/LModulesColims.v

@@ -431,15 +431,13 @@ qu'on complète par propriété de [d e] en temps que morphisme de module
     dmor d e · LModule_coconeIn v = LModule_coconeIn u.
   Proof.
     apply LModule_Mor_equiv.
-    - exact C.
-    - apply (coconeInCommutes (colimCocone (coFunc d'))).
+    apply (coconeInCommutes (colimCocone (coFunc d'))).
   Defined.
   Lemma LModule_coneOut_commutes (u v : vertex g) (e : edge u v) :
       LModule_coneOut u · dmor d e = LModule_coneOut v.
   Proof.
     apply LModule_Mor_equiv.
-    - exact C.
-    - apply (coneOutCommutes (limCone (limFunc d'))).
+    apply (coneOutCommutes (limCone (limFunc d'))).
   Defined.
 
 
@@ -510,7 +508,7 @@ qu'on complète par propriété de [d e] en temps que morphisme de module
     use unique_exists.
     - exact (LModule_colimArrow cc).
     - intro v.
-      apply LModule_Mor_equiv;[exact C|].
+      apply LModule_Mor_equiv.
       apply (colimArrowCommutes (coFunc d')).
     - intro y.
       cbn -[isaprop].
@@ -519,7 +517,7 @@ qu'on complète par propriété de [d e] en temps que morphisme de module
       use has_homsets_LModule.
     - cbn.
       intros y h.
-      apply LModule_Mor_equiv;[exact C|].
+      apply LModule_Mor_equiv.
       apply (colimArrowUnique (coFunc d')).
       intro u.
       exact (  maponpaths pr1 (h u)).
@@ -530,7 +528,7 @@ qu'on complète par propriété de [d e] en temps que morphisme de module
     use unique_exists.
     - exact (LModule_limArrow cc).
     - intro v.
-      apply LModule_Mor_equiv;[exact C|].
+      apply LModule_Mor_equiv.
       apply (limArrowCommutes (limFunc d')).
     - intro y.
       cbn -[isaprop].
@@ -539,7 +537,7 @@ qu'on complète par propriété de [d e] en temps que morphisme de module
       use has_homsets_LModule.
     - cbn.
       intros y h.
-      apply LModule_Mor_equiv;[exact C|].
+      apply LModule_Mor_equiv.
       apply (limArrowUnique (limFunc d')).
       intro u.
       exact (  maponpaths pr1 (h u)).
@@ -622,8 +620,8 @@ Section pullback_lims.
   Qed.
 
   Definition pb_LModule_colim_iso : iso (C := MOD R) cR (pb_LModule f cS) :=
-    LModule_same_func_iso _ _ pb_colims_eq_mult (homset_property _).
+    LModule_same_func_iso _ _ pb_colims_eq_mult.
 
   Definition pb_LModule_lim_iso : iso (C := MOD R) lR (pb_LModule f lS) :=
-    LModule_same_func_iso _ _ pb_lims_eq_mult (homset_property _).
+    LModule_same_func_iso _ _ pb_lims_eq_mult.
 End pullback_lims.

Modules/Prelims/LModulesComplements.v

@@ -11,7 +11,7 @@ Require Import UniMath.CategoryTheory.Monads.LModules.
 
 (** strangely enough, I didn't find the following lemma : 
  *) 
-Lemma monad_mor_to_lmodule_law {C : precategory} {R S : Monad C} 
+Lemma monad_mor_to_lmodule_law {C : category} {R S : Monad C} 
            (f : Monad_Mor R S) : 
   LModule_Mor_laws R (T := tautological_LModule R) 
                    (T' := pb_LModule f (tautological_LModule S)) f. 
@@ -24,6 +24,6 @@ Proof.
   apply Monad_Mor_μ. 
 Qed. 
 
-Definition monad_mor_to_lmodule {C : precategory} {R S : Monad C} 
+Definition monad_mor_to_lmodule {C : category} {R S : Monad C} 
   (f : Monad_Mor R S) : LModule_Mor R (tautological_LModule R) (pb_LModule f (tautological_LModule S)) 
-  := (f : nat_trans _ _) ,, monad_mor_to_lmodule_law f. 
+  := (f : nat_trans _ _) ,, monad_mor_to_lmodule_law f. 

Modules/Prelims/LModulesCoproducts.v

@@ -144,7 +144,7 @@ Section ColimsModule.
     use unique_exists.
     - exact (LModule_coproductArrow cc).
     - intro v.
-      apply LModule_Mor_equiv;[exact C|].
+      apply LModule_Mor_equiv.
       apply (CoproductInCommutes _ _ _ (cpFunc d')).
     - intro y.
       cbn -[isaprop].
@@ -153,7 +153,7 @@ Section ColimsModule.
       use has_homsets_LModule.
     - cbn.
       intros y h.
-      apply LModule_Mor_equiv;[exact C|].
+      apply LModule_Mor_equiv.
       apply (CoproductArrowUnique _ _ _ (cpFunc d')).
       intro u.
       exact (  maponpaths pr1 (h u)).

Modules/Prelims/LModulesFibration.v

@@ -48,7 +48,7 @@ Proof.
     apply pb_LModule_id_iso.
   - intros x y z f g xx yy zz ff gg.
     set (pbm_g := pb_LModule_Mor f gg).
-    set (pbm_gf := (LModule_composition _ pbm_g (morphism_from_iso (pb_LModule_comp_iso f g _ _)))).
+    set (pbm_gf := (LModule_composition _ pbm_g (morphism_from_iso (pb_LModule_comp_iso f g _)))).
     simpl in ff.
     exact (compose (C:=category_LModule _ _ ) ff pbm_gf).
 Defined.
@@ -75,7 +75,7 @@ Proof.
   repeat apply tpair; intros; try apply homset_property.
   - simpl.
     unfold id_disp; simpl.
-    apply (invmap ((@LModule_Mor_equiv _ x _ (homset_property D) _ _ _ _  ))).
+    apply (invmap ((@LModule_Mor_equiv _ x _ _ _ _ _))).
     apply nat_trans_eq; try apply homset_property.
     intros c; simpl.
     simpl.
@@ -84,7 +84,7 @@ Proof.
     etrans; [apply bmod_transport |].
     rewrite id_right,id_left; apply idpath.
   - set (heqf := id_right f).
-    apply (invmap ((@LModule_Mor_equiv _ x _ (homset_property D) _ _ _ _  ))).
+    apply (invmap ((@LModule_Mor_equiv _ x _ _ _ _ _))).
     apply nat_trans_eq; try apply homset_property.
     simpl.
     intros c.
@@ -94,7 +94,7 @@ Proof.
     intros; simpl.
     reflexivity.
   - set (heqf:= assoc f g h).
-    apply (invmap ((@LModule_Mor_equiv _ x _ (homset_property D) _ _ _ _  ))).
+    apply (invmap ((@LModule_Mor_equiv _ x _ _ _ _ _))).
     apply nat_trans_eq; try apply homset_property.
     intros c; simpl.
     apply pathsinv0.
@@ -118,9 +118,9 @@ Proof.
       cbn in *.
       use unique_exists.
       * use (LModule_composition R'' a). 
-        exact ( inv_from_iso (pb_LModule_comp_iso (C := D) f' f M _)).
+        exact ( inv_from_iso (pb_LModule_comp_iso (C := D) f' f M)).
       * hnf.
-        apply (invmap ((@LModule_Mor_equiv _ _  _ (homset_property D) _ _ _ _  ))).
+        apply (invmap ((@LModule_Mor_equiv _ _  _ _ _ _ _  ))).
         cbn.
         apply nat_trans_eq. { apply homset_property. }
         intro c. cbn. 
@@ -129,10 +129,10 @@ Proof.
         apply (has_homsets_LModule).
       * intros s Hs.
         hnf in Hs.
-        apply (invmap ((@LModule_Mor_equiv _ _  _ (homset_property D) _ _ _ _  ))).
+        apply (invmap ((@LModule_Mor_equiv _ _  _ _ _ _ _  ))).
         apply nat_trans_eq. { apply homset_property. }
         intro c. cbn.
-        apply (((@LModule_Mor_equiv _ _  _ (homset_property D) _ _ _ _  ))) in Hs.
+        apply (((@LModule_Mor_equiv _ _  _ _ _ _ _  ))) in Hs.
         set (XR := nat_trans_eq_pointwise Hs c). cbn in XR.
         repeat rewrite id_right in XR.
         repeat rewrite id_right.

Modules/Prelims/deriveadj.v

@@ -324,7 +324,7 @@ et on utilise les 2 lois de monades
   Proof.
     intros M M' m.
     simpl in M,M',m.
-    apply LModule_Mor_equiv;[exact hsS|].
+    apply LModule_Mor_equiv.
     apply nat_trans_eq;[exact hsS|].
     intro X.
     apply funextfun.
@@ -495,7 +495,7 @@ R(T+RX) -------> RR(T+X)
                                                  deriv_counit_data.
   Proof.
     intros M N m.
-    apply LModule_Mor_equiv;[exact hsC|].
+    apply LModule_Mor_equiv.
     apply nat_trans_eq;[exact hsC|].
     intro x.
     unfold compose.
@@ -566,7 +566,7 @@ Section derivadj.
     split.
     - intro M.
       cbn in M.
-      apply LModule_Mor_equiv;[exact hsS|].
+      apply LModule_Mor_equiv.
       apply nat_trans_eq;[exact hsS|].
       intro X.
       cbn -[isasetcoprod].
@@ -603,7 +603,7 @@ Section derivadj.
         apply (Monad_law1  (T := R)).
     - intro M.
       cbn in M.
-      apply LModule_Mor_equiv;[exact hsS|].
+      apply LModule_Mor_equiv.
       apply nat_trans_eq;[exact hsS|].
       intro X.
       cbn -[isasetcoprod].
@@ -750,7 +750,7 @@ Local Lemma adj_law1 : (∏ (R S : Monad SET) (f : Monad_Mor R S) (M N : LModule
       (tautological_LModule R), N ⟧) · v).
 Proof.
   intros R S f M N A u v.
-  apply LModule_Mor_equiv;[apply (homset_property SET)|].
+  apply LModule_Mor_equiv.
   apply nat_trans_eq;[apply (homset_property SET)|].
   intros X.
   apply funextfun.
@@ -803,7 +803,7 @@ Local Lemma adj_law2 :
    pb_LModule_Mor f ((adj1 S A B) v)).
 Proof.
   intros.
-  apply LModule_Mor_equiv;[apply (homset_property SET)|].
+  apply LModule_Mor_equiv.
   apply nat_trans_eq;[apply (homset_property SET)|].
   intro X.
   cbn -[isasetcoprod].

Modules/Signatures/EpiArePointwise.v

@@ -43,7 +43,7 @@ Section pwEpiAr.
     intros x y z e.
     apply signature_Mor_eq.
     intro R.
-    apply LModule_Mor_equiv;[apply homset_property|].
+    apply LModule_Mor_equiv.
     apply hepi.
     exact (maponpaths (T1 := signature_Mor _ _) (fun z => (z R : nat_trans _ _)) e).
   Qed.
@@ -112,7 +112,7 @@ Proof.
     cbn in f,g.
     apply signature_Mor_eq.
     intro R.
-    apply LModule_Mor_equiv; [apply homset_property|].
+    apply LModule_Mor_equiv.
     apply epiF.
     exact (maponpaths (T1 := signature_Mor _ _) (fun h => pr1 (h R)) eqf).
 Qed.

Modules/Signatures/EpiSigRepresentability.v

@@ -521,7 +521,6 @@ Proof.
   apply LModule_Mor_equiv in h.
   eapply nat_trans_eq_pointwise in h.
   apply h.
-  apply homset_property.
   etrans;revgoals.
   etrans;[|apply assoc].
   apply cancel_precomposition.

Modules/Signatures/HssSignatureCommutation.v

@@ -85,7 +85,7 @@ Section GenericStrat.
     iso (C := category_LModule R _)
         (S1 R)
         ( S2 R) :=
-    LModule_same_func_iso _ _ (m12_eq _) _.
+    LModule_same_func_iso _ _ (m12_eq _).
 
 
   Hypothesis (Sf12_eq : ∏ R S f c, (Sf2 R S f c)  = (Sf1 R S f c) ).