Skip to content

remove workaround for coq/coq#8994 #1807

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
Alizter wants to merge 1 commit into
base: master
Choose a base branch
from
Open

remove workaround for coq/coq#8994 #1807

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
22 changes: 9 additions & 13 deletions theories/WildCat/Equiv.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand All @@ -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
Expand Down
2 changes: 1 addition & 1 deletion theories/WildCat/FunctorCat.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
4 changes: 2 additions & 2 deletions theories/WildCat/Induced.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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'.
Expand Down
2 changes: 1 addition & 1 deletion theories/WildCat/NatTrans.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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).
Expand Down
2 changes: 1 addition & 1 deletion theories/WildCat/Opposite.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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'.
Expand Down
4 changes: 2 additions & 2 deletions theories/WildCat/Prod.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down