From 93d0e0630aafd1909b25290ad451e3c65e31bce4 Mon Sep 17 00:00:00 2001
From: Ralph Matthes <rmatthes@users.noreply.github.com>
Date: Fri, 21 Jul 2023 19:01:44 +0200
Subject: [PATCH] makes this satellite compile again after merging UniMath
 PR1739

only small adaptations
---
 Modules/Prelims/quotientmonad.v             |  8 +++----
 Modules/Prelims/quotientmonadslice.v        |  4 +++-
 Modules/Signatures/EpiSigRepresentability.v | 14 ++++++------
 Modules/Signatures/ModelCat.v               | 14 ++++++------
 Modules/Signatures/Signature.v              | 25 ++++++++++-----------
 Modules/SoftEquations/CatOfTwoSignatures.v  |  2 +-
 6 files changed, 34 insertions(+), 33 deletions(-)

diff --git a/Modules/Prelims/quotientmonad.v b/Modules/Prelims/quotientmonad.v
index 4bbb298..7896912 100644
--- a/Modules/Prelims/quotientmonad.v
+++ b/Modules/Prelims/quotientmonad.v
@@ -70,7 +70,7 @@ is so slow when R' is definitely equal to quot_functor !
 ----
 *)
 
-Definition R': functor SET SET := quot_functor (pr1 (pr1 R)) _ congr_equivc.
+Definition R': functor SET SET := quot_functor (pr1 R) _ congr_equivc.
 
 Definition projR : (R:functor _ _) ⟹ R' := pr_quot_functor _ _ congr_equivc.
 
@@ -169,7 +169,7 @@ Proof.
   apply univ_surj_nt_ax_pw.
 Qed.
 
-Definition R'_Monad_data : Monad_data SET := ((R' ,, R'_μ) ,, R'_η).
+Definition R'_Monad_data : disp_Monad_data R' := (R'_μ ,, R'_η).
 
  
 
@@ -339,7 +339,7 @@ Legend of the diagram :
   apply assoc_ppprojR.
 Qed.
 
-Lemma R'_Monad_laws : Monad_laws R'_Monad_data.
+Lemma R'_Monad_laws : disp_Monad_laws R'_Monad_data.
 Proof.
   repeat split.
   -  apply R'_Monad_law_η1.
@@ -349,7 +349,7 @@ Qed.
 
 (* Le QED précédent prend énormément de temps.. pourquoi ? *)
 
-Definition R'_monad : Monad _ := _ ,, R'_Monad_laws.
+Definition R'_monad : Monad _ := _ ,, _ ,, R'_Monad_laws.
 
 (*
 FIN DE LA PREMIERE ETAPE
diff --git a/Modules/Prelims/quotientmonadslice.v b/Modules/Prelims/quotientmonadslice.v
index 044fa75..bbd96ef 100644
--- a/Modules/Prelims/quotientmonadslice.v
+++ b/Modules/Prelims/quotientmonadslice.v
@@ -63,6 +63,8 @@ Section QuotientMonad.
 
   Context {R : Monad SET}.
 
+  Local Definition R0 : functor SET SET := R.
+
 (**
   R preserves epimorphisms.
     This is needed to prove the the horizontal composition of the
@@ -141,7 +143,7 @@ Let projR := projR  congr_equivc.
     of actions
 *)
 Lemma compat_slice (j : J) ( m := ff j)
-  : ∏ (X : SET) (x y : (pr1 R X : hSet)),
+  : ∏ (X : SET) (x y : (R0 X : hSet)),
     projR X x = projR X y → m X x =  m X y.
 Proof.
   intros X x y eqpr.
diff --git a/Modules/Signatures/EpiSigRepresentability.v b/Modules/Signatures/EpiSigRepresentability.v
index 41b5fc6..fcf5686 100644
--- a/Modules/Signatures/EpiSigRepresentability.v
+++ b/Modules/Signatures/EpiSigRepresentability.v
@@ -88,7 +88,7 @@ Example EpiSignatureThetaTheta
 Proof.
   intro hepi.
   apply is_nat_trans_epi_from_pointwise_epis.
-  assert (hf : ∏ x, isEpi (pr1 f x)).
+  assert (hf : ∏ x, isEpi (pr1 (pr1 f) x)).
   {
     apply epi_nt_SET_pw.
     exact hepi.
@@ -196,7 +196,7 @@ Definition u {S : REP b} (m : R -->[ F] S)
   := u_monad R_epi dd ff (S ,, m) .
 
 (** The induced natural transformation makes a triangle commute *)
-Lemma u_def {S : REP b} (m : R -->[ F] S) : ∏ x, ## m x = projR x · u m x.
+Lemma u_def {S : REP b} (m : R -->[ F] S) : ∏ x, pr1 (## m) x = projR x · u m x.
 Proof.
   apply (u_def dd ff (S ,, m)).
 Qed.
@@ -223,7 +223,7 @@ Lemma Rep_mor_is_composition
       {S : REP b} (m : R -->[ F] S)
   : pr1 m = compose (C:=category_Monad _) projR (u m) .
 Proof.
-  use (invmap (Monad_Mor_equiv _ _ _)).
+  use (invmap (Monad_Mor_equiv _ _)).
   apply nat_trans_eq.
   - apply (homset_property SET).
   - intro X'.
@@ -248,7 +248,7 @@ Qed.
 
 Lemma eq_mr
       {S : REP b} (m : R -->[ F] S) (X : SET)
-  : model_τ R X · ## m X 
+  : model_τ R X · pr1 (## m) X 
     =
     pr1 (# a projR)%ar X · (F (R' ))%ar X 
         ·
@@ -511,7 +511,7 @@ Proof.
   apply cancel_postcomposition.
   etrans.
   apply (cancel_ar_on _ (compose (C:=category_Monad _) projR (u m))).
-  use (invmap (Monad_Mor_equiv _ _ _)).
+  use (invmap (Monad_Mor_equiv _ _)).
   (* { apply homset_property. } *)
   { apply nat_trans_eq.
     apply homset_property.
@@ -571,9 +571,9 @@ Lemma helper
       (S : model b)
   : ∏ (u' : Rep_b ⟦ rep_of_b_in_R' R R_epi epiab cond_F, S ⟧) x,
     projR R R_epi x · (u' : model_mor_mor _ _ _ _ _) x =
-    pr1 (pr1 (compose (C:=Rep_a) (b:=FF (rep_of_b_in_R' R R_epi epiab cond_F))
+    pr1 (compose (C:=Rep_a) (b:=FF (rep_of_b_in_R' R R_epi epiab cond_F))
                       (projR_rep R R_epi epiab cond_F : model_mor_mor _ _ _ _ _)
-                      (# FF u'))) x.
+                      (# FF u')) x.
 Proof.
   intros u' x.
   apply pathsinv0.
diff --git a/Modules/Signatures/ModelCat.v b/Modules/Signatures/ModelCat.v
index 1e7820c..2b296fa 100644
--- a/Modules/Signatures/ModelCat.v
+++ b/Modules/Signatures/ModelCat.v
@@ -73,7 +73,7 @@ Lemma isaset_rep_fiber_mor {a : SIG} (M N : model a)  :
 Proof.
   intros.
   apply isaset_total2 .
-  - apply has_homsets_Monad.
+  - apply isaset_Monad_Mor.
   - intros.
     apply isasetaprop.
     apply isaprop_rep_fiber_mor_law.
@@ -99,14 +99,14 @@ Proof.
   use (invmap (subtypeInjectivity _ _ _ _  )). 
   - intro g.
     apply isaprop_rep_fiber_mor_law.
-  - use (invmap (Monad_Mor_equiv _ _  _  )).  
+  - use (invmap (Monad_Mor_equiv _ _)).  
      +  assumption.
 Qed.
 
 (** If two 1-model morphisms are pointwise equal, then they are equal *)
 Lemma rep_fiber_mor_eq {a : SIG} (R S:model a)
       (u v: rep_fiber_mor R S) :
-  (∏ c, pr1 (pr1 u) c = pr1 (pr1 v) c) -> u = v.
+  (∏ c, pr1 u c = pr1 v c) -> u = v.
 Proof.
   intros.
   apply rep_fiber_mor_eq_nt.
@@ -407,8 +407,8 @@ M (M + Id) ---------> M R --------> M
   Defined.
 
   (** Data for the (M + Id) monad *)
-  Definition mod_id_monad_data : Monad_data C :=
-    ((IdM ,, mod_id_μ) ,, mod_id_η).
+  Definition mod_id_monad_data : disp_Monad_data IdM :=
+    (mod_id_μ ,, mod_id_η).
 
   Local Infix "++f" := (BinCoproductOfArrows _ _ _) (at level 6).
   Local Notation "[[ f , g ]]" := (BinCoproductArrow _ f g).
@@ -506,7 +506,7 @@ M (M + Id) ---------> M R --------> M
 
 
   (** Monad laws for (M + Id) *)
-  Lemma mod_id_monad_laws : Monad_laws mod_id_monad_data.
+  Lemma mod_id_monad_laws : disp_Monad_laws mod_id_monad_data.
   Proof.
     repeat split.
     - intro c.
@@ -584,7 +584,7 @@ M (M + Id) ---------> M R --------> M
   
 
   (** The M + Id monad *)
-  Definition mod_id_monad : Monad C := _ ,, mod_id_monad_laws.
+  Definition mod_id_monad : Monad C := _ ,, _ ,, mod_id_monad_laws.
 
   (** The morphism M + Id  --> R is a monad morphism *)
   Lemma mod_id_monad_mor_laws : Monad_Mor_laws (T := mod_id_monad) mod_id_nt.
diff --git a/Modules/Signatures/Signature.v b/Modules/Signatures/Signature.v
index e146006..a8d4cee 100644
--- a/Modules/Signatures/Signature.v
+++ b/Modules/Signatures/Signature.v
@@ -385,7 +385,7 @@ Lemma isaset_model_mor_mor (a b : SIGNATURE) (M : model a) (N : model b) f :
 Proof.
   intros.
   apply isaset_total2 .
-  - apply has_homsets_Monad.
+  - apply isaset_Monad_Mor.
   - intros.
     apply isasetaprop.
     apply isaprop_model_mor_law.
@@ -404,7 +404,7 @@ Definition rep_disp_ob_mor : disp_cat_ob_mor PRECAT_SIGNATURE :=
   (model,, model_mor_mor).
 
 Lemma rep_id_law (a : SIGNATURE) (RM : rep_disp_ob_mor a) :
-  model_mor_law RM RM (identity (C:=PRECAT_SIGNATURE) _) (Monad_identity _).
+  model_mor_law RM RM (identity (C:=PRECAT_SIGNATURE) _) (identity _).
 Proof.
   intro c.
   apply pathsinv0.
@@ -421,7 +421,7 @@ Definition rep_id  (a : SIGNATURE) (RM : rep_disp_ob_mor a) :
   RM -->[ identity (C:=PRECAT_SIGNATURE) a] RM.
 Proof.
   intros.
-  exists (Monad_identity _).
+  exists (identity _).
   apply rep_id_law.
 Defined.
 
@@ -432,8 +432,7 @@ Lemma transport_signature_mor (x y : SIGNATURE) (f g : signature_Mor x y)
       (xx : rep_disp_ob_mor x)
       (yy : rep_disp_ob_mor y)
       (ff : xx -->[ f] yy)
-      (c : C) :
-  pr1 (pr1 (transportf (mor_disp xx yy) e ff)) c = pr1 (pr1 ff) c.
+      (c : C) : pr1 (transportf (mor_disp xx yy) e ff) c = pr1 ff c.
 Proof.
   induction e.
   apply idpath.
@@ -446,13 +445,13 @@ Qed.
 Lemma model_mor_mor_equiv (a b : SIGNATURE) (R:rep_disp_ob_mor a)
       (S:rep_disp_ob_mor b) (f:signature_Mor a b)
       (u v: R -->[ f] S) :
-  (∏ c, pr1 (pr1 u) c = pr1 (pr1 v) c) -> u = v.
+  (∏ c, pr1 u c = pr1 v c) -> u = v.
 Proof.
   intros.
   use (invmap (subtypeInjectivity _ _ _ _  )). 
   - intro g.
     apply isaprop_model_mor_law.
-  - use (invmap (Monad_Mor_equiv _ _  _  )).  
+  - use (invmap (Monad_Mor_equiv _ _)).  
      +  apply nat_trans_eq.
         apply homset_property.
         assumption.
@@ -544,12 +543,12 @@ Proof.
   - set (heqf:= assoc f g h).
     apply model_mor_mor_equiv.
     intros c.
-    etrans. Focus 2.
-      symmetry.
-      apply transport_signature_mor.
-      cbn.
-      rewrite assoc.
-      apply idpath.
+    etrans.
+    2: { symmetry.
+         apply transport_signature_mor. }
+    cbn.
+    rewrite assoc.
+    apply idpath.
   - apply isaset_model_mor_mor.
 Qed.
 
diff --git a/Modules/SoftEquations/CatOfTwoSignatures.v b/Modules/SoftEquations/CatOfTwoSignatures.v
index d079cee..d756fc4 100644
--- a/Modules/SoftEquations/CatOfTwoSignatures.v
+++ b/Modules/SoftEquations/CatOfTwoSignatures.v
@@ -380,7 +380,7 @@ Lemma transport_signature_mor (x y : TwoSignature) (f g :  x →→ y)
       (yy : two_model_disp_ob_mor y)
       (ff : xx -->[ f] yy)
       (c : C) :
-  pr1 (pr1 (transportf (mor_disp xx yy) e ff)) c = pr1 (pr1 ff) c.
+  pr1 (transportf (mor_disp xx yy) e ff) c = pr1 ff c.
 Proof.
   induction e.
   apply idpath.