I'd like to declare a coercion, but don't know how to formulate it to coq. My situation is this:

```
Definition Ensemble (X : Type) := X -> Prop.
Definition In {X : Type} (U : Ensemble X) (x : X) := U x.
Record TopologicalSpace := {
point_set :> Type;
}.
Definition SubspaceTopology {X : TopologicalSpace} (U : Ensemble X) :=
{| point_set := { x : X | In U x }; |}.
Axiom connected : TopologicalSpace -> Prop.
```

Now I'd like to write the following:

```
Coercion SubspaceTopology : Ensemble >-> TopologicalSpace.
Section S.
Variable X : TopologicalSpace.
Variable U : Ensemble X.
Fail Variable V : Ensemble U.
Fail Variable p : U. (* should be interpreted as [p : { x : point_set X | In U x }] *)
Fail Variable f : U -> X.
Fail Goal connected U. (* should be interpreted as [connected (SubspaceTopology U)] *)
End Section S.
```

Is there some way to make this work?

Your coercion does not respect the uniform inheritance. For some obscure reason, Coq is extremely crippled in that case, and meaningful examples like yours fail. This restriction was removed in Coq 8.16 and most of (all?) your examples should go through. But with 8.15 or earlier, I cannot think of a good way to make it succeed.

Maybe it helps you to know that coercions don't do any unification - the involved types must match literally without any reduction.

Your intuition around U and V is not clear to me. Did you mean `Definition U := Ensemble X.`

?

I wanted U to be a subset of X and simultaneously consider it as a space endowed with the subspace topology.

Oh, nice! Thanks for mentioning that @Guillaume Melquiond. It really works now.

Last updated: Jun 25 2024 at 14:01 UTC