The Coq mailing list

[Maximilian Wuttke <mwuttke97 AT posteo.de>]

Hi Club,

Quite some time after I finished a complicated Coq development, I
noticed that I could have simplified it a lot by admitting the following
axiom:

```
From Coq.Vectors Require Import Vector.
Axiom tam :
  forall ϕ1 ϕ2 (f : forall {X}, ((Vector.t nat ϕ1) -> X) -> ((Vector.t
nat ϕ2) -> X)),
  exists g : (Vector.t nat ϕ2) -> (Vector.t nat ϕ1),
    forall (X : Type) (i : Vector.t nat ϕ1 -> X) (ys : Vector.t nat ϕ2),
      f i ys = i (g ys).
```

I believe this axiom is admissible but not provable inside Coq. It looks
like an axiom that should hold due to parametricity.

The special case ϕ1=ϕ2=0 can be simplified to the following goal:

```
f : forall X : Type, (unit -> X) -> unit -> X
X : Type
i : unit -> X
============================
f X i tt = i tt
```

Entirely out of curiosity (I don't plan to change my Coq development):
Are there "standard" axioms, that entail this goal?


-- Maximilian