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?

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.

I'm not sure to understand what's the issue. What happens if you replace `Definition`

with `Coercion`

?

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.

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.

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)

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).

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

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

And "canonical structures for the working mathematician" IIRC has a good introduction

Last updated: Jun 20 2024 at 11:02 UTC