Hello everyone, new around here, glad to be here.

Suppose I have a record,

Record foo :=

{tp:Type; coloftpprop:(tp -> Prop) -> Prop}.

and two foos , foo1 and foo2 and a proof of (tp foo1 = tp foo2). How can I make this definition type check?

Definition fooimpfoo (foo1 foo2:foo) :=

forall fp, (coloftp foo1) fp -> (coloftp foo2) fp.

The error i'm given is:

Error:

In environment

foo1 : foo

foo2 : foo

fp : tp foo1 -> Prop

The term "fp" has type "tp foo1 -> Prop" while it is expected to have type

"tp foo2 -> Prop" (cannot unify "tp foo2" and "tp foo1").

you need to use explicitly the equality. For instance, something like:

```
Definition fooimpfoo (foo1 foo2:foo).
Proof.
refine (forall fp, (coloftp foo1) fp -> (coloftp foo2) _).
rewrite <-your_equality.
exact fp.
Defined.
```

I didn't try it out in Coq, but I hope it gives the idea — feel free to ask question.

One can also write the proof term by hand, but I feel that's more advanced (I'd have to look it up).

Thank you very much, I made it work by :

Definition fooimpfoo (foo1 foo2:foo) (p:tp foo1 = tp foo2):Prop.

Proof.

refine (forall fp, (coloftp foo1) fp -> (coloftp foo2) _).

rewrite <-p.

exact fp.

Defined.

Last updated: Feb 08 2023 at 23:03 UTC