From Tealeaves Require Export
  Tactics.Prelude
  Classes.Functor
  Misc.Product
  Misc.Strength
  Functors.Identity
  Functors.Compose
  Classes.Categorical.Applicative (Pure, pure).

#[local] Generalizable Variables G A B C.

(** * Applicative Functors *)
(**********************************************************************)
Class Ap (F: Type -> Type) :=
  ap: forall {A B: Type}, F (A -> B) -> F A -> F B.

Notation "Gf <⋆> Ga" :=
  (ap Gf Ga) (at level 50, left associativity).

Class Applicative
  (G: Type -> Type)
  `{Pure G} `{Ap G} :=
  { ap1: forall `(t: G A), pure id <⋆> t = t;
    ap2: forall `(f: A -> B) (a: A),
      pure f <⋆> pure a = pure (f a);
    ap3: forall `(f: G (A -> B)) (a: A),
      f <⋆> pure a = pure (fun f => f a) <⋆> f;
    ap4: forall {A B C: Type}
           (f: G (B -> C)) (g: G (A -> B)) (a: G A),
      (pure compose) <⋆> f <⋆> g <⋆> a =
        f <⋆> (g <⋆> a)
  }.

(** ** Derived Categorical Applicative Functor *)
(**********************************************************************)
Section Derived.

  Context
    `{Pure G} `{Ap G}.

  #[local] Instance Map_PureAp: Map G :=
    fun A B (f: A -> B) (a: G A) => pure f <⋆> a.

  #[export] Instance Functor_Applicative
    `{! Applicative G}: Functor G.
G: Type -> Type
H: Pure G
H0: Ap G
Applicative0: Applicative G
Functor G
  Proof.
G: Type -> Type
H: Pure G
H0: Ap G
Applicative0: Applicative G
Functor G
    constructor.
G: Type -> Type
H: Pure G
H0: Ap G
Applicative0: Applicative G
forall A : Type, map id = id
G: Type -> Type
H: Pure G
H0: Ap G
Applicative0: Applicative G
forall (A B C : Type) (f : A -> B) (g : B -> C),
map g ∘ map f = map (g ∘ f)
    -
G: Type -> Type
H: Pure G
H0: Ap G
Applicative0: Applicative G
forall A : Type, map id = id intros.
G: Type -> Type
H: Pure G
H0: Ap G
Applicative0: Applicative G
A: Type
map id = id unfold_ops @Map_PureAp.
G: Type -> Type
H: Pure G
H0: Ap G
Applicative0: Applicative G
A: Type
(fun a : G A => pure id <⋆> a) = id
      ext a.
G: Type -> Type
H: Pure G
H0: Ap G
Applicative0: Applicative G
A: Type
a: G A
pure id <⋆> a = id a apply ap1.
    -
G: Type -> Type
H: Pure G
H0: Ap G
Applicative0: Applicative G
forall (A B C : Type) (f : A -> B) (g : B -> C),
map g ∘ map f = map (g ∘ f) intros.
G: Type -> Type
H: Pure G
H0: Ap G
Applicative0: Applicative G
A, B, C: Type
f: A -> B
g: B -> C
map g ∘ map f = map (g ∘ f) unfold_ops @Map_PureAp.
G: Type -> Type
H: Pure G
H0: Ap G
Applicative0: Applicative G
A, B, C: Type
f: A -> B
g: B -> C
(fun a : G B => pure g <⋆> a)
∘ (fun a : G A => pure f <⋆> a) =
(fun a : G A => pure (g ∘ f) <⋆> a)
      ext a.
G: Type -> Type
H: Pure G
H0: Ap G
Applicative0: Applicative G
A, B, C: Type
f: A -> B
g: B -> C
a: G A
((fun a : G B => pure g <⋆> a)
 ∘ (fun a : G A => pure f <⋆> a)) a =
pure (g ∘ f) <⋆> a unfold compose.
G: Type -> Type
H: Pure G
H0: Ap G
Applicative0: Applicative G
A, B, C: Type
f: A -> B
g: B -> C
a: G A
pure g <⋆> (pure f <⋆> a) = pure (g ○ f) <⋆> a
      rewrite <- ap4.
G: Type -> Type
H: Pure G
H0: Ap G
Applicative0: Applicative G
A, B, C: Type
f: A -> B
g: B -> C
a: G A
pure compose <⋆> pure g <⋆> pure f <⋆> a =
pure (g ○ f) <⋆> a
      rewrite ap2.
G: Type -> Type
H: Pure G
H0: Ap G
Applicative0: Applicative G
A, B, C: Type
f: A -> B
g: B -> C
a: G A
pure (compose g) <⋆> pure f <⋆> a = pure (g ○ f) <⋆> a
      rewrite ap2.
G: Type -> Type
H: Pure G
H0: Ap G
Applicative0: Applicative G
A, B, C: Type
f: A -> B
g: B -> C
a: G A
pure (g ∘ f) <⋆> a = pure (g ○ f) <⋆> a
      reflexivity.
  Qed.

  Import Categorical.Applicative (Mult).

  #[local] Instance Mult_PureAp: Mult G :=
    fun A B (p: G A * G B) =>
      match p with
      | (a, b) => pure pair <⋆> a <⋆> b: G (A * B)
      end.

  #[local] Instance CatApp_App
    (* I want to write
       `{! Kleisli.Applicative.Applicative G}:
       but Alectryon complains about it for unknown reasons
     *)
    `{! Applicative G}:
    Categorical.Applicative.Applicative G.
G: Type -> Type
H: Pure G
H0: Ap G
Applicative0: Applicative G
Categorical.Applicative.Applicative G
  Proof.
G: Type -> Type
H: Pure G
H0: Ap G
Applicative0: Applicative G
Categorical.Applicative.Applicative G
    constructor.
G: Type -> Type
H: Pure G
H0: Ap G
Applicative0: Applicative G
Functor G
G: Type -> Type
H: Pure G
H0: Ap G
Applicative0: Applicative G
forall (A B : Type) (f : A -> B) (x : A),
map f (pure x) = pure (f x)
G: Type -> Type
H: Pure G
H0: Ap G
Applicative0: Applicative G
forall (A B C D : Type) 
  (f : A -> C) (g : B -> D) 
  (x : G A) (y : G B),
Applicative.mult (map f x, map g y) =
map (map_tensor f g) (Applicative.mult (x, y))
G: Type -> Type
H: Pure G
H0: Ap G
Applicative0: Applicative G
forall (A B C : Type) (x : G A) (y : G B) (z : G C),
map associator
  (Applicative.mult (Applicative.mult (x, y), z)) =
Applicative.mult (x, Applicative.mult (y, z))
G: Type -> Type
H: Pure G
H0: Ap G
Applicative0: Applicative G
forall (A : Type) (x : G A),
map left_unitor (Applicative.mult (pure tt, x)) = x
G: Type -> Type
H: Pure G
H0: Ap G
Applicative0: Applicative G
forall (A : Type) (x : G A),
map right_unitor (Applicative.mult (x, pure tt)) = x
G: Type -> Type
H: Pure G
H0: Ap G
Applicative0: Applicative G
forall (A B : Type) (a : A) (b : B),
Applicative.mult (pure a, pure b) = pure (a, b)
    -
G: Type -> Type
H: Pure G
H0: Ap G
Applicative0: Applicative G
Functor G typeclasses eauto.
    -
G: Type -> Type
H: Pure G
H0: Ap G
Applicative0: Applicative G
forall (A B : Type) (f : A -> B) (x : A),
map f (pure x) = pure (f x) intros.
G: Type -> Type
H: Pure G
H0: Ap G
Applicative0: Applicative G
A, B: Type
f: A -> B
x: A
map f (pure x) = pure (f x)
      unfold_ops @Map_PureAp.
G: Type -> Type
H: Pure G
H0: Ap G
Applicative0: Applicative G
A, B: Type
f: A -> B
x: A
pure f <⋆> pure x = pure (f x)
      now rewrite ap2.
    -
G: Type -> Type
H: Pure G
H0: Ap G
Applicative0: Applicative G
forall (A B C D : Type) (f : A -> C) (g : B -> D)
  (x : G A) (y : G B),
Applicative.mult (map f x, map g y) =
map (map_tensor f g) (Applicative.mult (x, y)) intros.
G: Type -> Type
H: Pure G
H0: Ap G
Applicative0: Applicative G
A, B, C, D: Type
f: A -> C
g: B -> D
x: G A
y: G B
Applicative.mult (map f x, map g y) =
map (map_tensor f g) (Applicative.mult (x, y))
      unfold_ops @Mult_PureAp @Map_PureAp.
G: Type -> Type
H: Pure G
H0: Ap G
Applicative0: Applicative G
A, B, C, D: Type
f: A -> C
g: B -> D
x: G A
y: G B
pure pair <⋆> (pure f <⋆> x) <⋆> (pure g <⋆> y) =
pure (map_tensor f g) <⋆> (pure pair <⋆> x <⋆> y)
      repeat rewrite <- ap4.
G: Type -> Type
H: Pure G
H0: Ap G
Applicative0: Applicative G
A, B, C, D: Type
f: A -> C
g: B -> D
x: G A
y: G B
pure compose <⋆> pure compose <⋆> pure compose <⋆>
pure compose <⋆> pure compose <⋆> pure compose <⋆>
pure pair <⋆> pure f <⋆> x <⋆> pure g <⋆> y =
pure compose <⋆> pure compose <⋆> pure compose <⋆>
pure (map_tensor f g) <⋆> pure pair <⋆> x <⋆> y
      repeat rewrite ap2.
G: Type -> Type
H: Pure G
H0: Ap G
Applicative0: Applicative G
A, B, C, D: Type
f: A -> C
g: B -> D
x: G A
y: G B
pure
  ((compose ∘ compose) compose compose compose pair f) <⋆>
x <⋆> pure g <⋆> y =
pure ((compose ∘ compose) (map_tensor f g) pair) <⋆> x <⋆>
y
      rewrite ap3.
G: Type -> Type
H: Pure G
H0: Ap G
Applicative0: Applicative G
A, B, C, D: Type
f: A -> C
g: B -> D
x: G A
y: G B
pure (fun f : (B -> D) -> B -> C * D => f g) <⋆>
(pure
   ((compose ∘ compose) compose compose compose pair f) <⋆>
 x) <⋆> y =
pure ((compose ∘ compose) (map_tensor f g) pair) <⋆> x <⋆>
y
      repeat rewrite <- ap4.
G: Type -> Type
H: Pure G
H0: Ap G
Applicative0: Applicative G
A, B, C, D: Type
f: A -> C
g: B -> D
x: G A
y: G B
pure compose <⋆>
pure (fun f : (B -> D) -> B -> C * D => f g) <⋆>
pure
  ((compose ∘ compose) compose compose compose pair f) <⋆>
x <⋆> y =
pure ((compose ∘ compose) (map_tensor f g) pair) <⋆> x <⋆>
y
      repeat rewrite ap2.
G: Type -> Type
H: Pure G
H0: Ap G
Applicative0: Applicative G
A, B, C, D: Type
f: A -> C
g: B -> D
x: G A
y: G B
pure
  ((fun f : (B -> D) -> B -> C * D => f g)
   ∘ (compose ∘ compose) compose compose compose pair
       f) <⋆> x <⋆> y =
pure ((compose ∘ compose) (map_tensor f g) pair) <⋆> x <⋆>
y
      reflexivity.
    -
G: Type -> Type
H: Pure G
H0: Ap G
Applicative0: Applicative G
forall (A B C : Type) (x : G A) (y : G B) (z : G C),
map associator
  (Applicative.mult (Applicative.mult (x, y), z)) =
Applicative.mult (x, Applicative.mult (y, z)) intros.
G: Type -> Type
H: Pure G
H0: Ap G
Applicative0: Applicative G
A, B, C: Type
x: G A
y: G B
z: G C
map associator
  (Applicative.mult (Applicative.mult (x, y), z)) =
Applicative.mult (x, Applicative.mult (y, z))
      unfold_ops @Mult_PureAp @Map_PureAp.
G: Type -> Type
H: Pure G
H0: Ap G
Applicative0: Applicative G
A, B, C: Type
x: G A
y: G B
z: G C
pure associator <⋆>
(pure pair <⋆> (pure pair <⋆> x <⋆> y) <⋆> z) =
pure pair <⋆> x <⋆> (pure pair <⋆> y <⋆> z)
      repeat (rewrite <- ap4; repeat rewrite ap2).
G: Type -> Type
H: Pure G
H0: Ap G
Applicative0: Applicative G
A, B, C: Type
x: G A
y: G B
z: G C
pure (compose (compose associator ∘ pair) ∘ pair) <⋆>
x <⋆> y <⋆> z =
pure (compose ∘ compose ∘ pair) <⋆> x <⋆> pure pair <⋆>
y <⋆> z
      rewrite ap3.
G: Type -> Type
H: Pure G
H0: Ap G
Applicative0: Applicative G
A, B, C: Type
x: G A
y: G B
z: G C
pure (compose (compose associator ∘ pair) ∘ pair) <⋆>
x <⋆> y <⋆> z =
pure
  (fun f : (B -> C -> B * C) -> B -> C -> A * (B * C)
   => f pair) <⋆>
(pure (compose ∘ compose ∘ pair) <⋆> x) <⋆> y <⋆> z
      repeat (rewrite <- ap4; repeat rewrite ap2).
G: Type -> Type
H: Pure G
H0: Ap G
Applicative0: Applicative G
A, B, C: Type
x: G A
y: G B
z: G C
pure (compose (compose associator ∘ pair) ∘ pair) <⋆>
x <⋆> y <⋆> z =
pure
  ((fun f : (B -> C -> B * C) -> B -> C -> A * (B * C)
    => f pair) ∘ (compose ∘ compose ∘ pair)) <⋆> x <⋆>
y <⋆> z
      reflexivity.
    -
G: Type -> Type
H: Pure G
H0: Ap G
Applicative0: Applicative G
forall (A : Type) (x : G A),
map left_unitor (Applicative.mult (pure tt, x)) = x intros.
G: Type -> Type
H: Pure G
H0: Ap G
Applicative0: Applicative G
A: Type
x: G A
map left_unitor (Applicative.mult (pure tt, x)) = x
      unfold_ops @Mult_PureAp @Map_PureAp.
G: Type -> Type
H: Pure G
H0: Ap G
Applicative0: Applicative G
A: Type
x: G A
pure left_unitor <⋆> (pure pair <⋆> pure tt <⋆> x) = x
      repeat (rewrite <- ap4; repeat rewrite ap2).
G: Type -> Type
H: Pure G
H0: Ap G
Applicative0: Applicative G
A: Type
x: G A
pure (left_unitor ∘ pair tt) <⋆> x = x
      change (left_unitor ∘ pair tt) with (@id A).
G: Type -> Type
H: Pure G
H0: Ap G
Applicative0: Applicative G
A: Type
x: G A
pure id <⋆> x = x
      rewrite ap1.
G: Type -> Type
H: Pure G
H0: Ap G
Applicative0: Applicative G
A: Type
x: G A
x = x
      reflexivity.
    -
G: Type -> Type
H: Pure G
H0: Ap G
Applicative0: Applicative G
forall (A : Type) (x : G A),
map right_unitor (Applicative.mult (x, pure tt)) = x intros.
G: Type -> Type
H: Pure G
H0: Ap G
Applicative0: Applicative G
A: Type
x: G A
map right_unitor (Applicative.mult (x, pure tt)) = x
      unfold_ops @Mult_PureAp @Map_PureAp.
G: Type -> Type
H: Pure G
H0: Ap G
Applicative0: Applicative G
A: Type
x: G A
pure right_unitor <⋆> (pure pair <⋆> x <⋆> pure tt) =
x
      repeat (rewrite <- ap4; repeat rewrite ap2).
G: Type -> Type
H: Pure G
H0: Ap G
Applicative0: Applicative G
A: Type
x: G A
pure (compose right_unitor ∘ pair) <⋆> x <⋆> pure tt =
x
      rewrite ap3.
G: Type -> Type
H: Pure G
H0: Ap G
Applicative0: Applicative G
A: Type
x: G A
pure (fun f : unit -> A => f tt) <⋆>
(pure (compose right_unitor ∘ pair) <⋆> x) = x
      repeat (rewrite <- ap4; repeat rewrite ap2).
G: Type -> Type
H: Pure G
H0: Ap G
Applicative0: Applicative G
A: Type
x: G A
pure
  ((fun f : unit -> A => f tt)
   ∘ (compose right_unitor ∘ pair)) <⋆> x = x
      apply ap1.
    -
G: Type -> Type
H: Pure G
H0: Ap G
Applicative0: Applicative G
forall (A B : Type) (a : A) (b : B),
Applicative.mult (pure a, pure b) = pure (a, b) intros.
G: Type -> Type
H: Pure G
H0: Ap G
Applicative0: Applicative G
A, B: Type
a: A
b: B
Applicative.mult (pure a, pure b) = pure (a, b)
      unfold_ops @Mult_PureAp @Map_PureAp.
G: Type -> Type
H: Pure G
H0: Ap G
Applicative0: Applicative G
A, B: Type
a: A
b: B
pure pair <⋆> pure a <⋆> pure b = pure (a, b)
      repeat (rewrite <- ap4; repeat rewrite ap2).
G: Type -> Type
H: Pure G
H0: Ap G
Applicative0: Applicative G
A, B: Type
a: A
b: B
pure pair <⋆> pure a <⋆> pure b = pure (a, b)
      rewrite ap3.
G: Type -> Type
H: Pure G
H0: Ap G
Applicative0: Applicative G
A, B: Type
a: A
b: B
pure (fun f : B -> A * B => f b) <⋆>
(pure pair <⋆> pure a) = pure (a, b)
      repeat (rewrite <- ap4; repeat rewrite ap2).
G: Type -> Type
H: Pure G
H0: Ap G
Applicative0: Applicative G
A, B: Type
a: A
b: B
pure (((fun f : B -> A * B => f b) ∘ pair) a) =
pure (a, b)
      reflexivity.
  Qed.

End Derived.

(*
(** ** Penguin Operation *)
(**********************************************************************)
Definition penguin {A B: Type}
  `{G: Type -> Type} `{Map G} `{Mult G} `{Pure G}:
  forall (a: G A) (b: G B), G B :=
  fun a b => (map (F := G) (const (@id B)) a) <⋆> b.

Infix "|⋆>" := penguin (at level 50).
*)