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: Oct 13 2024 at 01:02 UTC