From Tealeaves Require Export
  Misc.Product
  Classes.Functor
  Functors.Identity
  Functors.Compose.

Import Product.Notations.

#[local] Generalizable Variables F G A B.

(** * Tensorial Strength *)
(**********************************************************************)

All endofunctors in the CoC have a tensorial strength with respect to the Cartesian product of types. This is just the operation that distributes a pairing over an endofunctor. See Tensorial Strength.

Section tensor_strength.

  Definition strength {F: Type -> Type}
    `{Map F} {A B}: forall (p: A * F B), F (A * B) :=
    fun '(a, t) => map (pair a) t.

  Lemma strength_I: forall (A B: Type),
      @strength (fun A: Type => A) _ A B = @id (A * B).
forall A B : Type, strength = id
  Proof.
forall A B : Type, strength = id
    intros.
A, B: Type
strength = id now ext [a b].
  Qed.

  Lemma strength_compose `{Functor F} `{Functor G}:
    forall (A B: Type),
      strength (F := F ∘ G) (A := A) (B := B) =
        map (F := F) (strength (F := G)) ∘ strength (F := F).
F: Type -> Type
Map_F: Map F
H: Functor F
G: Type -> Type
Map_F0: Map G
H0: Functor G
forall A B : Type, strength = map strength ∘ strength
  Proof.
F: Type -> Type
Map_F: Map F
H: Functor F
G: Type -> Type
Map_F0: Map G
H0: Functor G
forall A B : Type, strength = map strength ∘ strength
    intros.
F: Type -> Type
Map_F: Map F
H: Functor F
G: Type -> Type
Map_F0: Map G
H0: Functor G
A, B: Type
strength = map strength ∘ strength ext [x y].
F: Type -> Type
Map_F: Map F
H: Functor F
G: Type -> Type
Map_F0: Map G
H0: Functor G
A, B: Type
x: A
y: (F ∘ G) B
strength (x, y) = (map strength ∘ strength) (x, y) unfold strength, compose; cbn.
F: Type -> Type
Map_F: Map F
H: Functor F
G: Type -> Type
Map_F0: Map G
H0: Functor G
A, B: Type
x: A
y: (F ∘ G) B
map (pair x) y =
map (fun '(a, t) => map (pair a) t) (map (pair x) y)
    compose near y.
F: Type -> Type
Map_F: Map F
H: Functor F
G: Type -> Type
Map_F0: Map G
H0: Functor G
A, B: Type
x: A
y: (F ∘ G) B
(eq ∘ map (pair x)) y
  ((map (fun '(a, t) => map (pair a) t) ∘ map (pair x))
     y)
    now rewrite (fun_map_map).
  Qed.

  Context
    (F: Type -> Type)
    `{Functor F}.

  Lemma strength_1 {A B}: forall (a: A) (x: F B),
      strength (a, x) = map (pair a) x.
F: Type -> Type
Map_F: Map F
H: Functor F
A, B: Type
forall (a : A) (x : F B),
strength (a, x) = map (pair a) x
  Proof.
F: Type -> Type
Map_F: Map F
H: Functor F
A, B: Type
forall (a : A) (x : F B),
strength (a, x) = map (pair a) x
    reflexivity.
  Qed.

  Lemma strength_2 {A B}: forall (a: A),
      (strength ∘ pair a: F B -> F (A * B)) = map (pair a).
F: Type -> Type
Map_F: Map F
H: Functor F
A, B: Type
forall a : A,
(strength ∘ pair a : F B -> F (A * B)) = map (pair a)
  Proof.
F: Type -> Type
Map_F: Map F
H: Functor F
A, B: Type
forall a : A,
(strength ∘ pair a : F B -> F (A * B)) = map (pair a)
    reflexivity.
  Qed.

  Lemma strength_nat `{f: A1 -> B1} `{g: A2 -> B2}:
    forall (p: A1 * F A2),
      strength (map_tensor f (map g) p) =
        map (map_tensor f g) (strength p).
F: Type -> Type
Map_F: Map F
H: Functor F
A1, B1: Type
f: A1 -> B1
A2, B2: Type
g: A2 -> B2
forall p : A1 * F A2,
strength (map_tensor f (map g) p) =
map (map_tensor f g) (strength p)
  Proof.
F: Type -> Type
Map_F: Map F
H: Functor F
A1, B1: Type
f: A1 -> B1
A2, B2: Type
g: A2 -> B2
forall p : A1 * F A2,
strength (map_tensor f (map g) p) =
map (map_tensor f g) (strength p)
    intros [a t].
F: Type -> Type
Map_F: Map F
H: Functor F
A1, B1: Type
f: A1 -> B1
A2, B2: Type
g: A2 -> B2
a: A1
t: F A2
strength (map_tensor f (map g) (a, t)) =
map (map_tensor f g) (strength (a, t)) cbn.
F: Type -> Type
Map_F: Map F
H: Functor F
A1, B1: Type
f: A1 -> B1
A2, B2: Type
g: A2 -> B2
a: A1
t: F A2
map (pair (f a)) (map g t) =
map (map_tensor f g) (map (pair a) t)
    compose near t on left.
F: Type -> Type
Map_F: Map F
H: Functor F
A1, B1: Type
f: A1 -> B1
A2, B2: Type
g: A2 -> B2
a: A1
t: F A2
(map (pair (f a)) ∘ map g) t =
map (map_tensor f g) (map (pair a) t)
    compose near t on right.
F: Type -> Type
Map_F: Map F
H: Functor F
A1, B1: Type
f: A1 -> B1
A2, B2: Type
g: A2 -> B2
a: A1
t: F A2
(map (pair (f a)) ∘ map g) t =
(map (map_tensor f g) ∘ map (pair a)) t
    now rewrite 2(fun_map_map).
  Qed.

  Corollary strength_nat_l {A B C} {f: A -> B}: forall (p: A * F C),
      map (map_fst f) (strength p) = strength (map_fst f p).
F: Type -> Type
Map_F: Map F
H: Functor F
A, B, C: Type
f: A -> B
forall p : A * F C,
map (map_fst f) (strength p) = strength (map_fst f p)
  Proof.
F: Type -> Type
Map_F: Map F
H: Functor F
A, B, C: Type
f: A -> B
forall p : A * F C,
map (map_fst f) (strength p) = strength (map_fst f p)
    intros.
F: Type -> Type
Map_F: Map F
H: Functor F
A, B, C: Type
f: A -> B
p: A * F C
map (map_fst f) (strength p) = strength (map_fst f p) unfold map_fst.
F: Type -> Type
Map_F: Map F
H: Functor F
A, B, C: Type
f: A -> B
p: A * F C
map (map_tensor f id) (strength p) =
strength (map_tensor f id p)
    rewrite <- strength_nat.
F: Type -> Type
Map_F: Map F
H: Functor F
A, B, C: Type
f: A -> B
p: A * F C
strength (map_tensor f (map id) p) =
strength (map_tensor f id p)
    now rewrite (fun_map_id).
  Qed.

  Corollary strength_nat_r {A B C} {f: A -> B}: forall (p: C * F A),
      map (map_snd f) (strength p) = strength (map_snd (map f) p).
F: Type -> Type
Map_F: Map F
H: Functor F
A, B, C: Type
f: A -> B
forall p : C * F A,
map (map_snd f) (strength p) =
strength (map_snd (map f) p)
  Proof.
F: Type -> Type
Map_F: Map F
H: Functor F
A, B, C: Type
f: A -> B
forall p : C * F A,
map (map_snd f) (strength p) =
strength (map_snd (map f) p)
    intros.
F: Type -> Type
Map_F: Map F
H: Functor F
A, B, C: Type
f: A -> B
p: C * F A
map (map_snd f) (strength p) =
strength (map_snd (map f) p) unfold map_snd.
F: Type -> Type
Map_F: Map F
H: Functor F
A, B, C: Type
f: A -> B
p: C * F A
map (map_tensor id f) (strength p) =
strength (map_tensor id (map f) p)
    now rewrite <- strength_nat.
  Qed.

  Lemma strength_triangle {A}: forall (p: unit * F A),
      map left_unitor (strength p) = left_unitor p.
F: Type -> Type
Map_F: Map F
H: Functor F
A: Type
forall p : unit * F A,
map left_unitor (strength p) = left_unitor p
  Proof.
F: Type -> Type
Map_F: Map F
H: Functor F
A: Type
forall p : unit * F A,
map left_unitor (strength p) = left_unitor p
    intros [u t].
F: Type -> Type
Map_F: Map F
H: Functor F
A: Type
u: unit
t: F A
map left_unitor (strength (u, t)) = left_unitor (u, t) destruct u.
F: Type -> Type
Map_F: Map F
H: Functor F
A: Type
t: F A
map left_unitor (strength (tt, t)) =
left_unitor (tt, t) cbn.
F: Type -> Type
Map_F: Map F
H: Functor F
A: Type
t: F A
map left_unitor (map (pair tt) t) = t
    compose_near t.
F: Type -> Type
Map_F: Map F
H: Functor F
A: Type
t: F A
(map left_unitor ∘ map (pair tt)) t = t rewrite (fun_map_map).
F: Type -> Type
Map_F: Map F
H: Functor F
A: Type
t: F A
map (left_unitor ∘ pair tt) t = t
    now rewrite (fun_map_id).
  Qed.

  Lemma strength_assoc {A B C}:
    map α ∘ (@strength F _ (A * B) C) = strength ∘ map_snd strength ∘ α.
F: Type -> Type
Map_F: Map F
H: Functor F
A, B, C: Type
map α ∘ strength = strength ∘ map_snd strength ∘ α
  Proof.
F: Type -> Type
Map_F: Map F
H: Functor F
A, B, C: Type
map α ∘ strength = strength ∘ map_snd strength ∘ α
    ext [[? ?] t].
F: Type -> Type
Map_F: Map F
H: Functor F
A, B, C: Type
a: A
b: B
t: F C
(map α ∘ strength) (a, b, t) =
(strength ∘ map_snd strength ∘ α) (a, b, t) unfold strength, compose.
F: Type -> Type
Map_F: Map F
H: Functor F
A, B, C: Type
a: A
b: B
t: F C
map α (map (pair (a, b)) t) =
(let
 '(a, t) :=
  map_snd (fun '(a, t) => map (pair a) t)
    (α (a, b, t)) in map (pair a) t) cbn.
F: Type -> Type
Map_F: Map F
H: Functor F
A, B, C: Type
a: A
b: B
t: F C
map α (map (pair (a, b)) t) =
map (pair (id a)) (map (pair b) t)
    compose_near t.
F: Type -> Type
Map_F: Map F
H: Functor F
A, B, C: Type
a: A
b: B
t: F C
(map α ∘ map (pair (a, b))) t =
(map (pair (id a)) ∘ map (pair b)) t do 2 rewrite (fun_map_map).
F: Type -> Type
Map_F: Map F
H: Functor F
A, B, C: Type
a: A
b: B
t: F C
map (α ∘ pair (a, b)) t = map (pair (id a) ∘ pair b) t
    reflexivity.

  Qed.

End tensor_strength.

(** * Notations *)
(**********************************************************************)
Module Notations.

  #[local] Arguments strength F%function_scope {H} (A B)%type_scope _.
  Notation "'σ'":= (strength): tealeaves_scope.
End Notations.