I have a pointed type `X`

whose elements are themselves types, giving a function `f : pointed_type X -> Type`

from the underlying type of X. If I make this a coercion, Coq complains about UIC (because `pointed_type`

is not a class?). Now `pointed_type`

is itself already a coercion, so I can write `x0 x1 : X`

. Now I would like to write `x0 -> x1`

since by virtue of the coercion `f`

, `x0`

and `x1`

are types, but this doesn't work. Can this be made to work or is it a dead-end?

Let me add that I know the underlying type of `X`

, let's call it `UX`

. Given `x0`

and `x1`

as above, I can write `(x0 : UX) -> (x1 : UX)`

with a coercion `UX -> Type`

(which doesn't complain about UIC). So if I could get `pointed_type X`

to automatically convert to `UX`

that should solve my issues as well. Any input appreciated!

Minimal example (take 3):

```
Notation "A -> B" := (forall (_ : A), B) (at level 99, right associativity, B at level 200).
Record sig {A} (P : A -> Type) := exist {
proj1 : A ;
proj2 : P proj1 ;
}.
Arguments exist {A} P _ _.
Notation "( x ; y )" := (exist _ x y).
Record pType := {
ptype_type :> Type;
ptype_pt : ptype_type
}.
Axiom P : Type -> Type.
Axiom Px : forall X, P X.
Definition BAut (X : Type) := sig P.
Coercion BAut_pr1 X : BAut X -> Type := fun x => match x with (x;_) => x end.
Definition pBAut (X : Type) : pType
:= Build_pType (BAut X) (X; Px X).
Coercion pBAut_pr1 X : pBAut X -> Type := BAut_pr1 X.
Context (X : Type) (x0 x1 : pBAut X).
Check ((x0 : BAut X) -> (x1 : BAut X)).
Fail Check (x0 -> x1).
```

@Gaëtan Gilbert Do you know what would need to change to get the desired behavior here?

If I make this a coercion, Coq complains about UIC (because pointed_type is not a class?)

because pointed_type is applied to something that's not a variable

Is there a way to get the last line `Check (x0 -> x1).`

to work though, or something similar?

Last updated: Apr 14 2024 at 11:02 UTC