From Tealeaves Require Export
  Classes.Categorical.Applicative
  Classes.Kleisli.TraversableFunctor
  Functors.Early.List.

Import Applicative.Notations.

#[local] Generalizable Variables F.

(** * The <<Backwards>> Applicative *)
(**********************************************************************)
Section Backwards.

  Record Backwards (F: Type -> Type) A :=
    mkBackwards { forwards: F A }.

  #[global] Arguments mkBackwards {F}%function_scope
    {A}%type_scope forwards.
  #[global] Arguments forwards {F}%function_scope
    {A}%type_scope b.

  (** ** Functor Instance *)
  (********************************************************************)
  Section functor.

    Context `{Functor F}.

    #[export] Instance Map_Backwards: Map (Backwards F) :=
      fun A B f b => mkBackwards (map f (forwards b)).

    #[export] Instance Functor_Backwards: Functor (Backwards F).
F: Type -> Type
Map_F: Map F
H: Functor F
Functor (Backwards F)
    Proof.
F: Type -> Type
Map_F: Map F
H: Functor F
Functor (Backwards F)
      constructor.
F: Type -> Type
Map_F: Map F
H: Functor F
forall A : Type, map id = id
F: Type -> Type
Map_F: Map F
H: Functor F
forall (A B C : Type) (f : A -> B) (g : B -> C),
map g ∘ map f = map (g ∘ f)
      -
F: Type -> Type
Map_F: Map F
H: Functor F
forall A : Type, map id = id intros.
F: Type -> Type
Map_F: Map F
H: Functor F
A: Type
map id = id ext [x].
F: Type -> Type
Map_F: Map F
H: Functor F
A: Type
x: F A
map id {| forwards := x |} = id {| forwards := x |}
        unfold_ops Map_Backwards.
F: Type -> Type
Map_F: Map F
H: Functor F
A: Type
x: F A
{|
  forwards := map id (forwards {| forwards := x |})
|} = id {| forwards := x |}
        rewrite fun_map_id.
F: Type -> Type
Map_F: Map F
H: Functor F
A: Type
x: F A
{| forwards := id (forwards {| forwards := x |}) |} =
id {| forwards := x |}
        reflexivity.
      -
F: Type -> Type
Map_F: Map F
H: Functor F
forall (A B C : Type) (f : A -> B) (g : B -> C),
map g ∘ map f = map (g ∘ f) intros.
F: Type -> Type
Map_F: Map F
H: Functor F
A, B, C: Type
f: A -> B
g: B -> C
map g ∘ map f = map (g ∘ f) ext [x].
F: Type -> Type
Map_F: Map F
H: Functor F
A, B, C: Type
f: A -> B
g: B -> C
x: F A
(map g ∘ map f) {| forwards := x |} =
map (g ∘ f) {| forwards := x |}
        unfold_ops Map_Backwards.
F: Type -> Type
Map_F: Map F
H: Functor F
A, B, C: Type
f: A -> B
g: B -> C
x: F A
((fun b : Backwards F B =>
  {| forwards := map g (forwards b) |})
 ∘ (fun b : Backwards F A =>
    {| forwards := map f (forwards b) |}))
  {| forwards := x |} =
{|
  forwards :=
    map (g ∘ f) (forwards {| forwards := x |})
|}
        rewrite <- fun_map_map.
F: Type -> Type
Map_F: Map F
H: Functor F
A, B, C: Type
f: A -> B
g: B -> C
x: F A
((fun b : Backwards F B =>
  {| forwards := map g (forwards b) |})
 ∘ (fun b : Backwards F A =>
    {| forwards := map f (forwards b) |}))
  {| forwards := x |} =
{|
  forwards :=
    (map g ∘ map f) (forwards {| forwards := x |})
|}
        reflexivity.
    Qed.

    #[export] Instance Natural_forwards: Natural (@forwards F).
F: Type -> Type
Map_F: Map F
H: Functor F
Natural (@forwards F)
    Proof.
F: Type -> Type
Map_F: Map F
H: Functor F
Natural (@forwards F)
      constructor; try typeclasses eauto.
F: Type -> Type
Map_F: Map F
H: Functor F
forall (A B : Type) (f : A -> B),
map f ∘ forwards = forwards ∘ map f
      intros.
F: Type -> Type
Map_F: Map F
H: Functor F
A, B: Type
f: A -> B
map f ∘ forwards = forwards ∘ map f ext [x].
F: Type -> Type
Map_F: Map F
H: Functor F
A, B: Type
f: A -> B
x: F A
(map f ∘ forwards) {| forwards := x |} =
(forwards ∘ map f) {| forwards := x |} reflexivity.
    Qed.

  End functor.

  (** ** Applicative Instance *)
  (********************************************************************)
  Section applicative.

    Context
      `{Applicative F}.

    #[export] Instance Pure_Backwards: Pure (Backwards F) :=
      fun A a => mkBackwards (pure a).

    Definition swap {A B}: B * A -> A * B :=
      fun '(b, a) => (a, b).

    Definition mult_Backwards {A B}:
      Backwards F A -> Backwards F B -> Backwards F (A * B) :=
      fun ba bb => mkBackwards (map swap (forwards bb ⊗ forwards ba)).

    #[export] Instance Mult_Backwards: Mult (Backwards F) :=
      fun A B '(x, y) => mult_Backwards x y.

    #[export] Instance Applicative_Backwards: Applicative (Backwards F).
F: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Applicative (Backwards F)
    Proof.
F: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Applicative (Backwards F)
      constructor;
        intros;
        unfold_ops Pure_Backwards;
        unfold_ops @Map_Backwards;
        unfold_ops @Mult_Backwards;
        unfold mult_Backwards;
        cbn.
F: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Functor (Backwards F)
F: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
A, B: Type
f: A -> B
x: A
{| forwards := map f (pure x) |} =
{| forwards := pure (f x) |}
F: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
A, B, C, D: Type
f: A -> C
g: B -> D
x: Backwards F A
y: Backwards F B
{|
  forwards :=
    map swap (map g (forwards y) ⊗ map f (forwards x))
|} =
{|
  forwards :=
    map (map_tensor f g)
      (map swap (forwards y ⊗ forwards x))
|}
F: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
A, B, C: Type
x: Backwards F A
y: Backwards F B
z: Backwards F C
{|
  forwards :=
    map associator
      (map swap
         (forwards z
          ⊗ map swap (forwards y ⊗ forwards x)))
|} =
{|
  forwards :=
    map swap
      (map swap (forwards z ⊗ forwards y) ⊗ forwards x)
|}
F: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
A: Type
x: Backwards F A
{|
  forwards :=
    map left_unitor (map swap (forwards x ⊗ pure tt))
|} = x
F: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
A: Type
x: Backwards F A
{|
  forwards :=
    map right_unitor (map swap (pure tt ⊗ forwards x))
|} = x
F: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
A, B: Type
a: A
b: B
{| forwards := map swap (pure b ⊗ pure a) |} =
{| forwards := pure (a, b) |}
      -
F: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
Functor (Backwards F) typeclasses eauto.
      -
F: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
A, B: Type
f: A -> B
x: A
{| forwards := map f (pure x) |} =
{| forwards := pure (f x) |} now rewrite app_pure_natural.
      -
F: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
A, B, C, D: Type
f: A -> C
g: B -> D
x: Backwards F A
y: Backwards F B
{|
  forwards :=
    map swap (map g (forwards y) ⊗ map f (forwards x))
|} =
{|
  forwards :=
    map (map_tensor f g)
      (map swap (forwards y ⊗ forwards x))
|} fequal.
F: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
A, B, C, D: Type
f: A -> C
g: B -> D
x: Backwards F A
y: Backwards F B
map swap (map g (forwards y) ⊗ map f (forwards x)) =
map (map_tensor f g)
  (map swap (forwards y ⊗ forwards x))
        rewrite app_mult_natural.
F: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
A, B, C, D: Type
f: A -> C
g: B -> D
x: Backwards F A
y: Backwards F B
map swap
  (map (map_tensor g f) (forwards y ⊗ forwards x)) =
map (map_tensor f g)
  (map swap (forwards y ⊗ forwards x))
        compose near (forwards y ⊗ forwards x).
F: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
A, B, C, D: Type
f: A -> C
g: B -> D
x: Backwards F A
y: Backwards F B
(map swap ∘ map (map_tensor g f))
  (forwards y ⊗ forwards x) =
(map (map_tensor f g) ∘ map swap)
  (forwards y ⊗ forwards x)
        do 2 rewrite fun_map_map.
F: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
A, B, C, D: Type
f: A -> C
g: B -> D
x: Backwards F A
y: Backwards F B
map (swap ∘ map_tensor g f) (forwards y ⊗ forwards x) =
map (map_tensor f g ∘ swap) (forwards y ⊗ forwards x)
        fequal.
F: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
A, B, C, D: Type
f: A -> C
g: B -> D
x: Backwards F A
y: Backwards F B
swap ∘ map_tensor g f = map_tensor f g ∘ swap
        now ext [p q].
      -
F: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
A, B, C: Type
x: Backwards F A
y: Backwards F B
z: Backwards F C
{|
  forwards :=
    map associator
      (map swap
         (forwards z
          ⊗ map swap (forwards y ⊗ forwards x)))
|} =
{|
  forwards :=
    map swap
      (map swap (forwards z ⊗ forwards y) ⊗ forwards x)
|} fequal.
F: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
A, B, C: Type
x: Backwards F A
y: Backwards F B
z: Backwards F C
map associator
  (map swap
     (forwards z ⊗ map swap (forwards y ⊗ forwards x))) =
map swap
  (map swap (forwards z ⊗ forwards y) ⊗ forwards x)
        rewrite (app_mult_natural_r F).
F: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
A, B, C: Type
x: Backwards F A
y: Backwards F B
z: Backwards F C
map associator
  (map swap
     (map (map_snd swap)
        (forwards z ⊗ (forwards y ⊗ forwards x)))) =
map swap
  (map swap (forwards z ⊗ forwards y) ⊗ forwards x)
        rewrite (app_mult_natural_l F).
F: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
A, B, C: Type
x: Backwards F A
y: Backwards F B
z: Backwards F C
map associator
  (map swap
     (map (map_snd swap)
        (forwards z ⊗ (forwards y ⊗ forwards x)))) =
map swap
  (map (map_fst swap)
     (forwards z ⊗ forwards y ⊗ forwards x))
        rewrite <- (app_assoc).
F: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
A, B, C: Type
x: Backwards F A
y: Backwards F B
z: Backwards F C
map associator
  (map swap
     (map (map_snd swap)
        (map associator
           (forwards z ⊗ forwards y ⊗ forwards x)))) =
map swap
  (map (map_fst swap)
     (forwards z ⊗ forwards y ⊗ forwards x))
        compose near (forwards z ⊗ forwards y ⊗ forwards x) on left.
F: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
A, B, C: Type
x: Backwards F A
y: Backwards F B
z: Backwards F C
map associator
  (map swap
     ((map (map_snd swap) ∘ map associator)
        (forwards z ⊗ forwards y ⊗ forwards x))) =
map swap
  (map (map_fst swap)
     (forwards z ⊗ forwards y ⊗ forwards x))
        compose near (forwards z ⊗ forwards y ⊗ forwards x) on left.
F: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
A, B, C: Type
x: Backwards F A
y: Backwards F B
z: Backwards F C
map associator
  ((map swap ∘ (map (map_snd swap) ∘ map associator))
     (forwards z ⊗ forwards y ⊗ forwards x)) =
map swap
  (map (map_fst swap)
     (forwards z ⊗ forwards y ⊗ forwards x))
        compose near (forwards z ⊗ forwards y ⊗ forwards x) on left.
F: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
A, B, C: Type
x: Backwards F A
y: Backwards F B
z: Backwards F C
(map associator
 ∘ (map swap ∘ (map (map_snd swap) ∘ map associator)))
  (forwards z ⊗ forwards y ⊗ forwards x) =
map swap
  (map (map_fst swap)
     (forwards z ⊗ forwards y ⊗ forwards x))
        compose near (forwards z ⊗ forwards y ⊗ forwards x) on right.
F: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
A, B, C: Type
x: Backwards F A
y: Backwards F B
z: Backwards F C
(map associator
 ∘ (map swap ∘ (map (map_snd swap) ∘ map associator)))
  (forwards z ⊗ forwards y ⊗ forwards x) =
(map swap ∘ map (map_fst swap))
  (forwards z ⊗ forwards y ⊗ forwards x)
        repeat rewrite (fun_map_map).
F: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
A, B, C: Type
x: Backwards F A
y: Backwards F B
z: Backwards F C
map
  (associator ∘ (swap ∘ (map_snd swap ∘ associator)))
  (forwards z ⊗ forwards y ⊗ forwards x) =
map (swap ∘ map_fst swap)
  (forwards z ⊗ forwards y ⊗ forwards x)
        fequal.
F: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
A, B, C: Type
x: Backwards F A
y: Backwards F B
z: Backwards F C
associator ∘ (swap ∘ (map_snd swap ∘ associator)) =
swap ∘ map_fst swap
        ext [[c b] a].
F: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
A, B, C: Type
x: Backwards F A
y: Backwards F B
z: Backwards F C
c: C
b: B
a: A
(associator ∘ (swap ∘ (map_snd swap ∘ associator)))
  (c, b, a) = (swap ∘ map_fst swap) (c, b, a)
        reflexivity.
      -
F: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
A: Type
x: Backwards F A
{|
  forwards :=
    map left_unitor (map swap (forwards x ⊗ pure tt))
|} = x destruct x as [forward].
F: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
A: Type
forward: F A
{|
  forwards :=
    map left_unitor
      (map swap
         (forwards {| forwards := forward |} ⊗ pure tt))
|} = {| forwards := forward |}
        cbn.
F: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
A: Type
forward: F A
{|
  forwards :=
    map left_unitor (map swap (forward ⊗ pure tt))
|} = {| forwards := forward |}
        fequal.
F: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
A: Type
forward: F A
map left_unitor (map swap (forward ⊗ pure tt)) =
forward
        compose near (forward ⊗ pure tt).
F: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
A: Type
forward: F A
(map left_unitor ∘ map swap) (forward ⊗ pure tt) =
forward
        rewrite (fun_map_map).
F: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
A: Type
forward: F A
map (left_unitor ∘ swap) (forward ⊗ pure tt) = forward
        replace (left_unitor ∘ swap) with (@right_unitor A).
F: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
A: Type
forward: F A
map right_unitor (forward ⊗ pure tt) = forward
F: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
A: Type
forward: F A
right_unitor = left_unitor ∘ swap
        now rewrite app_unital_r.
F: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
A: Type
forward: F A
right_unitor = left_unitor ∘ swap
        now ext [a tt].
      -
F: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
A: Type
x: Backwards F A
{|
  forwards :=
    map right_unitor (map swap (pure tt ⊗ forwards x))
|} = x destruct x as [forward].
F: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
A: Type
forward: F A
{|
  forwards :=
    map right_unitor
      (map swap
         (pure tt ⊗ forwards {| forwards := forward |}))
|} = {| forwards := forward |}
        cbn.
F: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
A: Type
forward: F A
{|
  forwards :=
    map right_unitor (map swap (pure tt ⊗ forward))
|} = {| forwards := forward |}
        fequal.
F: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
A: Type
forward: F A
map right_unitor (map swap (pure tt ⊗ forward)) =
forward
        compose near (pure tt ⊗ forward).
F: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
A: Type
forward: F A
(map right_unitor ∘ map swap) (pure tt ⊗ forward) =
forward
        rewrite (fun_map_map).
F: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
A: Type
forward: F A
map (right_unitor ∘ swap) (pure tt ⊗ forward) =
forward
        replace (right_unitor ∘ swap) with (@left_unitor A).
F: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
A: Type
forward: F A
map left_unitor (pure tt ⊗ forward) = forward
F: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
A: Type
forward: F A
left_unitor = right_unitor ∘ swap
        now rewrite app_unital_l.
F: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
A: Type
forward: F A
left_unitor = right_unitor ∘ swap
        now ext [a tt].
      -
F: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
A, B: Type
a: A
b: B
{| forwards := map swap (pure b ⊗ pure a) |} =
{| forwards := pure (a, b) |} fequal.
F: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
A, B: Type
a: A
b: B
map swap (pure b ⊗ pure a) = pure (a, b)
        rewrite app_mult_pure.
F: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
A, B: Type
a: A
b: B
map swap (pure (b, a)) = pure (a, b)
        rewrite app_pure_natural.
F: Type -> Type
Map_G: Map F
Pure_G: Pure F
Mult_G: Mult F
H: Applicative F
A, B: Type
a: A
b: B
pure (swap (b, a)) = pure (a, b)
        reflexivity.
    Qed.

  End applicative.

  (** ** Involutive Properties *)
  (********************************************************************)
  Section involution.

    Context
      {T G: Type -> Type}
      `{TraversableFunctor T}
      `{Applicative G}.

    Instance ApplicativeMorphism_double_forwards:
      ApplicativeMorphism (Backwards (Backwards G)) G
        (fun A => forwards ∘ forwards).
T, G: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
ApplicativeMorphism (Backwards (Backwards G)) G
  (fun A : Type => forwards ∘ forwards)
    Proof.
T, G: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
ApplicativeMorphism (Backwards (Backwards G)) G
  (fun A : Type => forwards ∘ forwards)
      constructor;
        try typeclasses eauto;
        intros;
        repeat (match goal with
                | x: Backwards (Backwards G) ?A
                  |- _ =>
                    destruct x as [[x]]
                end);
        try easy; cbn.
T, G: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
A, B: Type
x: G A
y: G B
map swap (map swap (x ⊗ y)) = x ⊗ y
      compose near (x ⊗ y).
T, G: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
A, B: Type
x: G A
y: G B
(map swap ∘ map swap) (x ⊗ y) = x ⊗ y
      rewrite fun_map_map.
T, G: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
A, B: Type
x: G A
y: G B
map (swap ∘ swap) (x ⊗ y) = x ⊗ y
      replace (swap ∘ swap) with (@id (A * B)).
T, G: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
A, B: Type
x: G A
y: G B
map id (x ⊗ y) = x ⊗ y
T, G: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
A, B: Type
x: G A
y: G B
id = swap ∘ swap
      now rewrite fun_map_id.
T, G: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
A, B: Type
x: G A
y: G B
id = swap ∘ swap
      now ext [a b].
    Qed.

    Instance ApplicativeMorphism_double_backwards:
      ApplicativeMorphism G (Backwards (Backwards G))
        (fun A => mkBackwards ∘ mkBackwards).
T, G: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
ApplicativeMorphism G (Backwards (Backwards G))
  (fun A : Type => mkBackwards ∘ mkBackwards)
    Proof.
T, G: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
ApplicativeMorphism G (Backwards (Backwards G))
  (fun A : Type => mkBackwards ∘ mkBackwards)
      constructor;
        try typeclasses eauto;
        intros;
        repeat (match goal with
                | x: Backwards (Backwards G) ?A
                  |- _ =>
                    destruct x as [[x]]
                end);
        try easy; cbn.
T, G: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
A, B: Type
x: G A
y: G B
(mkBackwards ∘ mkBackwards) (x ⊗ y) =
mult_Backwards ((mkBackwards ∘ mkBackwards) x)
  ((mkBackwards ∘ mkBackwards) y)
      unfold compose.
T, G: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
A, B: Type
x: G A
y: G B
{| forwards := {| forwards := x ⊗ y |} |} =
mult_Backwards {| forwards := {| forwards := x |} |}
  {| forwards := {| forwards := y |} |}
      unfold_ops @Mult_Backwards.
T, G: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
A, B: Type
x: G A
y: G B
{| forwards := {| forwards := x ⊗ y |} |} =
mult_Backwards {| forwards := {| forwards := x |} |}
  {| forwards := {| forwards := y |} |}
      unfold mult_Backwards.
T, G: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
A, B: Type
x: G A
y: G B
{| forwards := {| forwards := x ⊗ y |} |} =
{|
  forwards :=
    map swap
      (forwards {| forwards := {| forwards := y |} |}
       ⊗ forwards
           {| forwards := {| forwards := x |} |})
|}
      cbn.
T, G: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
A, B: Type
x: G A
y: G B
{| forwards := {| forwards := x ⊗ y |} |} =
{|
  forwards :=
    map swap {| forwards := map swap (x ⊗ y) |}
|}
      fequal.
T, G: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
A, B: Type
x: G A
y: G B
{| forwards := x ⊗ y |} =
map swap {| forwards := map swap (x ⊗ y) |}
      unfold_ops @Map_Backwards.
T, G: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
A, B: Type
x: G A
y: G B
{| forwards := x ⊗ y |} =
{|
  forwards :=
    map swap
      (forwards {| forwards := map swap (x ⊗ y) |})
|}
      cbn.
T, G: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
A, B: Type
x: G A
y: G B
{| forwards := x ⊗ y |} =
{| forwards := map swap (map swap (x ⊗ y)) |}
      do 2 fequal.
T, G: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
A, B: Type
x: G A
y: G B
x ⊗ y = map swap (map swap (x ⊗ y))
      compose near (x ⊗ y).
T, G: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
A, B: Type
x: G A
y: G B
x ⊗ y = (map swap ∘ map swap) (x ⊗ y)
      rewrite fun_map_map.
T, G: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
A, B: Type
x: G A
y: G B
x ⊗ y = map (swap ∘ swap) (x ⊗ y)
      replace (swap ∘ swap) with (@id (A * B)).
T, G: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
A, B: Type
x: G A
y: G B
x ⊗ y = map id (x ⊗ y)
T, G: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
A, B: Type
x: G A
y: G B
id = swap ∘ swap
      now rewrite fun_map_id.
T, G: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
A, B: Type
x: G A
y: G B
id = swap ∘ swap
      now ext [a b].
    Qed.

    Context
      {A B: Type}
      {f: A -> G B}
      (t: T A).


    (** ** Traversing by <<Backwards (Backwards G)>> *)
    (******************************************************************)
    Lemma traverse_double_backwards:
      forwards (forwards
                  (traverse (G := Backwards (Backwards G))
                     (mkBackwards ∘ (mkBackwards ∘ f)) t)) =
        traverse f t.
T, G: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
A, B: Type
f: A -> G B
t: T A
forwards
  (forwards
     (traverse (mkBackwards ∘ (mkBackwards ∘ f)) t)) =
traverse f t
    Proof.
T, G: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
A, B: Type
f: A -> G B
t: T A
forwards
  (forwards
     (traverse (mkBackwards ∘ (mkBackwards ∘ f)) t)) =
traverse f t
      intros.
T, G: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
A, B: Type
f: A -> G B
t: T A
forwards
  (forwards
     (traverse (mkBackwards ∘ (mkBackwards ∘ f)) t)) =
traverse f t
      compose near t on left.
T, G: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
A, B: Type
f: A -> G B
t: T A
forwards
  ((forwards
    ∘ traverse (mkBackwards ∘ (mkBackwards ∘ f))) t) =
traverse f t
      change_left (((forwards ∘ forwards)
                      ∘ traverse (T := T)
                      (G := Backwards (Backwards G))
                      (mkBackwards ∘ (mkBackwards ∘ f))) t).
T, G: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
A, B: Type
f: A -> G B
t: T A
(forwards ∘ forwards
 ∘ traverse (mkBackwards ∘ (mkBackwards ∘ f))) t =
traverse f t
      rewrite (trf_traverse_morphism
                 (morphism := ApplicativeMorphism_double_forwards)).
T, G: Type -> Type
Traverse_T: Traverse T
H: TraversableFunctor T
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H0: Applicative G
A, B: Type
f: A -> G B
t: T A
traverse
  (forwards ∘ forwards
   ∘ (mkBackwards ∘ (mkBackwards ∘ f))) t =
traverse f t
      reflexivity.
    Qed.

  End involution.

  (** ** Miscellaneous *)
  (********************************************************************)
  Lemma forwards_ap {G} `{Applicative G}:
    forall {A B: Type} (f: (Backwards G) (A -> B)) (a: (Backwards G) A),
      forwards (f <⋆> a) =
        map evalAt (forwards a) <⋆> forwards f.
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
forall (A B : Type) (f : Backwards G (A -> B))
  (a : Backwards G A),
forwards (f <⋆> a) =
map evalAt (forwards a) <⋆> forwards f
  Proof.
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
forall (A B : Type) (f : Backwards G (A -> B))
  (a : Backwards G A),
forwards (f <⋆> a) =
map evalAt (forwards a) <⋆> forwards f
    intros.
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: Backwards G (A -> B)
a: Backwards G A
forwards (f <⋆> a) =
map evalAt (forwards a) <⋆> forwards f
    cbn.
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: Backwards G (A -> B)
a: Backwards G A
map (fun '(f, a) => f a)
  (map swap (forwards a ⊗ forwards f)) =
map evalAt (forwards a) <⋆> forwards f
    unfold ap.
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: Backwards G (A -> B)
a: Backwards G A
map (fun '(f, a) => f a)
  (map swap (forwards a ⊗ forwards f)) =
map (fun '(f, a) => f a)
  (map evalAt (forwards a) ⊗ forwards f)
    rewrite (app_mult_natural_l G).
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: Backwards G (A -> B)
a: Backwards G A
map (fun '(f, a) => f a)
  (map swap (forwards a ⊗ forwards f)) =
map (fun '(f, a) => f a)
  (map (map_fst evalAt) (forwards a ⊗ forwards f))
    compose near (forwards a ⊗ forwards  f).
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: Backwards G (A -> B)
a: Backwards G A
(map (fun '(f, a) => f a) ∘ map swap)
  (forwards a ⊗ forwards f) =
(map (fun '(f, a) => f a) ∘ map (map_fst evalAt))
  (forwards a ⊗ forwards f)
    do 2 rewrite (fun_map_map).
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: Backwards G (A -> B)
a: Backwards G A
map ((fun '(f, a) => f a) ∘ swap)
  (forwards a ⊗ forwards f) =
map ((fun '(f, a) => f a) ∘ map_fst evalAt)
  (forwards a ⊗ forwards f)
    fequal.
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: Backwards G (A -> B)
a: Backwards G A
(fun '(f, a) => f a) ∘ swap =
(fun '(f, a) => f a) ∘ map_fst evalAt
    now ext [p q].
  Qed.

  (** ** Traversing over Lists Backwards *)
  (********************************************************************)
  Lemma traverse_backwards_list1 {G} `{Applicative G}:
    forall {A B: Type} (f: A -> G B) (l: list A),
      traverse f l =
        map (@List.rev B)
          (forwards
             (traverse (G := Backwards G)
                (mkBackwards ∘ f)
                (List.rev l))).
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
forall (A B : Type) (f : A -> G B) (l : list A),
traverse f l =
map (List.rev (A:=B))
  (forwards (traverse (mkBackwards ∘ f) (List.rev l)))
  Proof.
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
forall (A B : Type) (f : A -> G B) (l : list A),
traverse f l =
map (List.rev (A:=B))
  (forwards (traverse (mkBackwards ∘ f) (List.rev l)))
    intros.
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G B
l: list A
traverse f l =
map (List.rev (A:=B))
  (forwards (traverse (mkBackwards ∘ f) (List.rev l)))
    induction l.
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G B
traverse f nil =
map (List.rev (A:=B))
  (forwards
     (traverse (mkBackwards ∘ f) (List.rev nil)))
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G B
a: A
l: list A
IHl: traverse f l =
map (List.rev (A:=B))
  (forwards
     (traverse (mkBackwards ∘ f) (List.rev l)))
traverse f (a :: l) =
map (List.rev (A:=B))
  (forwards
     (traverse (mkBackwards ∘ f) (List.rev (a :: l))))
    -
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G B
traverse f nil =
map (List.rev (A:=B))
  (forwards
     (traverse (mkBackwards ∘ f) (List.rev nil))) cbn.
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G B
pure nil = map (List.rev (A:=B)) (pure nil)
      rewrite app_pure_natural.
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G B
pure nil = pure (List.rev nil)
      reflexivity.
    -
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G B
a: A
l: list A
IHl: traverse f l =
map (List.rev (A:=B))
  (forwards
     (traverse (mkBackwards ∘ f) (List.rev l)))
traverse f (a :: l) =
map (List.rev (A:=B))
  (forwards
     (traverse (mkBackwards ∘ f) (List.rev (a :: l)))) cbn.
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G B
a: A
l: list A
IHl: traverse f l =
map (List.rev (A:=B))
  (forwards
     (traverse (mkBackwards ∘ f) (List.rev l)))
pure cons <⋆> f a <⋆> traverse f l =
map (List.rev (A:=B))
  (forwards
     (traverse (mkBackwards ∘ f)
        (List.rev l ++ a :: nil)))
      (* left *)
      rewrite IHl.
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G B
a: A
l: list A
IHl: traverse f l =
map (List.rev (A:=B))
  (forwards
     (traverse (mkBackwards ∘ f) (List.rev l)))
pure cons <⋆> f a <⋆>
map (List.rev (A:=B))
  (forwards (traverse (mkBackwards ∘ f) (List.rev l))) =
map (List.rev (A:=B))
  (forwards
     (traverse (mkBackwards ∘ f)
        (List.rev l ++ a :: nil)))
      rewrite map_to_ap.
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G B
a: A
l: list A
IHl: traverse f l =
map (List.rev (A:=B))
  (forwards
     (traverse (mkBackwards ∘ f) (List.rev l)))
pure cons <⋆> f a <⋆>
(pure (List.rev (A:=B)) <⋆>
 forwards (traverse (mkBackwards ∘ f) (List.rev l))) =
map (List.rev (A:=B))
  (forwards
     (traverse (mkBackwards ∘ f)
        (List.rev l ++ a :: nil)))
      repeat rewrite <- ap4;
        repeat rewrite ap2.
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G B
a: A
l: list A
IHl: traverse f l =
map (List.rev (A:=B))
  (forwards
     (traverse (mkBackwards ∘ f) (List.rev l)))
pure (compose ∘ cons) <⋆> f a <⋆>
pure (List.rev (A:=B)) <⋆>
forwards (traverse (mkBackwards ∘ f) (List.rev l)) =
map (List.rev (A:=B))
  (forwards
     (traverse (mkBackwards ∘ f)
        (List.rev l ++ a :: nil)))
      rewrite ap3;
        unfold evalAt;
        repeat rewrite <- ap4;
        repeat rewrite ap2.
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G B
a: A
l: list A
IHl: traverse f l =
map (List.rev (A:=B))
  (forwards
     (traverse (mkBackwards ∘ f) (List.rev l)))
pure
  ((fun f : (list B -> list B) -> list B -> list B =>
    f (List.rev (A:=B))) ∘ (compose ∘ cons)) <⋆> f a <⋆>
forwards (traverse (mkBackwards ∘ f) (List.rev l)) =
map (List.rev (A:=B))
  (forwards
     (traverse (mkBackwards ∘ f)
        (List.rev l ++ a :: nil)))
      unfold compose.
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G B
a: A
l: list A
IHl: traverse f l =
map (List.rev (A:=B))
  (forwards
     (traverse (mkBackwards ∘ f) (List.rev l)))
pure (fun a : B => cons a ○ List.rev (A:=B)) <⋆> f a <⋆>
forwards (traverse (mkBackwards ○ f) (List.rev l)) =
map (List.rev (A:=B))
  (forwards
     (traverse (mkBackwards ○ f)
        (List.rev l ++ a :: nil)))
      assert
        (cut:
          (fun (b:B) => cons b ○ List.rev (A := B)) =
            (compose (List.rev (A := B)) ∘ Basics.flip (@snoc B))).
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G B
a: A
l: list A
IHl: traverse f l =
map (List.rev (A:=B))
  (forwards
     (traverse (mkBackwards ∘ f) (List.rev l)))
(fun b : B => cons b ○ List.rev (A:=B)) =
compose (List.rev (A:=B)) ∘ Basics.flip snoc
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G B
a: A
l: list A
IHl: traverse f l =
map (List.rev (A:=B))
  (forwards
     (traverse (mkBackwards ∘ f) (List.rev l)))
cut: (fun b : B => cons b ○ List.rev (A:=B)) =
compose (List.rev (A:=B)) ∘ Basics.flip snoc
pure (fun a : B => cons a ○ List.rev (A:=B)) <⋆> f a <⋆>
forwards (traverse (mkBackwards ○ f) (List.rev l)) =
map (List.rev (A:=B))
  (forwards
     (traverse (mkBackwards ○ f)
        (List.rev l ++ a :: nil)))
      {
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G B
a: A
l: list A
IHl: traverse f l =
map (List.rev (A:=B))
  (forwards
     (traverse (mkBackwards ∘ f) (List.rev l)))
(fun b : B => cons b ○ List.rev (A:=B)) =
compose (List.rev (A:=B)) ∘ Basics.flip snoc ext x y.
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G B
a: A
l: list A
IHl: traverse f l =
map (List.rev (A:=B))
  (forwards
     (traverse (mkBackwards ∘ f) (List.rev l)))
x: B
y: list B
x :: List.rev y =
(compose (List.rev (A:=B)) ∘ Basics.flip snoc) x y unfold compose, Basics.flip, snoc.
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G B
a: A
l: list A
IHl: traverse f l =
map (List.rev (A:=B))
  (forwards
     (traverse (mkBackwards ∘ f) (List.rev l)))
x: B
y: list B
x :: List.rev y = List.rev (y ++ x :: nil)
        rewrite List.rev_unit.
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G B
a: A
l: list A
IHl: traverse f l =
map (List.rev (A:=B))
  (forwards
     (traverse (mkBackwards ∘ f) (List.rev l)))
x: B
y: list B
x :: List.rev y = x :: List.rev y
        reflexivity. }
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G B
a: A
l: list A
IHl: traverse f l =
map (List.rev (A:=B))
  (forwards
     (traverse (mkBackwards ∘ f) (List.rev l)))
cut: (fun b : B => cons b ○ List.rev (A:=B)) =
compose (List.rev (A:=B)) ∘ Basics.flip snoc
pure (fun a : B => cons a ○ List.rev (A:=B)) <⋆> f a <⋆>
forwards (traverse (mkBackwards ○ f) (List.rev l)) =
map (List.rev (A:=B))
  (forwards
     (traverse (mkBackwards ○ f)
        (List.rev l ++ a :: nil)))
      rewrite cut.
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G B
a: A
l: list A
IHl: traverse f l =
map (List.rev (A:=B))
  (forwards
     (traverse (mkBackwards ∘ f) (List.rev l)))
cut: (fun b : B => cons b ○ List.rev (A:=B)) =
compose (List.rev (A:=B)) ∘ Basics.flip snoc
pure (compose (List.rev (A:=B)) ∘ Basics.flip snoc) <⋆>
f a <⋆>
forwards (traverse (mkBackwards ○ f) (List.rev l)) =
map (List.rev (A:=B))
  (forwards
     (traverse (mkBackwards ○ f)
        (List.rev l ++ a :: nil)))
      (* right *)
      rewrite traverse_list_snoc; [|typeclasses eauto].
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G B
a: A
l: list A
IHl: traverse f l =
map (List.rev (A:=B))
  (forwards
     (traverse (mkBackwards ∘ f) (List.rev l)))
cut: (fun b : B => cons b ○ List.rev (A:=B)) =
compose (List.rev (A:=B)) ∘ Basics.flip snoc
pure (compose (List.rev (A:=B)) ∘ Basics.flip snoc) <⋆>
f a <⋆>
forwards (traverse (mkBackwards ○ f) (List.rev l)) =
map (List.rev (A:=B))
  (forwards
     (pure snoc <⋆>
      traverse (mkBackwards ○ f) (List.rev l) <⋆>
      {| forwards := f a |}))
      change (map ?f (forwards ?x)) with
        (forwards (map f x)).
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G B
a: A
l: list A
IHl: traverse f l =
map (List.rev (A:=B))
  (forwards
     (traverse (mkBackwards ∘ f) (List.rev l)))
cut: (fun b : B => cons b ○ List.rev (A:=B)) =
compose (List.rev (A:=B)) ∘ Basics.flip snoc
pure (compose (List.rev (A:=B)) ∘ Basics.flip snoc) <⋆>
f a <⋆>
forwards (traverse (mkBackwards ○ f) (List.rev l)) =
forwards
  (map (List.rev (A:=B))
     (pure snoc <⋆>
      traverse (mkBackwards ○ f) (List.rev l) <⋆>
      {| forwards := f a |}))
      rewrite map_to_ap.
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G B
a: A
l: list A
IHl: traverse f l =
map (List.rev (A:=B))
  (forwards
     (traverse (mkBackwards ∘ f) (List.rev l)))
cut: (fun b : B => cons b ○ List.rev (A:=B)) =
compose (List.rev (A:=B)) ∘ Basics.flip snoc
pure (compose (List.rev (A:=B)) ∘ Basics.flip snoc) <⋆>
f a <⋆>
forwards (traverse (mkBackwards ○ f) (List.rev l)) =
forwards
  (pure (List.rev (A:=B)) <⋆>
   (pure snoc <⋆>
    traverse (mkBackwards ○ f) (List.rev l) <⋆>
    {| forwards := f a |}))
      repeat rewrite <- ap4;
        repeat rewrite ap2.
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G B
a: A
l: list A
IHl: traverse f l =
map (List.rev (A:=B))
  (forwards
     (traverse (mkBackwards ∘ f) (List.rev l)))
cut: (fun b : B => cons b ○ List.rev (A:=B)) =
compose (List.rev (A:=B)) ∘ Basics.flip snoc
pure (compose (List.rev (A:=B)) ∘ Basics.flip snoc) <⋆>
f a <⋆>
forwards (traverse (mkBackwards ○ f) (List.rev l)) =
forwards
  (pure ((compose ∘ compose) (List.rev (A:=B)) snoc) <⋆>
   traverse (mkBackwards ○ f) (List.rev l) <⋆>
   {| forwards := f a |})
      rewrite forwards_ap.
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G B
a: A
l: list A
IHl: traverse f l =
map (List.rev (A:=B))
  (forwards
     (traverse (mkBackwards ∘ f) (List.rev l)))
cut: (fun b : B => cons b ○ List.rev (A:=B)) =
compose (List.rev (A:=B)) ∘ Basics.flip snoc
pure (compose (List.rev (A:=B)) ∘ Basics.flip snoc) <⋆>
f a <⋆>
forwards (traverse (mkBackwards ○ f) (List.rev l)) =
map evalAt (forwards {| forwards := f a |}) <⋆>
forwards
  (pure ((compose ∘ compose) (List.rev (A:=B)) snoc) <⋆>
   traverse (mkBackwards ○ f) (List.rev l))
      rewrite forwards_ap.
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G B
a: A
l: list A
IHl: traverse f l =
map (List.rev (A:=B))
  (forwards
     (traverse (mkBackwards ∘ f) (List.rev l)))
cut: (fun b : B => cons b ○ List.rev (A:=B)) =
compose (List.rev (A:=B)) ∘ Basics.flip snoc
pure (compose (List.rev (A:=B)) ∘ Basics.flip snoc) <⋆>
f a <⋆>
forwards (traverse (mkBackwards ○ f) (List.rev l)) =
map evalAt (forwards {| forwards := f a |}) <⋆>
(map evalAt
   (forwards (traverse (mkBackwards ○ f) (List.rev l))) <⋆>
 forwards
   (pure ((compose ∘ compose) (List.rev (A:=B)) snoc)))
      rewrite map_to_ap;
        repeat rewrite <- ap4;
        repeat rewrite ap2.
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G B
a: A
l: list A
IHl: traverse f l =
map (List.rev (A:=B))
  (forwards
     (traverse (mkBackwards ∘ f) (List.rev l)))
cut: (fun b : B => cons b ○ List.rev (A:=B)) =
compose (List.rev (A:=B)) ∘ Basics.flip snoc
pure (compose (List.rev (A:=B)) ∘ Basics.flip snoc) <⋆>
f a <⋆>
forwards (traverse (mkBackwards ○ f) (List.rev l)) =
pure (compose ∘ evalAt) <⋆>
forwards {| forwards := f a |} <⋆>
map evalAt
  (forwards (traverse (mkBackwards ○ f) (List.rev l))) <⋆>
forwards
  (pure ((compose ∘ compose) (List.rev (A:=B)) snoc))
      cbn.
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G B
a: A
l: list A
IHl: traverse f l =
map (List.rev (A:=B))
  (forwards
     (traverse (mkBackwards ∘ f) (List.rev l)))
cut: (fun b : B => cons b ○ List.rev (A:=B)) =
compose (List.rev (A:=B)) ∘ Basics.flip snoc
pure (compose (List.rev (A:=B)) ∘ Basics.flip snoc) <⋆>
f a <⋆>
forwards (traverse (mkBackwards ○ f) (List.rev l)) =
pure (compose ∘ evalAt) <⋆> f a <⋆>
map evalAt
  (forwards (traverse (mkBackwards ○ f) (List.rev l))) <⋆>
pure ((compose ∘ compose) (List.rev (A:=B)) snoc)
      rewrite map_to_ap;
        repeat rewrite <- ap4;
        repeat rewrite ap2.
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G B
a: A
l: list A
IHl: traverse f l =
map (List.rev (A:=B))
  (forwards
     (traverse (mkBackwards ∘ f) (List.rev l)))
cut: (fun b : B => cons b ○ List.rev (A:=B)) =
compose (List.rev (A:=B)) ∘ Basics.flip snoc
pure (compose (List.rev (A:=B)) ∘ Basics.flip snoc) <⋆>
f a <⋆>
forwards (traverse (mkBackwards ○ f) (List.rev l)) =
pure (compose ∘ (compose ∘ evalAt)) <⋆> f a <⋆>
pure evalAt <⋆>
forwards (traverse (mkBackwards ○ f) (List.rev l)) <⋆>
pure ((compose ∘ compose) (List.rev (A:=B)) snoc)
      rewrite ap3;
        unfold evalAt;
        repeat rewrite <- ap4;
        repeat rewrite ap2.
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G B
a: A
l: list A
IHl: traverse f l =
map (List.rev (A:=B))
  (forwards
     (traverse (mkBackwards ∘ f) (List.rev l)))
cut: (fun b : B => cons b ○ List.rev (A:=B)) =
compose (List.rev (A:=B)) ∘ Basics.flip snoc
pure (compose (List.rev (A:=B)) ∘ Basics.flip snoc) <⋆>
f a <⋆>
forwards (traverse (mkBackwards ○ f) (List.rev l)) =
pure
  ((compose ∘ compose) compose compose compose compose
     compose
     (fun f : (list B -> B -> list B) -> list B =>
      f ((compose ∘ compose) (List.rev (A:=B)) snoc))
     (compose
      ∘ (compose
         ∘ (fun (a : B) (f : B -> list B) => f a)))) <⋆>
f a <⋆>
pure
  (fun (a : list B) (f : list B -> B -> list B) => f a) <⋆>
forwards (traverse (mkBackwards ○ f) (List.rev l))
      rewrite ap3;
        unfold evalAt;
        repeat rewrite <- ap4;
        repeat rewrite ap2.
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G B
a: A
l: list A
IHl: traverse f l =
map (List.rev (A:=B))
  (forwards
     (traverse (mkBackwards ∘ f) (List.rev l)))
cut: (fun b : B => cons b ○ List.rev (A:=B)) =
compose (List.rev (A:=B)) ∘ Basics.flip snoc
pure (compose (List.rev (A:=B)) ∘ Basics.flip snoc) <⋆>
f a <⋆>
forwards (traverse (mkBackwards ○ f) (List.rev l)) =
pure
  ((fun
      f : (list B ->
           (list B -> B -> list B) -> B -> list B) ->
          list B -> list B =>
    f
      (fun (a : list B) (f0 : list B -> B -> list B)
       => f0 a))
   ∘ (compose ∘ compose) compose compose compose
       compose compose
       (fun f : (list B -> B -> list B) -> list B =>
        f ((compose ∘ compose) (List.rev (A:=B)) snoc))
       (compose
        ∘ (compose
           ∘ (fun (a : B) (f : B -> list B) => f a)))) <⋆>
f a <⋆>
forwards (traverse (mkBackwards ○ f) (List.rev l))
      reflexivity.
  Qed.

  Lemma traverse_backwards_list2 {G} `{Applicative G}:
    forall {A B: Type} (f: A -> G B) (l: list A),
      traverse f (List.rev l) =
        forwards (map (List.rev (A:=B))
                    (traverse (G := Backwards G)
                       (mkBackwards ∘ f) l)).
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
forall (A B : Type) (f : A -> G B) (l : list A),
traverse f (List.rev l) =
forwards
  (map (List.rev (A:=B))
     (traverse (mkBackwards ∘ f) l))
  Proof.
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
forall (A B : Type) (f : A -> G B) (l : list A),
traverse f (List.rev l) =
forwards
  (map (List.rev (A:=B))
     (traverse (mkBackwards ∘ f) l))
    intros.
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G B
l: list A
traverse f (List.rev l) =
forwards
  (map (List.rev (A:=B))
     (traverse (mkBackwards ∘ f) l))
    rewrite traverse_backwards_list1.
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G B
l: list A
map (List.rev (A:=B))
  (forwards
     (traverse (mkBackwards ∘ f)
        (List.rev (List.rev l)))) =
forwards
  (map (List.rev (A:=B))
     (traverse (mkBackwards ∘ f) l))
    change (map ?f (forwards ?x)) with
      (forwards (map f x)).
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G B
l: list A
forwards
  (map (List.rev (A:=B))
     (traverse (mkBackwards ∘ f)
        (List.rev (List.rev l)))) =
forwards
  (map (List.rev (A:=B))
     (traverse (mkBackwards ∘ f) l))
    rewrite List.rev_involutive.
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> G B
l: list A
forwards
  (map (List.rev (A:=B))
     (traverse (mkBackwards ∘ f) l)) =
forwards
  (map (List.rev (A:=B))
     (traverse (mkBackwards ∘ f) l))
    reflexivity.
  Qed.

End Backwards.