From Tealeaves Require Import
  Classes.Kleisli.Theory.TraversableFunctor
  Classes.Categorical.ApplicativeCommutativeIdempotent
  Functors.Diagonal.

Import List.ListNotations.
Import Applicative.Notations.

(** * Examples of Commutative-Idempotent-Traversable Homomorphisms *)
(**********************************************************************)
Section ci_traversable_hom_examples.

  Context
    `{G: Type -> Type} `{Map G} `{Mult G} `{Pure G}
    `{! ApplicativeCommutativeIdempotent G}.

  (** ** Traverse Commutes with List Reversal *)
  (********************************************************************)
  Lemma rev_traverse_ci_hom {A B: Type}
    (f: A  -> G B) (l: list A):
    map (F := G) (List.rev (A := B))
      (traverse f l) = traverse f (List.rev l).
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
l: list A
map (List.rev (A:=B)) (traverse f l) =
traverse f (List.rev l)
  Proof.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
l: list A
map (List.rev (A:=B)) (traverse f l) =
traverse f (List.rev l)
    induction l.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
map (List.rev (A:=B)) (traverse f []) =
traverse f (List.rev [])
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a: A
l: list A
IHl: map (List.rev (A:=B)) (traverse f l) =
traverse f (List.rev l)
map (List.rev (A:=B)) (traverse f (a :: l)) =
traverse f (List.rev (a :: l))
    -
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
map (List.rev (A:=B)) (traverse f []) =
traverse f (List.rev []) cbn.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
map (List.rev (A:=B)) (pure []) = pure [] rewrite app_pure_natural.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
pure (List.rev []) = pure [] reflexivity.
    -
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a: A
l: list A
IHl: map (List.rev (A:=B)) (traverse f l) =
traverse f (List.rev l)
map (List.rev (A:=B)) (traverse f (a :: l)) =
traverse f (List.rev (a :: l)) rewrite traverse_list_cons.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a: A
l: list A
IHl: map (List.rev (A:=B)) (traverse f l) =
traverse f (List.rev l)
map (List.rev (A:=B))
  (pure cons <⋆> f a <⋆> traverse f l) =
traverse f (List.rev (a :: l))
      rewrite map_ap.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a: A
l: list A
IHl: map (List.rev (A:=B)) (traverse f l) =
traverse f (List.rev l)
map (compose (List.rev (A:=B))) (pure cons <⋆> f a) <⋆>
traverse f l = traverse f (List.rev (a :: l))
      rewrite map_ap.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a: A
l: list A
IHl: map (List.rev (A:=B)) (traverse f l) =
traverse f (List.rev l)
map (compose (compose (List.rev (A:=B)))) (pure cons) <⋆>
f a <⋆> traverse f l = traverse f (List.rev (a :: l))
      rewrite app_pure_natural.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a: A
l: list A
IHl: map (List.rev (A:=B)) (traverse f l) =
traverse f (List.rev l)
pure (compose (List.rev (A:=B)) ∘ cons) <⋆> f a <⋆>
traverse f l = traverse f (List.rev (a :: l))
      (* rhs *)
      cbn.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a: A
l: list A
IHl: map (List.rev (A:=B)) (traverse f l) =
traverse f (List.rev l)
pure (compose (List.rev (A:=B)) ∘ cons) <⋆> f a <⋆>
traverse f l = traverse f (List.rev l ++ [a])
      rewrite (traverse_list_app G).
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a: A
l: list A
IHl: map (List.rev (A:=B)) (traverse f l) =
traverse f (List.rev l)
pure (compose (List.rev (A:=B)) ∘ cons) <⋆> f a <⋆>
traverse f l =
pure (app (A:=B)) <⋆> traverse f (List.rev l) <⋆>
traverse f [a]
      rewrite <- IHl.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a: A
l: list A
IHl: map (List.rev (A:=B)) (traverse f l) =
traverse f (List.rev l)
pure (compose (List.rev (A:=B)) ∘ cons) <⋆> f a <⋆>
traverse f l =
pure (app (A:=B)) <⋆>
map (List.rev (A:=B)) (traverse f l) <⋆>
traverse f [a]
      rewrite <- ap_map.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a: A
l: list A
IHl: map (List.rev (A:=B)) (traverse f l) =
traverse f (List.rev l)
pure (compose (List.rev (A:=B)) ∘ cons) <⋆> f a <⋆>
traverse f l =
map (precompose (List.rev (A:=B))) (pure (app (A:=B))) <⋆>
traverse f l <⋆> traverse f [a]
      rewrite app_pure_natural.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a: A
l: list A
IHl: map (List.rev (A:=B)) (traverse f l) =
traverse f (List.rev l)
pure (compose (List.rev (A:=B)) ∘ cons) <⋆> f a <⋆>
traverse f l =
pure (precompose (List.rev (A:=B)) (app (A:=B))) <⋆>
traverse f l <⋆> traverse f [a]
      change [a] with (ret a).
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a: A
l: list A
IHl: map (List.rev (A:=B)) (traverse f l) =
traverse f (List.rev l)
pure (compose (List.rev (A:=B)) ∘ cons) <⋆> f a <⋆>
traverse f l =
pure (precompose (List.rev (A:=B)) (app (A:=B))) <⋆>
traverse f l <⋆> traverse f (ret a)
      rewrite (traverse_list_one G).
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a: A
l: list A
IHl: map (List.rev (A:=B)) (traverse f l) =
traverse f (List.rev l)
pure (compose (List.rev (A:=B)) ∘ cons) <⋆> f a <⋆>
traverse f l =
pure (precompose (List.rev (A:=B)) (app (A:=B))) <⋆>
traverse f l <⋆> map ret (f a)
      rewrite <- ap_map.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a: A
l: list A
IHl: map (List.rev (A:=B)) (traverse f l) =
traverse f (List.rev l)
pure (compose (List.rev (A:=B)) ∘ cons) <⋆> f a <⋆>
traverse f l =
map (precompose ret)
  (pure (precompose (List.rev (A:=B)) (app (A:=B))) <⋆>
   traverse f l) <⋆> f a
      rewrite map_ap.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a: A
l: list A
IHl: map (List.rev (A:=B)) (traverse f l) =
traverse f (List.rev l)
pure (compose (List.rev (A:=B)) ∘ cons) <⋆> f a <⋆>
traverse f l =
map (compose (precompose ret))
  (pure (precompose (List.rev (A:=B)) (app (A:=B)))) <⋆>
traverse f l <⋆> f a
      rewrite app_pure_natural.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a: A
l: list A
IHl: map (List.rev (A:=B)) (traverse f l) =
traverse f (List.rev l)
pure (compose (List.rev (A:=B)) ∘ cons) <⋆> f a <⋆>
traverse f l =
pure
  (precompose ret
   ∘ precompose (List.rev (A:=B)) (app (A:=B))) <⋆>
traverse f l <⋆> f a
      rewrite (ap_ci_flip _ (traverse f l) (f a)).
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a: A
l: list A
IHl: map (List.rev (A:=B)) (traverse f l) =
traverse f (List.rev l)
pure (compose (List.rev (A:=B)) ∘ cons) <⋆> f a <⋆>
traverse f l =
map flip
  (pure
     (precompose ret
      ∘ precompose (List.rev (A:=B)) (app (A:=B)))) <⋆>
f a <⋆> traverse f l
      rewrite app_pure_natural.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a: A
l: list A
IHl: map (List.rev (A:=B)) (traverse f l) =
traverse f (List.rev l)
pure (compose (List.rev (A:=B)) ∘ cons) <⋆> f a <⋆>
traverse f l =
pure
  (flip
     (precompose ret
      ∘ precompose (List.rev (A:=B)) (app (A:=B)))) <⋆>
f a <⋆> traverse f l
      fequal.
  Qed.

  (** ** "Duplicate First Element" *)
  (********************************************************************)
  Definition dupfst {A:Type} (l: list A): list A :=
    match l with
    | nil => nil
    | cons a l' =>  cons a (cons a l')
    end.

  Lemma dupfst_pointfree: forall (A: Type) (a: A) (l: list A),
      (* (compose dec ∘ cons) a l = dec (cons a l).*)
      (*
        (compose dupfst ∘ cons) a l = (precompose dup ∘ cons) a l.
       *)
      1 = 1.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
forall A : Type, A -> list A -> 1 = 1
  Proof.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
forall A : Type, A -> list A -> 1 = 1
    reflexivity.
  Qed.

  Lemma key_principle_simplified {A B: Type}
    (f: A  -> G B) (l: list A):
    map (F := G) dupfst (traverse f l) = traverse f (dupfst l).
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
l: list A
map dupfst (traverse f l) = traverse f (dupfst l)
  Proof.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
l: list A
map dupfst (traverse f l) = traverse f (dupfst l)
    intros.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
l: list A
map dupfst (traverse f l) = traverse f (dupfst l)
    induction l.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
map dupfst (traverse f []) = traverse f (dupfst [])
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a: A
l: list A
IHl: map dupfst (traverse f l) =
traverse f (dupfst l)
map dupfst (traverse f (a :: l)) =
traverse f (dupfst (a :: l))
    -
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
map dupfst (traverse f []) = traverse f (dupfst []) cbn.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
map dupfst (pure []) = pure [] rewrite app_pure_natural.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
pure (dupfst []) = pure [] reflexivity.
    -
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a: A
l: list A
IHl: map dupfst (traverse f l) =
traverse f (dupfst l)
map dupfst (traverse f (a :: l)) =
traverse f (dupfst (a :: l)) rewrite traverse_list_cons.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a: A
l: list A
IHl: map dupfst (traverse f l) =
traverse f (dupfst l)
map dupfst (pure cons <⋆> f a <⋆> traverse f l) =
traverse f (dupfst (a :: l))
      cbn.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a: A
l: list A
IHl: map dupfst (traverse f l) =
traverse f (dupfst l)
map dupfst (pure cons <⋆> f a <⋆> traverse f l) =
pure cons <⋆> f a <⋆>
(pure cons <⋆> f a <⋆> traverse f l)
      rewrite map_ap.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a: A
l: list A
IHl: map dupfst (traverse f l) =
traverse f (dupfst l)
map (compose dupfst) (pure cons <⋆> f a) <⋆>
traverse f l =
pure cons <⋆> f a <⋆>
(pure cons <⋆> f a <⋆> traverse f l)
      rewrite map_ap.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a: A
l: list A
IHl: map dupfst (traverse f l) =
traverse f (dupfst l)
map (compose (compose dupfst)) (pure cons) <⋆> f a <⋆>
traverse f l =
pure cons <⋆> f a <⋆>
(pure cons <⋆> f a <⋆> traverse f l)
      rewrite app_pure_natural.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a: A
l: list A
IHl: map dupfst (traverse f l) =
traverse f (dupfst l)
pure (compose dupfst ∘ cons) <⋆> f a <⋆> traverse f l =
pure cons <⋆> f a <⋆>
(pure cons <⋆> f a <⋆> traverse f l)
      rewrite <- ap4.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a: A
l: list A
IHl: map dupfst (traverse f l) =
traverse f (dupfst l)
pure (compose dupfst ∘ cons) <⋆> f a <⋆> traverse f l =
pure compose <⋆> (pure cons <⋆> f a) <⋆>
(pure cons <⋆> f a) <⋆> traverse f l
      rewrite (ap_ci_swap (f := pure (@cons B)) (a := f a)) at 2.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a: A
l: list A
IHl: map dupfst (traverse f l) =
traverse f (dupfst l)
pure (compose dupfst ∘ cons) <⋆> f a <⋆> traverse f l =
pure compose <⋆> (pure cons <⋆> f a) <⋆>
(map evalAt (f a) <⋆> pure cons) <⋆> traverse f l
      rewrite <- ap4.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a: A
l: list A
IHl: map dupfst (traverse f l) =
traverse f (dupfst l)
pure (compose dupfst ∘ cons) <⋆> f a <⋆> traverse f l =
pure compose <⋆>
(pure compose <⋆> (pure cons <⋆> f a)) <⋆>
map evalAt (f a) <⋆> pure cons <⋆> traverse f l
      rewrite <- ap4.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a: A
l: list A
IHl: map dupfst (traverse f l) =
traverse f (dupfst l)
pure (compose dupfst ∘ cons) <⋆> f a <⋆> traverse f l =
pure compose <⋆> pure compose <⋆> pure compose <⋆>
(pure cons <⋆> f a) <⋆> map evalAt (f a) <⋆> pure cons <⋆>
traverse f l
      rewrite <- ap4.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a: A
l: list A
IHl: map dupfst (traverse f l) =
traverse f (dupfst l)
pure (compose dupfst ∘ cons) <⋆> f a <⋆> traverse f l =
pure compose <⋆>
(pure compose <⋆> pure compose <⋆> pure compose) <⋆>
pure cons <⋆> f a <⋆> map evalAt (f a) <⋆> pure cons <⋆>
traverse f l
      rewrite <- ap4.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a: A
l: list A
IHl: map dupfst (traverse f l) =
traverse f (dupfst l)
pure (compose dupfst ∘ cons) <⋆> f a <⋆> traverse f l =
pure compose <⋆> pure compose <⋆>
(pure compose <⋆> pure compose) <⋆> pure compose <⋆>
pure cons <⋆> f a <⋆> map evalAt (f a) <⋆> pure cons <⋆>
traverse f l
      rewrite <- ap4.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a: A
l: list A
IHl: map dupfst (traverse f l) =
traverse f (dupfst l)
pure (compose dupfst ∘ cons) <⋆> f a <⋆> traverse f l =
pure compose <⋆> (pure compose <⋆> pure compose) <⋆>
pure compose <⋆> pure compose <⋆> pure compose <⋆>
pure cons <⋆> f a <⋆> map evalAt (f a) <⋆> pure cons <⋆>
traverse f l
      rewrite <- ap4.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a: A
l: list A
IHl: map dupfst (traverse f l) =
traverse f (dupfst l)
pure (compose dupfst ∘ cons) <⋆> f a <⋆> traverse f l =
pure compose <⋆> pure compose <⋆> pure compose <⋆>
pure compose <⋆> pure compose <⋆> pure compose <⋆>
pure compose <⋆> pure cons <⋆> f a <⋆>
map evalAt (f a) <⋆> pure cons <⋆> traverse f l
      repeat rewrite ap2.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a: A
l: list A
IHl: map dupfst (traverse f l) =
traverse f (dupfst l)
pure (compose dupfst ∘ cons) <⋆> f a <⋆> traverse f l =
pure
  ((compose ∘ compose) compose compose compose compose
     cons) <⋆> f a <⋆> map evalAt (f a) <⋆> pure cons <⋆>
traverse f l
      rewrite <- ap_map.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a: A
l: list A
IHl: map dupfst (traverse f l) =
traverse f (dupfst l)
pure (compose dupfst ∘ cons) <⋆> f a <⋆> traverse f l =
map (precompose evalAt)
  (pure
     ((compose ∘ compose) compose compose compose
        compose cons) <⋆> f a) <⋆> f a <⋆> pure cons <⋆>
traverse f l
      rewrite map_ap.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a: A
l: list A
IHl: map dupfst (traverse f l) =
traverse f (dupfst l)
pure (compose dupfst ∘ cons) <⋆> f a <⋆> traverse f l =
map (compose (precompose evalAt))
  (pure
     ((compose ∘ compose) compose compose compose
        compose cons)) <⋆> f a <⋆> f a <⋆> pure cons <⋆>
traverse f l
      rewrite app_pure_natural.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a: A
l: list A
IHl: map dupfst (traverse f l) =
traverse f (dupfst l)
pure (compose dupfst ∘ cons) <⋆> f a <⋆> traverse f l =
pure
  (precompose evalAt
   ∘ (compose ∘ compose) compose compose compose
       compose cons) <⋆> f a <⋆> f a <⋆> pure cons <⋆>
traverse f l
      rewrite ap_ci_contract.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a: A
l: list A
IHl: map dupfst (traverse f l) =
traverse f (dupfst l)
pure (compose dupfst ∘ cons) <⋆> f a <⋆> traverse f l =
map double_input
  (pure
     (precompose evalAt
      ∘ (compose ∘ compose) compose compose compose
          compose cons)) <⋆> f a <⋆> pure cons <⋆>
traverse f l
      rewrite app_pure_natural.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a: A
l: list A
IHl: map dupfst (traverse f l) =
traverse f (dupfst l)
pure (compose dupfst ∘ cons) <⋆> f a <⋆> traverse f l =
pure
  (double_input
     (precompose evalAt
      ∘ (compose ∘ compose) compose compose compose
          compose cons)) <⋆> f a <⋆> pure cons <⋆>
traverse f l
      rewrite ap3.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a: A
l: list A
IHl: map dupfst (traverse f l) =
traverse f (dupfst l)
pure (compose dupfst ∘ cons) <⋆> f a <⋆> traverse f l =
pure (evalAt cons) <⋆>
(pure
   (double_input
      (precompose evalAt
       ∘ (compose ∘ compose) compose compose compose
           compose cons)) <⋆> f a) <⋆> traverse f l
      rewrite <- ap4.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a: A
l: list A
IHl: map dupfst (traverse f l) =
traverse f (dupfst l)
pure (compose dupfst ∘ cons) <⋆> f a <⋆> traverse f l =
pure compose <⋆> pure (evalAt cons) <⋆>
pure
  (double_input
     (precompose evalAt
      ∘ (compose ∘ compose) compose compose compose
          compose cons)) <⋆> f a <⋆> traverse f l
      rewrite ap2.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a: A
l: list A
IHl: map dupfst (traverse f l) =
traverse f (dupfst l)
pure (compose dupfst ∘ cons) <⋆> f a <⋆> traverse f l =
pure (compose (evalAt cons)) <⋆>
pure
  (double_input
     (precompose evalAt
      ∘ (compose ∘ compose) compose compose compose
          compose cons)) <⋆> f a <⋆> traverse f l
      rewrite ap2.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a: A
l: list A
IHl: map dupfst (traverse f l) =
traverse f (dupfst l)
pure (compose dupfst ∘ cons) <⋆> f a <⋆> traverse f l =
pure
  (evalAt cons
   ∘ double_input
       (precompose evalAt
        ∘ (compose ∘ compose) compose compose compose
            compose cons)) <⋆> f a <⋆> traverse f l
      reflexivity.
  Qed.

  (** ** "Pair All with First Element" *)
  (********************************************************************)
  Definition pairall {A:Type} (l: list A): list (A * A) :=
    match l with
    | nil => nil
    | cons a l' =>  cons (a, a) (map (pair a) l')
    end.

  Lemma pairall_spec {A} (a: A) (l: list A):
    pairall (a :: l) = map (pair a) (a :: l).
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A: Type
a: A
l: list A
pairall (a :: l) = map (pair a) (a :: l)
  Proof.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A: Type
a: A
l: list A
pairall (a :: l) = map (pair a) (a :: l)
    cbn.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A: Type
a: A
l: list A
(a, a) :: map (pair a) l = (a, a) :: map (pair a) l reflexivity.
  Qed.

  Lemma pairall_cons_pf {A:Type}:
    (compose pairall ∘ (@cons A)) =
      (uncurry compose ∘ map_snd cons ∘
         map_fst (fun a => map (F := list) (pair a)) ∘ (@dup A)).
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A: Type
compose pairall ∘ cons =
uncurry compose ∘ map_snd cons ∘ map_fst (map ○ pair)
∘ dup
  Proof.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A: Type
compose pairall ∘ cons =
uncurry compose ∘ map_snd cons ∘ map_fst (map ○ pair)
∘ dup
    reflexivity.
  Qed.

  (*

    Lemma pairall_commute_cons_simpler {A B: Type}
    (f: A -> G B) (a: A) (x: A) (l: list A):
    map (map ∘ pair) (f a) <⋆>
traverse f l = traverse (traverse f) (map (pair a) l) ->
    map (map ∘ pair) (f a) <⋆>
 traverse f (x :: l) = traverse (traverse f) (map (pair a) (x :: l)).
    Proof.
    introv IH.
    (* RHS *)
    rewrite map_list_cons.
    rewrite (traverse_list_cons _ _ _ _ (a, x)).
    rewrite traverse_Diagonal_rw.
    rewrite <- IH.
    clear IH.
    (* LHS *)
    rewrite traverse_list_cons.
    rewrite <- ap4.
    rewrite <- ap4.
    rewrite <- ap4.
    rewrite ap2.
    rewrite ap2.
    rewrite ap3.
    rewrite <- ap4.
    rewrite ap2.
    rewrite ap2.
    rewrite <- map_to_ap.
    compose near (f a) on left.
    rewrite (fun_map_map).
    rewrite <- ap4.
    rewrite <- ap4.
    rewrite <- ap4.
    do 8 rewrite <- ap4.
    repeat rewrite ap2.
    rewrite <- map_to_ap.
    rewrite <- ap_map.
    rewrite map_ap.
    compose near (f a) on right.
    compose near (f a) on right.
    rewrite (fun_map_map).
    unfold compose at 7.
    rewrite (ap_ci2 _ _ (f a)).
    compose near (f a) on right.
    compose near (f a) on right.
    rewrite (fun_map_map).
    unfold compose at 7.
    rewrite map_to_ap.
    rewrite map_to_ap.
    rewrite ap_cidup.
    rewrite <- map_to_ap.
    rewrite app_pure_natural.
    rewrite <- map_to_ap.
    fequal.
    Qed.

    Lemma pairall_commute_cons {A B: Type}
    (f: A -> G B) (a: A) (l: list A):
    l <> nil ->
    map (F := G) (map (F := list) ∘ pair) (f a)
    <⋆> (traverse (T := list) f l) =
    traverse (traverse (T := fun A => A * A) f) (map (pair a) l).
    Proof.
    introv Hnotnil.
    induction l as [| x xs IHxs ].
    - contradiction.
    - destruct xs.
    + cbn.
    rewrite map_to_ap.
    rewrite <- ap4.
    rewrite <- ap4.
    rewrite <- ap4.
    rewrite <- ap4.
    rewrite ap2.
    rewrite ap2.
    rewrite ap2.
    rewrite ap2.
    rewrite ap3.
    rewrite <- ap4.
    rewrite ap2.
    rewrite <- ap4.
    rewrite ap2.
    rewrite <- ap4.
    rewrite ap2.
    rewrite ap2.
    rewrite ap3.
    rewrite <- ap4.
    rewrite ap2.
    rewrite ap2.
    rewrite ap3.
    rewrite <- ap4.
    rewrite ap2.
    rewrite ap2.
    rewrite <- ap4.
    rewrite ap2.
    rewrite <- ap4.
    rewrite ap2.
    rewrite ap2.
    fequal.
    + specialize (IHxs ltac:(easy)).
    remember (a0 :: xs).
    apply pairall_commute_cons_simpler.
    assumption.
    Qed.
   *)

  Lemma pairall_commute_cons_Inductive_Step {A B: Type}
    (f: A -> G B) (a: A) (x: A) (l: list A):
    traverse (traverse f) (map (pair a) l) =
      map (map ∘ pair) (f a) <⋆> traverse f l ->
    traverse (traverse f) (map (pair a) (x :: l)) =
      map (map ∘ pair) (f a) <⋆> traverse f (x :: l).
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a, x: A
l: list A
traverse (traverse f) (map (pair a) l) =
map (map ∘ pair) (f a) <⋆> traverse f l ->
traverse (traverse f) (map (pair a) (x :: l)) =
map (map ∘ pair) (f a) <⋆> traverse f (x :: l)
  Proof.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a, x: A
l: list A
traverse (traverse f) (map (pair a) l) =
map (map ∘ pair) (f a) <⋆> traverse f l ->
traverse (traverse f) (map (pair a) (x :: l)) =
map (map ∘ pair) (f a) <⋆> traverse f (x :: l)
    introv IH.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a, x: A
l: list A
IH: traverse (traverse f) (map (pair a) l) =
map (map ∘ pair) (f a) <⋆> traverse f l
traverse (traverse f) (map (pair a) (x :: l)) =
map (map ∘ pair) (f a) <⋆> traverse f (x :: l)
    (* LHS *)
    rewrite map_list_cons.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a, x: A
l: list A
IH: traverse (traverse f) (map (pair a) l) =
map (map ∘ pair) (f a) <⋆> traverse f l
traverse (traverse f) ((a, x) :: map (pair a) l) =
map (map ∘ pair) (f a) <⋆> traverse f (x :: l)
    rewrite (traverse_list_cons _ _ _ _ (a, x)).
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a, x: A
l: list A
IH: traverse (traverse f) (map (pair a) l) =
map (map ∘ pair) (f a) <⋆> traverse f l
pure cons <⋆> traverse f (a, x) <⋆>
traverse (traverse f) (map (pair a) l) =
map (map ∘ pair) (f a) <⋆> traverse f (x :: l)
    rewrite IH.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a, x: A
l: list A
IH: traverse (traverse f) (map (pair a) l) =
map (map ∘ pair) (f a) <⋆> traverse f l
pure cons <⋆> traverse f (a, x) <⋆>
(map (map ∘ pair) (f a) <⋆> traverse f l) =
map (map ∘ pair) (f a) <⋆> traverse f (x :: l)
    clear IH.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a, x: A
l: list A
pure cons <⋆> traverse f (a, x) <⋆>
(map (map ∘ pair) (f a) <⋆> traverse f l) =
map (map ∘ pair) (f a) <⋆> traverse f (x :: l)
    rewrite <- ap4.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a, x: A
l: list A
pure compose <⋆> (pure cons <⋆> traverse f (a, x)) <⋆>
map (map ∘ pair) (f a) <⋆> traverse f l =
map (map ∘ pair) (f a) <⋆> traverse f (x :: l)
    rewrite <- ap4.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a, x: A
l: list A
pure compose <⋆> pure compose <⋆> pure cons <⋆>
traverse f (a, x) <⋆> map (map ∘ pair) (f a) <⋆>
traverse f l =
map (map ∘ pair) (f a) <⋆> traverse f (x :: l)
    rewrite ap2.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a, x: A
l: list A
pure (compose compose) <⋆> pure cons <⋆>
traverse f (a, x) <⋆> map (map ∘ pair) (f a) <⋆>
traverse f l =
map (map ∘ pair) (f a) <⋆> traverse f (x :: l)
    rewrite ap2.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a, x: A
l: list A
pure (compose ∘ cons) <⋆> traverse f (a, x) <⋆>
map (map ∘ pair) (f a) <⋆> traverse f l =
map (map ∘ pair) (f a) <⋆> traverse f (x :: l)
    rewrite traverse_Diagonal_rw.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a, x: A
l: list A
pure (compose ∘ cons) <⋆> (pure pair <⋆> f a <⋆> f x) <⋆>
map (map ∘ pair) (f a) <⋆> traverse f l =
map (map ∘ pair) (f a) <⋆> traverse f (x :: l)
    rewrite <- ap4.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a, x: A
l: list A
pure compose <⋆> pure (compose ∘ cons) <⋆>
(pure pair <⋆> f a) <⋆> f x <⋆> map (map ∘ pair) (f a) <⋆>
traverse f l =
map (map ∘ pair) (f a) <⋆> traverse f (x :: l)
    rewrite ap2.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a, x: A
l: list A
pure (compose (compose ∘ cons)) <⋆>
(pure pair <⋆> f a) <⋆> f x <⋆> map (map ∘ pair) (f a) <⋆>
traverse f l =
map (map ∘ pair) (f a) <⋆> traverse f (x :: l)
    rewrite <- ap4.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a, x: A
l: list A
pure compose <⋆> pure (compose (compose ∘ cons)) <⋆>
pure pair <⋆> f a <⋆> f x <⋆> map (map ∘ pair) (f a) <⋆>
traverse f l =
map (map ∘ pair) (f a) <⋆> traverse f (x :: l)
    rewrite ap2.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a, x: A
l: list A
pure (compose (compose (compose ∘ cons))) <⋆>
pure pair <⋆> f a <⋆> f x <⋆> map (map ∘ pair) (f a) <⋆>
traverse f l =
map (map ∘ pair) (f a) <⋆> traverse f (x :: l)
    rewrite ap2.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a, x: A
l: list A
pure (compose (compose ∘ cons) ∘ pair) <⋆> f a <⋆> f x <⋆>
map (map ∘ pair) (f a) <⋆> traverse f l =
map (map ∘ pair) (f a) <⋆> traverse f (x :: l)

    rewrite <- ap_map.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a, x: A
l: list A
map (precompose (map ∘ pair))
  (pure (compose (compose ∘ cons) ∘ pair) <⋆> f a <⋆>
   f x) <⋆> f a <⋆> traverse f l =
map (map ∘ pair) (f a) <⋆> traverse f (x :: l)
    rewrite map_ap.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a, x: A
l: list A
map (compose (precompose (map ∘ pair)))
  (pure (compose (compose ∘ cons) ∘ pair) <⋆> f a) <⋆>
f x <⋆> f a <⋆> traverse f l =
map (map ∘ pair) (f a) <⋆> traverse f (x :: l)
    rewrite map_ap.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a, x: A
l: list A
map (compose (compose (precompose (map ∘ pair))))
  (pure (compose (compose ∘ cons) ∘ pair)) <⋆> f a <⋆>
f x <⋆> f a <⋆> traverse f l =
map (map ∘ pair) (f a) <⋆> traverse f (x :: l)
    rewrite app_pure_natural.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a, x: A
l: list A
pure
  (compose (precompose (map ∘ pair))
   ∘ (compose (compose ∘ cons) ∘ pair)) <⋆> f a <⋆>
f x <⋆> f a <⋆> traverse f l =
map (map ∘ pair) (f a) <⋆> traverse f (x :: l)
    reassociate <- near (compose (precompose (map ∘ pair))).
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a, x: A
l: list A
pure
  (compose (precompose (map ∘ pair))
   ∘ compose (compose ∘ cons) ∘ pair) <⋆> f a <⋆> 
f x <⋆> f a <⋆> traverse f l =
map (map ∘ pair) (f a) <⋆> traverse f (x :: l)
    rewrite compose_compose.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a, x: A
l: list A
pure
  (compose
     (precompose (map ∘ pair) ∘ (compose ∘ cons))
   ∘ pair) <⋆> f a <⋆> f x <⋆> f a <⋆> traverse f l =
map (map ∘ pair) (f a) <⋆> traverse f (x :: l)
    reassociate <- near (precompose (map ∘ pair)).
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a, x: A
l: list A
pure
  (compose (precompose (map ∘ pair) ∘ compose ∘ cons)
   ∘ pair) <⋆> f a <⋆> f x <⋆> f a <⋆> traverse f l =
map (map ∘ pair) (f a) <⋆> traverse f (x :: l)

    rewrite (ap_ci_flip _ (f a) (f x)).
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a, x: A
l: list A
map flip
  (pure
     (compose
        (precompose (map ∘ pair) ∘ compose ∘ cons)
      ∘ pair)) <⋆> f x <⋆> f a <⋆> f a <⋆>
traverse f l =
map (map ∘ pair) (f a) <⋆> traverse f (x :: l)
    rewrite app_pure_natural.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a, x: A
l: list A
pure
  (flip
     (compose
        (precompose (map ∘ pair) ∘ compose ∘ cons)
      ∘ pair)) <⋆> f x <⋆> f a <⋆> f a <⋆>
traverse f l =
map (map ∘ pair) (f a) <⋆> traverse f (x :: l)

    rewrite ap_ci_contract.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a, x: A
l: list A
map double_input
  (pure
     (flip
        (compose
           (precompose (map ∘ pair) ∘ compose ∘ cons)
         ∘ pair)) <⋆> f x) <⋆> f a <⋆> traverse f l =
map (map ∘ pair) (f a) <⋆> traverse f (x :: l)
    rewrite map_ap.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a, x: A
l: list A
map (compose double_input)
  (pure
     (flip
        (compose
           (precompose (map ∘ pair) ∘ compose ∘ cons)
         ∘ pair))) <⋆> f x <⋆> f a <⋆> traverse f l =
map (map ∘ pair) (f a) <⋆> traverse f (x :: l)
    rewrite app_pure_natural.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a, x: A
l: list A
pure
  (double_input
   ∘ flip
       (compose
          (precompose (map ∘ pair) ∘ compose ∘ cons)
        ∘ pair)) <⋆> f x <⋆> f a <⋆> traverse f l =
map (map ∘ pair) (f a) <⋆> traverse f (x :: l)

    rewrite (ap_ci_flip _ (f x) (f a)).
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a, x: A
l: list A
map flip
  (pure
     (double_input
      ∘ flip
          (compose
             (precompose (map ∘ pair) ∘ compose ∘ cons)
           ∘ pair))) <⋆> f a <⋆> f x <⋆> traverse f l =
map (map ∘ pair) (f a) <⋆> traverse f (x :: l)
    rewrite app_pure_natural.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a, x: A
l: list A
pure
  (flip
     (double_input
      ∘ flip
          (compose
             (precompose (map ∘ pair) ∘ compose ∘ cons)
           ∘ pair))) <⋆> f a <⋆> f x <⋆> traverse f l =
map (map ∘ pair) (f a) <⋆> traverse f (x :: l)

    (* RHS *)
    rewrite (traverse_list_cons _ _ _ _ x).
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a, x: A
l: list A
pure
  (flip
     (double_input
      ∘ flip
          (compose
             (precompose (map ∘ pair) ∘ compose ∘ cons)
           ∘ pair))) <⋆> f a <⋆> f x <⋆> traverse f l =
map (map ∘ pair) (f a) <⋆>
(pure cons <⋆> f x <⋆> traverse f l)
    rewrite <- (ap4 (map (map ∘ pair) (f a)) _ (traverse f l)).
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a, x: A
l: list A
pure
  (flip
     (double_input
      ∘ flip
          (compose
             (precompose (map ∘ pair) ∘ compose ∘ cons)
           ∘ pair))) <⋆> f a <⋆> f x <⋆> traverse f l =
pure compose <⋆> map (map ∘ pair) (f a) <⋆>
(pure cons <⋆> f x) <⋆> traverse f l
    rewrite pure_ap_map.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a, x: A
l: list A
pure
  (flip
     (double_input
      ∘ flip
          (compose
             (precompose (map ∘ pair) ∘ compose ∘ cons)
           ∘ pair))) <⋆> f a <⋆> f x <⋆> traverse f l =
map (compose ∘ (map ∘ pair)) (f a) <⋆>
(pure cons <⋆> f x) <⋆> traverse f l
    rewrite <- (ap4 _ (pure cons) (f x)).
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a, x: A
l: list A
pure
  (flip
     (double_input
      ∘ flip
          (compose
             (precompose (map ∘ pair) ∘ compose ∘ cons)
           ∘ pair))) <⋆> f a <⋆> f x <⋆> traverse f l =
pure compose <⋆> map (compose ∘ (map ∘ pair)) (f a) <⋆>
pure cons <⋆> f x <⋆> traverse f l
    rewrite pure_ap_map.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a, x: A
l: list A
pure
  (flip
     (double_input
      ∘ flip
          (compose
             (precompose (map ∘ pair) ∘ compose ∘ cons)
           ∘ pair))) <⋆> f a <⋆> f x <⋆> traverse f l =
map (compose ∘ (compose ∘ (map ∘ pair))) (f a) <⋆>
pure cons <⋆> f x <⋆> traverse f l
    rewrite ap3.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a, x: A
l: list A
pure
  (flip
     (double_input
      ∘ flip
          (compose
             (precompose (map ∘ pair) ∘ compose ∘ cons)
           ∘ pair))) <⋆> f a <⋆> f x <⋆> traverse f l =
pure (evalAt cons) <⋆>
map (compose ∘ (compose ∘ (map ∘ pair))) (f a) <⋆> 
f x <⋆> traverse f l
    rewrite pure_ap_map.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a, x: A
l: list A
pure
  (flip
     (double_input
      ∘ flip
          (compose
             (precompose (map ∘ pair) ∘ compose ∘ cons)
           ∘ pair))) <⋆> f a <⋆> f x <⋆> traverse f l =
map
  (evalAt cons ∘ (compose ∘ (compose ∘ (map ∘ pair))))
  (f a) <⋆> f x <⋆> traverse f l

    (* Done ! *)
    rewrite map_to_ap.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a, x: A
l: list A
pure
  (flip
     (double_input
      ∘ flip
          (compose
             (precompose (map ∘ pair) ∘ compose ∘ cons)
           ∘ pair))) <⋆> f a <⋆> f x <⋆> traverse f l =
pure
  (evalAt cons ∘ (compose ∘ (compose ∘ (map ∘ pair)))) <⋆>
f a <⋆> f x <⋆> traverse f l
    reflexivity.
  Qed.

  Lemma pairall_commute_cons {A B: Type}
    (f: A -> G B) (a: A) (l: list A):
    l <> nil ->
    traverse (traverse (T := fun A => A * A) f) (map (pair a) l) =
      map (F := G) (map (F := list) ∘ pair) (f a) <⋆>
        (traverse (T := list) f l).
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a: A
l: list A
l <> [] ->
traverse (traverse f) (map (pair a) l) =
map (map ∘ pair) (f a) <⋆> traverse f l
  Proof.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a: A
l: list A
l <> [] ->
traverse (traverse f) (map (pair a) l) =
map (map ∘ pair) (f a) <⋆> traverse f l
    introv Hnotnil.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a: A
l: list A
Hnotnil: l <> []
traverse (traverse f) (map (pair a) l) =
map (map ∘ pair) (f a) <⋆> traverse f l
    induction l as [| x xs IHxs ].
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a: A
Hnotnil: [] <> []
traverse (traverse f) (map (pair a) []) =
map (map ∘ pair) (f a) <⋆> traverse f []
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a, x: A
xs: list A
Hnotnil: x :: xs <> []
IHxs: xs <> [] ->
traverse (traverse f) (map (pair a) xs) =
map (map ∘ pair) (f a) <⋆> traverse f xs
traverse (traverse f) (map (pair a) (x :: xs)) =
map (map ∘ pair) (f a) <⋆> traverse f (x :: xs)
    -
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a: A
Hnotnil: [] <> []
traverse (traverse f) (map (pair a) []) =
map (map ∘ pair) (f a) <⋆> traverse f [] contradiction.
    -
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a, x: A
xs: list A
Hnotnil: x :: xs <> []
IHxs: xs <> [] ->
traverse (traverse f) (map (pair a) xs) =
map (map ∘ pair) (f a) <⋆> traverse f xs
traverse (traverse f) (map (pair a) (x :: xs)) =
map (map ∘ pair) (f a) <⋆> traverse f (x :: xs) clear Hnotnil.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a, x: A
xs: list A
IHxs: xs <> [] ->
traverse (traverse f) (map (pair a) xs) =
map (map ∘ pair) (f a) <⋆> traverse f xs
traverse (traverse f) (map (pair a) (x :: xs)) =
map (map ∘ pair) (f a) <⋆> traverse f (x :: xs)
      destruct xs as [| y ys ].
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a, x: A
IHxs: [] <> [] ->
traverse (traverse f) (map (pair a) []) =
map (map ∘ pair) (f a) <⋆> traverse f []
traverse (traverse f) (map (pair a) [x]) =
map (map ∘ pair) (f a) <⋆> traverse f [x]
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a, x, y: A
ys: list A
IHxs: y :: ys <> [] ->
traverse (traverse f) (map (pair a) (y :: ys)) =
map (map ∘ pair) (f a) <⋆> traverse f (y :: ys)
traverse (traverse f) (map (pair a) (x :: y :: ys)) =
map (map ∘ pair) (f a) <⋆> traverse f (x :: y :: ys)
      +
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a, x: A
IHxs: [] <> [] ->
traverse (traverse f) (map (pair a) []) =
map (map ∘ pair) (f a) <⋆> traverse f []
traverse (traverse f) (map (pair a) [x]) =
map (map ∘ pair) (f a) <⋆> traverse f [x] clear IHxs.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a, x: A
traverse (traverse f) (map (pair a) [x]) =
map (map ∘ pair) (f a) <⋆> traverse f [x]
        (* LHS *)
        rewrite map_list_one.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a, x: A
traverse (traverse f) [(a, x)] =
map (map ∘ pair) (f a) <⋆> traverse f [x]
        change ([(a, x)]) with (ret (a, x)).
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a, x: A
traverse (traverse f) (ret (a, x)) =
map (map ∘ pair) (f a) <⋆> traverse f [x]
        rewrite (traverse_list_one G).
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a, x: A
map ret (traverse f (a, x)) =
map (map ∘ pair) (f a) <⋆> traverse f [x]
        rewrite traverse_Diagonal_rw.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a, x: A
map ret (pure pair <⋆> f a <⋆> f x) =
map (map ∘ pair) (f a) <⋆> traverse f [x]
        rewrite map_ap.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a, x: A
map (compose ret) (pure pair <⋆> f a) <⋆> f x =
map (map ∘ pair) (f a) <⋆> traverse f [x]
        rewrite map_ap.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a, x: A
map (compose (compose ret)) (pure pair) <⋆> f a <⋆>
f x = map (map ∘ pair) (f a) <⋆> traverse f [x]
        rewrite app_pure_natural.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a, x: A
pure (compose ret ∘ pair) <⋆> f a <⋆> f x =
map (map ∘ pair) (f a) <⋆> traverse f [x]

        (* RHS *)
        change ([x]) with (ret x) at 1.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a, x: A
pure (compose ret ∘ pair) <⋆> f a <⋆> f x =
map (map ∘ pair) (f a) <⋆> traverse f (ret x)
        rewrite (traverse_list_one G).
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a, x: A
pure (compose ret ∘ pair) <⋆> f a <⋆> f x =
map (map ∘ pair) (f a) <⋆> map ret (f x)

        rewrite (map_to_ap (G := G)).
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a, x: A
pure (compose ret ∘ pair) <⋆> f a <⋆> f x =
pure (map ∘ pair) <⋆> f a <⋆> map ret (f x)
        rewrite (map_to_ap (G := G)).
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a, x: A
pure (compose ret ∘ pair) <⋆> f a <⋆> f x =
pure (map ∘ pair) <⋆> f a <⋆> (pure ret <⋆> f x)

        rewrite <- ap4.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a, x: A
pure (compose ret ∘ pair) <⋆> f a <⋆> f x =
pure compose <⋆> (pure (map ∘ pair) <⋆> f a) <⋆>
pure ret <⋆> f x
        rewrite <- ap4.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a, x: A
pure (compose ret ∘ pair) <⋆> f a <⋆> f x =
pure compose <⋆> pure compose <⋆> pure (map ∘ pair) <⋆>
f a <⋆> pure ret <⋆> f x
        rewrite ap2.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a, x: A
pure (compose ret ∘ pair) <⋆> f a <⋆> f x =
pure (compose compose) <⋆> pure (map ∘ pair) <⋆> f a <⋆>
pure ret <⋆> f x
        rewrite ap2.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a, x: A
pure (compose ret ∘ pair) <⋆> f a <⋆> f x =
pure (compose ∘ (map ∘ pair)) <⋆> f a <⋆> pure ret <⋆>
f x

        rewrite ap3.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a, x: A
pure (compose ret ∘ pair) <⋆> f a <⋆> f x =
pure (evalAt ret) <⋆>
(pure (compose ∘ (map ∘ pair)) <⋆> f a) <⋆> f x
        rewrite <- ap4.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a, x: A
pure (compose ret ∘ pair) <⋆> f a <⋆> f x =
pure compose <⋆> pure (evalAt ret) <⋆>
pure (compose ∘ (map ∘ pair)) <⋆> f a <⋆> f x
        rewrite ap2.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a, x: A
pure (compose ret ∘ pair) <⋆> f a <⋆> f x =
pure (compose (evalAt ret)) <⋆>
pure (compose ∘ (map ∘ pair)) <⋆> f a <⋆> f x
        rewrite ap2.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a, x: A
pure (compose ret ∘ pair) <⋆> f a <⋆> f x =
pure (evalAt ret ∘ (compose ∘ (map ∘ pair))) <⋆> f a <⋆>
f x

        (* Done! *)
        reflexivity.

      +
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a, x, y: A
ys: list A
IHxs: y :: ys <> [] ->
traverse (traverse f) (map (pair a) (y :: ys)) =
map (map ∘ pair) (f a) <⋆> traverse f (y :: ys)
traverse (traverse f) (map (pair a) (x :: y :: ys)) =
map (map ∘ pair) (f a) <⋆> traverse f (x :: y :: ys) specialize (IHxs ltac:(discriminate)).
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a, x, y: A
ys: list A
IHxs: traverse (traverse f) (map (pair a) (y :: ys)) =
map (map ∘ pair) (f a) <⋆> traverse f (y :: ys)
traverse (traverse f) (map (pair a) (x :: y :: ys)) =
map (map ∘ pair) (f a) <⋆> traverse f (x :: y :: ys)
        remember (y :: ys) as rest.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a, x, y: A
ys, rest: list A
Heqrest: rest = y :: ys
IHxs: traverse (traverse f) (map (pair a) rest) =
map (map ∘ pair) (f a) <⋆> traverse f rest
traverse (traverse f) (map (pair a) (x :: rest)) =
map (map ∘ pair) (f a) <⋆> traverse f (x :: rest)
        apply pairall_commute_cons_Inductive_Step.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a, x, y: A
ys, rest: list A
Heqrest: rest = y :: ys
IHxs: traverse (traverse f) (map (pair a) rest) =
map (map ∘ pair) (f a) <⋆> traverse f rest
traverse (traverse f) (map (pair a) rest) =
map (map ∘ pair) (f a) <⋆> traverse f rest
        assumption.
  Qed.

  Lemma pairall_commute {A B: Type}
    (f: A  -> G B) (l: list A):
    map (F := G) pairall (traverse f l) =
      traverse (traverse (T := fun A => A * A) f) (pairall l).
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
l: list A
map pairall (traverse f l) =
traverse (traverse f) (pairall l)
  Proof.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
l: list A
map pairall (traverse f l) =
traverse (traverse f) (pairall l)
    destruct l as [| a as'].
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
map pairall (traverse f []) =
traverse (traverse f) (pairall [])
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a: A
as': list A
map pairall (traverse f (a :: as')) =
traverse (traverse f) (pairall (a :: as'))
    -
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
map pairall (traverse f []) =
traverse (traverse f) (pairall []) cbn.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
map pairall (pure []) = pure []
      rewrite app_pure_natural.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
pure (pairall []) = pure []
      reflexivity.
    - (* LHS *)
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a: A
as': list A
map pairall (traverse f (a :: as')) =
traverse (traverse f) (pairall (a :: as'))
      rewrite traverse_list_cons.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a: A
as': list A
map pairall (pure cons <⋆> f a <⋆> traverse f as') =
traverse (traverse f) (pairall (a :: as'))
      rewrite map_ap.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a: A
as': list A
map (compose pairall) (pure cons <⋆> f a) <⋆>
traverse f as' =
traverse (traverse f) (pairall (a :: as'))
      rewrite map_ap.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a: A
as': list A
map (compose (compose pairall)) (pure cons) <⋆> f a <⋆>
traverse f as' =
traverse (traverse f) (pairall (a :: as'))
      rewrite app_pure_natural.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a: A
as': list A
pure (compose pairall ∘ cons) <⋆> f a <⋆>
traverse f as' =
traverse (traverse f) (pairall (a :: as'))

      (* RHS *)
      rewrite pairall_spec.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a: A
as': list A
pure (compose pairall ∘ cons) <⋆> f a <⋆>
traverse f as' =
traverse (traverse f) (map (pair a) (a :: as'))
      rewrite pairall_commute_cons; [| discriminate].
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a: A
as': list A
pure (compose pairall ∘ cons) <⋆> f a <⋆>
traverse f as' =
map (map ∘ pair) (f a) <⋆> traverse f (a :: as')
      rewrite map_to_ap.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a: A
as': list A
pure (compose pairall ∘ cons) <⋆> f a <⋆>
traverse f as' =
pure (map ∘ pair) <⋆> f a <⋆> traverse f (a :: as')

      rewrite traverse_list_cons.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a: A
as': list A
pure (compose pairall ∘ cons) <⋆> f a <⋆>
traverse f as' =
pure (map ∘ pair) <⋆> f a <⋆>
(pure cons <⋆> f a <⋆> traverse f as')
      rewrite <- ap4.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a: A
as': list A
pure (compose pairall ∘ cons) <⋆> f a <⋆>
traverse f as' =
pure compose <⋆> (pure (map ∘ pair) <⋆> f a) <⋆>
(pure cons <⋆> f a) <⋆> traverse f as'
      rewrite <- (ap4 (pure compose) _ (f a)).
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a: A
as': list A
pure (compose pairall ∘ cons) <⋆> f a <⋆>
traverse f as' =
pure compose <⋆> pure compose <⋆> pure (map ∘ pair) <⋆>
f a <⋆> (pure cons <⋆> f a) <⋆> traverse f as'
      rewrite ap2.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a: A
as': list A
pure (compose pairall ∘ cons) <⋆> f a <⋆>
traverse f as' =
pure (compose compose) <⋆> pure (map ∘ pair) <⋆> f a <⋆>
(pure cons <⋆> f a) <⋆> traverse f as'
      rewrite ap2.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a: A
as': list A
pure (compose pairall ∘ cons) <⋆> f a <⋆>
traverse f as' =
pure (compose ∘ (map ∘ pair)) <⋆> f a <⋆>
(pure cons <⋆> f a) <⋆> traverse f as'
      rewrite <- ap4.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a: A
as': list A
pure (compose pairall ∘ cons) <⋆> f a <⋆>
traverse f as' =
pure compose <⋆>
(pure (compose ∘ (map ∘ pair)) <⋆> f a) <⋆> pure cons <⋆>
f a <⋆> traverse f as'
      rewrite <- (ap4 (pure compose) _ (f a)).
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a: A
as': list A
pure (compose pairall ∘ cons) <⋆> f a <⋆>
traverse f as' =
pure compose <⋆> pure compose <⋆>
pure (compose ∘ (map ∘ pair)) <⋆> f a <⋆> pure cons <⋆>
f a <⋆> traverse f as'
      rewrite ap2.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a: A
as': list A
pure (compose pairall ∘ cons) <⋆> f a <⋆>
traverse f as' =
pure (compose compose) <⋆>
pure (compose ∘ (map ∘ pair)) <⋆> f a <⋆> pure cons <⋆>
f a <⋆> traverse f as'
      rewrite ap2.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a: A
as': list A
pure (compose pairall ∘ cons) <⋆> f a <⋆>
traverse f as' =
pure (compose ∘ (compose ∘ (map ∘ pair))) <⋆> f a <⋆>
pure cons <⋆> f a <⋆> traverse f as'

      rewrite ap3.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a: A
as': list A
pure (compose pairall ∘ cons) <⋆> f a <⋆>
traverse f as' =
pure (evalAt cons) <⋆>
(pure (compose ∘ (compose ∘ (map ∘ pair))) <⋆> f a) <⋆>
f a <⋆> traverse f as'
      rewrite <- (ap4 (pure (evalAt cons)) _ (f a)).
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a: A
as': list A
pure (compose pairall ∘ cons) <⋆> f a <⋆>
traverse f as' =
pure compose <⋆> pure (evalAt cons) <⋆>
pure (compose ∘ (compose ∘ (map ∘ pair))) <⋆> f a <⋆>
f a <⋆> traverse f as'
      rewrite ap2.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a: A
as': list A
pure (compose pairall ∘ cons) <⋆> f a <⋆>
traverse f as' =
pure (compose (evalAt cons)) <⋆>
pure (compose ∘ (compose ∘ (map ∘ pair))) <⋆> f a <⋆>
f a <⋆> traverse f as'
      rewrite ap2.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a: A
as': list A
pure (compose pairall ∘ cons) <⋆> f a <⋆>
traverse f as' =
pure
  (evalAt cons ∘ (compose ∘ (compose ∘ (map ∘ pair)))) <⋆>
f a <⋆> f a <⋆> traverse f as'
      rewrite ap_ci_contract.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a: A
as': list A
pure (compose pairall ∘ cons) <⋆> f a <⋆>
traverse f as' =
map double_input
  (pure
     (evalAt cons
      ∘ (compose ∘ (compose ∘ (map ∘ pair))))) <⋆> 
f a <⋆> traverse f as'
      rewrite app_pure_natural.
G: Type -> Type
H: Map G
H0: Mult G
H1: Pure G
ApplicativeCommutativeIdempotent0: ApplicativeCommutativeIdempotent
  G
A, B: Type
f: A -> G B
a: A
as': list A
pure (compose pairall ∘ cons) <⋆> f a <⋆>
traverse f as' =
pure
  (double_input
     (evalAt cons
      ∘ (compose ∘ (compose ∘ (map ∘ pair))))) <⋆> 
f a <⋆> traverse f as'
      reflexivity.
  Qed.

End ci_traversable_hom_examples.