From c830a8ba2c0d589a363218867962a2fcf06eefa2 Mon Sep 17 00:00:00 2001
From: gio256 <102917377+gio256@users.noreply.github.com>
Date: Mon, 19 Feb 2024 12:19:54 -0700
Subject: [PATCH 1/2] Fix resolution in WildCat/DisplayedEquiv.v

---
 theories/WildCat/DisplayedEquiv.v | 14 +++++++-------
 theories/WildCat/Equiv.v          |  1 +
 2 files changed, 8 insertions(+), 7 deletions(-)

diff --git a/theories/WildCat/DisplayedEquiv.v b/theories/WildCat/DisplayedEquiv.v
index 3a207682f58..51e6b3a5b31 100644
--- a/theories/WildCat/DisplayedEquiv.v
+++ b/theories/WildCat/DisplayedEquiv.v
@@ -17,11 +17,11 @@ Class DHasEquivs {A : Type} `{HasEquivs A}
     DCatEquiv f a' b' -> DHom f a' b';
   dcate_isequiv : forall {a b} {f : a $<~> b} {a'} {b'}
     (f' : DCatEquiv f a' b'), DCatIsEquiv (dcate_fun f');
-  dcate_buildequiv : forall {a b} {f : a $-> b} `{!CatIsEquiv f} {a'} {b'}
+  dcate_buildequiv : forall {a b} {f : a $-> b} {fe : CatIsEquiv f} {a'} {b'}
     (f' : DHom f a' b') {fe' : DCatIsEquiv f'},
-    DCatEquiv (Build_CatEquiv f) a' b';
-  dcate_buildequiv_fun : forall {a b} {f : a $-> b} `{!CatIsEquiv f}
-    {a'} {b'} (f' : DHom f a' b') {fe' : DCatIsEquiv f'},
+    DCatEquiv (Build_CatEquiv (fe:=fe) f) a' b';
+  dcate_buildequiv_fun : forall {a b} {f : a $-> b} {fe : CatIsEquiv f}
+    {a'} {b'} (f' : DHom f a' b') {fe' : DCatIsEquiv (fe:=fe) f'},
     DGpdHom (cate_buildequiv_fun f)
     (dcate_fun (dcate_buildequiv f' (fe':=fe'))) f';
   dcate_inv' : forall {a b} {f : a $<~> b} {a'} {b'} (f' : DCatEquiv f a' b'),
@@ -44,8 +44,8 @@ Global Existing Instance dcate_isequiv.
 Coercion dcate_fun : DCatEquiv >-> DHom.
 
 Definition Build_DCatEquiv {A} {D : A -> Type} `{DHasEquivs A D}
-  {a b : A} {f : a $-> b} `{!CatIsEquiv f} {a' : D a} {b' : D b}
-  (f' : DHom f a' b') {fe' : DCatIsEquiv f'}
+  {a b : A} {f : a $-> b} {fe : CatIsEquiv f} {a' : D a} {b' : D b}
+  (f' : DHom f a' b') {fe' : DCatIsEquiv (fe:=fe) f'}
   : DCatEquiv (Build_CatEquiv f) a' b'
   := dcate_buildequiv f' (fe':=fe').
 
@@ -142,7 +142,7 @@ Proof.
   snrapply Build_HasEquivs.
   1:{ intros [a a'] [b b']. exact {f : a $<~> b & DCatEquiv f a' b'}. }
   all: intros aa' bb' [f f'].
-  - exact {fe : CatIsEquiv f & DCatIsEquiv f'}.
+  - exact {fe : CatIsEquiv f & DCatIsEquiv (fe:=fe) f'}.
   - exists f. exact f'.
   - exact (cate_isequiv f; dcate_isequiv f').
   - intros [fe fe'].
diff --git a/theories/WildCat/Equiv.v b/theories/WildCat/Equiv.v
index bbb35f95ff4..c73f85761ed 100644
--- a/theories/WildCat/Equiv.v
+++ b/theories/WildCat/Equiv.v
@@ -31,6 +31,7 @@ Class HasEquivs (A : Type) `{Is1Cat A} :=
 Existing Class CatIsEquiv.
 Arguments CatIsEquiv {A _ _ _ _ _ a b} f.
 Global Existing Instance cate_isequiv.
+Arguments cate_isequiv {A _ _ _ _ _ a b} f.
 
 (** Since apparently a field of a record can't be the source of a coercion (Coq complains about the uniform inheritance condition, although as officially stated that condition appears to be satisfied), we redefine all the fields of [HasEquivs]. *)
 

From 8b15ef2cea17d27e29a5f479dab6a4e4fc74618e Mon Sep 17 00:00:00 2001
From: gio256 <102917377+gio256@users.noreply.github.com>
Date: Mon, 19 Feb 2024 16:32:47 -0700
Subject: [PATCH 2/2] Wildcat equivs: remove prime fields, dx bad coercion

---
 theories/Homotopy/ExactSequence.v |  2 ++
 theories/WildCat/Equiv.v          | 38 +++++++++++--------------------
 theories/WildCat/Induced.v        |  6 ++---
 theories/WildCat/Opposite.v       |  6 ++---
 4 files changed, 21 insertions(+), 31 deletions(-)

diff --git a/theories/Homotopy/ExactSequence.v b/theories/Homotopy/ExactSequence.v
index c42fcae4485..7e15df813a6 100644
--- a/theories/Homotopy/ExactSequence.v
+++ b/theories/Homotopy/ExactSequence.v
@@ -461,6 +461,7 @@ Definition connecting_map {F X Y}
   : loops Y ->* F
   := i_fiberseq (connect_fiberseq i f).
 
+Set Printing Coercions.
 Global Instance isexact_connect_R {F X Y}
   (i : F ->* X) (f : X ->* Y) `{IsExact purely F X Y i f}
   : IsExact purely (fmap loops f) (connecting_map i f).
@@ -472,6 +473,7 @@ Proof.
            (pequiv_pfiber _ _ (square_pequiv_pfiber _ _ (square_pfib_pequiv_cxfib i f))))^-1*)
           (((pfiber2_loops f) o*E (pequiv_pfiber _ _ (square_pfib_pequiv_cxfib i f)))^-1*)
           _ (pfib i)).
+(** @todo: this proof hangs on Defined when the method cate_fun is directly declared as a coercion CatEquiv >-> Hom *)
   refine (vinverse 
             ((loops_inv X) o*E
              (pfiber2_loops (pfib f)) o*E
diff --git a/theories/WildCat/Equiv.v b/theories/WildCat/Equiv.v
index c73f85761ed..17ccd1c07ef 100644
--- a/theories/WildCat/Equiv.v
+++ b/theories/WildCat/Equiv.v
@@ -12,31 +12,29 @@ Declare Scope wc_iso_scope.
 
 Class HasEquivs (A : Type) `{Is1Cat A} :=
 {
-  CatEquiv' : A -> A -> Type where "a $<~> b" := (CatEquiv' a b);
+  CatEquiv : A -> A -> Type where "a $<~> b" := (CatEquiv a b);
   CatIsEquiv : forall a b, (a $-> b) -> Type;
   cate_fun' : forall a b, (a $<~> b) -> (a $-> b);
   cate_isequiv : forall a b (f : a $<~> b), CatIsEquiv a b (cate_fun' a b f);
-  cate_buildequiv' : forall a b (f : a $-> b), CatIsEquiv a b f -> CatEquiv' a b;
-  cate_buildequiv_fun' : forall a b (f : a $-> b) (fe : CatIsEquiv a b f),
-      cate_fun' a b (cate_buildequiv' a b f fe) $== f;
+  cate_buildequiv : forall a b (f : a $-> b), CatIsEquiv a b f -> CatEquiv a b;
+  cate_buildequiv_fun : forall a b (f : a $-> b) (fe : CatIsEquiv a b f),
+      cate_fun' a b (cate_buildequiv a b f fe) $== f;
   cate_inv' : forall a b (f : a $<~> b), b $-> a;
   cate_issect' : forall a b (f : a $<~> b),
     cate_inv' _ _ f $o cate_fun' _ _ f $== Id a;
   cate_isretr' : forall a b (f : a $<~> b),
       cate_fun' _ _ f $o cate_inv' _ _ f $== Id b;
-  catie_adjointify' : forall a b (f : a $-> b) (g : b $-> a)
+  catie_adjointify : forall a b (f : a $-> b) (g : b $-> a)
     (r : f $o g $== Id b) (s : g $o f $== Id a), CatIsEquiv a b f;
 }.
 
-Existing Class CatIsEquiv.
 Arguments CatIsEquiv {A _ _ _ _ _ a b} f.
-Global Existing Instance cate_isequiv.
 Arguments cate_isequiv {A _ _ _ _ _ a b} f.
+Arguments cate_buildequiv_fun {A _ _ _ _ _ a b} f {fe}.
+Arguments catie_adjointify {A _ _ _ _ _ a b} f g r s.
 
-(** Since apparently a field of a record can't be the source of a coercion (Coq complains about the uniform inheritance condition, although as officially stated that condition appears to be satisfied), we redefine all the fields of [HasEquivs]. *)
-
-Definition CatEquiv {A} `{HasEquivs A} (a b : A)
-  := @CatEquiv' A _ _ _ _ _ a b.
+Existing Class CatIsEquiv.
+Global Existing Instance cate_isequiv.
 
 Notation "a $<~> b" := (CatEquiv a b).
 Infix "≅" := CatEquiv : wc_iso_scope.
@@ -46,23 +44,13 @@ Definition cate_fun {A} `{HasEquivs A} {a b : A} (f : a $<~> b)
   : a $-> b
   := @cate_fun' A _ _ _ _ _ a b f.
 
+Arguments cate_fun {A _ _ _ _ _ a b} f.
 Coercion cate_fun : CatEquiv >-> Hom.
 
 Definition Build_CatEquiv {A} `{HasEquivs A} {a b : A}
            (f : a $-> b) {fe : CatIsEquiv f}
   : a $<~> b
-  := cate_buildequiv' a b f fe.
-
-Definition cate_buildequiv_fun {A} `{HasEquivs A} {a b : A}
-           (f : a $-> b) {fe : CatIsEquiv f}
-  : cate_fun (Build_CatEquiv f) $== f
-  := cate_buildequiv_fun' a b f fe.
-
-Definition catie_adjointify {A} `{HasEquivs A} {a b : A}
-           (f : a $-> b) (g : b $-> a)
-           (r : f $o g $== Id b) (s : g $o f $== Id a)
-  : CatIsEquiv f
-  := catie_adjointify' a b f g r s.
+  := cate_buildequiv a b f fe.
 
 Definition cate_adjointify {A} `{HasEquivs A} {a b : A}
            (f : a $-> b) (g : b $-> a)
@@ -87,7 +75,7 @@ Definition cate_issect {A} `{HasEquivs A} {a b} (f : a $<~> b)
 Proof.
   refine (_ $@ cate_issect' a b f).
   refine (_ $@R f).
-  apply cate_buildequiv_fun'.
+  apply cate_buildequiv_fun.
 Defined.
 
 Definition cate_isretr {A} `{HasEquivs A} {a b} (f : a $<~> b)
@@ -95,7 +83,7 @@ Definition cate_isretr {A} `{HasEquivs A} {a b} (f : a $<~> b)
 Proof.
   refine (_ $@ cate_isretr' a b f).
   refine (f $@L _).
-  apply cate_buildequiv_fun'.
+  apply cate_buildequiv_fun.
 Defined.
 
 (** If [g] is a section of an equivalence, then it is the inverse. *)
diff --git a/theories/WildCat/Induced.v b/theories/WildCat/Induced.v
index fe68ccdbb62..b842be62ed3 100644
--- a/theories/WildCat/Induced.v
+++ b/theories/WildCat/Induced.v
@@ -81,12 +81,12 @@ Section Induced_category.
     + apply CatIsEquiv.
     + apply cate_fun.
     + apply cate_isequiv.
-    + apply cate_buildequiv'.
-    + nrapply cate_buildequiv_fun'.
+    + apply Build_CatEquiv.
+    + nrapply cate_buildequiv_fun.
     + apply cate_inv'.
     + nrapply cate_issect'.
     + nrapply cate_isretr'.
-    + nrapply catie_adjointify'.
+    + nrapply catie_adjointify.
   Defined.
 
 End Induced_category.
diff --git a/theories/WildCat/Opposite.v b/theories/WildCat/Opposite.v
index 522bcf5b52e..c544a15c03c 100644
--- a/theories/WildCat/Opposite.v
+++ b/theories/WildCat/Opposite.v
@@ -163,10 +163,10 @@ Proof.
   srapply Build_HasEquivs; intros a b; unfold op in *; cbn.
   - exact (b $<~> a).
   - apply CatIsEquiv.
-  - apply cate_fun'.
+  - apply cate_fun.
   - apply cate_isequiv.
-  - apply cate_buildequiv'.
-  - rapply cate_buildequiv_fun'.
+  - apply Build_CatEquiv.
+  - rapply cate_buildequiv_fun.
   - apply cate_inv'.
   - rapply cate_isretr'.
   - rapply cate_issect'.