ApplicativeCommutativeIdempotent.v

From Tealeaves Require Export
  Classes.Categorical.Applicative.
From Tealeaves Require Import
  Classes.Comonoid.

Import Applicative.Notations.
Import Product.Notations.

#[local] Generalizable Variables ϕ F G A B C.

(** * Commutative and Idempotent Elements and Functors *)
(**********************************************************************)

(** ** The Center of an Applicative Functor *)
(**********************************************************************)
Class Center (G: Type -> Type)
  `{mapG: Map G} `{pureG: Pure G} `{multG: Mult G}
  (A: Type) (a: G A): Prop :=
    { appcenter_left: forall (B: Type) (x: G B),
        x ⊗ a = map (fun '(x, y) => (y, x)) (a ⊗ x);
      appcenter_right: forall (B: Type) (x: G B),
        a ⊗ x = map (fun '(x, y) => (y, x)) (x ⊗ a);
    }.

(** ** The Idempotent and Central Elements of an Applicative Functor *)
(**********************************************************************)
Class Idempotent (G: Type -> Type)
  `{mapG: Map G} `{pureG: Pure G} `{multG: Mult G}
  (A: Type) (a: G A): Prop :=
  { appidem: a ⊗ a = map (fun a => (a, a)) a;
  }.

Class IdempotentCenter (G: Type -> Type)
  `{mapG: Map G} `{pureG: Pure G} `{multG: Mult G}
  (A: Type) (a: G A): Prop :=
  { appic_idem :> Idempotent G A a;
    appic_center :> Center G A a;
  }.

#[global] Arguments appcenter_left {G}%function_scope {mapG pureG multG}
  {A}%type_scope (a) {Center} {B}%type_scope x.
#[global] Arguments appcenter_right {G}%function_scope {mapG pureG multG}
  {A}%type_scope (a) {Center} {B}%type_scope x.
#[global] Arguments appidem {G}%function_scope {mapG pureG multG}
  {A}%type_scope (a) {Idempotent}.


(** ** <<pure>> is always CI *)
(**********************************************************************)
Section purity.

  Context `{Applicative G}.

  #[export] Instance Idempotent_Pure: forall (A: Type) (a: A),
      Idempotent G A (pure a).G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
forall (A : Type) (a : A), Idempotent G A (pure a)
  Proof.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
forall (A : Type) (a : A), Idempotent G A (pure a)
    intros.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
a: A
Idempotent G A (pure a)
    constructor.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
a: A
pure a ⊗ pure a = map (fun a : A => (a, a)) (pure a)
    rewrite app_mult_pure.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
a: A
pure (a, a) = map (fun a : A => (a, a)) (pure a)
    rewrite app_pure_natural.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
a: A
pure (a, a) = pure (a, a)
    reflexivity.
  Qed.

  #[export] Instance Center_Pure: forall (A: Type) (a: A),
      Center G A (pure a).G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
forall (A : Type) (a : A), Center G A (pure a)
  Proof.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
forall (A : Type) (a : A), Center G A (pure a)
    intros.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
a: A
Center G A (pure a)
    constructor; intros.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
a: A
B: Type
x: G B
x ⊗ pure a = map (fun '(x, y) => (y, x)) (pure a ⊗ x)
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
a: A
B: Type
x: G B
pure a ⊗ x = map (fun '(x, y) => (y, x)) (x ⊗ pure a)
    -G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
a: A
B: Type
x: G B
x ⊗ pure a = map (fun '(x, y) => (y, x)) (pure a ⊗ x) rewrite triangle_3.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
a: A
B: Type
x: G B
x ⊗ pure a =
map (fun '(x, y) => (y, x)) (strength (a, x))
      rewrite triangle_4.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
a: A
B: Type
x: G B
map (fun b : B => (b, a)) x =
map (fun '(x, y) => (y, x)) (strength (a, x))
      unfold strength.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
a: A
B: Type
x: G B
map (fun b : B => (b, a)) x =
map (fun '(x, y) => (y, x)) (map (pair a) x)
      compose near x on right.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
a: A
B: Type
x: G B
map (fun b : B => (b, a)) x =
(map (fun '(x, y) => (y, x)) ∘ map (pair a)) x
      rewrite (fun_map_map).G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
a: A
B: Type
x: G B
map (fun b : B => (b, a)) x =
map ((fun '(x, y) => (y, x)) ∘ pair a) x
      reflexivity.
    -G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
a: A
B: Type
x: G B
pure a ⊗ x = map (fun '(x, y) => (y, x)) (x ⊗ pure a) rewrite triangle_3.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
a: A
B: Type
x: G B
strength (a, x) =
map (fun '(x, y) => (y, x)) (x ⊗ pure a)
      rewrite triangle_4.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
a: A
B: Type
x: G B
strength (a, x) =
map (fun '(x, y) => (y, x))
  (map (fun b : B => (b, a)) x)
      unfold strength.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
a: A
B: Type
x: G B
map (pair a) x =
map (fun '(x, y) => (y, x))
  (map (fun b : B => (b, a)) x)
      compose near x on right.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
a: A
B: Type
x: G B
map (pair a) x =
(map (fun '(x, y) => (y, x))
 ∘ map (fun b : B => (b, a))) x
      rewrite (fun_map_map).G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
a: A
B: Type
x: G B
map (pair a) x =
map ((fun '(x, y) => (y, x)) ∘ (fun b : B => (b, a)))
  x
      reflexivity.
  Qed.


  #[export] Instance IdempotentCenter_Pure: forall (A: Type) (a: A),
      IdempotentCenter G A (pure a).G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
forall (A : Type) (a : A),
IdempotentCenter G A (pure a)
  Proof.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
forall (A : Type) (a : A),
IdempotentCenter G A (pure a)
    constructor;
      typeclasses eauto.
  Qed.

End purity.

(** ** Everything is always CI for <<(fun A => A)>> *)
(**********************************************************************)
Section purity.

  #[export] Instance Idempotent_I: forall (A: Type) (a: A),
      Idempotent (fun A => A) A (pure a).forall (A : Type) (a : A),
Idempotent (fun A0 : Type => A0) A (pure a)
  Proof.forall (A : Type) (a : A),
Idempotent (fun A0 : Type => A0) A (pure a)
    intros.A: Type
a: A
Idempotent (fun A : Type => A) A (pure a)
    constructor.A: Type
a: A
pure a ⊗ pure a = map (fun a : A => (a, a)) (pure a)
    reflexivity.
  Qed.

  #[export] Instance Center_I: forall (A: Type) (a: A),
      Center (fun A => A) A (pure a).forall (A : Type) (a : A),
Center (fun A0 : Type => A0) A (pure a)
  Proof.forall (A : Type) (a : A),
Center (fun A0 : Type => A0) A (pure a)
    intros.A: Type
a: A
Center (fun A : Type => A) A (pure a)
    constructor.A: Type
a: A
forall (B : Type) (x : B),
x ⊗ pure a =
map (fun '(x0, y) => (y, x0)) (pure a ⊗ x)
A: Type
a: A
forall (B : Type) (x : B),
pure a ⊗ x =
map (fun '(x0, y) => (y, x0)) (x ⊗ pure a)
    reflexivity.A: Type
a: A
forall (B : Type) (x : B),
pure a ⊗ x =
map (fun '(x0, y) => (y, x0)) (x ⊗ pure a)
    reflexivity.
  Qed.

  #[export] Instance IdempotentCenter_I: forall (A: Type) (a: A),
      IdempotentCenter (fun A => A) A (pure a).forall (A : Type) (a : A),
IdempotentCenter (fun A0 : Type => A0) A (pure a)
  Proof.forall (A : Type) (a : A),
IdempotentCenter (fun A0 : Type => A0) A (pure a)
    constructor;
      typeclasses eauto.
  Qed.

End purity.

(** ** Rewriting Laws for C-I Elements *)
(**********************************************************************)
Section rewriting_commutative_idempotent_element.

  Context
    {G: Type -> Type}
    `{mapG: Map G} `{pureG: Pure G} `{multG: Mult G}
    `{appG: ! Applicative G}.

  Lemma ap_swap
    {A B: Type}
    {f: G (A -> B)}
    {a: G A}
    `{center_a: ! Center G A a}:
    f <⋆> a = (map evalAt a) <⋆> f.G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B: Type
f: G (A -> B)
a: G A
center_a: Center G A a
f <⋆> a = map evalAt a <⋆> f
  Proof.G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B: Type
f: G (A -> B)
a: G A
center_a: Center G A a
f <⋆> a = map evalAt a <⋆> f
    unfold ap.G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B: Type
f: G (A -> B)
a: G A
center_a: Center G A a
map (fun '(f, a) => f a) (f ⊗ a) =
map (fun '(f, a) => f a) (map evalAt a ⊗ f)
    rewrite (appcenter_left a).G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B: Type
f: G (A -> B)
a: G A
center_a: Center G A a
map (fun '(f, a) => f a)
  (map (fun '(x, y) => (y, x)) (a ⊗ f)) =
map (fun '(f, a) => f a) (map evalAt a ⊗ f)
    compose near (a ⊗ f).G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B: Type
f: G (A -> B)
a: G A
center_a: Center G A a
(map (fun '(f, a) => f a)
 ∘ map (fun '(x, y) => (y, x))) (a ⊗ f) =
map (fun '(f, a) => f a) (map evalAt a ⊗ f)
    rewrite (fun_map_map).G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B: Type
f: G (A -> B)
a: G A
center_a: Center G A a
map ((fun '(f, a) => f a) ∘ (fun '(x, y) => (y, x)))
  (a ⊗ f) =
map (fun '(f, a) => f a) (map evalAt a ⊗ f)
    rewrite (app_mult_natural_l G).G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B: Type
f: G (A -> B)
a: G A
center_a: Center G A a
map ((fun '(f, a) => f a) ∘ (fun '(x, y) => (y, x)))
  (a ⊗ f) =
map (fun '(f, a) => f a)
  (map (map_fst evalAt) (a ⊗ f))
    compose near (a ⊗ f) on right.G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B: Type
f: G (A -> B)
a: G A
center_a: Center G A a
map ((fun '(f, a) => f a) ∘ (fun '(x, y) => (y, x)))
  (a ⊗ f) =
(map (fun '(f, a) => f a) ∘ map (map_fst evalAt))
  (a ⊗ f)
    rewrite (fun_map_map).G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B: Type
f: G (A -> B)
a: G A
center_a: Center G A a
map ((fun '(f, a) => f a) ∘ (fun '(x, y) => (y, x)))
  (a ⊗ f) =
map ((fun '(f, a) => f a) ∘ map_fst evalAt) (a ⊗ f)
    fequal.G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B: Type
f: G (A -> B)
a: G A
center_a: Center G A a
(fun '(f, a) => f a) ∘ (fun '(x, y) => (y, x)) =
(fun '(f, a) => f a) ∘ map_fst evalAt
    ext [x y].G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B: Type
f: G (A -> B)
a: G A
center_a: Center G A a
x: A
y: A -> B
((fun '(f, a) => f a) ∘ (fun '(x, y) => (y, x)))
  (x, y) =
((fun '(f, a) => f a) ∘ map_fst evalAt) (x, y)
    cbn.G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B: Type
f: G (A -> B)
a: G A
center_a: Center G A a
x: A
y: A -> B
y x = evalAt x (id y) reflexivity.
  Qed.

  Lemma ap_flip1
    {A B C: Type}
    {f: G (A -> B -> C)}
    {lhs: G A}
    {rhs: G B}
    `{center_rhs: ! Center G B rhs}:
    f <⋆> lhs <⋆> rhs =
      (map flip f) <⋆> rhs <⋆> lhs.G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B, C: Type
f: G (A -> B -> C)
lhs: G A
rhs: G B
center_rhs: Center G B rhs
f <⋆> lhs <⋆> rhs = map flip f <⋆> rhs <⋆> lhs
  Proof.G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B, C: Type
f: G (A -> B -> C)
lhs: G A
rhs: G B
center_rhs: Center G B rhs
f <⋆> lhs <⋆> rhs = map flip f <⋆> rhs <⋆> lhs
    (* LHS *)
    rewrite ap_swap.G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B, C: Type
f: G (A -> B -> C)
lhs: G A
rhs: G B
center_rhs: Center G B rhs
map evalAt rhs <⋆> (f <⋆> lhs) =
map flip f <⋆> rhs <⋆> lhs
    rewrite map_to_ap.G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B, C: Type
f: G (A -> B -> C)
lhs: G A
rhs: G B
center_rhs: Center G B rhs
pure evalAt <⋆> rhs <⋆> (f <⋆> lhs) =
map flip f <⋆> rhs <⋆> lhs
    rewrite <- ap4.G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B, C: Type
f: G (A -> B -> C)
lhs: G A
rhs: G B
center_rhs: Center G B rhs
pure compose <⋆> (pure evalAt <⋆> rhs) <⋆> f <⋆> lhs =
map flip f <⋆> rhs <⋆> lhs
    rewrite <- ap4.G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B, C: Type
f: G (A -> B -> C)
lhs: G A
rhs: G B
center_rhs: Center G B rhs
pure compose <⋆> pure compose <⋆> pure evalAt <⋆> rhs <⋆>
f <⋆> lhs = map flip f <⋆> rhs <⋆> lhs
    rewrite ap2.G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B, C: Type
f: G (A -> B -> C)
lhs: G A
rhs: G B
center_rhs: Center G B rhs
pure (compose compose) <⋆> pure evalAt <⋆> rhs <⋆> f <⋆>
lhs = map flip f <⋆> rhs <⋆> lhs
    rewrite ap2.G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B, C: Type
f: G (A -> B -> C)
lhs: G A
rhs: G B
center_rhs: Center G B rhs
pure (compose ∘ evalAt) <⋆> rhs <⋆> f <⋆> lhs =
map flip f <⋆> rhs <⋆> lhs
    (* RHS *)
    rewrite (ap_swap (f := map flip f) (a := rhs)).G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B, C: Type
f: G (A -> B -> C)
lhs: G A
rhs: G B
center_rhs: Center G B rhs
pure (compose ∘ evalAt) <⋆> rhs <⋆> f <⋆> lhs =
map evalAt rhs <⋆> map flip f <⋆> lhs
    rewrite map_to_ap.G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B, C: Type
f: G (A -> B -> C)
lhs: G A
rhs: G B
center_rhs: Center G B rhs
pure (compose ∘ evalAt) <⋆> rhs <⋆> f <⋆> lhs =
pure evalAt <⋆> rhs <⋆> map flip f <⋆> lhs
    rewrite map_to_ap.G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B, C: Type
f: G (A -> B -> C)
lhs: G A
rhs: G B
center_rhs: Center G B rhs
pure (compose ∘ evalAt) <⋆> rhs <⋆> f <⋆> lhs =
pure evalAt <⋆> rhs <⋆> (pure flip <⋆> f) <⋆> lhs
    rewrite <- ap4.G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B, C: Type
f: G (A -> B -> C)
lhs: G A
rhs: G B
center_rhs: Center G B rhs
pure (compose ∘ evalAt) <⋆> rhs <⋆> f <⋆> lhs =
pure compose <⋆> (pure evalAt <⋆> rhs) <⋆> pure flip <⋆>
f <⋆> lhs
    rewrite <- ap4.G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B, C: Type
f: G (A -> B -> C)
lhs: G A
rhs: G B
center_rhs: Center G B rhs
pure (compose ∘ evalAt) <⋆> rhs <⋆> f <⋆> lhs =
pure compose <⋆> pure compose <⋆> pure evalAt <⋆> rhs <⋆>
pure flip <⋆> f <⋆> lhs
    rewrite ap2.G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B, C: Type
f: G (A -> B -> C)
lhs: G A
rhs: G B
center_rhs: Center G B rhs
pure (compose ∘ evalAt) <⋆> rhs <⋆> f <⋆> lhs =
pure (compose compose) <⋆> pure evalAt <⋆> rhs <⋆>
pure flip <⋆> f <⋆> lhs
    rewrite ap2.G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B, C: Type
f: G (A -> B -> C)
lhs: G A
rhs: G B
center_rhs: Center G B rhs
pure (compose ∘ evalAt) <⋆> rhs <⋆> f <⋆> lhs =
pure (compose ∘ evalAt) <⋆> rhs <⋆> pure flip <⋆> f <⋆>
lhs
    rewrite ap3.G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B, C: Type
f: G (A -> B -> C)
lhs: G A
rhs: G B
center_rhs: Center G B rhs
pure (compose ∘ evalAt) <⋆> rhs <⋆> f <⋆> lhs =
pure (evalAt flip) <⋆>
(pure (compose ∘ evalAt) <⋆> rhs) <⋆> f <⋆> lhs
    rewrite <- ap4.G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B, C: Type
f: G (A -> B -> C)
lhs: G A
rhs: G B
center_rhs: Center G B rhs
pure (compose ∘ evalAt) <⋆> rhs <⋆> f <⋆> lhs =
pure compose <⋆> pure (evalAt flip) <⋆>
pure (compose ∘ evalAt) <⋆> rhs <⋆> f <⋆> lhs
    rewrite ap2.G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B, C: Type
f: G (A -> B -> C)
lhs: G A
rhs: G B
center_rhs: Center G B rhs
pure (compose ∘ evalAt) <⋆> rhs <⋆> f <⋆> lhs =
pure (compose (evalAt flip)) <⋆>
pure (compose ∘ evalAt) <⋆> rhs <⋆> f <⋆> lhs
    rewrite ap2.G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B, C: Type
f: G (A -> B -> C)
lhs: G A
rhs: G B
center_rhs: Center G B rhs
pure (compose ∘ evalAt) <⋆> rhs <⋆> f <⋆> lhs =
pure (evalAt flip ∘ (compose ∘ evalAt)) <⋆> rhs <⋆> f <⋆>
lhs
    reflexivity.
  Qed.

  Lemma ap_flip2
    {A B C: Type}
    {f: G (A -> B -> C)}
    {lhs: G A}
    {rhs: G B}
    `{center_lhs: ! Center G A lhs}:
    f <⋆> lhs <⋆> rhs =
      (map flip f) <⋆> rhs <⋆> lhs.G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B, C: Type
f: G (A -> B -> C)
lhs: G A
rhs: G B
center_lhs: Center G A lhs
f <⋆> lhs <⋆> rhs = map flip f <⋆> rhs <⋆> lhs
  Proof.G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B, C: Type
f: G (A -> B -> C)
lhs: G A
rhs: G B
center_lhs: Center G A lhs
f <⋆> lhs <⋆> rhs = map flip f <⋆> rhs <⋆> lhs
    (* LHS *)
    rewrite (ap_flip1 (rhs := lhs)).G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B, C: Type
f: G (A -> B -> C)
lhs: G A
rhs: G B
center_lhs: Center G A lhs
f <⋆> lhs <⋆> rhs =
map flip (map flip f) <⋆> lhs <⋆> rhs
    compose near f.G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B, C: Type
f: G (A -> B -> C)
lhs: G A
rhs: G B
center_lhs: Center G A lhs
f <⋆> lhs <⋆> rhs =
(map flip ∘ map flip) f <⋆> lhs <⋆> rhs
    rewrite fun_map_map.G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B, C: Type
f: G (A -> B -> C)
lhs: G A
rhs: G B
center_lhs: Center G A lhs
f <⋆> lhs <⋆> rhs =
map (flip ∘ flip) f <⋆> lhs <⋆> rhs
    change (flip ∘ flip) with (@id (A -> B -> C)).G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B, C: Type
f: G (A -> B -> C)
lhs: G A
rhs: G B
center_lhs: Center G A lhs
f <⋆> lhs <⋆> rhs = map id f <⋆> lhs <⋆> rhs
    rewrite fun_map_id.G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B, C: Type
f: G (A -> B -> C)
lhs: G A
rhs: G B
center_lhs: Center G A lhs
f <⋆> lhs <⋆> rhs = id f <⋆> lhs <⋆> rhs
    reflexivity.
  Qed.

  (* compose flip = (fun f a c b => f a b c) *)
  Corollary ap_flip_x3
    {A B C D: Type}
    {f: G (A -> B -> C -> D)}
    {a: G A}
    {lhs: G B}
    {rhs: G C}
    `{center_rhs: ! Center G C rhs}:
    f <⋆> a <⋆> lhs <⋆> rhs =
      map (compose flip) f <⋆> a <⋆> rhs <⋆> lhs.G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B, C, D: Type
f: G (A -> B -> C -> D)
a: G A
lhs: G B
rhs: G C
center_rhs: Center G C rhs
f <⋆> a <⋆> lhs <⋆> rhs =
map (compose flip) f <⋆> a <⋆> rhs <⋆> lhs
  Proof.G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B, C, D: Type
f: G (A -> B -> C -> D)
a: G A
lhs: G B
rhs: G C
center_rhs: Center G C rhs
f <⋆> a <⋆> lhs <⋆> rhs =
map (compose flip) f <⋆> a <⋆> rhs <⋆> lhs
    rewrite ap_flip1.G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B, C, D: Type
f: G (A -> B -> C -> D)
a: G A
lhs: G B
rhs: G C
center_rhs: Center G C rhs
map flip (f <⋆> a) <⋆> rhs <⋆> lhs =
map (compose flip) f <⋆> a <⋆> rhs <⋆> lhs
    rewrite map_ap.G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B, C, D: Type
f: G (A -> B -> C -> D)
a: G A
lhs: G B
rhs: G C
center_rhs: Center G C rhs
map (compose flip) f <⋆> a <⋆> rhs <⋆> lhs =
map (compose flip) f <⋆> a <⋆> rhs <⋆> lhs
    reflexivity.
  Qed.

  Corollary ap_flip_x4
    {A B C D E: Type}
    {f: G (A -> B -> C -> D -> E)}
    {a: G A}
    {b: G B}
    {lhs: G C}
    {rhs: G D}
    `{center_rhs: ! Center G D rhs}:
    f <⋆> a <⋆> b <⋆> lhs <⋆> rhs =
      map (compose (compose flip)) f <⋆> a <⋆> b <⋆> rhs <⋆> lhs.G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B, C, D, E: Type
f: G (A -> B -> C -> D -> E)
a: G A
b: G B
lhs: G C
rhs: G D
center_rhs: Center G D rhs
f <⋆> a <⋆> b <⋆> lhs <⋆> rhs =
map (compose (compose flip)) f <⋆> a <⋆> b <⋆> rhs <⋆>
lhs
  Proof.G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B, C, D, E: Type
f: G (A -> B -> C -> D -> E)
a: G A
b: G B
lhs: G C
rhs: G D
center_rhs: Center G D rhs
f <⋆> a <⋆> b <⋆> lhs <⋆> rhs =
map (compose (compose flip)) f <⋆> a <⋆> b <⋆> rhs <⋆>
lhs
    rewrite ap_flip1.G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B, C, D, E: Type
f: G (A -> B -> C -> D -> E)
a: G A
b: G B
lhs: G C
rhs: G D
center_rhs: Center G D rhs
map flip (f <⋆> a <⋆> b) <⋆> rhs <⋆> lhs =
map (compose (compose flip)) f <⋆> a <⋆> b <⋆> rhs <⋆>
lhs
    rewrite map_ap.G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B, C, D, E: Type
f: G (A -> B -> C -> D -> E)
a: G A
b: G B
lhs: G C
rhs: G D
center_rhs: Center G D rhs
map (compose flip) (f <⋆> a) <⋆> b <⋆> rhs <⋆> lhs =
map (compose (compose flip)) f <⋆> a <⋆> b <⋆> rhs <⋆>
lhs
    rewrite map_ap.G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B, C, D, E: Type
f: G (A -> B -> C -> D -> E)
a: G A
b: G B
lhs: G C
rhs: G D
center_rhs: Center G D rhs
map (compose (compose flip)) f <⋆> a <⋆> b <⋆> rhs <⋆>
lhs =
map (compose (compose flip)) f <⋆> a <⋆> b <⋆> rhs <⋆>
lhs
    reflexivity.
  Qed.

  Corollary ap_flip_x5
    {A B C D E F: Type}
    {f: G (A -> B -> C -> D -> E -> F)}
    {a: G A}
    {b: G B}
    {c: G C}
    {lhs: G D}
    {rhs: G E}
    `{center_rhs: ! Center G E rhs}:
      f <⋆> a <⋆> b <⋆> c <⋆> lhs <⋆> rhs =
      map (compose (compose (compose flip))) f <⋆>
        a <⋆> b <⋆> c <⋆> rhs <⋆> lhs.G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B, C, D, E, F: Type
f: G (A -> B -> C -> D -> E -> F)
a: G A
b: G B
c: G C
lhs: G D
rhs: G E
center_rhs: Center G E rhs
f <⋆> a <⋆> b <⋆> c <⋆> lhs <⋆> rhs =
map (compose (compose (compose flip))) f <⋆> a <⋆> b <⋆>
c <⋆> rhs <⋆> lhs
  Proof.G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B, C, D, E, F: Type
f: G (A -> B -> C -> D -> E -> F)
a: G A
b: G B
c: G C
lhs: G D
rhs: G E
center_rhs: Center G E rhs
f <⋆> a <⋆> b <⋆> c <⋆> lhs <⋆> rhs =
map (compose (compose (compose flip))) f <⋆> a <⋆> b <⋆>
c <⋆> rhs <⋆> lhs
    rewrite ap_flip1.G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B, C, D, E, F: Type
f: G (A -> B -> C -> D -> E -> F)
a: G A
b: G B
c: G C
lhs: G D
rhs: G E
center_rhs: Center G E rhs
map flip (f <⋆> a <⋆> b <⋆> c) <⋆> rhs <⋆> lhs =
map (compose (compose (compose flip))) f <⋆> a <⋆> b <⋆>
c <⋆> rhs <⋆> lhs
    rewrite map_ap.G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B, C, D, E, F: Type
f: G (A -> B -> C -> D -> E -> F)
a: G A
b: G B
c: G C
lhs: G D
rhs: G E
center_rhs: Center G E rhs
map (compose flip) (f <⋆> a <⋆> b) <⋆> c <⋆> rhs <⋆>
lhs =
map (compose (compose (compose flip))) f <⋆> a <⋆> b <⋆>
c <⋆> rhs <⋆> lhs
    rewrite map_ap.G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B, C, D, E, F: Type
f: G (A -> B -> C -> D -> E -> F)
a: G A
b: G B
c: G C
lhs: G D
rhs: G E
center_rhs: Center G E rhs
map (compose (compose flip)) (f <⋆> a) <⋆> b <⋆> c <⋆>
rhs <⋆> lhs =
map (compose (compose (compose flip))) f <⋆> a <⋆> b <⋆>
c <⋆> rhs <⋆> lhs
    rewrite map_ap.G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B, C, D, E, F: Type
f: G (A -> B -> C -> D -> E -> F)
a: G A
b: G B
c: G C
lhs: G D
rhs: G E
center_rhs: Center G E rhs
map (compose (compose (compose flip))) f <⋆> a <⋆> b <⋆>
c <⋆> rhs <⋆> lhs =
map (compose (compose (compose flip))) f <⋆> a <⋆> b <⋆>
c <⋆> rhs <⋆> lhs
    reflexivity.
  Qed.

  Corollary ap_flip_x6
    {A B C D E F J: Type}
    {f: G (A -> B -> C -> D -> E -> F -> J)}
    {a: G A}
    {b: G B}
    {c: G C}
    {d: G D}
    {lhs: G E}
    {rhs: G F}
    `{center_rhs: ! Center G F rhs}:
    f <⋆> a <⋆> b <⋆> c <⋆> d <⋆> lhs <⋆> rhs =
      map (compose (compose (compose (compose flip)))) f <⋆>
        a <⋆> b <⋆> c <⋆> d <⋆> rhs <⋆> lhs.G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B, C, D, E, F, J: Type
f: G (A -> B -> C -> D -> E -> F -> J)
a: G A
b: G B
c: G C
d: G D
lhs: G E
rhs: G F
center_rhs: Center G F rhs
f <⋆> a <⋆> b <⋆> c <⋆> d <⋆> lhs <⋆> rhs =
map (compose (compose (compose (compose flip)))) f <⋆>
a <⋆> b <⋆> c <⋆> d <⋆> rhs <⋆> lhs
  Proof.G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B, C, D, E, F, J: Type
f: G (A -> B -> C -> D -> E -> F -> J)
a: G A
b: G B
c: G C
d: G D
lhs: G E
rhs: G F
center_rhs: Center G F rhs
f <⋆> a <⋆> b <⋆> c <⋆> d <⋆> lhs <⋆> rhs =
map (compose (compose (compose (compose flip)))) f <⋆>
a <⋆> b <⋆> c <⋆> d <⋆> rhs <⋆> lhs
    rewrite ap_flip1.G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B, C, D, E, F, J: Type
f: G (A -> B -> C -> D -> E -> F -> J)
a: G A
b: G B
c: G C
d: G D
lhs: G E
rhs: G F
center_rhs: Center G F rhs
map flip (f <⋆> a <⋆> b <⋆> c <⋆> d) <⋆> rhs <⋆> lhs =
map (compose (compose (compose (compose flip)))) f <⋆>
a <⋆> b <⋆> c <⋆> d <⋆> rhs <⋆> lhs
    rewrite map_ap.G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B, C, D, E, F, J: Type
f: G (A -> B -> C -> D -> E -> F -> J)
a: G A
b: G B
c: G C
d: G D
lhs: G E
rhs: G F
center_rhs: Center G F rhs
map (compose flip) (f <⋆> a <⋆> b <⋆> c) <⋆> d <⋆> rhs <⋆>
lhs =
map (compose (compose (compose (compose flip)))) f <⋆>
a <⋆> b <⋆> c <⋆> d <⋆> rhs <⋆> lhs
    rewrite map_ap.G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B, C, D, E, F, J: Type
f: G (A -> B -> C -> D -> E -> F -> J)
a: G A
b: G B
c: G C
d: G D
lhs: G E
rhs: G F
center_rhs: Center G F rhs
map (compose (compose flip)) (f <⋆> a <⋆> b) <⋆> c <⋆>
d <⋆> rhs <⋆> lhs =
map (compose (compose (compose (compose flip)))) f <⋆>
a <⋆> b <⋆> c <⋆> d <⋆> rhs <⋆> lhs
    rewrite map_ap.G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B, C, D, E, F, J: Type
f: G (A -> B -> C -> D -> E -> F -> J)
a: G A
b: G B
c: G C
d: G D
lhs: G E
rhs: G F
center_rhs: Center G F rhs
map (compose (compose (compose flip))) (f <⋆> a) <⋆> b <⋆>
c <⋆> d <⋆> rhs <⋆> lhs =
map (compose (compose (compose (compose flip)))) f <⋆>
a <⋆> b <⋆> c <⋆> d <⋆> rhs <⋆> lhs
    rewrite map_ap.G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B, C, D, E, F, J: Type
f: G (A -> B -> C -> D -> E -> F -> J)
a: G A
b: G B
c: G C
d: G D
lhs: G E
rhs: G F
center_rhs: Center G F rhs
map (compose (compose (compose (compose flip)))) f <⋆>
a <⋆> b <⋆> c <⋆> d <⋆> rhs <⋆> lhs =
map (compose (compose (compose (compose flip)))) f <⋆>
a <⋆> b <⋆> c <⋆> d <⋆> rhs <⋆> lhs
    reflexivity.
  Qed.

  Definition double_input {A B: Type} (f: A -> A -> B): A -> B :=
    uncurry f ∘ dup.

  Lemma ap_contract
    {A B: Type}
    {f: G (A -> A -> B)}
    {contract: G A}
    `{idem_contract: ! Idempotent G A contract}:
    f <⋆> contract <⋆> contract = (map double_input f) <⋆> contract.G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B: Type
f: G (A -> A -> B)
contract: G A
idem_contract: Idempotent G A contract
f <⋆> contract <⋆> contract =
map double_input f <⋆> contract
  Proof.G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B: Type
f: G (A -> A -> B)
contract: G A
idem_contract: Idempotent G A contract
f <⋆> contract <⋆> contract =
map double_input f <⋆> contract
    unfold ap.G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B: Type
f: G (A -> A -> B)
contract: G A
idem_contract: Idempotent G A contract
map (fun '(f, a) => f a)
  (map (fun '(f, a) => f a) (f ⊗ contract) ⊗ contract) =
map (fun '(f, a) => f a)
  (map double_input f ⊗ contract)
    unfold ap.G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B: Type
f: G (A -> A -> B)
contract: G A
idem_contract: Idempotent G A contract
map (fun '(f, a) => f a)
  (map (fun '(f, a) => f a) (f ⊗ contract) ⊗ contract) =
map (fun '(f, a) => f a)
  (map double_input f ⊗ contract)
    rewrite (app_mult_natural_l G).G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B: Type
f: G (A -> A -> B)
contract: G A
idem_contract: Idempotent G A contract
map (fun '(f, a) => f a)
  (map (map_fst (fun '(f, a) => f a))
     (f ⊗ contract ⊗ contract)) =
map (fun '(f, a) => f a)
  (map double_input f ⊗ contract)
    compose near (f ⊗ contract ⊗ contract).G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B: Type
f: G (A -> A -> B)
contract: G A
idem_contract: Idempotent G A contract
(map (fun '(f, a) => f a)
 ∘ map (map_fst (fun '(f, a) => f a)))
  (f ⊗ contract ⊗ contract) =
map (fun '(f, a) => f a)
  (map double_input f ⊗ contract)
    rewrite (fun_map_map).G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B: Type
f: G (A -> A -> B)
contract: G A
idem_contract: Idempotent G A contract
map
  ((fun '(f, a) => f a) ∘ map_fst (fun '(f, a) => f a))
  (f ⊗ contract ⊗ contract) =
map (fun '(f, a) => f a)
  (map double_input f ⊗ contract)
    rewrite <- (app_assoc_inv G).G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B: Type
f: G (A -> A -> B)
contract: G A
idem_contract: Idempotent G A contract
map
  ((fun '(f, a) => f a) ∘ map_fst (fun '(f, a) => f a))
  (map α^-1 (f ⊗ (contract ⊗ contract))) =
map (fun '(f, a) => f a)
  (map double_input f ⊗ contract)
    rewrite (appidem contract).G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B: Type
f: G (A -> A -> B)
contract: G A
idem_contract: Idempotent G A contract
map
  ((fun '(f, a) => f a) ∘ map_fst (fun '(f, a) => f a))
  (map α^-1 (f ⊗ map (fun a : A => (a, a)) contract)) =
map (fun '(f, a) => f a)
  (map double_input f ⊗ contract)
    rewrite (app_mult_natural_r G).G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B: Type
f: G (A -> A -> B)
contract: G A
idem_contract: Idempotent G A contract
map
  ((fun '(f, a) => f a) ∘ map_fst (fun '(f, a) => f a))
  (map α^-1
     (map (map_snd (fun a : A => (a, a)))
        (f ⊗ contract))) =
map (fun '(f, a) => f a)
  (map double_input f ⊗ contract)
    compose near (f ⊗ contract).G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B: Type
f: G (A -> A -> B)
contract: G A
idem_contract: Idempotent G A contract
map
  ((fun '(f, a) => f a) ∘ map_fst (fun '(f, a) => f a))
  ((map α^-1 ∘ map (map_snd (fun a : A => (a, a))))
     (f ⊗ contract)) =
map (fun '(f, a) => f a)
  (map double_input f ⊗ contract)
    rewrite (fun_map_map).G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B: Type
f: G (A -> A -> B)
contract: G A
idem_contract: Idempotent G A contract
map
  ((fun '(f, a) => f a) ∘ map_fst (fun '(f, a) => f a))
  (map (α^-1 ∘ map_snd (fun a : A => (a, a)))
     (f ⊗ contract)) =
map (fun '(f, a) => f a)
  (map double_input f ⊗ contract)
    compose near (f ⊗ contract).G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B: Type
f: G (A -> A -> B)
contract: G A
idem_contract: Idempotent G A contract
(map
   ((fun '(f, a) => f a)
    ∘ map_fst (fun '(f, a) => f a))
 ∘ map (α^-1 ∘ map_snd (fun a : A => (a, a))))
  (f ⊗ contract) =
map (fun '(f, a) => f a)
  (map double_input f ⊗ contract)
    rewrite (fun_map_map).G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B: Type
f: G (A -> A -> B)
contract: G A
idem_contract: Idempotent G A contract
map
  ((fun '(f, a) => f a) ∘ map_fst (fun '(f, a) => f a)
   ∘ (α^-1 ∘ map_snd (fun a : A => (a, a))))
  (f ⊗ contract) =
map (fun '(f, a) => f a)
  (map double_input f ⊗ contract)
    (* rhs *)
    rewrite (app_mult_natural_l G).G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B: Type
f: G (A -> A -> B)
contract: G A
idem_contract: Idempotent G A contract
map
  ((fun '(f, a) => f a) ∘ map_fst (fun '(f, a) => f a)
   ∘ (α^-1 ∘ map_snd (fun a : A => (a, a))))
  (f ⊗ contract) =
map (fun '(f, a) => f a)
  (map (map_fst double_input) (f ⊗ contract))
    compose near (f ⊗ contract).G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B: Type
f: G (A -> A -> B)
contract: G A
idem_contract: Idempotent G A contract
(eq
 ∘ map
     ((fun '(f, a) => f a)
      ∘ map_fst (fun '(f, a) => f a)
      ∘ (α^-1 ∘ map_snd (fun a : A => (a, a)))))
  (f ⊗ contract)
  ((map (fun '(f, a) => f a)
    ∘ map (map_fst double_input)) (f ⊗ contract))
    rewrite (fun_map_map).G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B: Type
f: G (A -> A -> B)
contract: G A
idem_contract: Idempotent G A contract
(eq
 ∘ map
     ((fun '(f, a) => f a)
      ∘ map_fst (fun '(f, a) => f a)
      ∘ (α^-1 ∘ map_snd (fun a : A => (a, a)))))
  (f ⊗ contract)
  (map ((fun '(f, a) => f a) ∘ map_fst double_input)
     (f ⊗ contract))
    fequal.G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B: Type
f: G (A -> A -> B)
contract: G A
idem_contract: Idempotent G A contract
(fun '(f, a) => f a) ∘ map_fst (fun '(f, a) => f a)
∘ (α^-1 ∘ map_snd (fun a : A => (a, a))) =
(fun '(f, a) => f a) ∘ map_fst double_input
    ext [x y].G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B: Type
f: G (A -> A -> B)
contract: G A
idem_contract: Idempotent G A contract
x: A -> A -> B
y: A
((fun '(f, a) => f a) ∘ map_fst (fun '(f, a) => f a)
 ∘ (α^-1 ∘ map_snd (fun a : A => (a, a)))) (x, y) =
((fun '(f, a) => f a) ∘ map_fst double_input) (x, y)
    cbn.G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B: Type
f: G (A -> A -> B)
contract: G A
idem_contract: Idempotent G A contract
x: A -> A -> B
y: A
id x y (id y) = x (id y) (id y) reflexivity.
  Qed.

  Corollary ap_contract2
    {A B C: Type}
    {f: G (A -> B -> B -> C)}
    {a: G A}
    {contract: G B}
    `{idem_contract: ! Idempotent G B contract}:
    f <⋆> a <⋆> contract <⋆> contract =
      (map (compose double_input) f) <⋆> a <⋆> contract.G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B, C: Type
f: G (A -> B -> B -> C)
a: G A
contract: G B
idem_contract: Idempotent G B contract
f <⋆> a <⋆> contract <⋆> contract =
map (compose double_input) f <⋆> a <⋆> contract
  Proof.G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B, C: Type
f: G (A -> B -> B -> C)
a: G A
contract: G B
idem_contract: Idempotent G B contract
f <⋆> a <⋆> contract <⋆> contract =
map (compose double_input) f <⋆> a <⋆> contract
    rewrite ap_contract.G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B, C: Type
f: G (A -> B -> B -> C)
a: G A
contract: G B
idem_contract: Idempotent G B contract
map double_input (f <⋆> a) <⋆> contract =
map (compose double_input) f <⋆> a <⋆> contract
    rewrite map_ap.G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B, C: Type
f: G (A -> B -> B -> C)
a: G A
contract: G B
idem_contract: Idempotent G B contract
map (compose double_input) f <⋆> a <⋆> contract =
map (compose double_input) f <⋆> a <⋆> contract
    reflexivity.
  Qed.

  Corollary ap_contract3
    {A B C D: Type}
    {f: G (A -> B -> C -> C -> D)}
    {a: G A}
    {b: G B}
    {contract: G C}
    `{idem_contract: ! Idempotent G C contract}:
    f <⋆> a <⋆> b <⋆> contract <⋆> contract =
      (map (compose (compose double_input)) f) <⋆> a <⋆> b <⋆> contract.G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B, C, D: Type
f: G (A -> B -> C -> C -> D)
a: G A
b: G B
contract: G C
idem_contract: Idempotent G C contract
f <⋆> a <⋆> b <⋆> contract <⋆> contract =
map (compose (compose double_input)) f <⋆> a <⋆> b <⋆>
contract
  Proof.G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B, C, D: Type
f: G (A -> B -> C -> C -> D)
a: G A
b: G B
contract: G C
idem_contract: Idempotent G C contract
f <⋆> a <⋆> b <⋆> contract <⋆> contract =
map (compose (compose double_input)) f <⋆> a <⋆> b <⋆>
contract
    rewrite ap_contract.G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B, C, D: Type
f: G (A -> B -> C -> C -> D)
a: G A
b: G B
contract: G C
idem_contract: Idempotent G C contract
map double_input (f <⋆> a <⋆> b) <⋆> contract =
map (compose (compose double_input)) f <⋆> a <⋆> b <⋆>
contract
    rewrite map_ap.G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B, C, D: Type
f: G (A -> B -> C -> C -> D)
a: G A
b: G B
contract: G C
idem_contract: Idempotent G C contract
map (compose double_input) (f <⋆> a) <⋆> b <⋆>
contract =
map (compose (compose double_input)) f <⋆> a <⋆> b <⋆>
contract
    rewrite map_ap.G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B, C, D: Type
f: G (A -> B -> C -> C -> D)
a: G A
b: G B
contract: G C
idem_contract: Idempotent G C contract
map (compose (compose double_input)) f <⋆> a <⋆> b <⋆>
contract =
map (compose (compose double_input)) f <⋆> a <⋆> b <⋆>
contract
    reflexivity.
  Qed.

  Corollary ap_contract4
    {A B C D E: Type}
    {f: G (A -> B -> C -> D -> D -> E)}
    {a: G A}
    {b: G B}
    {c: G C}
    {contract: G D}
    `{idem_contract: ! Idempotent G D contract}:
    f <⋆> a <⋆> b <⋆> c <⋆> contract <⋆> contract =
      (map (compose (compose (compose double_input))) f) <⋆>
        a <⋆> b <⋆> c <⋆> contract.G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B, C, D, E: Type
f: G (A -> B -> C -> D -> D -> E)
a: G A
b: G B
c: G C
contract: G D
idem_contract: Idempotent G D contract
f <⋆> a <⋆> b <⋆> c <⋆> contract <⋆> contract =
map (compose (compose (compose double_input))) f <⋆> a <⋆>
b <⋆> c <⋆> contract
  Proof.G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B, C, D, E: Type
f: G (A -> B -> C -> D -> D -> E)
a: G A
b: G B
c: G C
contract: G D
idem_contract: Idempotent G D contract
f <⋆> a <⋆> b <⋆> c <⋆> contract <⋆> contract =
map (compose (compose (compose double_input))) f <⋆> a <⋆>
b <⋆> c <⋆> contract
    rewrite ap_contract.G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B, C, D, E: Type
f: G (A -> B -> C -> D -> D -> E)
a: G A
b: G B
c: G C
contract: G D
idem_contract: Idempotent G D contract
map double_input (f <⋆> a <⋆> b <⋆> c) <⋆> contract =
map (compose (compose (compose double_input))) f <⋆> a <⋆>
b <⋆> c <⋆> contract
    rewrite map_ap.G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B, C, D, E: Type
f: G (A -> B -> C -> D -> D -> E)
a: G A
b: G B
c: G C
contract: G D
idem_contract: Idempotent G D contract
map (compose double_input) (f <⋆> a <⋆> b) <⋆> c <⋆>
contract =
map (compose (compose (compose double_input))) f <⋆> a <⋆>
b <⋆> c <⋆> contract
    rewrite map_ap.G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B, C, D, E: Type
f: G (A -> B -> C -> D -> D -> E)
a: G A
b: G B
c: G C
contract: G D
idem_contract: Idempotent G D contract
map (compose (compose double_input)) (f <⋆> a) <⋆> b <⋆>
c <⋆> contract =
map (compose (compose (compose double_input))) f <⋆> a <⋆>
b <⋆> c <⋆> contract
    rewrite map_ap.G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B, C, D, E: Type
f: G (A -> B -> C -> D -> D -> E)
a: G A
b: G B
c: G C
contract: G D
idem_contract: Idempotent G D contract
map (compose (compose (compose double_input))) f <⋆> a <⋆>
b <⋆> c <⋆> contract =
map (compose (compose (compose double_input))) f <⋆> a <⋆>
b <⋆> c <⋆> contract
    reflexivity.
  Qed.

  Corollary ap_contract5
    {A B C D E F: Type}
    {f: G (A -> B -> C -> D -> E -> E -> F)}
    {a: G A}
    {b: G B}
    {c: G C}
    {d: G D}
    {contract: G E}
    `{idem_contract: ! Idempotent G E contract}:
    f <⋆> a <⋆> b <⋆> c <⋆> d <⋆> contract <⋆> contract =
      (map (compose (compose (compose (compose double_input)))) f) <⋆>
        a <⋆> b <⋆> c <⋆> d <⋆> contract.G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B, C, D, E, F: Type
f: G (A -> B -> C -> D -> E -> E -> F)
a: G A
b: G B
c: G C
d: G D
contract: G E
idem_contract: Idempotent G E contract
f <⋆> a <⋆> b <⋆> c <⋆> d <⋆> contract <⋆> contract =
map
  (compose (compose (compose (compose double_input))))
  f <⋆> a <⋆> b <⋆> c <⋆> d <⋆> contract
  Proof.G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B, C, D, E, F: Type
f: G (A -> B -> C -> D -> E -> E -> F)
a: G A
b: G B
c: G C
d: G D
contract: G E
idem_contract: Idempotent G E contract
f <⋆> a <⋆> b <⋆> c <⋆> d <⋆> contract <⋆> contract =
map
  (compose (compose (compose (compose double_input))))
  f <⋆> a <⋆> b <⋆> c <⋆> d <⋆> contract
    rewrite ap_contract.G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B, C, D, E, F: Type
f: G (A -> B -> C -> D -> E -> E -> F)
a: G A
b: G B
c: G C
d: G D
contract: G E
idem_contract: Idempotent G E contract
map double_input (f <⋆> a <⋆> b <⋆> c <⋆> d) <⋆>
contract =
map
  (compose (compose (compose (compose double_input))))
  f <⋆> a <⋆> b <⋆> c <⋆> d <⋆> contract
    rewrite map_ap.G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B, C, D, E, F: Type
f: G (A -> B -> C -> D -> E -> E -> F)
a: G A
b: G B
c: G C
d: G D
contract: G E
idem_contract: Idempotent G E contract
map (compose double_input) (f <⋆> a <⋆> b <⋆> c) <⋆> d <⋆>
contract =
map
  (compose (compose (compose (compose double_input))))
  f <⋆> a <⋆> b <⋆> c <⋆> d <⋆> contract
    rewrite map_ap.G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B, C, D, E, F: Type
f: G (A -> B -> C -> D -> E -> E -> F)
a: G A
b: G B
c: G C
d: G D
contract: G E
idem_contract: Idempotent G E contract
map (compose (compose double_input)) (f <⋆> a <⋆> b) <⋆>
c <⋆> d <⋆> contract =
map
  (compose (compose (compose (compose double_input))))
  f <⋆> a <⋆> b <⋆> c <⋆> d <⋆> contract
    rewrite map_ap.G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B, C, D, E, F: Type
f: G (A -> B -> C -> D -> E -> E -> F)
a: G A
b: G B
c: G C
d: G D
contract: G E
idem_contract: Idempotent G E contract
map (compose (compose (compose double_input)))
  (f <⋆> a) <⋆> b <⋆> c <⋆> d <⋆> contract =
map
  (compose (compose (compose (compose double_input))))
  f <⋆> a <⋆> b <⋆> c <⋆> d <⋆> contract
    rewrite map_ap.G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B, C, D, E, F: Type
f: G (A -> B -> C -> D -> E -> E -> F)
a: G A
b: G B
c: G C
d: G D
contract: G E
idem_contract: Idempotent G E contract
map
  (compose (compose (compose (compose double_input))))
  f <⋆> a <⋆> b <⋆> c <⋆> d <⋆> contract =
map
  (compose (compose (compose (compose double_input))))
  f <⋆> a <⋆> b <⋆> c <⋆> d <⋆> contract
    reflexivity.
  Qed.

  Corollary ap_contract6
    {A B C D E F J: Type}
    {f: G (A -> B -> C -> D -> E -> F -> F -> J)}
    {a: G A}
    {b: G B}
    {c: G C}
    {d: G D}
    {e: G E}
    {contract: G F}
    `{idem_contract: ! Idempotent G F contract}:
    f <⋆> a <⋆> b <⋆> c <⋆> d <⋆> e <⋆> contract <⋆> contract =
      (map (compose (compose (compose (compose (compose double_input))))) f) <⋆>
        a <⋆> b <⋆> c <⋆> d <⋆> e <⋆> contract.G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B, C, D, E, F, J: Type
f: G (A -> B -> C -> D -> E -> F -> F -> J)
a: G A
b: G B
c: G C
d: G D
e: G E
contract: G F
idem_contract: Idempotent G F contract
f <⋆> a <⋆> b <⋆> c <⋆> d <⋆> e <⋆> contract <⋆>
contract =
map
  (compose
     (compose
        (compose (compose (compose double_input))))) f <⋆>
a <⋆> b <⋆> c <⋆> d <⋆> e <⋆> contract
  Proof.G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B, C, D, E, F, J: Type
f: G (A -> B -> C -> D -> E -> F -> F -> J)
a: G A
b: G B
c: G C
d: G D
e: G E
contract: G F
idem_contract: Idempotent G F contract
f <⋆> a <⋆> b <⋆> c <⋆> d <⋆> e <⋆> contract <⋆>
contract =
map
  (compose
     (compose
        (compose (compose (compose double_input))))) f <⋆>
a <⋆> b <⋆> c <⋆> d <⋆> e <⋆> contract
    rewrite ap_contract.G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B, C, D, E, F, J: Type
f: G (A -> B -> C -> D -> E -> F -> F -> J)
a: G A
b: G B
c: G C
d: G D
e: G E
contract: G F
idem_contract: Idempotent G F contract
map double_input (f <⋆> a <⋆> b <⋆> c <⋆> d <⋆> e) <⋆>
contract =
map
  (compose
     (compose
        (compose (compose (compose double_input))))) f <⋆>
a <⋆> b <⋆> c <⋆> d <⋆> e <⋆> contract
    rewrite map_ap.G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B, C, D, E, F, J: Type
f: G (A -> B -> C -> D -> E -> F -> F -> J)
a: G A
b: G B
c: G C
d: G D
e: G E
contract: G F
idem_contract: Idempotent G F contract
map (compose double_input) (f <⋆> a <⋆> b <⋆> c <⋆> d) <⋆>
e <⋆> contract =
map
  (compose
     (compose
        (compose (compose (compose double_input))))) f <⋆>
a <⋆> b <⋆> c <⋆> d <⋆> e <⋆> contract
    rewrite map_ap.G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B, C, D, E, F, J: Type
f: G (A -> B -> C -> D -> E -> F -> F -> J)
a: G A
b: G B
c: G C
d: G D
e: G E
contract: G F
idem_contract: Idempotent G F contract
map (compose (compose double_input))
  (f <⋆> a <⋆> b <⋆> c) <⋆> d <⋆> e <⋆> contract =
map
  (compose
     (compose
        (compose (compose (compose double_input))))) f <⋆>
a <⋆> b <⋆> c <⋆> d <⋆> e <⋆> contract
    rewrite map_ap.G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B, C, D, E, F, J: Type
f: G (A -> B -> C -> D -> E -> F -> F -> J)
a: G A
b: G B
c: G C
d: G D
e: G E
contract: G F
idem_contract: Idempotent G F contract
map (compose (compose (compose double_input)))
  (f <⋆> a <⋆> b) <⋆> c <⋆> d <⋆> e <⋆> contract =
map
  (compose
     (compose
        (compose (compose (compose double_input))))) f <⋆>
a <⋆> b <⋆> c <⋆> d <⋆> e <⋆> contract
    rewrite map_ap.G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B, C, D, E, F, J: Type
f: G (A -> B -> C -> D -> E -> F -> F -> J)
a: G A
b: G B
c: G C
d: G D
e: G E
contract: G F
idem_contract: Idempotent G F contract
map
  (compose (compose (compose (compose double_input))))
  (f <⋆> a) <⋆> b <⋆> c <⋆> d <⋆> e <⋆> contract =
map
  (compose
     (compose
        (compose (compose (compose double_input))))) f <⋆>
a <⋆> b <⋆> c <⋆> d <⋆> e <⋆> contract
    rewrite map_ap.G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
appG: Applicative G
A, B, C, D, E, F, J: Type
f: G (A -> B -> C -> D -> E -> F -> F -> J)
a: G A
b: G B
c: G C
d: G D
e: G E
contract: G F
idem_contract: Idempotent G F contract
map
  (compose
     (compose
        (compose (compose (compose double_input))))) f <⋆>
a <⋆> b <⋆> c <⋆> d <⋆> e <⋆> contract =
map
  (compose
     (compose
        (compose (compose (compose double_input))))) f <⋆>
a <⋆> b <⋆> c <⋆> d <⋆> e <⋆> contract
    reflexivity.
  Qed.

End rewriting_commutative_idempotent_element.

(** ** Commutative Idempotent Applicative Functors *)
(**********************************************************************)
Class ApplicativeCommutativeIdempotent (G: Type -> Type)
  `{mapG: Map G} `{pureG: Pure G} `{multG: Mult G} :=
  { appci_applicative :> Applicative G;
    appci_appic :> forall (A: Type) (a: G A),
        IdempotentCenter G A a;
  }.
Class ApplicativeCommutative (G: Type -> Type)
  `{mapG: Map G} `{pureG: Pure G} `{multG: Mult G} :=
  { appc_applicative :> Applicative G;
    appc_appc :> forall (A: Type) (a: G A),
        Center G A a;
  }.

(** ** Rewriting Laws for C-I Applicative Funtors *)
(**********************************************************************)
Section rewrite_commutative_idempotent_functor.

  Context
    `{ApplicativeCommutativeIdempotent G}.

  Lemma ap_ci_swap
    {A B: Type}
    {f: G (A -> B)}
    {a: G A}:
    f <⋆> a = (map evalAt a) <⋆> f.G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
H: ApplicativeCommutativeIdempotent G
A, B: Type
f: G (A -> B)
a: G A
f <⋆> a = map evalAt a <⋆> f
  Proof.G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
H: ApplicativeCommutativeIdempotent G
A, B: Type
f: G (A -> B)
a: G A
f <⋆> a = map evalAt a <⋆> f
    now rewrite ap_swap.
  Qed.

  Lemma ap_ci_flip:
    forall {A B C: Type} (f: G (A -> B -> C)) (a: G A) (b: G B),
      f <⋆> a <⋆> b = (map flip f) <⋆> b <⋆> a.G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
H: ApplicativeCommutativeIdempotent G
forall (A B C : Type) (f : G (A -> B -> C)) (a : G A)
  (b : G B), f <⋆> a <⋆> b = map flip f <⋆> b <⋆> a
  Proof.G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
H: ApplicativeCommutativeIdempotent G
forall (A B C : Type) (f : G (A -> B -> C)) (a : G A)
  (b : G B), f <⋆> a <⋆> b = map flip f <⋆> b <⋆> a
    intros.G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
H: ApplicativeCommutativeIdempotent G
A, B, C: Type
f: G (A -> B -> C)
a: G A
b: G B
f <⋆> a <⋆> b = map flip f <⋆> b <⋆> a
    now rewrite ap_flip1.
  Qed.

  Lemma ap_ci_contract:
    forall {A B: Type} (f: G (A -> A -> B)) (a: G A),
      f <⋆> a <⋆> a = (map double_input f) <⋆> a.G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
H: ApplicativeCommutativeIdempotent G
forall (A B : Type) (f : G (A -> A -> B)) (a : G A),
f <⋆> a <⋆> a = map double_input f <⋆> a
  Proof.G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
H: ApplicativeCommutativeIdempotent G
forall (A B : Type) (f : G (A -> A -> B)) (a : G A),
f <⋆> a <⋆> a = map double_input f <⋆> a
    intros.G: Type -> Type
mapG: Map G
pureG: Pure G
multG: Mult G
H: ApplicativeCommutativeIdempotent G
A, B: Type
f: G (A -> A -> B)
a: G A
f <⋆> a <⋆> a = map double_input f <⋆> a
    now rewrite ap_contract.
  Qed.

End rewrite_commutative_idempotent_functor.