remove workaround for coq/coq#8994

- fixes HoTT#1541 Signed-off-by: Ali Caglayan <alizter@gmail.com>
Alizter · Feb 19, 2024 · cc98084 · cc98084
1 parent 2673d0f
commit cc98084
Show file tree

Hide file tree

Showing 6 changed files with 16 additions and 20 deletions.
diff --git a/theories/WildCat/Equiv.v b/theories/WildCat/Equiv.v
@@ -13,21 +13,25 @@ Declare Scope wc_iso_scope.
 Class HasEquivs (A : Type) `{Is1Cat A} :=
 {
   CatEquiv' : A -> A -> Type where "a $<~> b" := (CatEquiv' a b);
-  CatIsEquiv' : forall a b, (a $-> b) -> Type;
+  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_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_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)
-    (r : f $o g $== Id b) (s : g $o f $== Id a), CatIsEquiv' a b f;
+    (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.
+
 (** 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)
@@ -43,14 +47,6 @@ Definition cate_fun {A} `{HasEquivs A} {a b : A} (f : a $<~> b)
 
 Coercion cate_fun : CatEquiv >-> Hom.
 
-(* Being an equivalence should be a typeclass, but we have to redefine it to work around https://github.com/coq/coq/issues/8994 . *)
-Class CatIsEquiv {A} `{HasEquivs A} {a b : A} (f : a $-> b)
-  := catisequiv : CatIsEquiv' a b f.
-
-Global Instance cate_isequiv {A} `{HasEquivs A} {a b : A} (f : a $<~> b)
-  : CatIsEquiv f
-  := cate_isequiv' a b f.
-
 Definition Build_CatEquiv {A} `{HasEquivs A} {a b : A}
            (f : a $-> b) {fe : CatIsEquiv f}
   : a $<~> b

diff --git a/theories/WildCat/FunctorCat.v b/theories/WildCat/FunctorCat.v
@@ -92,7 +92,7 @@ Proof.
   - intros a; exact _.
   - intros ?.
     snrapply Build_NatEquiv.
-    + intros a; exact (Build_CatEquiv (alpha a)).
+    + intros a; by nrapply (Build_CatEquiv (alpha a)).
     + cbn. refine (is1natural_homotopic alpha _).
       intros a; apply cate_buildequiv_fun.
   - cbn; intros; apply cate_buildequiv_fun.

diff --git a/theories/WildCat/Induced.v b/theories/WildCat/Induced.v
@@ -78,9 +78,9 @@ Section Induced_category.
   Proof.
     srapply Build_HasEquivs; intros a b; cbn.
     + exact (f a $<~> f b).
-    + apply CatIsEquiv'.
+    + apply CatIsEquiv.
     + apply cate_fun.
-    + apply cate_isequiv'.
+    + apply cate_isequiv.
     + apply cate_buildequiv'.
     + nrapply cate_buildequiv_fun'.
     + apply cate_inv'.

diff --git a/theories/WildCat/NatTrans.v b/theories/WildCat/NatTrans.v
@@ -212,7 +212,7 @@ Definition Build_NatEquiv' {A B : Type} `{IsGraph A} `{HasEquivs B}
 Proof.
   snrapply Build_NatEquiv.
   - intro a.
-    refine (Build_CatEquiv (alpha a)).
+    by refine (Build_CatEquiv (alpha a)).
   - intros a a' f.
     refine (cate_buildequiv_fun _ $@R _ $@ _ $@ (_ $@L cate_buildequiv_fun _)^$).
     apply (isnat alpha).

diff --git a/theories/WildCat/Opposite.v b/theories/WildCat/Opposite.v
@@ -164,7 +164,7 @@ Proof.
   - exact (b $<~> a).
   - apply CatIsEquiv.
   - apply cate_fun'.
-  - apply cate_isequiv'.
+  - apply cate_isequiv.
   - apply cate_buildequiv'.
   - rapply cate_buildequiv_fun'.
   - apply cate_inv'.

diff --git a/theories/WildCat/Prod.v b/theories/WildCat/Prod.v
@@ -81,8 +81,8 @@ Proof.
   - split; [ exact (fst f) | exact (snd f) ].
   - split; exact _.
   - intros [fe1 fe2]; split.
-    + exact (Build_CatEquiv (fst f)).
-    + exact (Build_CatEquiv (snd f)).
+    + by rapply (Build_CatEquiv (fst f)).
+    + by rapply (Build_CatEquiv (snd f)).
   - intros [fe1 fe2]; cbn; split; apply cate_buildequiv_fun.
   - split; [ exact ((fst f)^-1$) | exact ((snd f)^-1$) ].
   - split; apply cate_issect.