Dennis H (Apr 10 2023 at 12:46): Dennis H (Apr 10 2023 at 12:46):Is it possible to define a Coercion with implicit parameters? For example, I have the following
Definition arrow_mor {C : category} (f : arrow C) := pr2 f.
Definition mor_to_arrow_ob {C : category} {x y : C} (f : x --> y) : arrow C :=
(make_dirprod x y,, f).
and I would like to make both of these coercions (the domain of arrow_mor is also dependent on the parameter f). Would something like this be possible?
Raul (Apr 11 2023 at 22:25):I can't help but to ask it again in hopes somebody knows it :sweat_smile: .
Most of my inductive types have parameters, which must be taken in account in the coercions.
Pierre Roux (Apr 11 2023 at 22:36):I'm not sure to understand what's the issue. What happens if you replace Definition with Coercion?
Raul (Apr 12 2023 at 09:03):On of the coercions where I have problems is this one
Inductive signed T :=
| sign : 'Z_2 -> T -> signed T.
Coercion emb := fun T => (sign T 0%R) : T >-> signed T.
Gives the error
Error: Syntax error: '.' expected after [gallina_ext] (in [vernac_aux]).
In contrast, the following works fine
Variable n : nat.
Class ary_Connective {A : Connectives} := {
ca : @Connective A;
eqc_arity : n = @sk_arity skeleton
}.
Coercion ca : ary_Connective >-> Connective.
I suppose in the first case I can't hide the parameter, but in the second I can.
Pierre Roux (Apr 12 2023 at 09:07):You should probably read the doc of coercion in the refman: https://coq.inria.fr/distrib/current/refman/addendum/implicit-coercions.html
In particular, the _ >-> _ syntax expects coercion classes which should be constants or local variables, as coercion only work on the head symbol.
Raul (Apr 12 2023 at 09:18):Then 'ary_Connective' is constant as a dependent type?
Is it possible to have a coercion going out of "the identity functor"?
Do you have any recommendation about the type-theoretical/whatever nature of Coercions and Canonical commands?
I don't understand how they work.
(of all the questions I would rather say this is the more important, I don't really need to solve the others right now)
Pierre Roux (Apr 12 2023 at 09:59):Well, coercion are pretty dumb, they are very syntactical and only activated on the head constant of the type (with the special cases of funclass and sortclass).
Paolo Giarrusso (Apr 12 2023 at 16:53):So, you can't have coercions from the "identity functor", but you can write an identity function and have a coercion from uses of that function
Paolo Giarrusso (Apr 12 2023 at 16:54):If type-theoretically = after type inference/elaboration, coercions are functions and Canonical things are constants/definitions. If you're asking how they're used in inference, the manual has the rules
Paolo Giarrusso (Apr 12 2023 at 16:54):And "canonical structures for the working mathematician" IIRC has a good introduction
Last updated: Oct 04 2023 at 19:01 UTC