Multifunctor.v

From Tealeaves Require Export
  Classes.Functor
  Functors.Writer
  Classes.Categorical.Comonad (Extract, extract).
From Tealeaves.Categories Require Export
  TypeFamily.

Import Product.Notations.
Import TypeFamily.Notations.

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

Section assume_some_index_type.

  Context
    `{ix: Index}.

  Implicit Type (k: K).

  (** * Multisorted Functors *)
  (********************************************************************)
  Section MultisortedFunctor_operation.

    Context
      (F: Type -> Type).

    Class MMap: Type :=
      mmap: forall {A B}, (A -k-> B) -> F A -> F B.

  End MultisortedFunctor_operation.

  Section Multifunctor.

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

    Class MultisortedFunctor :=
      { mfun_mmap_id:
        `(mmap F kid = @id (F A));
        mfun_mmap_mmap: forall `(f: A -k-> B) `(g: B -k-> C),
          mmap F g ∘ mmap F f = mmap F (g ◻ f);
      }.

  End Multifunctor.

  (** ** Natural Transformations *)
  (********************************************************************)
  Section MultisortedNatural.

    Context
      `{MultisortedFunctor F}
      `{MultisortedFunctor G}.

    Class MultisortedNatural (η: F ⇒ G) :=
      mnaturality: forall {A B} (f: K -> A -> B),
          mmap G f ∘ η A = η B ∘ mmap F f.

  End MultisortedNatural.

  (** ** Identity Multisorted Functors at a Some <<k: K>> *)
  (** For each <<k: K>> one obtains a K-sorted functor whose object
      map is the identity operation and whose <<mmap>> treats
      values <<a: A>> as if tagged by <<k: K>>. *)
  (********************************************************************)
  Section MultisortedFunctor_identity.

    Context
      (k: K).

    #[global] Instance MMap_I_k: MMap (fun A => A) :=
      fun `(f: A -k-> B) => f k.

    #[global, program] Instance MultisortedFunctor_I_k:
      @MultisortedFunctor (fun A => A) MMap_I_k.

  End MultisortedFunctor_identity.

  (** ** Composition with Ordinary Functors *)
  (********************************************************************)
  #[global] Instance MMap_compose_Map
    `{MMap F2} `{Map F1}: MMap (F2 ∘ F1) :=
    fun A B f => mmap F2 (fun (k: K) (a: F1 A) => map (F := F1) (f k) a).

  Section MultisortedFunctor_compose_Functor.

    Context
      `{MultisortedFunctor F} `{Functor G}.

    Lemma mmap_id_compose_map: forall (A: Type),
        mmap (F ∘ G) kid = @id (F (G A)).ix: Index
F: Type -> Type
H: MMap F
H0: MultisortedFunctor F
G: Type -> Type
Map_F: Map G
H1: Functor G
forall A : Type, mmap (F ∘ G) kid = id
    Proof.ix: Index
F: Type -> Type
H: MMap F
H0: MultisortedFunctor F
G: Type -> Type
Map_F: Map G
H1: Functor G
forall A : Type, mmap (F ∘ G) kid = id
      intros.ix: Index
F: Type -> Type
H: MMap F
H0: MultisortedFunctor F
G: Type -> Type
Map_F: Map G
H1: Functor G
A: Type
mmap (F ∘ G) kid = id ext x.ix: Index
F: Type -> Type
H: MMap F
H0: MultisortedFunctor F
G: Type -> Type
Map_F: Map G
H1: Functor G
A: Type
x: (F ∘ G) A
mmap (F ∘ G) kid x = id x cbv in x.ix: Index
F: Type -> Type
H: MMap F
H0: MultisortedFunctor F
G: Type -> Type
Map_F: Map G
H1: Functor G
A: Type
x: F (G A)
mmap (F ∘ G) kid x = id x
      unfold_ops @MMap_compose_Map.ix: Index
F: Type -> Type
H: MMap F
H0: MultisortedFunctor F
G: Type -> Type
Map_F: Map G
H1: Functor G
A: Type
x: F (G A)
mmap F (fun k (a : G A) => map (kid k) a) x = id x
      change (fun (k: K) (a: G A) => map (F := G) (kid k) a)
        with (fun (_: K) (a: G A) => map (F := G) id a).ix: Index
F: Type -> Type
H: MMap F
H0: MultisortedFunctor F
G: Type -> Type
Map_F: Map G
H1: Functor G
A: Type
x: F (G A)
mmap F (fun (_ : K) (a : G A) => map id a) x = id x
      now rewrite (fun_map_id), (mfun_mmap_id F).
    Qed.

    Lemma mmap_mmap_compose_map: forall `(f: A -k-> B) `(g: B -k-> C),
        mmap (F ∘ G) g ∘ mmap (F ∘ G) f = mmap (F ∘ G) (g ◻ f).ix: Index
F: Type -> Type
H: MMap F
H0: MultisortedFunctor F
G: Type -> Type
Map_F: Map G
H1: Functor G
forall (A B : Type) (f : A -k-> B) (C : Type)
  (g : B -k-> C),
mmap (F ∘ G) g ∘ mmap (F ∘ G) f = mmap (F ∘ G) (g ◻ f)
    Proof.ix: Index
F: Type -> Type
H: MMap F
H0: MultisortedFunctor F
G: Type -> Type
Map_F: Map G
H1: Functor G
forall (A B : Type) (f : A -k-> B) (C : Type)
  (g : B -k-> C),
mmap (F ∘ G) g ∘ mmap (F ∘ G) f = mmap (F ∘ G) (g ◻ f)
      introv.ix: Index
F: Type -> Type
H: MMap F
H0: MultisortedFunctor F
G: Type -> Type
Map_F: Map G
H1: Functor G
A, B: Type
f: A -k-> B
C: Type
g: B -k-> C
mmap (F ∘ G) g ∘ mmap (F ∘ G) f = mmap (F ∘ G) (g ◻ f) ext t.ix: Index
F: Type -> Type
H: MMap F
H0: MultisortedFunctor F
G: Type -> Type
Map_F: Map G
H1: Functor G
A, B: Type
f: A -k-> B
C: Type
g: B -k-> C
t: (F ∘ G) A
(mmap (F ∘ G) g ∘ mmap (F ∘ G) f) t =
mmap (F ∘ G) (g ◻ f) t unfold compose.ix: Index
F: Type -> Type
H: MMap F
H0: MultisortedFunctor F
G: Type -> Type
Map_F: Map G
H1: Functor G
A, B: Type
f: A -k-> B
C: Type
g: B -k-> C
t: (F ∘ G) A
mmap (F ○ G) g (mmap (F ○ G) f t) =
mmap (F ○ G) (g ◻ f) t unfold_ops @MMap_compose_Map.ix: Index
F: Type -> Type
H: MMap F
H0: MultisortedFunctor F
G: Type -> Type
Map_F: Map G
H1: Functor G
A, B: Type
f: A -k-> B
C: Type
g: B -k-> C
t: (F ∘ G) A
mmap F (fun k (a : G B) => map (g k) a)
  (mmap F (fun k (a : G A) => map (f k) a) t) =
mmap F (fun k (a : G A) => map ((g ◻ f) k) a) t
      compose near t on left.ix: Index
F: Type -> Type
H: MMap F
H0: MultisortedFunctor F
G: Type -> Type
Map_F: Map G
H1: Functor G
A, B: Type
f: A -k-> B
C: Type
g: B -k-> C
t: (F ∘ G) A
(mmap F (fun k (a : G B) => map (g k) a)
 ∘ mmap F (fun k (a : G A) => map (f k) a)) t =
mmap F (fun k (a : G A) => map ((g ◻ f) k) a) t rewrite (mfun_mmap_mmap F).ix: Index
F: Type -> Type
H: MMap F
H0: MultisortedFunctor F
G: Type -> Type
Map_F: Map G
H1: Functor G
A, B: Type
f: A -k-> B
C: Type
g: B -k-> C
t: (F ∘ G) A
mmap F
  ((fun k (a : G B) => map (g k) a)
   ◻ (fun k (a : G A) => map (f k) a)) t =
mmap F (fun k (a : G A) => map ((g ◻ f) k) a) t
      fequal.ix: Index
F: Type -> Type
H: MMap F
H0: MultisortedFunctor F
G: Type -> Type
Map_F: Map G
H1: Functor G
A, B: Type
f: A -k-> B
C: Type
g: B -k-> C
t: (F ∘ G) A
(fun k (a : G B) => map (g k) a)
◻ (fun k (a : G A) => map (f k) a) =
(fun k (a : G A) => map ((g ◻ f) k) a) ext k x.ix: Index
F: Type -> Type
H: MMap F
H0: MultisortedFunctor F
G: Type -> Type
Map_F: Map G
H1: Functor G
A, B: Type
f: A -k-> B
C: Type
g: B -k-> C
t: (F ∘ G) A
k: K
x: G A
((fun k (a : G B) => map (g k) a)
 ◻ (fun k (a : G A) => map (f k) a)) k x =
map ((g ◻ f) k) x
      unfold vec_compose, compose.ix: Index
F: Type -> Type
H: MMap F
H0: MultisortedFunctor F
G: Type -> Type
Map_F: Map G
H1: Functor G
A, B: Type
f: A -k-> B
C: Type
g: B -k-> C
t: (F ∘ G) A
k: K
x: G A
map (g k) (map (f k) x) = map (g k ○ f k) x
      compose near x on left.ix: Index
F: Type -> Type
H: MMap F
H0: MultisortedFunctor F
G: Type -> Type
Map_F: Map G
H1: Functor G
A, B: Type
f: A -k-> B
C: Type
g: B -k-> C
t: (F ∘ G) A
k: K
x: G A
(map (g k) ∘ map (f k)) x = map (g k ○ f k) x
      now rewrite (fun_map_map).
    Qed.

    #[global] Instance MultisortedFunctor_compose_Functor:
      MultisortedFunctor (F ∘ G) :=
      {| mfun_mmap_id := mmap_id_compose_map;
         mfun_mmap_mmap := @mmap_mmap_compose_map;
      |}.

  End MultisortedFunctor_compose_Functor.

  (** ** Tensorial Strength *)
  (********************************************************************)
  Section tensorial_strength.

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

    Definition mstrength {B A}: B * F A -> F (B * A) :=
      fun '(b, x) => mmap F (fun k => pair b) x.

    Lemma strength_extract {W: Type} {A: Type}:
      mmap F (const (extract (W := (W ×)))) ∘ mstrength (B:=W) (A:=A) =
        extract (W := (W ×)) (A := F A).ix: Index
F: Type -> Type
H: MMap F
H0: MultisortedFunctor F
W, A: Type
mmap F (const extract) ∘ mstrength = extract
    Proof.ix: Index
F: Type -> Type
H: MMap F
H0: MultisortedFunctor F
W, A: Type
mmap F (const extract) ∘ mstrength = extract
      unfold mstrength.ix: Index
F: Type -> Type
H: MMap F
H0: MultisortedFunctor F
W, A: Type
mmap F (const extract)
∘ (fun '(b, x) => mmap F (fun _ : K => pair b) x) =
extract ext [w t].ix: Index
F: Type -> Type
H: MMap F
H0: MultisortedFunctor F
W, A: Type
w: W
t: F A
(mmap F (const extract)
 ∘ (fun '(b, x) => mmap F (fun _ : K => pair b) x))
  (w, t) = extract (w, t)
      unfold compose; cbn.ix: Index
F: Type -> Type
H: MMap F
H0: MultisortedFunctor F
W, A: Type
w: W
t: F A
mmap F (const extract)
  (mmap F (fun _ : K => pair w) t) = t compose near t on left.ix: Index
F: Type -> Type
H: MMap F
H0: MultisortedFunctor F
W, A: Type
w: W
t: F A
(mmap F (const extract) ∘ mmap F (fun _ : K => pair w))
  t = t
      now rewrite (mfun_mmap_mmap F), (mfun_mmap_id F).
    Qed.

  End tensorial_strength.

  (** * Single-Sorted Maps: [mapk] *)
  (********************************************************************)
  Definition mapk {A} F `{! MMap F}: K -> (A -> A) -> F A -> F A :=
    fun k f => mmap F (tgt k f).

  (** ** Identity and composition laws for [mapk] *)
  (********************************************************************)
  Context
    (F: Type -> Type)
    `{MultisortedFunctor F}.

  Lemma mapk_id k: forall A,
      mapk F k id = @id (F A).ix: Index
F: Type -> Type
H: MMap F
H0: MultisortedFunctor F
k: K
forall A : Type, mapk F k id = id
  Proof.ix: Index
F: Type -> Type
H: MMap F
H0: MultisortedFunctor F
k: K
forall A : Type, mapk F k id = id
    introv.ix: Index
F: Type -> Type
H: MMap F
H0: MultisortedFunctor F
k: K
A: Type
mapk F k id = id unfold mapk.ix: Index
F: Type -> Type
H: MMap F
H0: MultisortedFunctor F
k: K
A: Type
mmap F (tgt k id) = id
    now rewrite tgt_id, (mfun_mmap_id F).
  Qed.

  Lemma mapk_mapk_eq: forall k `(f: A -> A) `(g: A -> A),
      mapk F k g ∘ mapk F k f = mapk F k (g ∘ f).ix: Index
F: Type -> Type
H: MMap F
H0: MultisortedFunctor F
forall k (A : Type) (f g : A -> A),
mapk F k g ∘ mapk F k f = mapk F k (g ∘ f)
  Proof.ix: Index
F: Type -> Type
H: MMap F
H0: MultisortedFunctor F
forall k (A : Type) (f g : A -> A),
mapk F k g ∘ mapk F k f = mapk F k (g ∘ f)
    introv.ix: Index
F: Type -> Type
H: MMap F
H0: MultisortedFunctor F
k: K
A: Type
f, g: A -> A
mapk F k g ∘ mapk F k f = mapk F k (g ∘ f) unfold mapk.ix: Index
F: Type -> Type
H: MMap F
H0: MultisortedFunctor F
k: K
A: Type
f, g: A -> A
mmap F (tgt k g) ∘ mmap F (tgt k f) =
mmap F (tgt k (g ∘ f))
    now rewrite (mfun_mmap_mmap F), tgt_tgt_eq.
  Qed.

  Lemma mapk_mapk_neq: forall k1 k2 `(f: A -> A) `(g: A -> A),
      k1 <> k2 -> mapk F k2 g ∘ mapk F k1 f = mapk F k1 f ∘ mapk F k2 g.ix: Index
F: Type -> Type
H: MMap F
H0: MultisortedFunctor F
forall k1 k2 (A : Type) (f g : A -> A),
k1 <> k2 ->
mapk F k2 g ∘ mapk F k1 f = mapk F k1 f ∘ mapk F k2 g
  Proof.ix: Index
F: Type -> Type
H: MMap F
H0: MultisortedFunctor F
forall k1 k2 (A : Type) (f g : A -> A),
k1 <> k2 ->
mapk F k2 g ∘ mapk F k1 f = mapk F k1 f ∘ mapk F k2 g
    introv p.ix: Index
F: Type -> Type
H: MMap F
H0: MultisortedFunctor F
k1, k2: K
A: Type
f, g: A -> A
p: (k1 <> k2)%type
mapk F k2 g ∘ mapk F k1 f = mapk F k1 f ∘ mapk F k2 g unfold mapk.ix: Index
F: Type -> Type
H: MMap F
H0: MultisortedFunctor F
k1, k2: K
A: Type
f, g: A -> A
p: (k1 <> k2)%type
mmap F (tgt k2 g) ∘ mmap F (tgt k1 f) =
mmap F (tgt k1 f) ∘ mmap F (tgt k2 g) rewrite 2(mfun_mmap_mmap F).ix: Index
F: Type -> Type
H: MMap F
H0: MultisortedFunctor F
k1, k2: K
A: Type
f, g: A -> A
p: (k1 <> k2)%type
mmap F (tgt k2 g ◻ tgt k1 f) =
mmap F (tgt k1 f ◻ tgt k2 g)
    rewrite tgt_tgt_neq; auto.
  Qed.

End assume_some_index_type.