Vector.v

From Tealeaves Require Export
  Classes.Categorical.Applicative
  Classes.Kleisli.TraversableFunctor
  Classes.Categorical.TraversableFunctor.

(*
From Tealeaves Require Import
  Adapters.CategoricalToKleisli.TraversableFunctor.
*)

#[local] Generalizable Variables ϕ T G A M F.

Import Applicative.Notations.

(*
(** * Vectors *)
(******************************************************************************)
Inductive Vector (A : Type) : forall (n : nat), Type :=
| Vnil : Vector A 0
| Vcons : A -> forall (n : nat), Vector A n -> Vector A (S n).
 *)

#[global] Notation "'VEC' n" := (fun A => Vector.t A n) (at level 3).

Definition unone {A : Type} : Vector.t A 1 -> A.A: Type
Vector.t A 1 -> A
Proof.A: Type
Vector.t A 1 -> A
  intros v.A: Type
v: Vector.t A 1
A remember 1.A: Type
n: nat
Heqn: n = 1
v: Vector.t A n
A induction v.A: Type
Heqn: 0 = 1
A
A: Type
n: nat
Heqn: S n = 1
h: A
v: Vector.t A n
IHv: n = 1 -> A
A
  -A: Type
Heqn: 0 = 1
A inversion Heqn.
  -A: Type
n: nat
Heqn: S n = 1
h: A
v: Vector.t A n
IHv: n = 1 -> A
A assumption.
Defined.

(** ** Properties of vectors *)
(******************************************************************************)
Lemma toNil {B : Type} : forall (b : Vector.t B 0), b = Vector.nil B.B: Type
forall b : Vector.t B 0, b = Vector.nil B
Proof.B: Type
forall b : Vector.t B 0, b = Vector.nil B
  intros.B: Type
b: Vector.t B 0
b = Vector.nil B
  apply (Vector.case0 (A := B) (fun v : Vector.t B 0 => v = Vector.nil B)).B: Type
b: Vector.t B 0
Vector.nil B = Vector.nil B
  reflexivity.
Qed.

(** ** Functor instance *)
(******************************************************************************)
Fixpoint map_Vector (n : nat) {A B : Type} (f : A -> B) (v : VEC n A) : VEC n B :=
  match v in Vector.t _ n return Vector.t B n with
  | Vector.nil _(*=A*) => Vector.nil B
  | Vector.cons _(*=A*) a(*:A*) m(*n = S m*) rest =>
      Vector.cons B (f a) m (map_Vector m f rest)
  end.

#[export] Instance Map_Vector (n : nat) : Map (VEC n) := @map_Vector n.

Lemma fun_map_id_Vector : forall (n : nat) (A : Type),
    map (F := VEC n) id = @id (VEC n A).forall (n : nat) (A : Type), map id = id
Proof.forall (n : nat) (A : Type), map id = id
  intros.n: nat
A: Type
map id = id
  ext v.n: nat
A: Type
v: Vector.t A n
map id v = id v
  induction v.A: Type
map id (Vector.nil A) = id (Vector.nil A)
A: Type
h: A
n: nat
v: Vector.t A n
IHv: map id v = id v
map id (Vector.cons A h n v) =
id (Vector.cons A h n v)
  -A: Type
map id (Vector.nil A) = id (Vector.nil A) reflexivity.
  -A: Type
h: A
n: nat
v: Vector.t A n
IHv: map id v = id v
map id (Vector.cons A h n v) =
id (Vector.cons A h n v) cbn.A: Type
h: A
n: nat
v: Vector.t A n
IHv: map id v = id v
Vector.cons A (id h) n (map_Vector n id v) =
id (Vector.cons A h n v) unfold id.A: Type
h: A
n: nat
v: Vector.t A n
IHv: map id v = id v
Vector.cons A h n (map_Vector n (fun x : A => x) v) =
Vector.cons A h n v fequal.A: Type
h: A
n: nat
v: Vector.t A n
IHv: map id v = id v
map_Vector n (fun x : A => x) v = v apply IHv.
Qed.

Lemma fun_map_map_Vector : forall (n : nat) (A B C : Type) (f : A -> B) (g : B -> C),
    map (F := VEC n) g ∘ map (F := VEC n) f = map (F := VEC n) (g ∘ f).forall (n : nat) (A B C : Type) (f : A -> B)
  (g : B -> C), map g ∘ map f = map (g ∘ f)
Proof.forall (n : nat) (A B C : Type) (f : A -> B)
  (g : B -> C), map g ∘ map f = map (g ∘ f)
  intros.n: nat
A, B, C: Type
f: A -> B
g: B -> C
map g ∘ map f = map (g ∘ f)
  ext v.n: nat
A, B, C: Type
f: A -> B
g: B -> C
v: Vector.t A n
(map g ∘ map f) v = map (g ∘ f) v
  induction v.A, B, C: Type
f: A -> B
g: B -> C
(map g ∘ map f) (Vector.nil A) =
map (g ∘ f) (Vector.nil A)
A, B, C: Type
f: A -> B
g: B -> C
h: A
n: nat
v: Vector.t A n
IHv: (map g ∘ map f) v = map (g ∘ f) v
(map g ∘ map f) (Vector.cons A h n v) =
map (g ∘ f) (Vector.cons A h n v)
  -A, B, C: Type
f: A -> B
g: B -> C
(map g ∘ map f) (Vector.nil A) =
map (g ∘ f) (Vector.nil A) reflexivity.
  -A, B, C: Type
f: A -> B
g: B -> C
h: A
n: nat
v: Vector.t A n
IHv: (map g ∘ map f) v = map (g ∘ f) v
(map g ∘ map f) (Vector.cons A h n v) =
map (g ∘ f) (Vector.cons A h n v) cbn.A, B, C: Type
f: A -> B
g: B -> C
h: A
n: nat
v: Vector.t A n
IHv: (map g ∘ map f) v = map (g ∘ f) v
Vector.cons C (g (f h)) n
  (map_Vector n g (map_Vector n f v)) =
Vector.cons C ((g ∘ f) h) n (map_Vector n (g ∘ f) v) unfold id.A, B, C: Type
f: A -> B
g: B -> C
h: A
n: nat
v: Vector.t A n
IHv: (map g ∘ map f) v = map (g ∘ f) v
Vector.cons C (g (f h)) n
  (map_Vector n g (map_Vector n f v)) =
Vector.cons C ((g ∘ f) h) n (map_Vector n (g ∘ f) v) fequal.A, B, C: Type
f: A -> B
g: B -> C
h: A
n: nat
v: Vector.t A n
IHv: (map g ∘ map f) v = map (g ∘ f) v
map_Vector n g (map_Vector n f v) =
map_Vector n (g ∘ f) v apply IHv.
Qed.

#[export] Instance Functor_Vector (n : nat) : Functor (VEC n) :=
  {| fun_map_id := fun_map_id_Vector n;
    fun_map_map := fun_map_map_Vector n;
  |}.

(** ** Traversable instance *)
(******************************************************************************)
Fixpoint dist_Vector (n : nat) (G : Type -> Type) `{Map G} `{Pure G} `{Mult G}
  {A : Type} (v : VEC n (G A)) : G (VEC n A) :=
  match v in Vector.t _ n return G (Vector.t A n) with
  | Vector.nil _(*=A*) => pure (F := G) (Vector.nil A)
  | Vector.cons _(*=A*) a(*:FA*) m(*n = S m*) rest =>
      pure (F := G) (Basics.flip (fun a => Vector.cons A a m))
      <⋆> dist_Vector m G rest
      <⋆> a
      (*
      pure (F := G) (fun a => Vector.cons A a m) <⋆> a <⋆> dist_Vector m G rest
       *)
  end.

#[export] Instance Dist_Vector (n : nat):
  ApplicativeDist (VEC n) := @dist_Vector n.

Tactic Notation "cleanup_Vector" :=
  repeat (change (map_Vector ?n (A := ?x) (B := ?y))
           with (map (F := VEC n) (A := x) (B := y)) +
                  change (dist_Vector ?n ?G (A := ?x))
             with (dist (VEC n) G (A := x))).

Tactic Notation "cleanup_Vector_*" :=
  repeat ((change (map_Vector ?n (A := ?x) (B := ?y))
            with (map (F := VEC n) (A := x) (B := y)) in *) ||
                   change (dist_Vector ?n ?G (A := ?x))
              with (dist (VEC n) G (A := x)) in *).

Lemma dist_natural_Vector (n : nat) :
  forall (G : Type -> Type) (H1 : Map G)
    (H2 : Pure G) (H3 : Mult G),
    Applicative G -> Natural (F := (VEC n ∘ G)) (G := (G ∘ VEC n)) (@dist_Vector n G _ _ _).n: nat
forall (G : Type -> Type) (H1 : Map G) (H2 : Pure G)
  (H3 : Mult G),
Applicative G -> Natural (@dist_Vector n G H1 H2 H3)
Proof.n: nat
forall (G : Type -> Type) (H1 : Map G) (H2 : Pure G)
  (H3 : Mult G),
Applicative G -> Natural (@dist_Vector n G H1 H2 H3)
  intros.n: nat
G: Type -> Type
H1: Map G
H2: Pure G
H3: Mult G
H: Applicative G
Natural (@dist_Vector n G H1 H2 H3) constructor; try typeclasses eauto.n: nat
G: Type -> Type
H1: Map G
H2: Pure G
H3: Mult G
H: Applicative G
forall (A B : Type) (f : A -> B),
map f ∘ dist_Vector n G = dist_Vector n G ∘ map f
  intros.n: nat
G: Type -> Type
H1: Map G
H2: Pure G
H3: Mult G
H: Applicative G
A, B: Type
f: A -> B
map f ∘ dist_Vector n G = dist_Vector n G ∘ map f unfold_ops @Map_compose.n: nat
G: Type -> Type
H1: Map G
H2: Pure G
H3: Mult G
H: Applicative G
A, B: Type
f: A -> B
map (map f) ∘ dist_Vector n G =
dist_Vector n G ∘ map (map f) unfold compose at 3 7.n: nat
G: Type -> Type
H1: Map G
H2: Pure G
H3: Mult G
H: Applicative G
A, B: Type
f: A -> B
map (map f) ○ dist_Vector n G =
dist_Vector n G ○ map (map f)
  ext v.n: nat
G: Type -> Type
H1: Map G
H2: Pure G
H3: Mult G
H: Applicative G
A, B: Type
f: A -> B
v: (VEC n ∘ G) A
map (map f) (dist_Vector n G v) =
dist_Vector n G (map (map f) v) induction v.G: Type -> Type
H1: Map G
H2: Pure G
H3: Mult G
H: Applicative G
A, B: Type
f: A -> B
map (map f) (dist_Vector 0 G (Vector.nil (G A))) =
dist_Vector 0 G (map (map f) (Vector.nil (G A)))
G: Type -> Type
H1: Map G
H2: Pure G
H3: Mult G
H: Applicative G
A, B: Type
f: A -> B
h: G A
n: nat
v: Vector.t (G A) n
IHv: map (map f) (dist_Vector n G v) = dist_Vector n G (map (map f) v)
map (map f)
  (dist_Vector (S n) G (Vector.cons (G A) h n v)) =
dist_Vector (S n) G
  (map (map f) (Vector.cons (G A) h n v))
  -G: Type -> Type
H1: Map G
H2: Pure G
H3: Mult G
H: Applicative G
A, B: Type
f: A -> B
map (map f) (dist_Vector 0 G (Vector.nil (G A))) =
dist_Vector 0 G (map (map f) (Vector.nil (G A))) cbn.G: Type -> Type
H1: Map G
H2: Pure G
H3: Mult G
H: Applicative G
A, B: Type
f: A -> B
map (map f) (pure (Vector.nil A)) =
pure (Vector.nil B) compose near (Vector.nil A).G: Type -> Type
H1: Map G
H2: Pure G
H3: Mult G
H: Applicative G
A, B: Type
f: A -> B
(map (map f) ∘ pure) (Vector.nil A) =
pure (Vector.nil B)
    apply (app_pure_natural (G := G)).
  -G: Type -> Type
H1: Map G
H2: Pure G
H3: Mult G
H: Applicative G
A, B: Type
f: A -> B
h: G A
n: nat
v: Vector.t (G A) n
IHv: map (map f) (dist_Vector n G v) = dist_Vector n G (map (map f) v)
map (map f)
  (dist_Vector (S n) G (Vector.cons (G A) h n v)) =
dist_Vector (S n) G
  (map (map f) (Vector.cons (G A) h n v)) cbn.G: Type -> Type
H1: Map G
H2: Pure G
H3: Mult G
H: Applicative G
A, B: Type
f: A -> B
h: G A
n: nat
v: Vector.t (G A) n
IHv: map (map f) (dist_Vector n G v) = dist_Vector n G (map (map f) v)
map (map f)
  (pure (Basics.flip (fun a : A => Vector.cons A a n)) <⋆>
   dist_Vector n G v <⋆> h) =
pure (Basics.flip (fun a : B => Vector.cons B a n)) <⋆>
dist_Vector n G (map_Vector n (map f) v) <⋆> map f h
    (* LHS *)
    rewrite (map_ap).G: Type -> Type
H1: Map G
H2: Pure G
H3: Mult G
H: Applicative G
A, B: Type
f: A -> B
h: G A
n: nat
v: Vector.t (G A) n
IHv: map (map f) (dist_Vector n G v) = dist_Vector n G (map (map f) v)
map (compose (map f))
  (pure (Basics.flip (fun a : A => Vector.cons A a n)) <⋆>
   dist_Vector n G v) <⋆> h =
pure (Basics.flip (fun a : B => Vector.cons B a n)) <⋆>
dist_Vector n G (map_Vector n (map f) v) <⋆> map f h
    rewrite (map_ap).G: Type -> Type
H1: Map G
H2: Pure G
H3: Mult G
H: Applicative G
A, B: Type
f: A -> B
h: G A
n: nat
v: Vector.t (G A) n
IHv: map (map f) (dist_Vector n G v) = dist_Vector n G (map (map f) v)
map (compose (compose (map f)))
  (pure (Basics.flip (fun a : A => Vector.cons A a n))) <⋆>
dist_Vector n G v <⋆> h =
pure (Basics.flip (fun a : B => Vector.cons B a n)) <⋆>
dist_Vector n G (map_Vector n (map f) v) <⋆> map f h
    rewrite (app_pure_natural (G := G)).G: Type -> Type
H1: Map G
H2: Pure G
H3: Mult G
H: Applicative G
A, B: Type
f: A -> B
h: G A
n: nat
v: Vector.t (G A) n
IHv: map (map f) (dist_Vector n G v) = dist_Vector n G (map (map f) v)
pure
  (compose (map f)
   ∘ Basics.flip (fun a : A => Vector.cons A a n)) <⋆>
dist_Vector n G v <⋆> h =
pure (Basics.flip (fun a : B => Vector.cons B a n)) <⋆>
dist_Vector n G (map_Vector n (map f) v) <⋆> map f h
    (* RHS *)
    cleanup_Vector_*.G: Type -> Type
H1: Map G
H2: Pure G
H3: Mult G
H: Applicative G
A, B: Type
f: A -> B
h: G A
n: nat
v: Vector.t (G A) n
IHv: map (map f) (dist VEC n G v) = dist VEC n G (map (map f) v)
pure
  (compose (map f)
   ∘ Basics.flip (fun a : A => Vector.cons A a n)) <⋆>
dist VEC n G v <⋆> h =
pure (Basics.flip (fun a : B => Vector.cons B a n)) <⋆>
dist VEC n G (map (map f) v) <⋆> map f h
    rewrite <- IHv.G: Type -> Type
H1: Map G
H2: Pure G
H3: Mult G
H: Applicative G
A, B: Type
f: A -> B
h: G A
n: nat
v: Vector.t (G A) n
IHv: map (map f) (dist VEC n G v) = dist VEC n G (map (map f) v)
pure
  (compose (map f)
   ∘ Basics.flip (fun a : A => Vector.cons A a n)) <⋆>
dist VEC n G v <⋆> h =
pure (Basics.flip (fun a : B => Vector.cons B a n)) <⋆>
map (map f) (dist VEC n G v) <⋆> map f h
    rewrite <- (ap_map).G: Type -> Type
H1: Map G
H2: Pure G
H3: Mult G
H: Applicative G
A, B: Type
f: A -> B
h: G A
n: nat
v: Vector.t (G A) n
IHv: map (map f) (dist VEC n G v) = dist VEC n G (map (map f) v)
pure
  (compose (map f)
   ∘ Basics.flip (fun a : A => Vector.cons A a n)) <⋆>
dist VEC n G v <⋆> h =
map (precompose f)
  (pure (Basics.flip (fun a : B => Vector.cons B a n)) <⋆>
   map (map f) (dist VEC n G v)) <⋆> h
    rewrite <- (ap_map).G: Type -> Type
H1: Map G
H2: Pure G
H3: Mult G
H: Applicative G
A, B: Type
f: A -> B
h: G A
n: nat
v: Vector.t (G A) n
IHv: map (map f) (dist VEC n G v) = dist VEC n G (map (map f) v)
pure
  (compose (map f)
   ∘ Basics.flip (fun a : A => Vector.cons A a n)) <⋆>
dist VEC n G v <⋆> h =
map (precompose f)
  (map (precompose (map f))
     (pure
        (Basics.flip (fun a : B => Vector.cons B a n))) <⋆>
   dist VEC n G v) <⋆> h
    rewrite (map_ap).G: Type -> Type
H1: Map G
H2: Pure G
H3: Mult G
H: Applicative G
A, B: Type
f: A -> B
h: G A
n: nat
v: Vector.t (G A) n
IHv: map (map f) (dist VEC n G v) = dist VEC n G (map (map f) v)
pure
  (compose (map f)
   ∘ Basics.flip (fun a : A => Vector.cons A a n)) <⋆>
dist VEC n G v <⋆> h =
map (compose (precompose f))
  (map (precompose (map f))
     (pure
        (Basics.flip (fun a : B => Vector.cons B a n)))) <⋆>
dist VEC n G v <⋆> h
    compose near (pure (F := G) (Basics.flip (fun a0 : B => Vector.cons B a0 n))).G: Type -> Type
H1: Map G
H2: Pure G
H3: Mult G
H: Applicative G
A, B: Type
f: A -> B
h: G A
n: nat
v: Vector.t (G A) n
IHv: map (map f) (dist VEC n G v) = dist VEC n G (map (map f) v)
pure
  (compose (map f)
   ∘ Basics.flip (fun a : A => Vector.cons A a n)) <⋆>
dist VEC n G v <⋆> h =
(map (compose (precompose f))
 ∘ map (precompose (map f)))
  (pure
     (Basics.flip (fun a0 : B => Vector.cons B a0 n))) <⋆>
dist VEC n G v <⋆> h
    rewrite (fun_map_map (F := G)).G: Type -> Type
H1: Map G
H2: Pure G
H3: Mult G
H: Applicative G
A, B: Type
f: A -> B
h: G A
n: nat
v: Vector.t (G A) n
IHv: map (map f) (dist VEC n G v) = dist VEC n G (map (map f) v)
pure
  (compose (map f)
   ∘ Basics.flip (fun a : A => Vector.cons A a n)) <⋆>
dist VEC n G v <⋆> h =
map (compose (precompose f) ∘ precompose (map f))
  (pure
     (Basics.flip (fun a0 : B => Vector.cons B a0 n))) <⋆>
dist VEC n G v <⋆> h
    rewrite (app_pure_natural).G: Type -> Type
H1: Map G
H2: Pure G
H3: Mult G
H: Applicative G
A, B: Type
f: A -> B
h: G A
n: nat
v: Vector.t (G A) n
IHv: map (map f) (dist VEC n G v) = dist VEC n G (map (map f) v)
pure
  (compose (map f)
   ∘ Basics.flip (fun a : A => Vector.cons A a n)) <⋆>
dist VEC n G v <⋆> h =
pure
  ((compose (precompose f) ∘ precompose (map f))
     (Basics.flip (fun a0 : B => Vector.cons B a0 n))) <⋆>
dist VEC n G v <⋆> h
    reflexivity.
Qed.

Lemma dist_morph_Vector (n : nat) :
  forall (G1 G2 : Type -> Type) (H1 : Map G1) (H3 : Mult G1) (H2 : Pure G1) (H4 : Map G2)
    (H6 : Mult G2) (H5 : Pure G2) (ϕ : forall A : Type, G1 A -> G2 A),
    ApplicativeMorphism G1 G2 ϕ -> forall A : Type,
      dist (VEC n) G2 ∘ map (F := VEC n) (ϕ A) = ϕ (VEC n A) ∘ dist (VEC n) G1.n: nat
forall (G1 G2 : Type -> Type) (H1 : Map G1)
  (H3 : Mult G1) (H2 : Pure G1) (H4 : Map G2)
  (H6 : Mult G2) (H5 : Pure G2)
  (ϕ : forall A : Type, G1 A -> G2 A),
ApplicativeMorphism G1 G2 ϕ ->
forall A : Type,
dist VEC n G2 ∘ map (ϕ A) =
ϕ (VEC n A) ∘ dist VEC n G1
Proof.n: nat
forall (G1 G2 : Type -> Type) (H1 : Map G1)
  (H3 : Mult G1) (H2 : Pure G1) (H4 : Map G2)
  (H6 : Mult G2) (H5 : Pure G2)
  (ϕ : forall A : Type, G1 A -> G2 A),
ApplicativeMorphism G1 G2 ϕ ->
forall A : Type,
dist VEC n G2 ∘ map (ϕ A) =
ϕ (VEC n A) ∘ dist VEC n G1
  intros.n: nat
G1, G2: Type -> Type
H1: Map G1
H3: Mult G1
H2: Pure G1
H4: Map G2
H6: Mult G2
H5: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
H: ApplicativeMorphism G1 G2 ϕ
A: Type
dist VEC n G2 ∘ map (ϕ A) =
ϕ (VEC n A) ∘ dist VEC n G1 unfold compose at 1 2.n: nat
G1, G2: Type -> Type
H1: Map G1
H3: Mult G1
H2: Pure G1
H4: Map G2
H6: Mult G2
H5: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
H: ApplicativeMorphism G1 G2 ϕ
A: Type
dist VEC n G2 ○ map (ϕ A) =
ϕ (Vector.t A n) ○ dist VEC n G1
  ext v.n: nat
G1, G2: Type -> Type
H1: Map G1
H3: Mult G1
H2: Pure G1
H4: Map G2
H6: Mult G2
H5: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
H: ApplicativeMorphism G1 G2 ϕ
A: Type
v: Vector.t (G1 A) n
dist VEC n G2 (map (ϕ A) v) =
ϕ (Vector.t A n) (dist VEC n G1 v) induction v.G1, G2: Type -> Type
H1: Map G1
H3: Mult G1
H2: Pure G1
H4: Map G2
H6: Mult G2
H5: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
H: ApplicativeMorphism G1 G2 ϕ
A: Type
dist VEC 0 G2 (map (ϕ A) (Vector.nil (G1 A))) =
ϕ (Vector.t A 0) (dist VEC 0 G1 (Vector.nil (G1 A)))
G1, G2: Type -> Type
H1: Map G1
H3: Mult G1
H2: Pure G1
H4: Map G2
H6: Mult G2
H5: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
H: ApplicativeMorphism G1 G2 ϕ
A: Type
h: G1 A
n: nat
v: Vector.t (G1 A) n
IHv: dist VEC n G2 (map (ϕ A) v) = ϕ (Vector.t A n) (dist VEC n G1 v)
dist VEC (S n) G2
  (map (ϕ A) (Vector.cons (G1 A) h n v)) =
ϕ (Vector.t A (S n))
  (dist VEC (S n) G1 (Vector.cons (G1 A) h n v))
  -G1, G2: Type -> Type
H1: Map G1
H3: Mult G1
H2: Pure G1
H4: Map G2
H6: Mult G2
H5: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
H: ApplicativeMorphism G1 G2 ϕ
A: Type
dist VEC 0 G2 (map (ϕ A) (Vector.nil (G1 A))) =
ϕ (Vector.t A 0) (dist VEC 0 G1 (Vector.nil (G1 A))) cbn.G1, G2: Type -> Type
H1: Map G1
H3: Mult G1
H2: Pure G1
H4: Map G2
H6: Mult G2
H5: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
H: ApplicativeMorphism G1 G2 ϕ
A: Type
pure (Vector.nil A) =
ϕ (Vector.t A 0) (pure (Vector.nil A)) rewrite (appmor_pure (F := G1) (G := G2)).G1, G2: Type -> Type
H1: Map G1
H3: Mult G1
H2: Pure G1
H4: Map G2
H6: Mult G2
H5: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
H: ApplicativeMorphism G1 G2 ϕ
A: Type
pure (Vector.nil A) = pure (Vector.nil A) reflexivity.
  -G1, G2: Type -> Type
H1: Map G1
H3: Mult G1
H2: Pure G1
H4: Map G2
H6: Mult G2
H5: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
H: ApplicativeMorphism G1 G2 ϕ
A: Type
h: G1 A
n: nat
v: Vector.t (G1 A) n
IHv: dist VEC n G2 (map (ϕ A) v) = ϕ (Vector.t A n) (dist VEC n G1 v)
dist VEC (S n) G2
  (map (ϕ A) (Vector.cons (G1 A) h n v)) =
ϕ (Vector.t A (S n))
  (dist VEC (S n) G1 (Vector.cons (G1 A) h n v)) cbn.G1, G2: Type -> Type
H1: Map G1
H3: Mult G1
H2: Pure G1
H4: Map G2
H6: Mult G2
H5: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
H: ApplicativeMorphism G1 G2 ϕ
A: Type
h: G1 A
n: nat
v: Vector.t (G1 A) n
IHv: dist VEC n G2 (map (ϕ A) v) = ϕ (Vector.t A n) (dist VEC n G1 v)
pure (Basics.flip (fun a : A => Vector.cons A a n)) <⋆>
dist_Vector n G2 (map_Vector n (ϕ A) v) <⋆> ϕ A h =
ϕ (Vector.t A (S n))
  (pure (Basics.flip (fun a : A => Vector.cons A a n)) <⋆>
   dist_Vector n G1 v <⋆> h) cleanup_Vector.G1, G2: Type -> Type
H1: Map G1
H3: Mult G1
H2: Pure G1
H4: Map G2
H6: Mult G2
H5: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
H: ApplicativeMorphism G1 G2 ϕ
A: Type
h: G1 A
n: nat
v: Vector.t (G1 A) n
IHv: dist VEC n G2 (map (ϕ A) v) = ϕ (Vector.t A n) (dist VEC n G1 v)
pure (Basics.flip (fun a : A => Vector.cons A a n)) <⋆>
dist VEC n G2 (map (ϕ A) v) <⋆> ϕ A h =
ϕ (Vector.t A (S n))
  (pure (Basics.flip (fun a : A => Vector.cons A a n)) <⋆>
   dist VEC n G1 v <⋆> h)
    (* LHS *)
    rewrite IHv.G1, G2: Type -> Type
H1: Map G1
H3: Mult G1
H2: Pure G1
H4: Map G2
H6: Mult G2
H5: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
H: ApplicativeMorphism G1 G2 ϕ
A: Type
h: G1 A
n: nat
v: Vector.t (G1 A) n
IHv: dist VEC n G2 (map (ϕ A) v) = ϕ (Vector.t A n) (dist VEC n G1 v)
pure (Basics.flip (fun a : A => Vector.cons A a n)) <⋆>
ϕ (Vector.t A n) (dist VEC n G1 v) <⋆> ϕ A h =
ϕ (Vector.t A (S n))
  (pure (Basics.flip (fun a : A => Vector.cons A a n)) <⋆>
   dist VEC n G1 v <⋆> h)
    inversion H.G1, G2: Type -> Type
H1: Map G1
H3: Mult G1
H2: Pure G1
H4: Map G2
H6: Mult G2
H5: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
H: ApplicativeMorphism G1 G2 ϕ
A: Type
h: G1 A
n: nat
v: Vector.t (G1 A) n
IHv: dist VEC n G2 (map (ϕ A) v) = ϕ (Vector.t A n) (dist VEC n G1 v)
appmor_app_F: Applicative G1
appmor_app_G: Applicative G2
appmor_natural: forall (A B : Type) (f : A -> B)
  (x : G1 A),
ϕ B (map f x) = map f (ϕ A x)
appmor_pure: forall (A : Type) (a : A),
ϕ A (pure a) = pure a
appmor_mult: forall (A B : Type) (x : G1 A)
  (y : G1 B),
ϕ (A * B) (x ⊗ y) = ϕ A x ⊗ ϕ B y
pure (Basics.flip (fun a : A => Vector.cons A a n)) <⋆>
ϕ (Vector.t A n) (dist VEC n G1 v) <⋆> ϕ A h =
ϕ (Vector.t A (S n))
  (pure (Basics.flip (fun a : A => Vector.cons A a n)) <⋆>
   dist VEC n G1 v <⋆> h)
    (* RHS *)
    rewrite (ap_morphism_1).G1, G2: Type -> Type
H1: Map G1
H3: Mult G1
H2: Pure G1
H4: Map G2
H6: Mult G2
H5: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
H: ApplicativeMorphism G1 G2 ϕ
A: Type
h: G1 A
n: nat
v: Vector.t (G1 A) n
IHv: dist VEC n G2 (map (ϕ A) v) =
ϕ (Vector.t A n) (dist VEC n G1 v)
appmor_app_F: Applicative G1
appmor_app_G: Applicative G2
appmor_natural: forall (A B : Type) (f : A -> B)
  (x : G1 A),
ϕ B (map f x) = map f (ϕ A x)
appmor_pure: forall (A : Type) (a : A),
ϕ A (pure a) = pure a
appmor_mult: forall (A B : Type) (x : G1 A)
  (y : G1 B),
ϕ (A * B) (x ⊗ y) = ϕ A x ⊗ ϕ B y
pure (Basics.flip (fun a : A => Vector.cons A a n)) <⋆>
ϕ (Vector.t A n) (dist VEC n G1 v) <⋆> 
ϕ A h =
ϕ (A -> Vector.t A (S n))
  (pure (Basics.flip (fun a : A => Vector.cons A a n)) <⋆>
   dist VEC n G1 v) <⋆> 
ϕ A h
    rewrite (ap_morphism_1).G1, G2: Type -> Type
H1: Map G1
H3: Mult G1
H2: Pure G1
H4: Map G2
H6: Mult G2
H5: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
H: ApplicativeMorphism G1 G2 ϕ
A: Type
h: G1 A
n: nat
v: Vector.t (G1 A) n
IHv: dist VEC n G2 (map (ϕ A) v) =
ϕ (Vector.t A n) (dist VEC n G1 v)
appmor_app_F: Applicative G1
appmor_app_G: Applicative G2
appmor_natural: forall (A B : Type) (f : A -> B)
  (x : G1 A),
ϕ B (map f x) = map f (ϕ A x)
appmor_pure: forall (A : Type) (a : A),
ϕ A (pure a) = pure a
appmor_mult: forall (A B : Type) (x : G1 A)
  (y : G1 B),
ϕ (A * B) (x ⊗ y) = ϕ A x ⊗ ϕ B y
pure (Basics.flip (fun a : A => Vector.cons A a n)) <⋆>
ϕ (Vector.t A n) (dist VEC n G1 v) <⋆> 
ϕ A h =
ϕ (Vector.t A n -> A -> Vector.t A (S n))
  (pure (Basics.flip (fun a : A => Vector.cons A a n))) <⋆>
ϕ (Vector.t A n) (dist VEC n G1 v) <⋆> 
ϕ A h
    rewrite (appmor_pure).G1, G2: Type -> Type
H1: Map G1
H3: Mult G1
H2: Pure G1
H4: Map G2
H6: Mult G2
H5: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
H: ApplicativeMorphism G1 G2 ϕ
A: Type
h: G1 A
n: nat
v: Vector.t (G1 A) n
IHv: dist VEC n G2 (map (ϕ A) v) =
ϕ (Vector.t A n) (dist VEC n G1 v)
appmor_app_F: Applicative G1
appmor_app_G: Applicative G2
appmor_natural: forall (A B : Type) (f : A -> B)
  (x : G1 A),
ϕ B (map f x) = map f (ϕ A x)
appmor_pure: forall (A : Type) (a : A),
ϕ A (pure a) = pure a
appmor_mult: forall (A B : Type) (x : G1 A)
  (y : G1 B),
ϕ (A * B) (x ⊗ y) = ϕ A x ⊗ ϕ B y
pure (Basics.flip (fun a : A => Vector.cons A a n)) <⋆>
ϕ (Vector.t A n) (dist VEC n G1 v) <⋆> 
ϕ A h =
pure (Basics.flip (fun a : A => Vector.cons A a n)) <⋆>
ϕ (Vector.t A n) (dist VEC n G1 v) <⋆> 
ϕ A h
    reflexivity.
Qed.

Lemma dist_unit_Vector (n : nat) : forall A : Type, dist (A := A) (VEC n) (fun A : Type => A) = id.n: nat
forall A : Type, dist VEC n (fun A0 : Type => A0) = id
Proof.n: nat
forall A : Type, dist VEC n (fun A0 : Type => A0) = id
  intros.n: nat
A: Type
dist VEC n (fun A : Type => A) = id ext v.n: nat
A: Type
v: Vector.t A n
dist VEC n (fun A : Type => A) v = id v induction v.A: Type
dist VEC 0 (fun A : Type => A) (Vector.nil A) =
id (Vector.nil A)
A: Type
h: A
n: nat
v: Vector.t A n
IHv: dist VEC n (fun A : Type => A) v = id v
dist VEC (S n) (fun A : Type => A)
  (Vector.cons A h n v) = id (Vector.cons A h n v)
  -A: Type
dist VEC 0 (fun A : Type => A) (Vector.nil A) =
id (Vector.nil A) cbn.A: Type
pure (Vector.nil A) = id (Vector.nil A) reflexivity.
  -A: Type
h: A
n: nat
v: Vector.t A n
IHv: dist VEC n (fun A : Type => A) v = id v
dist VEC (S n) (fun A : Type => A)
  (Vector.cons A h n v) = id (Vector.cons A h n v) cbn.A: Type
h: A
n: nat
v: Vector.t A n
IHv: dist VEC n (fun A : Type => A) v = id v
pure (Basics.flip (fun a : A => Vector.cons A a n))
  (dist_Vector n (fun A : Type => A) v) h =
id (Vector.cons A h n v) cleanup_Vector.A: Type
h: A
n: nat
v: Vector.t A n
IHv: dist VEC n (fun A : Type => A) v = id v
pure (Basics.flip (fun a : A => Vector.cons A a n))
  (dist VEC n (fun A : Type => A) v) h =
id (Vector.cons A h n v)
    (* LHS *)
    rewrite IHv.A: Type
h: A
n: nat
v: Vector.t A n
IHv: dist VEC n (fun A : Type => A) v = id v
pure (Basics.flip (fun a : A => Vector.cons A a n))
  (id v) h = id (Vector.cons A h n v)
    reflexivity.
Qed.

Lemma dist_linear_Vector (n : nat) :
  forall (G1 : Type -> Type) (H1 : Map G1) (H2 : Pure G1) (H3 : Mult G1),
    Applicative G1 ->
    forall (G2 : Type -> Type) (H5 : Map G2) (H6 : Pure G2) (H7 : Mult G2),
      Applicative G2 ->
      forall A : Type, dist (A := A) (VEC n) (G1 ∘ G2) = map (F := G1) (dist (VEC n) G2) ∘ dist (VEC n) G1.n: nat
forall (G1 : Type -> Type) (H1 : Map G1)
  (H2 : Pure G1) (H3 : Mult G1),
Applicative G1 ->
forall (G2 : Type -> Type) (H5 : Map G2)
  (H6 : Pure G2) (H7 : Mult G2),
Applicative G2 ->
forall A : Type,
dist VEC n (G1 ∘ G2) =
map (dist VEC n G2) ∘ dist VEC n G1
Proof.n: nat
forall (G1 : Type -> Type) (H1 : Map G1)
  (H2 : Pure G1) (H3 : Mult G1),
Applicative G1 ->
forall (G2 : Type -> Type) (H5 : Map G2)
  (H6 : Pure G2) (H7 : Mult G2),
Applicative G2 ->
forall A : Type,
dist VEC n (G1 ∘ G2) =
map (dist VEC n G2) ∘ dist VEC n G1
  intros.n: nat
G1: Type -> Type
H1: Map G1
H2: Pure G1
H3: Mult G1
H: Applicative G1
G2: Type -> Type
H5: Map G2
H6: Pure G2
H7: Mult G2
H0: Applicative G2
A: Type
dist VEC n (G1 ∘ G2) =
map (dist VEC n G2) ∘ dist VEC n G1 unfold compose at 4.n: nat
G1: Type -> Type
H1: Map G1
H2: Pure G1
H3: Mult G1
H: Applicative G1
G2: Type -> Type
H5: Map G2
H6: Pure G2
H7: Mult G2
H0: Applicative G2
A: Type
dist VEC n (G1 ∘ G2) =
map (dist VEC n G2) ○ dist VEC n G1
  ext v.n: nat
G1: Type -> Type
H1: Map G1
H2: Pure G1
H3: Mult G1
H: Applicative G1
G2: Type -> Type
H5: Map G2
H6: Pure G2
H7: Mult G2
H0: Applicative G2
A: Type
v: Vector.t ((G1 ∘ G2) A) n
dist VEC n (G1 ∘ G2) v =
map (dist VEC n G2) (dist VEC n G1 v) induction v.G1: Type -> Type
H1: Map G1
H2: Pure G1
H3: Mult G1
H: Applicative G1
G2: Type -> Type
H5: Map G2
H6: Pure G2
H7: Mult G2
H0: Applicative G2
A: Type
dist VEC 0 (G1 ∘ G2) (Vector.nil ((G1 ∘ G2) A)) =
map (dist VEC 0 G2)
  (dist VEC 0 G1 (Vector.nil ((G1 ∘ G2) A)))
G1: Type -> Type
H1: Map G1
H2: Pure G1
H3: Mult G1
H: Applicative G1
G2: Type -> Type
H5: Map G2
H6: Pure G2
H7: Mult G2
H0: Applicative G2
A: Type
h: (G1 ∘ G2) A
n: nat
v: Vector.t ((G1 ∘ G2) A) n
IHv: dist VEC n (G1 ∘ G2) v = map (dist VEC n G2) (dist VEC n G1 v)
dist VEC (S n) (G1 ∘ G2)
  (Vector.cons ((G1 ∘ G2) A) h n v) =
map (dist VEC (S n) G2)
  (dist VEC (S n) G1 (Vector.cons ((G1 ∘ G2) A) h n v))
  -G1: Type -> Type
H1: Map G1
H2: Pure G1
H3: Mult G1
H: Applicative G1
G2: Type -> Type
H5: Map G2
H6: Pure G2
H7: Mult G2
H0: Applicative G2
A: Type
dist VEC 0 (G1 ∘ G2) (Vector.nil ((G1 ∘ G2) A)) =
map (dist VEC 0 G2)
  (dist VEC 0 G1 (Vector.nil ((G1 ∘ G2) A))) cbn.G1: Type -> Type
H1: Map G1
H2: Pure G1
H3: Mult G1
H: Applicative G1
G2: Type -> Type
H5: Map G2
H6: Pure G2
H7: Mult G2
H0: Applicative G2
A: Type
pure (Vector.nil A) =
map (dist VEC 0 G2) (pure (Vector.nil (G2 A))) unfold_ops @Pure_compose.G1: Type -> Type
H1: Map G1
H2: Pure G1
H3: Mult G1
H: Applicative G1
G2: Type -> Type
H5: Map G2
H6: Pure G2
H7: Mult G2
H0: Applicative G2
A: Type
pure (pure (Vector.nil A)) =
map (dist VEC 0 G2) (pure (Vector.nil (G2 A)))
    rewrite (app_pure_natural (G := G1)).G1: Type -> Type
H1: Map G1
H2: Pure G1
H3: Mult G1
H: Applicative G1
G2: Type -> Type
H5: Map G2
H6: Pure G2
H7: Mult G2
H0: Applicative G2
A: Type
pure (pure (Vector.nil A)) =
pure (dist VEC 0 G2 (Vector.nil (G2 A)))
    reflexivity.
  -G1: Type -> Type
H1: Map G1
H2: Pure G1
H3: Mult G1
H: Applicative G1
G2: Type -> Type
H5: Map G2
H6: Pure G2
H7: Mult G2
H0: Applicative G2
A: Type
h: (G1 ∘ G2) A
n: nat
v: Vector.t ((G1 ∘ G2) A) n
IHv: dist VEC n (G1 ∘ G2) v = map (dist VEC n G2) (dist VEC n G1 v)
dist VEC (S n) (G1 ∘ G2)
  (Vector.cons ((G1 ∘ G2) A) h n v) =
map (dist VEC (S n) G2)
  (dist VEC (S n) G1 (Vector.cons ((G1 ∘ G2) A) h n v)) cbn.G1: Type -> Type
H1: Map G1
H2: Pure G1
H3: Mult G1
H: Applicative G1
G2: Type -> Type
H5: Map G2
H6: Pure G2
H7: Mult G2
H0: Applicative G2
A: Type
h: (G1 ∘ G2) A
n: nat
v: Vector.t ((G1 ∘ G2) A) n
IHv: dist VEC n (G1 ∘ G2) v = map (dist VEC n G2) (dist VEC n G1 v)
pure (Basics.flip (fun a : A => Vector.cons A a n)) <⋆>
dist_Vector n (G1 ∘ G2) v <⋆> h =
map (dist VEC (S n) G2)
  (pure
     (Basics.flip
        (fun a : G2 A => Vector.cons (G2 A) a n)) <⋆>
   dist_Vector n G1 v <⋆> h) cleanup_Vector.G1: Type -> Type
H1: Map G1
H2: Pure G1
H3: Mult G1
H: Applicative G1
G2: Type -> Type
H5: Map G2
H6: Pure G2
H7: Mult G2
H0: Applicative G2
A: Type
h: (G1 ∘ G2) A
n: nat
v: Vector.t ((G1 ∘ G2) A) n
IHv: dist VEC n (G1 ∘ G2) v = map (dist VEC n G2) (dist VEC n G1 v)
pure (Basics.flip (fun a : A => Vector.cons A a n)) <⋆>
dist VEC n (G1 ∘ G2) v <⋆> h =
map (dist VEC (S n) G2)
  (pure
     (Basics.flip
        (fun a : G2 A => Vector.cons (G2 A) a n)) <⋆>
   dist VEC n G1 v <⋆> h)
    (* LHS *)
    rewrite IHv.G1: Type -> Type
H1: Map G1
H2: Pure G1
H3: Mult G1
H: Applicative G1
G2: Type -> Type
H5: Map G2
H6: Pure G2
H7: Mult G2
H0: Applicative G2
A: Type
h: (G1 ∘ G2) A
n: nat
v: Vector.t ((G1 ∘ G2) A) n
IHv: dist VEC n (G1 ∘ G2) v = map (dist VEC n G2) (dist VEC n G1 v)
pure (Basics.flip (fun a : A => Vector.cons A a n)) <⋆>
map (dist VEC n G2) (dist VEC n G1 v) <⋆> h =
map (dist VEC (S n) G2)
  (pure
     (Basics.flip
        (fun a : G2 A => Vector.cons (G2 A) a n)) <⋆>
   dist VEC n G1 v <⋆> h)
    unfold_ops @Pure_compose.G1: Type -> Type
H1: Map G1
H2: Pure G1
H3: Mult G1
H: Applicative G1
G2: Type -> Type
H5: Map G2
H6: Pure G2
H7: Mult G2
H0: Applicative G2
A: Type
h: (G1 ∘ G2) A
n: nat
v: Vector.t ((G1 ∘ G2) A) n
IHv: dist VEC n (G1 ∘ G2) v = map (dist VEC n G2) (dist VEC n G1 v)
pure
  (pure (Basics.flip (fun a : A => Vector.cons A a n))) <⋆>
map (dist VEC n G2) (dist VEC n G1 v) <⋆> h =
map (dist VEC (S n) G2)
  (pure
     (Basics.flip
        (fun a : G2 A => Vector.cons (G2 A) a n)) <⋆>
   dist VEC n G1 v <⋆> h)
    rewrite (ap_compose2 G2 G1).G1: Type -> Type
H1: Map G1
H2: Pure G1
H3: Mult G1
H: Applicative G1
G2: Type -> Type
H5: Map G2
H6: Pure G2
H7: Mult G2
H0: Applicative G2
A: Type
h: (G1 ∘ G2) A
n: nat
v: Vector.t ((G1 ∘ G2) A) n
IHv: dist VEC n (G1 ∘ G2) v = map (dist VEC n G2) (dist VEC n G1 v)
map (ap G2)
  (pure
     (pure
        (Basics.flip (fun a : A => Vector.cons A a n))) <⋆>
   map (dist VEC n G2) (dist VEC n G1 v)) <⋆> h =
map (dist VEC (S n) G2)
  (pure
     (Basics.flip
        (fun a : G2 A => Vector.cons (G2 A) a n)) <⋆>
   dist VEC n G1 v <⋆> h)
    rewrite (ap_compose2 G2 G1).G1: Type -> Type
H1: Map G1
H2: Pure G1
H3: Mult G1
H: Applicative G1
G2: Type -> Type
H5: Map G2
H6: Pure G2
H7: Mult G2
H0: Applicative G2
A: Type
h: (G1 ∘ G2) A
n: nat
v: Vector.t ((G1 ∘ G2) A) n
IHv: dist VEC n (G1 ∘ G2) v = map (dist VEC n G2) (dist VEC n G1 v)
map (ap G2)
  (map (ap G2)
     (pure
        (pure
           (Basics.flip
              (fun a : A => Vector.cons A a n)))) <⋆>
   map (dist VEC n G2) (dist VEC n G1 v)) <⋆> h =
map (dist VEC (S n) G2)
  (pure
     (Basics.flip
        (fun a : G2 A => Vector.cons (G2 A) a n)) <⋆>
   dist VEC n G1 v <⋆> h)
    rewrite <- (ap_map (G := G1)).G1: Type -> Type
H1: Map G1
H2: Pure G1
H3: Mult G1
H: Applicative G1
G2: Type -> Type
H5: Map G2
H6: Pure G2
H7: Mult G2
H0: Applicative G2
A: Type
h: (G1 ∘ G2) A
n: nat
v: Vector.t ((G1 ∘ G2) A) n
IHv: dist VEC n (G1 ∘ G2) v = map (dist VEC n G2) (dist VEC n G1 v)
map (ap G2)
  (map (precompose (dist VEC n G2))
     (map (ap G2)
        (pure
           (pure
              (Basics.flip
                 (fun a : A => Vector.cons A a n))))) <⋆>
   dist VEC n G1 v) <⋆> h =
map (dist VEC (S n) G2)
  (pure
     (Basics.flip
        (fun a : G2 A => Vector.cons (G2 A) a n)) <⋆>
   dist VEC n G1 v <⋆> h)
    rewrite (map_ap (G := G1)).G1: Type -> Type
H1: Map G1
H2: Pure G1
H3: Mult G1
H: Applicative G1
G2: Type -> Type
H5: Map G2
H6: Pure G2
H7: Mult G2
H0: Applicative G2
A: Type
h: (G1 ∘ G2) A
n: nat
v: Vector.t ((G1 ∘ G2) A) n
IHv: dist VEC n (G1 ∘ G2) v = map (dist VEC n G2) (dist VEC n G1 v)
map (compose (ap G2))
  (map (precompose (dist VEC n G2))
     (map (ap G2)
        (pure
           (pure
              (Basics.flip
                 (fun a : A => Vector.cons A a n)))))) <⋆>
dist VEC n G1 v <⋆> h =
map (dist VEC (S n) G2)
  (pure
     (Basics.flip
        (fun a : G2 A => Vector.cons (G2 A) a n)) <⋆>
   dist VEC n G1 v <⋆> h)
    rewrite (map_ap (G := G1)).G1: Type -> Type
H1: Map G1
H2: Pure G1
H3: Mult G1
H: Applicative G1
G2: Type -> Type
H5: Map G2
H6: Pure G2
H7: Mult G2
H0: Applicative G2
A: Type
h: (G1 ∘ G2) A
n: nat
v: Vector.t ((G1 ∘ G2) A) n
IHv: dist VEC n (G1 ∘ G2) v = map (dist VEC n G2) (dist VEC n G1 v)
map (compose (ap G2))
  (map (precompose (dist VEC n G2))
     (map (ap G2)
        (pure
           (pure
              (Basics.flip
                 (fun a : A => Vector.cons A a n)))))) <⋆>
dist VEC n G1 v <⋆> h =
map (compose (dist VEC (S n) G2))
  (pure
     (Basics.flip
        (fun a : G2 A => Vector.cons (G2 A) a n)) <⋆>
   dist VEC n G1 v) <⋆> h
    compose near (pure (F := G1) (pure (F := G2)
                                       (Basics.flip (fun a0 : A => Vector.cons A a0 n)))).G1: Type -> Type
H1: Map G1
H2: Pure G1
H3: Mult G1
H: Applicative G1
G2: Type -> Type
H5: Map G2
H6: Pure G2
H7: Mult G2
H0: Applicative G2
A: Type
h: (G1 ∘ G2) A
n: nat
v: Vector.t ((G1 ∘ G2) A) n
IHv: dist VEC n (G1 ∘ G2) v = map (dist VEC n G2) (dist VEC n G1 v)
map (compose (ap G2))
  ((map (precompose (dist VEC n G2)) ∘ map (ap G2))
     (pure
        (pure
           (Basics.flip
              (fun a0 : A => Vector.cons A a0 n))))) <⋆>
dist VEC n G1 v <⋆> h =
map (compose (dist VEC (S n) G2))
  (pure
     (Basics.flip
        (fun a : G2 A => Vector.cons (G2 A) a n)) <⋆>
   dist VEC n G1 v) <⋆> h
    rewrite (fun_map_map (F := G1)).G1: Type -> Type
H1: Map G1
H2: Pure G1
H3: Mult G1
H: Applicative G1
G2: Type -> Type
H5: Map G2
H6: Pure G2
H7: Mult G2
H0: Applicative G2
A: Type
h: (G1 ∘ G2) A
n: nat
v: Vector.t ((G1 ∘ G2) A) n
IHv: dist VEC n (G1 ∘ G2) v = map (dist VEC n G2) (dist VEC n G1 v)
map (compose (ap G2))
  (map (precompose (dist VEC n G2) ∘ ap G2)
     (pure
        (pure
           (Basics.flip
              (fun a0 : A => Vector.cons A a0 n))))) <⋆>
dist VEC n G1 v <⋆> h =
map (compose (dist VEC (S n) G2))
  (pure
     (Basics.flip
        (fun a : G2 A => Vector.cons (G2 A) a n)) <⋆>
   dist VEC n G1 v) <⋆> h
    compose near (pure (F := G1) (pure (F := G2)
                                       (Basics.flip (fun a0 : A => Vector.cons A a0 n)))).G1: Type -> Type
H1: Map G1
H2: Pure G1
H3: Mult G1
H: Applicative G1
G2: Type -> Type
H5: Map G2
H6: Pure G2
H7: Mult G2
H0: Applicative G2
A: Type
h: (G1 ∘ G2) A
n: nat
v: Vector.t ((G1 ∘ G2) A) n
IHv: dist VEC n (G1 ∘ G2) v = map (dist VEC n G2) (dist VEC n G1 v)
(map (compose (ap G2))
 ∘ map (precompose (dist VEC n G2) ∘ ap G2))
  (pure
     (pure
        (Basics.flip
           (fun a0 : A => Vector.cons A a0 n)))) <⋆>
dist VEC n G1 v <⋆> h =
map (compose (dist VEC (S n) G2))
  (pure
     (Basics.flip
        (fun a : G2 A => Vector.cons (G2 A) a n)) <⋆>
   dist VEC n G1 v) <⋆> h
    rewrite (fun_map_map (F := G1)).G1: Type -> Type
H1: Map G1
H2: Pure G1
H3: Mult G1
H: Applicative G1
G2: Type -> Type
H5: Map G2
H6: Pure G2
H7: Mult G2
H0: Applicative G2
A: Type
h: (G1 ∘ G2) A
n: nat
v: Vector.t ((G1 ∘ G2) A) n
IHv: dist VEC n (G1 ∘ G2) v = map (dist VEC n G2) (dist VEC n G1 v)
map
  (compose (ap G2)
   ∘ (precompose (dist VEC n G2) ∘ ap G2))
  (pure
     (pure
        (Basics.flip
           (fun a0 : A => Vector.cons A a0 n)))) <⋆>
dist VEC n G1 v <⋆> h =
map (compose (dist VEC (S n) G2))
  (pure
     (Basics.flip
        (fun a : G2 A => Vector.cons (G2 A) a n)) <⋆>
   dist VEC n G1 v) <⋆> h
    rewrite (app_pure_natural (G := G1)).G1: Type -> Type
H1: Map G1
H2: Pure G1
H3: Mult G1
H: Applicative G1
G2: Type -> Type
H5: Map G2
H6: Pure G2
H7: Mult G2
H0: Applicative G2
A: Type
h: (G1 ∘ G2) A
n: nat
v: Vector.t ((G1 ∘ G2) A) n
IHv: dist VEC n (G1 ∘ G2) v = map (dist VEC n G2) (dist VEC n G1 v)
pure
  ((compose (ap G2)
    ∘ (precompose (dist VEC n G2) ∘ ap G2))
     (pure
        (Basics.flip
           (fun a0 : A => Vector.cons A a0 n)))) <⋆>
dist VEC n G1 v <⋆> h =
map (compose (dist VEC (S n) G2))
  (pure
     (Basics.flip
        (fun a : G2 A => Vector.cons (G2 A) a n)) <⋆>
   dist VEC n G1 v) <⋆> h
    (* RHS *)
    rewrite (map_ap (G := G1)).G1: Type -> Type
H1: Map G1
H2: Pure G1
H3: Mult G1
H: Applicative G1
G2: Type -> Type
H5: Map G2
H6: Pure G2
H7: Mult G2
H0: Applicative G2
A: Type
h: (G1 ∘ G2) A
n: nat
v: Vector.t ((G1 ∘ G2) A) n
IHv: dist VEC n (G1 ∘ G2) v = map (dist VEC n G2) (dist VEC n G1 v)
pure
  ((compose (ap G2)
    ∘ (precompose (dist VEC n G2) ∘ ap G2))
     (pure
        (Basics.flip
           (fun a0 : A => Vector.cons A a0 n)))) <⋆>
dist VEC n G1 v <⋆> h =
map (compose (compose (dist VEC (S n) G2)))
  (pure
     (Basics.flip
        (fun a : G2 A => Vector.cons (G2 A) a n))) <⋆>
dist VEC n G1 v <⋆> h
    rewrite (app_pure_natural (G := G1)).G1: Type -> Type
H1: Map G1
H2: Pure G1
H3: Mult G1
H: Applicative G1
G2: Type -> Type
H5: Map G2
H6: Pure G2
H7: Mult G2
H0: Applicative G2
A: Type
h: (G1 ∘ G2) A
n: nat
v: Vector.t ((G1 ∘ G2) A) n
IHv: dist VEC n (G1 ∘ G2) v = map (dist VEC n G2) (dist VEC n G1 v)
pure
  ((compose (ap G2)
    ∘ (precompose (dist VEC n G2) ∘ ap G2))
     (pure
        (Basics.flip
           (fun a0 : A => Vector.cons A a0 n)))) <⋆>
dist VEC n G1 v <⋆> h =
pure
  (compose (dist VEC (S n) G2)
   ∘ Basics.flip
       (fun a : G2 A => Vector.cons (G2 A) a n)) <⋆>
dist VEC n G1 v <⋆> h
    reflexivity.
Qed.

#[export] Instance TraversableFunctor_Vector (n : nat):
  Categorical.TraversableFunctor.TraversableFunctor (VEC n) :=
  {| dist_natural := dist_natural_Vector n;
    dist_morph := dist_morph_Vector n;
    dist_unit := dist_unit_Vector n;
    dist_linear := dist_linear_Vector n;
  |}.

(*
#[export] Instance Traverse_Vector (n : nat): Traverse (VEC n) :=
  Adapters.CategoricalToKleisli.TraversableFunctor.ToKleisli.Traverse_dist (VEC n).

#[export] Instance KleisliTraversableFunctor_Vector (n : nat):
  Kleisli.TraversableFunctor.TraversableFunctor (VEC n) :=
  Adapters.CategoricalToKleisli.TraversableFunctor.ToKleisli.TraversableFunctor_instance_0.
*)