Closed DanGrayson closed 10 years ago
DanGrayson
commented
10 years ago What's happening is that even though c' is ostensibly an object of C', with all that entails mathematically, it's really just an element of the type of objects of C', and can also be viewed as an object of C, and that's the context in which the notion of isomorphism gets interpreted: in C. The morphisms of C' are ignored, together with all the rest of its data and identities.
DanGrayson
commented
10 years ago Vladimir's code has similar behavior:
Require Import Foundations.hlevel2.algebra1a.
Parameter X : hSet.
Parameter n : X -> X -> X.
Parameter n': X -> X -> X.
Definition S := setwithbinoppair X n.
Definition S':= setwithbinoppair X n'.
Definition weird (s:S) (s':S') := op s s'.
Check weird.One way out would be to define an object of a precategory C to be a pair (C,c), where c:ob C.
mikeshulman
commented
10 years ago I haven't tested this myself, but it looks like it might be just a "feature" of Coq's coercions and implicit arguments.
DanGrayson
commented
10 years ago Yes, it is, you're right. In the latter example, S' is coerced to its underlying set. In the former example, C' is coerced to its underlying type of objects. The issue isn't just academic -- it confused me in my current formalization project, and it might confuse others, so if there is a work-around, it would be worth implementing it.
DanGrayson
commented
10 years ago In my situation C and C' were provably equal, but not definitionally equal. So I was expecting to get an error and to be forced to insert the proof of the equality somewhere, and to transport something along it. But the lemma got proven with no such error, convincing me coq was smarter than I was.
mikeshulman
commented
10 years ago Maybe it would be worth asking on a place like the Coq mailing list, then.
DanGrayson
commented
10 years ago Yes, they might know a simple technological work-around.
On Thu, Jan 16, 2014 at 8:32 PM, Mike Shulman notifications@github.comwrote:
Maybe it would be worth asking on a place like the Coq mailing list, then.
— Reply to this email directly or view it on GitHubhttps://github.com/benediktahrens/rezk_completion/issues/7#issuecomment-32572533 .
benediktahrens
commented
10 years ago If I understand correctly, the problem is the following: usually, when writing, for variables C and C', c : ob C , c' : ob C', f : c --> c' then Coq would need to check that C is convertible to C'. (Currently, it would actually amount to checking that the objects and morphisms of C and C' are convertible, since the coercion "ob" is defined on the the sigma type of (fun ob => ob -> ob -> hSet) rather than on the sigma type of precategories.) As long as C and C' are variables, no evaluation of ob C and ob C' can happen, so really C has to be convertible to C'. So it seems that what we want is that ob C and ob C' are not evaluated even when they could be, i.e. when C and C' unfold to constructor form. So we would want some kind of opacification?
JasonGross
commented
10 years ago When do you run in to this problem? That is, do you have a concrete example of two categories with the same type of objects, which you want to consider as having incompatible objects?
An alternative might be to make iso take an explicit precategory argument, so that you always have to say what category you want your objects in.
DanGrayson
commented
10 years ago Yes, the example is this. Let B be a precategory, let C = [B,HSET] and let C' = [B^op^op,HSET].
As long as c:C really means c:ob C, I see no way that adding C as a parameter could help.
On Fri, Jan 17, 2014 at 5:35 AM, Jason Gross notifications@github.comwrote:
When do you run in to this problem? That is, do you have a concrete example of two categories with the same type of objects, which you want to consider as having incompatible objects?
An alternative might be to make iso take an explicit precategoryargument, so that you always have to say what category you want your objects in.
— Reply to this email directly or view it on GitHubhttps://github.com/benediktahrens/rezk_completion/issues/7#issuecomment-32595279 .
DanGrayson
commented
10 years ago I'm not sure I know what you mean by "having incompatible objects". But in the same way that every object in type theory is born knowing what type it belongs to, every object in a category should be born knowing what category it belongs to, so that an accidental equality between part of the structures of the two categories doesn't allow us to construct nonsense terms such as " iso c c' ". Redesigning "iso" is not the right way to go, because the same issue will arise all sorts of binary operations. For example, what if I want the product of c and c', or the direct sum?
On Fri, Jan 17, 2014 at 5:35 AM, Jason Gross notifications@github.comwrote:
When do you run in to this problem? That is, do you have a concrete example of two categories with the same type of objects, which you want to consider as having incompatible objects?
An alternative might be to make iso take an explicit precategoryargument, so that you always have to say what category you want your objects in.
— Reply to this email directly or view it on GitHubhttps://github.com/benediktahrens/rezk_completion/issues/7#issuecomment-32595279 .
JasonGross
commented
10 years ago By "having incompatible objects", I just meant that the types don't unify. The suggestion to add an explicit parameter was to unconfuse people, rather than to unconfuse Coq.
Yes, the example is this. Let B be a precategory, let C = [C,HSET] and let C' = [C^op^op,HSET].
You don't mention B. Do you mean C = [B, HSET] and C' = [(Bᵒᵖ)ᵒᵖ, HSET]? But in this case B and (Bᵒᵖ)ᵒᵖ are really the same category (in HoTT/HoTT, they are judgmentally the same category up to eta for records, and once we move to the new version of coq (once Matthieu irons out the bugs that are blocking compilation), they will really be judgmentally the same category). If you mean about an iso between an object of B and an object of Bᵒᵖ, then I see that it might potentially be a problem, but in this case, an iso in one is an iso in the other. I guess it is more complicated in the case of product, because that turns into a coproduct. But I still think that the solution of "pass around an explicit category" is a reasonable one. Do you have an example where the objects just happen to be the same "by accident", and there's no relation between the morphisms?
Anyway, the technical solution, as @benediktahrens suggested, is to use the Opaque keyword on Mattheiu's polyproj branch, where it blocks reduction/unificiation. I believe there are also locking mechinisms used by ssreflect to block unification; Georges Gonthier explained them to me on a thread on coq-club. So if I recall correctly, you could do something like
Definition master_key : unit.
Proof.
exact tt.
Qed.
Definition locked A := let: tt := master_key in fun x : A => x.
Lemma lock key A x : x = locked key x :> A.
...
Qed.
Coercion ob : precategory -> Type := @locked (precategory -> type) (fun C : precategory => pr1 C).or something like that. It'll be annoying to build objects of any particular category, though.
DanGrayson
commented
10 years ago Hmm, that seems to depend on eta for unit never getting implemented in coq...
On Fri, Jan 17, 2014 at 5:21 PM, Jason Gross notifications@github.comwrote:
By "having incompatible objects", I just meant that the types don't unify. The suggestion to add an explicit parameter was to unconfuse people, rather than to unconfuse Coq.
Yes, the example is this. Let B be a precategory, let C = [C,HSET] and let C' = [C^op^op,HSET].
You don't mention B. Do you mean C = [B, HSET] and C' = [(Bᵒᵖ)ᵒᵖ, HSET]? But in this case B and (Bᵒᵖ)ᵒᵖ are really the same category (in HoTT/HoTT, they are judgmentally the same category up to eta for records, and once we move to the new version of coq (once Matthieu irons out the bugs that are blocking compilation), they will really be judgmentally the same category). If you mean about an iso between an object of B and an object of Bᵒᵖ, then I see that it might potentially be a problem, but in this case, an iso in one is an iso in the other. I guess it is more complicated in the case of product, because that turns into a coproduct. But I still think that the solution of "pass around an explicit category" is a reasonable one. Do you have an example where the objects just happen to be the same "by accident", and there's no relation between the morphisms?
Anyway, the technical solution, as @benediktahrenshttps://github.com/benediktahrenssuggested, is to use the Opaque keyword on Mattheiu's polyproj branchhttps://github.com/mattam82/coq/tree/polyproj, where it blocks reduction/unificiation. I believe there are also locking mechinisms used by ssreflect to block unification; Georges Gonthier explained them to me on a thread on coq-clubhttps://sympa.inria.fr/sympa/arc/coq-club/2013-07/msg00003.html. So if I recall correctly, you could do something like
Definition master_key : unit.Proof. exact tt.Qed. Definition locked A := let: tt := master_key in fun x : A => x.Lemma lock key A x : x = locked key x :> A....Qed. Coercion ob : precategory -> Type := @locked (precategory -> type) (fun C : precategory => pr1 C).
or something like that. It'll be annoying to build objects of any particular category, though.
— Reply to this email directly or view it on GitHubhttps://github.com/benediktahrens/rezk_completion/issues/7#issuecomment-32655676 .
DanGrayson
commented
10 years ago Yes, thanks for pointing out the misprint involving B -- I edited the remark.
On Fri, Jan 17, 2014 at 5:21 PM, Jason Gross notifications@github.comwrote:
By "having incompatible objects", I just meant that the types don't unify. The suggestion to add an explicit parameter was to unconfuse people, rather than to unconfuse Coq.
Yes, the example is this. Let B be a precategory, let C = [C,HSET] and let C' = [C^op^op,HSET].
You don't mention B. Do you mean C = [B, HSET] and C' = [(Bᵒᵖ)ᵒᵖ, HSET]? But in this case B and (Bᵒᵖ)ᵒᵖ are really the same category (in HoTT/HoTT, they are judgmentally the same category up to eta for records, and once we move to the new version of coq (once Matthieu irons out the bugs that are blocking compilation), they will really be judgmentally the same category). If you mean about an iso between an object of B and an object of Bᵒᵖ, then I see that it might potentially be a problem, but in this case, an iso in one is an iso in the other. I guess it is more complicated in the case of product, because that turns into a coproduct. But I still think that the solution of "pass around an explicit category" is a reasonable one. Do you have an example where the objects just happen to be the same "by accident", and there's no relation between the morphisms?
Anyway, the technical solution, as @benediktahrenshttps://github.com/benediktahrenssuggested, is to use the Opaque keyword on Mattheiu's polyproj branchhttps://github.com/mattam82/coq/tree/polyproj, where it blocks reduction/unificiation. I believe there are also locking mechinisms used by ssreflect to block unification; Georges Gonthier explained them to me on a thread on coq-clubhttps://sympa.inria.fr/sympa/arc/coq-club/2013-07/msg00003.html. So if I recall correctly, you could do something like
Definition master_key : unit.Proof. exact tt.Qed. Definition locked A := let: tt := master_key in fun x : A => x.Lemma lock key A x : x = locked key x :> A....Qed. Coercion ob : precategory -> Type := @locked (precategory -> type) (fun C : precategory => pr1 C).
or something like that. It'll be annoying to build objects of any particular category, though.
— Reply to this email directly or view it on GitHubhttps://github.com/benediktahrens/rezk_completion/issues/7#issuecomment-32655676 .
JasonGross
commented
10 years ago Eta for unit will not be implemented until 8.5, at least, (probably not until 8.6 or later), and by 8.5, you will be able to use Opaque instead.
DanGrayson
commented
10 years ago Is this sort of like what you meant?:
Definition key : unit. exact tt. Qed.
Definition locked A (x:A) : A := match key with tt => x end.
Lemma unlock A x : x = locked A x.
unfold locked. destruct key. reflexivity.
Defined.
Record total {T} ( P: T -> Type ) := tpair { pr1 : T; pr2 : P pr1 }.
Definition morfun (o:Type) := o -> o -> Type.
Definition category := total morfun.
Definition make_cat := tpair _ morfun.
Parameter o : Type.
Parameter m m' : o -> o -> Type.
Definition C := make_cat o m.
Definition C':= make_cat o m'.
Parameter x : o.
Definition ob (C:category) := pr1 _ C.
Check x : ob C.
Check x : ob C'.
Definition iso {C:category} (a b:ob C) := unit.
Definition funny (a:ob C) (b:ob C') := iso a b.
Definition ob' : category -> Type :=
locked (category -> Type) (fun C : category => ob C).
Definition iso' {C:category} (a b:ob' C) := unit.
(* Definition funny' (a:ob' C) (b:ob' C') := iso' a b. (* <-- fails, good *) *)
Definition open {C} : ob' C -> ob C.
unfold ob',locked. destruct key. exact (fun c => c).
Defined.
Definition close {C} : ob C -> ob' C.
unfold ob',locked. destruct key. exact (fun c => c).
Defined.
Definition iso2' {C:category} (a b:ob' C) := iso (open a) (open b).On Fri, Jan 17, 2014 at 5:21 PM, Jason Gross notifications@github.comwrote:
By "having incompatible objects", I just meant that the types don't unify. The suggestion to add an explicit parameter was to unconfuse people, rather than to unconfuse Coq.
Yes, the example is this. Let B be a precategory, let C = [C,HSET] and let C' = [C^op^op,HSET].
You don't mention B. Do you mean C = [B, HSET] and C' = [(Bᵒᵖ)ᵒᵖ, HSET]? But in this case B and (Bᵒᵖ)ᵒᵖ are really the same category (in HoTT/HoTT, they are judgmentally the same category up to eta for records, and once we move to the new version of coq (once Matthieu irons out the bugs that are blocking compilation), they will really be judgmentally the same category). If you mean about an iso between an object of B and an object of Bᵒᵖ, then I see that it might potentially be a problem, but in this case, an iso in one is an iso in the other. I guess it is more complicated in the case of product, because that turns into a coproduct. But I still think that the solution of "pass around an explicit category" is a reasonable one. Do you have an example where the objects just happen to be the same "by accident", and there's no relation between the morphisms?
Anyway, the technical solution, as @benediktahrenshttps://github.com/benediktahrenssuggested, is to use the Opaque keyword on Mattheiu's polyproj branchhttps://github.com/mattam82/coq/tree/polyproj, where it blocks reduction/unificiation. I believe there are also locking mechinisms used by ssreflect to block unification; Georges Gonthier explained them to me on a thread on coq-clubhttps://sympa.inria.fr/sympa/arc/coq-club/2013-07/msg00003.html. So if I recall correctly, you could do something like
Definition master_key : unit.Proof. exact tt.Qed. Definition locked A := let: tt := master_key in fun x : A => x.Lemma lock key A x : x = locked key x :> A....Qed. Coercion ob : precategory -> Type := @locked (precategory -> type) (fun C : precategory => pr1 C).
or something like that. It'll be annoying to build objects of any particular category, though.
— Reply to this email directly or view it on GitHubhttps://github.com/benediktahrens/rezk_completion/issues/7#issuecomment-32655676 .
vladimirias
commented
10 years ago This is really a bad style of coercion management of Coq - the system should produce an error if several different coercions leading tom non-equivalent terms are possible. At least we need to have it as a flag. (In this case this can be @iso C or @iso C'
V.
On Jan 16, 2014, at 6:25 PM, Daniel R. Grayson notifications@github.com wrote:
... and that's mathematically strange, or even incorrect, and can cause confusion.
However, it might be sort of convenient if it would check at least that the two categories have the same morphisms, the same identity arrows, and the same composition operations, but not check that the proofs of the identities are the same. But even that might lead to confusion, so better not.
Here is the code that shows the problem.
Require Import RezkCompletion.precategories. Import pathnotations.PathNotations. Local Notation "a --> b" := (precategory_morphisms a b)(at level 50). Require Import Foundations.Generalities.uu0. Require Import Foundations.hlevel2.hSet.
(* make two precategories with the same objects *) Parameter o : Type. Parameter m m' : o -> o -> Type. Parameter is : forall (c d:o), isaset (m c d). Parameter is': forall (c d:o), isaset (m' c d). Parameter id : forall c:o, m c c. Parameter id': forall c:o, m' c c. Parameter co : forall {c d e:o} (f:m c d) (g:m d e), m c e. Parameter co': forall {c d e:o} (f:m' c d) (g:m' d e), m' c e. Parameter rg: forall (c d:o) (f:m c d), co (id c) f == f. Parameter lf: forall (c d:o) (f:m c d), co f (id d) == f. Parameter rg': forall (c d:o) (f:m' c d), co' (id' c) f == f. Parameter lf': forall (c d:o) (f:m' c d), co' f (id' d) == f. Parameter ass: forall (a b c d : o) (f : m a b) (g : m b c) (h : m c d), co f (co g h) == co (co f g) h. Parameter ass': forall (a b c d : o) (f : m' a b) (g : m' b c) (h : m' c d), co' f (co' g h) == co' (co' f g) h.
Definition precategory_pair (C:precategory_data) (i:isprecategory C) : precategory := tpair C i.
Definition makePrecategory (obj : UU) (mor : obj -> obj -> UU) (imor : forall i j:obj, isaset (mor i j)) (identity : forall i:obj, mor i i) (compose : forall (i j k:obj) (f:mor i j) (g:mor j k), mor i k) (right : forall (i j:obj) (f:mor i j), compose (identity i) f == f) (left : forall (i j:obj) (f:mor i j), compose f (identity j) == f) (associativity : forall (a b c d:obj) (f:mor a b) (g:mor b c) (h:mor c d), compose f (compose g h) == compose (compose f g) h) : precategory. intros. set (C := precategory_data_pair (precategory_ob_mor_pair obj (fun i j:obj => hSetpair (mor i j) (imor i j))) identity compose). assert (iC : is_precategory C). split. split. exact right. exact left. exact associativity. exact (precategory_pair C iC). Defined.
Definition C := makePrecategory o m is id (@co) rg lf ass. Definition C':= makePrecategory o m' is' id' (@co') rg' lf' ass'.
Definition funny (c:C) (c':C') := iso c c'. — Reply to this email directly or view it on GitHub.
vladimirias
commented
10 years ago A patch. V.
On Jan 16, 2014, at 7:30 PM, Daniel R. Grayson notifications@github.com wrote:
Yes, it is, you're right. In the latter example, S' is coerced to its underlying set. In the former example, C' is coerced to its underlying type of objects. The issue isn't just academic -- it confused me in my current formalization project, and it might confuse others, so if there is a work-around, it would be worth implementing it.
— Reply to this email directly or view it on GitHub.
vladimirias
commented
10 years ago Dan,
do not worry about this. It is a misbehavior of Coq's coercion system and requires a request to Coq developers or a patch, not a change in definitions.
V.
On Jan 16, 2014, at 7:21 PM, Daniel R. Grayson notifications@github.com wrote:
One way out would be to define an object of a precategory C to be a pair (C,c), where c:ob C.
— Reply to this email directly or view it on GitHub.
vladimirias
commented
10 years ago On Jan 17, 2014, at 10:10 PM, Daniel R. Grayson notifications@github.com wrote:
Yes, the example is this. Let B be a precategory, let C = [C,HSET] and let C' = [C^op^op,HSET].
As long as c:C really means c:ob C, I see no way that adding C as a parameter could help.
Making C explicit in iso will make it clear that iso x x' is iso C x x' which is all you need - in any event the notation x:C is an abuse of notation since x:T only makes sense if T is a type and a category is not a type.
V.
benediktahrens
commented
10 years ago The only "fix" to this issue on the level of RezkCompletion would be to make the argument of iso of type precategory explicit, which would be too much in most situations. I suggest the use of "@iso" when there is the danger of ambiguity. I now close this issue.
DanGrayson
commented
10 years ago Okay.
I think Vladimir is right that c:C is an abuse of notation (via the coercion C goes to ob C), but I recall that I was the one that suggested it to you. Shall we undo that change? Having to write c:ob C would make it clearer what's really going on.
On Sun, Jan 19, 2014 at 11:00 AM, benediktahrens notifications@github.comwrote:
The only "fix" to this issue on the level of RezkCompletion would be to make the argument of iso of type precategory explicit, which would be too much in most situations. I suggest the use of "@isohttps://github.com/iso" when there is the danger of ambiguity. I now close this issue.
— Reply to this email directly or view it on GitHubhttps://github.com/benediktahrens/rezk_completion/issues/7#issuecomment-32711562 .
benediktahrens
commented
10 years ago No, it would not make anything clearer. You would still be able to write Definition funny (c : ob C) (c' : ob C') := iso c c'. which is not less confusing than your original funny. It is not a matter of coercions, in my opinion.
This "bug" really comes from declaring the argument of type precategory as implicit for (iso)morphisms. I recommend introducing different local notations for morphisms of different categories, e.g., relations vs total functions on sets, when one really needs it. Also note that the status of arguments can be changed locally from implicit to explicit, but one can also introduce different notation when only implicit arguments differ. Any of these solutions seems to be more reasonable than having a global change in the definition of (the implicit arguments of) (iso)morphisms.
vladimirias
commented
10 years ago I suggest not to worry about the possibility for confusion here and also to suggest a patch/feature in Coq to provide a warning where several non-equivalent applications of coercions are possible.
V.
On Jan 19, 2014, at 11:54 AM, Daniel R. Grayson notifications@github.com wrote:
Okay.
I think Vladimir is right that c:C is an abuse of notation (via the coercion C goes to ob C), but I recall that I was the one that suggested it to you. Shall we undo that change? Having to write c:ob C would make it clearer what's really going on.
On Sun, Jan 19, 2014 at 11:00 AM, benediktahrens notifications@github.comwrote:
The only "fix" to this issue on the level of RezkCompletion would be to make the argument of iso of type precategory explicit, which would be too much in most situations. I suggest the use of "@isohttps://github.com/iso" when there is the danger of ambiguity. I now close this issue.
— Reply to this email directly or view it on GitHubhttps://github.com/benediktahrens/rezk_completion/issues/7#issuecomment-32711562 .
— Reply to this email directly or view it on GitHub.
DanGrayson
commented
10 years ago Good idea, but actually, here it's a matter of multiple choices for an implicit argument, as iso c c' gets expanded either to @iso C c c' or to @iso C' c c'. Such a patch might consume too much time to be practical, though.
... and that's mathematically strange and can cause confusion.
However, it might be sort of convenient if it would check at least that the two categories have the same morphisms, the same identity arrows, and the same composition operations, but not check that the proofs of the identities are the same. But even that might lead to confusion, so better not.
Here is the code that shows the problem.