Non-uniqueness of pure without parametricity: a twisted applicative functor https://stackoverflow.com/questions/66555516/uniqueness-of-pure

twist.v

Set Implicit Arguments.
Set Maximal Implicit Insertion.

(** A non-parametric extension of System F. *)

(** Typecase, and flip all booleans *)
Axiom twist : forall a : Type, a -> a.
Axiom twist_fun : forall a b, @twist (a -> b) = fun f x => twist (f (twist x)).
Axiom twist_bool :            @twist bool     = negb.  (* Not the identity *)
(* [twist = id] for all other types *)

Axiom twist_inv : forall a, (fun x : a => twist (twist x)) = (fun x => x).

Corollary twist_inv' : forall a (x : a), twist (twist x) = x.
Proof.
  intros a x; apply (f_equal (fun w => w x) (twist_inv _)).
Qed.

(** Twisted Identity functor *)

Record I (a : Type) : Type := MkI { runI : a }.

Definition pure {a} (x : a) : I a := MkI (twist x).
Definition ap {a b} (x : I (a -> b)) (y : I a) : I b := MkI (runI x (runI y)).

(** Function composition *)
Definition dot {a b c} (f : b -> c) (g : a -> b) : a -> c :=
  fun x => f (g x).

Infix "<*>" := ap (at level 40).
Notation "(.)" := dot (at level 0).

Lemma pure_id {a} : pure (fun x : a => x) = MkI (fun x => x).
Proof.
  unfold pure. 
  rewrite twist_fun.
  rewrite twist_inv.
  reflexivity.
Qed.

Lemma pure_comp {a b c} : pure (@dot a b c) = MkI (.).
Proof.
  unfold pure, dot. f_equal.
  rewrite !twist_fun.
  change
    (((fun tt1 tt2 tt3 (x : b -> c) (x0 : a -> b) (x1 : a) => tt1 (x (tt2 (x0 (tt3 x1))))) (fun x => twist (twist x)) (fun x => twist (twist x)) (fun x => twist (twist x))) = fun f g x => f (g x)).
  match goal with
  | [ |- ?f _ _ _ = _ ] => remember f
  end.
  rewrite 3 twist_inv; subst; auto.
Qed.

(** The four Applicative laws
from https://hackage.haskell.org/package/base-4.14.1.0/docs/Control-Applicative.html *)

Lemma identity {a} (v : I a) : pure (fun x => x) <*> v = v.
Proof.
  destruct v; rewrite pure_id; reflexivity.
Qed.

Lemma composition {a b c} u v w : pure (@dot a b c) <*> u <*> v <*> w = u <*> (v <*> w).
Proof.
  destruct u, v, w; rewrite pure_comp; reflexivity.
Qed.

Lemma homomorphism {a b} (f : a -> b) (x : a)
  : pure f <*> pure x = pure (f x).
Proof.
  unfold pure, ap; cbn; f_equal.
  rewrite twist_fun. rewrite twist_inv'.
  reflexivity.
Qed.

Lemma interchange {a b} (u : I (a -> b)) (y : a)
  : u <*> pure y = pure (fun f => f y) <*> u.
Proof.
  unfold ap, pure; cbn; f_equal.
  rewrite 2 twist_fun, twist_inv'.
  reflexivity.
Qed.