Imports and setup

Since we are using the algebraic typeclass hierarchy, we import modules under the namespaces Classes.Algebraic and Theory.Algebraic.

From Tealeaves Require Export
  Classes.Categorical.DecoratedTraversableMonad
  Classes.Monoid
  Functors.Writer
  Misc.NaturalNumbers.

Import Categorical.TraversableFunctor.Notations.
Import List.ListNotations.
Import Strength.Notations.
Import Monoid.Notations.

#[local] Generalizable All Variables.
#[local] Set Implicit Arguments.

Language Definition

The first step with Tealeaves is to define the syntax of the language. We take a type base_typ of types we consider primitive (a/k/a atomic). The set of simple types is built up by forming arrows between types, starting with base types. The syntax of STLC is defined with three constructors as usual.

Parameter base_typ: Type.

Inductive typ :=
| base: base_typ -> typ
| arr: typ -> typ -> typ.

Coercion base: base_typ >-> typ.

(* we give more informative names to [Lam]'s arguments
 than Coq would infer otherwise *)
Inductive term (A: Type) :=
| Var: A -> term A
| Lam: forall (X: typ) (t: term A), term A
| Ap: term A -> term A -> term A.

Module Notations.
  Notation "'λ' X ⋅ body" :=
    (Lam X body) (at level 45): tealeaves_scope.
  Notation "[ t1 ] [ t2 ]" :=
    (Ap t1 t2) (at level 40): tealeaves_scope.
  Notation "A ⟹ B" :=
    (arr A B) (at level 40): tealeaves_scope.
End Notations.

Import Notations.

For convenience, we define an extremely rudimentary Ltac tactic that will solve the most trivial inductive steps automatically. Namely, they will attempt to solve a goal in one step by rewriting with the hypotheses in context (up to two times), then calling reflexivity.

Ltac basic t :=
  induction t;
  [ reflexivity |
    simpl; match goal with H: _ |- _ => rewrite H end; reflexivity |
    simpl; do 2 match goal with H: _ |- _ => rewrite H end; reflexivity ].

Functor instances

Plain Functor instance

Note that our datatype term is parameterized by a single type variable. The first thing we must show is that term is actually functor in this type argument.

Fixpoint map_term {A B: Type} (f: A -> B) (t: term A): term B :=
  match t with
  | Var a => Var (f a)
  | Lam X t => Lam X (map_term f t)
  | Ap t1 t2 => Ap (map_term f t1) (map_term f t2)
  end.

#[export] Instance Map_term: Map term := @map_term.

Theorem map_id: forall A, map id = @id (term A).forall A : Type, map id = id
Proof.forall A : Type, map id = id
  intros.A: Type
map id = id ext t.A: Type
t: term A
map id t = id t unfold transparent tcs.A: Type
t: term A
map_term id t = id t basic t.
Qed.

Theorem map_map: forall A B C (f: A -> B) (g: B -> C),
    map g ∘ map f = map (g ∘ f).forall (A B C : Type) (f : A -> B) (g : B -> C),
map g ∘ map f = map (g ∘ f)
Proof.forall (A B C : Type) (f : A -> B) (g : B -> C),
map g ∘ map f = map (g ∘ f)
  intros.A, B, C: Type
f: A -> B
g: B -> C
map g ∘ map f = map (g ∘ f) ext t.A, B, C: Type
f: A -> B
g: B -> C
t: term A
(map g ∘ map f) t = map (g ∘ f) t unfold transparent tcs.A, B, C: Type
f: A -> B
g: B -> C
t: term A
(map_term g ∘ map_term f) t = map_term (g ∘ f) t
  unfold compose.A, B, C: Type
f: A -> B
g: B -> C
t: term A
map_term g (map_term f t) = map_term (g ○ f) t basic t.
Qed.

#[export] Instance Functor_term: Functor term :=
  {| fun_map_id := @map_id;
     fun_map_map := @map_map;
  |}.

Rewriting rules for `map`

Section map_term_rewrite.

  Context
    `{f: A -> B}.

  Lemma map_term_ap: forall (t1 t2: term A),
      map f (@Ap A t1 t2) = @Ap B (map f t1) (map f t2).A, B: Type
f: A -> B
forall t1 t2 : term A,
map f ([t1][t2]) = [map f t1][map f t2]
  Proof.A, B: Type
f: A -> B
forall t1 t2 : term A,
map f ([t1][t2]) = [map f t1][map f t2]
    reflexivity.
  Qed.

End map_term_rewrite.

Decorated Functor instance

Fixpoint dec_term {A} (t: term A): term (nat * A) :=
  match t with
  | Var a => Var (Ƶ, a)
  | Lam τ t => Lam τ (shift term (1, dec_term t))
  | Ap t1 t2 => Ap (dec_term t1) (dec_term t2)
  end.

#[export] Instance Decorate_term: Decorate nat term := @dec_term.

Theorem dec_natural: forall A B (f: A -> B),
    map (F := term) (map f) ∘ dec term = dec term ∘ map (F := term) f.forall (A B : Type) (f : A -> B),
map (map f) ∘ dec term = dec term ∘ map f
Proof.forall (A B : Type) (f : A -> B),
map (map f) ∘ dec term = dec term ∘ map f
  intros.A, B: Type
f: A -> B
map (map f) ∘ dec term = dec term ∘ map f unfold compose.A, B: Type
f: A -> B
map (map f) ○ dec term = dec term ○ map f ext t.A, B: Type
f: A -> B
t: term A
map (map f) (dec term t) = dec term (map f t) induction t.A, B: Type
f: A -> B
a: A
map (map f) (dec term (Var a)) =
dec term (map f (Var a))
A, B: Type
f: A -> B
X: typ
t: term A
IHt: map (map f) (dec term t) = dec term (map f t)
map (map f) (dec term (λ X ⋅ t)) =
dec term (map f (λ X ⋅ t))
A, B: Type
f: A -> B
t1, t2: term A
IHt1: map (map f) (dec term t1) = dec term (map f t1)
IHt2: map (map f) (dec term t2) = dec term (map f t2)
map (map f) (dec term ([t1][t2])) =
dec term (map f ([t1][t2]))
  -A, B: Type
f: A -> B
a: A
map (map f) (dec term (Var a)) =
dec term (map f (Var a)) now cbn.
  -A, B: Type
f: A -> B
X: typ
t: term A
IHt: map (map f) (dec term t) = dec term (map f t)
map (map f) (dec term (λ X ⋅ t)) =
dec term (map f (λ X ⋅ t)) cbn -[shift].A, B: Type
f: A -> B
X: typ
t: term A
IHt: map (map f) (dec term t) = dec term (map f t)
λ X ⋅ map (map f) (shift term (1, dec term t)) =
λ X ⋅ shift term (1, dec term (map f t)) fequal.A, B: Type
f: A -> B
X: typ
t: term A
IHt: map (map f) (dec term t) = dec term (map f t)
map (map f) (shift term (1, dec term t)) =
shift term (1, dec term (map f t)) now rewrite dec_helper_1.
  -A, B: Type
f: A -> B
t1, t2: term A
IHt1: map (map f) (dec term t1) = dec term (map f t1)
IHt2: map (map f) (dec term t2) = dec term (map f t2)
map (map f) (dec term ([t1][t2])) =
dec term (map f ([t1][t2])) cbn.A, B: Type
f: A -> B
t1, t2: term A
IHt1: map (map f) (dec term t1) = dec term (map f t1)
IHt2: map (map f) (dec term t2) = dec term (map f t2)
[map (map f) (dec term t1)][map (map f) (dec term t2)] =
[dec term (map f t1)][dec term (map f t2)] now fequal.
Qed.

#[export] Instance: Natural (@dec nat term _).Natural (@dec nat term Decorate_term)
Proof.Natural (@dec nat term Decorate_term)
  constructor.Functor term
Functor (term ○ prod nat)
forall (A B : Type) (f : A -> B),
map f ∘ dec term = dec term ∘ map f
  -Functor term typeclasses eauto.
  -Functor (term ○ prod nat) apply Functor_compose;
      typeclasses eauto.
  -forall (A B : Type) (f : A -> B),
map f ∘ dec term = dec term ∘ map f apply dec_natural.
Qed.

Theorem dec_extract: forall A,
    map (F := term) (extract) ∘ dec term = @id (term A).forall A : Type, map extract ∘ dec term = id
Proof.forall A : Type, map extract ∘ dec term = id
  intros.A: Type
map extract ∘ dec term = id unfold compose.A: Type
map extract ○ dec term = id ext t.A: Type
t: term A
map extract (dec term t) = id t induction t.A: Type
a: A
map extract (dec term (Var a)) = id (Var a)
A: Type
X: typ
t: term A
IHt: map extract (dec term t) = id t
map extract (dec term (λ X ⋅ t)) = id (λ X ⋅ t)
A: Type
t1, t2: term A
IHt1: map extract (dec term t1) = id t1
IHt2: map extract (dec term t2) = id t2
map extract (dec term ([t1][t2])) = id ([t1][t2])
  -A: Type
a: A
map extract (dec term (Var a)) = id (Var a) reflexivity.
  -A: Type
X: typ
t: term A
IHt: map extract (dec term t) = id t
map extract (dec term (λ X ⋅ t)) = id (λ X ⋅ t) cbn -[shift].A: Type
X: typ
t: term A
IHt: map extract (dec term t) = id t
λ X ⋅ map extract (shift term (1, dec term t)) =
id (λ X ⋅ t) now rewrite dec_helper_2.
  -A: Type
t1, t2: term A
IHt1: map extract (dec term t1) = id t1
IHt2: map extract (dec term t2) = id t2
map extract (dec term ([t1][t2])) = id ([t1][t2]) unfold id.A: Type
t1, t2: term A
IHt1: map extract (dec term t1) = id t1
IHt2: map extract (dec term t2) = id t2
map extract (dec term ([t1][t2])) = [t1][t2] cbn.A: Type
t1, t2: term A
IHt1: map extract (dec term t1) = id t1
IHt2: map extract (dec term t2) = id t2
[map extract (dec term t1)][map extract (dec term t2)] =
[t1][t2] now fequal.
Qed.

Theorem dec_dec: forall A,
    dec term ∘ dec term = map (F := term) (cojoin) ∘ dec term (A := A).forall A : Type,
dec term ∘ dec term = map cojoin ∘ dec term
Proof.forall A : Type,
dec term ∘ dec term = map cojoin ∘ dec term
  intros.A: Type
dec term ∘ dec term = map cojoin ∘ dec term unfold compose.A: Type
dec term ○ dec term = map cojoin ○ dec term ext t.A: Type
t: term A
dec term (dec term t) = map cojoin (dec term t) induction t.A: Type
a: A
dec term (dec term (Var a)) =
map cojoin (dec term (Var a))
A: Type
X: typ
t: term A
IHt: dec term (dec term t) = map cojoin (dec term t)
dec term (dec term (λ X ⋅ t)) =
map cojoin (dec term (λ X ⋅ t))
A: Type
t1, t2: term A
IHt1: dec term (dec term t1) =
map cojoin (dec term t1)
IHt2: dec term (dec term t2) =
map cojoin (dec term t2)
dec term (dec term ([t1][t2])) =
map cojoin (dec term ([t1][t2]))
  -A: Type
a: A
dec term (dec term (Var a)) =
map cojoin (dec term (Var a)) reflexivity.
  -A: Type
X: typ
t: term A
IHt: dec term (dec term t) = map cojoin (dec term t)
dec term (dec term (λ X ⋅ t)) =
map cojoin (dec term (λ X ⋅ t)) cbn -[shift].A: Type
X: typ
t: term A
IHt: dec term (dec term t) = map cojoin (dec term t)
λ X
⋅ shift term
    (1, dec term (shift term (1, dec term t))) =
λ X ⋅ map cojoin (shift term (1, dec term t)) fequal.A: Type
X: typ
t: term A
IHt: dec term (dec term t) = map cojoin (dec term t)
shift term (1, dec term (shift term (1, dec term t))) =
map cojoin (shift term (1, dec term t)) now rewrite dec_helper_3.
  -A: Type
t1, t2: term A
IHt1: dec term (dec term t1) =
map cojoin (dec term t1)
IHt2: dec term (dec term t2) =
map cojoin (dec term t2)
dec term (dec term ([t1][t2])) =
map cojoin (dec term ([t1][t2])) cbn.A: Type
t1, t2: term A
IHt1: dec term (dec term t1) =
map cojoin (dec term t1)
IHt2: dec term (dec term t2) =
map cojoin (dec term t2)
[dec term (dec term t1)][dec term (dec term t2)] =
[map cojoin (dec term t1)][map cojoin (dec term t2)] fequal; auto.
Qed.

#[export] Instance DecoratedFunctor_term: DecoratedFunctor nat term.DecoratedFunctor nat term
Proof.DecoratedFunctor nat term
  constructor.Functor term
Natural (@dec nat term Decorate_term)
forall A : Type,
dec term ∘ dec term = map cojoin ∘ dec term
forall A : Type, map extract ∘ dec term = id
  -Functor term typeclasses eauto.
  -Natural (@dec nat term Decorate_term) typeclasses eauto.
  -forall A : Type,
dec term ∘ dec term = map cojoin ∘ dec term apply dec_dec.
  -forall A : Type, map extract ∘ dec term = id apply dec_extract.
Qed.

Rewriting rules for `dec`

Section dec_term_rewrite.

  Context
    `{f: A -> B}.

  Lemma dec_term1: forall (x: A),
      dec term (Var x) = Var (0, x).A, B: Type
f: A -> B
forall x : A, dec term (Var x) = Var (0, x)
  Proof.A, B: Type
f: A -> B
forall x : A, dec term (Var x) = Var (0, x)
    reflexivity.
  Qed.

  Lemma dec_term21: forall (X: typ) (t: term A),
      dec term (Lam X t) = shift term (1, Lam X (dec term t)).A, B: Type
f: A -> B
forall (X : typ) (t : term A),
dec term (λ X ⋅ t) = shift term (1, λ X ⋅ dec term t)
  Proof.A, B: Type
f: A -> B
forall (X : typ) (t : term A),
dec term (λ X ⋅ t) = shift term (1, λ X ⋅ dec term t)
    reflexivity.
  Qed.

  Lemma dec_term22: forall (X: typ) (t: term A),
      dec term (Lam X t) = Lam X (shift term (1, dec term t)).A, B: Type
f: A -> B
forall (X : typ) (t : term A),
dec term (λ X ⋅ t) = λ X ⋅ shift term (1, dec term t)
  Proof.A, B: Type
f: A -> B
forall (X : typ) (t : term A),
dec term (λ X ⋅ t) = λ X ⋅ shift term (1, dec term t)
    reflexivity.
  Qed.

  Lemma dec_term3: forall (t1 t2: term A),
      dec term (Ap t1 t2) = Ap (dec term t1) (dec term t2).A, B: Type
f: A -> B
forall t1 t2 : term A,
dec term ([t1][t2]) = [dec term t1][dec term t2]
  Proof.A, B: Type
f: A -> B
forall t1 t2 : term A,
dec term ([t1][t2]) = [dec term t1][dec term t2]
    reflexivity.
  Qed.

End dec_term_rewrite.

Traversable Functor instance

Import Applicative.Notations.

Fixpoint dist_term `{Map F} `{Pure F} `{Mult F} {A: Type}
         (t: term (F A)): F (term A) :=
  match t with
  | Var a => map (@Var A) a
  | Lam X t => map (Lam X) (dist_term t)
  | Ap t1 t2 => (pure (@Ap A))
                 <⋆> dist_term t1
                 <⋆> dist_term t2
  end.

#[export] Instance: ApplicativeDist term := @dist_term.

Rewriting rules for `dist`

Section term_dist_rewrite.

  Context
    `{Applicative G}.

  Variable (A: Type).

  Lemma dist_term_var_1: forall (x: G A),
    dist term G (@Var (G A) x) = pure (@Var A) <⋆> x.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
forall x : G A,
δ term G (Var x) = pure (Var (A:=A)) <⋆> x
  Proof.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
forall x : G A,
δ term G (Var x) = pure (Var (A:=A)) <⋆> x
    intros.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
x: G A
δ term G (Var x) = pure (Var (A:=A)) <⋆> x cbn.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
x: G A
map (Var (A:=A)) x = pure (Var (A:=A)) <⋆> x now rewrite map_to_ap.
  Qed.

  Lemma dist_term_var_2: forall (x: G A),
    dist term G (@Var (G A) x) = map (@Var A) x.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
forall x : G A, δ term G (Var x) = map (Var (A:=A)) x
  Proof.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
forall x : G A, δ term G (Var x) = map (Var (A:=A)) x
    reflexivity.
  Qed.

  Lemma dist_term_lam_1: forall (X: typ) (t: term (G A)),
      dist term G (Lam X t) = pure (Lam X) <⋆> (dist term G t).G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
forall (X : typ) (t : term (G A)),
δ term G (λ X ⋅ t) = pure (Lam X) <⋆> δ term G t
  Proof.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
forall (X : typ) (t : term (G A)),
δ term G (λ X ⋅ t) = pure (Lam X) <⋆> δ term G t
    intros.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
X: typ
t: term (G A)
δ term G (λ X ⋅ t) = pure (Lam X) <⋆> δ term G t cbn.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
X: typ
t: term (G A)
map (Lam X) (δ term G t) = pure (Lam X) <⋆> δ term G t now rewrite map_to_ap.
  Qed.

  Lemma dist_term_lam_2: forall (X: typ) (t: term (G A)),
      dist term G (Lam X t) = map (Lam X) (dist term G t).G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
forall (X : typ) (t : term (G A)),
δ term G (λ X ⋅ t) = map (Lam X) (δ term G t)
  Proof.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
forall (X : typ) (t : term (G A)),
δ term G (λ X ⋅ t) = map (Lam X) (δ term G t)
    reflexivity.
  Qed.

  Lemma dist_term_ap_1: forall (t1 t2: term (G A)),
      dist term G (Ap t1 t2) =
      (pure (@Ap A))
        <⋆> dist term G t1
        <⋆> dist term G t2.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
forall t1 t2 : term (G A),
δ term G ([t1][t2]) =
pure (Ap (A:=A)) <⋆> δ term G t1 <⋆> δ term G t2
  Proof.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
forall t1 t2 : term (G A),
δ term G ([t1][t2]) =
pure (Ap (A:=A)) <⋆> δ term G t1 <⋆> δ term G t2
    reflexivity.
  Qed.

  Lemma dist_term_ap_2: forall (t1 t2: term (G A)),
      dist term G (Ap t1 t2) =
      (map (@Ap A) (dist term G t1)
            <⋆> dist term G t2).G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
forall t1 t2 : term (G A),
δ term G ([t1][t2]) =
map (Ap (A:=A)) (δ term G t1) <⋆> δ term G t2
  Proof.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
forall t1 t2 : term (G A),
δ term G ([t1][t2]) =
map (Ap (A:=A)) (δ term G t1) <⋆> δ term G t2
    intros.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
t1, t2: term (G A)
δ term G ([t1][t2]) =
map (Ap (A:=A)) (δ term G t1) <⋆> δ term G t2 rewrite dist_term_ap_1.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
t1, t2: term (G A)
pure (Ap (A:=A)) <⋆> δ term G t1 <⋆> δ term G t2 =
map (Ap (A:=A)) (δ term G t1) <⋆> δ term G t2
    now rewrite map_to_ap.
  Qed.

End term_dist_rewrite.

Section dist_term_properties.

  Context
    `{Applicative G}.

Naturality of `dist`

  Lemma dist_natural_term: forall `(f: A -> B),
      map (F := G ∘ term) f ∘ dist term G =
      dist term G ∘ map (F := term ∘ G) f.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
forall (A B : Type) (f : A -> B),
map f ∘ δ term G = δ term G ∘ map 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 : A -> B),
map f ∘ δ term G = δ term G ∘ map f
    intros; cbn.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> B
map f ∘ δ term G = δ term G ∘ map f ext t.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> B
t: term (G A)
(map f ∘ δ term G) t = (δ term G ∘ map f) t
    unfold_ops @Map_compose.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> B
t: term (G A)
(map (map f) ∘ δ term G) t =
(δ term G ∘ map (map f)) t 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 -> B
t: term (G A)
map (map f) (δ term G t) = δ term G (map (map f) t) induction t.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> B
a: G A
map (map f) (δ term G (Var a)) =
δ term G (map (map f) (Var a))
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> B
X: typ
t: term (G A)
IHt: map (map f) (δ term G t) =
δ term G (map (map f) t)
map (map f) (δ term G (λ X ⋅ t)) =
δ term G (map (map f) (λ X ⋅ t))
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> B
t1, t2: term (G A)
IHt1: map (map f) (δ term G t1) =
δ term G (map (map f) t1)
IHt2: map (map f) (δ term G t2) =
δ term G (map (map f) t2)
map (map f) (δ term G ([t1][t2])) =
δ term G (map (map f) ([t1][t2]))
    +G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> B
a: G A
map (map f) (δ term G (Var a)) =
δ term G (map (map f) (Var a)) cbn.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> B
a: G A
map (map f) (map (Var (A:=A)) a) =
map (Var (A:=B)) (map f a) compose near a.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> B
a: G A
(map (map f) ∘ map (Var (A:=A))) a =
(map (Var (A:=B)) ∘ map f) a
      now rewrite 2(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: A -> B
X: typ
t: term (G A)
IHt: map (map f) (δ term G t) =
δ term G (map (map f) t)
map (map f) (δ term G (λ X ⋅ t)) =
δ term G (map (map f) (λ X ⋅ t)) cbn.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> B
X: typ
t: term (G A)
IHt: map (map f) (δ term G t) =
δ term G (map (map f) t)
map (map f) (map (Lam X) (δ term G t)) =
map (Lam X) (δ term G (map (map f) t)) rewrite <- IHt.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> B
X: typ
t: term (G A)
IHt: map (map f) (δ term G t) =
δ term G (map (map f) t)
map (map f) (map (Lam X) (δ term G t)) =
map (Lam X) (map (map f) (δ term G t))
      compose near (dist term G t).G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> B
X: typ
t: term (G A)
IHt: map (map f) (δ term G t) =
δ term G (map (map f) t)
(map (map f) ∘ map (Lam X)) (δ term G t) =
(map (Lam X) ∘ map (map f)) (δ term G t)
      now rewrite 2(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: A -> B
t1, t2: term (G A)
IHt1: map (map f) (δ term G t1) =
δ term G (map (map f) t1)
IHt2: map (map f) (δ term G t2) =
δ term G (map (map f) t2)
map (map f) (δ term G ([t1][t2])) =
δ term G (map (map f) ([t1][t2])) rewrite (dist_term_ap_2).G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> B
t1, t2: term (G A)
IHt1: map (map f) (δ term G t1) =
δ term G (map (map f) t1)
IHt2: map (map f) (δ term G t2) =
δ term G (map (map f) t2)
map (map f)
  (map (Ap (A:=A)) (δ term G t1) <⋆> δ term G t2) =
δ term G (map (map f) ([t1][t2]))
      rewrite (map_term_ap).G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> B
t1, t2: term (G A)
IHt1: map (map f) (δ term G t1) =
δ term G (map (map f) t1)
IHt2: map (map f) (δ term G t2) =
δ term G (map (map f) t2)
map (map f)
  (map (Ap (A:=A)) (δ term G t1) <⋆> δ term G t2) =
δ term G ([map (map f) t1][map (map f) t2])
      rewrite (dist_term_ap_2).G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> B
t1, t2: term (G A)
IHt1: map (map f) (δ term G t1) =
δ term G (map (map f) t1)
IHt2: map (map f) (δ term G t2) =
δ term G (map (map f) t2)
map (map f)
  (map (Ap (A:=A)) (δ term G t1) <⋆> δ term G t2) =
map (Ap (A:=B)) (δ term G (map (map f) t1)) <⋆>
δ term G (map (map f) t2)
      rewrite <- IHt1, <- IHt2.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> B
t1, t2: term (G A)
IHt1: map (map f) (δ term G t1) =
δ term G (map (map f) t1)
IHt2: map (map f) (δ term G t2) =
δ term G (map (map f) t2)
map (map f)
  (map (Ap (A:=A)) (δ term G t1) <⋆> δ term G t2) =
map (Ap (A:=B)) (map (map f) (δ term G t1)) <⋆>
map (map f) (δ term G t2)
      rewrite <- ap_map.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> B
t1, t2: term (G A)
IHt1: map (map f) (δ term G t1) =
δ term G (map (map f) t1)
IHt2: map (map f) (δ term G t2) =
δ term G (map (map f) t2)
map (map f)
  (map (Ap (A:=A)) (δ term G t1) <⋆> δ term G t2) =
map (precompose (map f))
  (map (Ap (A:=B)) (map (map f) (δ term G t1))) <⋆>
δ term G t2
      rewrite map_ap.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> B
t1, t2: term (G A)
IHt1: map (map f) (δ term G t1) =
δ term G (map (map f) t1)
IHt2: map (map f) (δ term G t2) =
δ term G (map (map f) t2)
map (compose (map f)) (map (Ap (A:=A)) (δ term G t1)) <⋆>
δ term G t2 =
map (precompose (map f))
  (map (Ap (A:=B)) (map (map f) (δ term G t1))) <⋆>
δ term G t2 fequal.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> B
t1, t2: term (G A)
IHt1: map (map f) (δ term G t1) =
δ term G (map (map f) t1)
IHt2: map (map f) (δ term G t2) =
δ term G (map (map f) t2)
map (compose (map f)) (map (Ap (A:=A)) (δ term G t1)) =
map (precompose (map f))
  (map (Ap (A:=B)) (map (map f) (δ term G t1)))
      compose near (dist term G t1).G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> B
t1, t2: term (G A)
IHt1: map (map f) (δ term G t1) =
δ term G (map (map f) t1)
IHt2: map (map f) (δ term G t2) =
δ term G (map (map f) t2)
(map (compose (map f)) ∘ map (Ap (A:=A)))
  (δ term G t1) =
map (precompose (map f))
  ((map (Ap (A:=B)) ∘ map (map f)) (δ term G t1))
      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: A -> B
t1, t2: term (G A)
IHt1: map (map f) (δ term G t1) =
δ term G (map (map f) t1)
IHt2: map (map f) (δ term G t2) =
δ term G (map (map f) t2)
map (compose (map f) ∘ Ap (A:=A)) (δ term G t1) =
map (precompose (map f))
  ((map (Ap (A:=B)) ∘ map (map f)) (δ term G t1))
      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: A -> B
t1, t2: term (G A)
IHt1: map (map f) (δ term G t1) =
δ term G (map (map f) t1)
IHt2: map (map f) (δ term G t2) =
δ term G (map (map f) t2)
map (compose (map f) ∘ Ap (A:=A)) (δ term G t1) =
map (precompose (map f))
  (map (Ap (A:=B) ∘ map f) (δ term G t1))
      compose near (dist term G t1) on right.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> B
t1, t2: term (G A)
IHt1: map (map f) (δ term G t1) =
δ term G (map (map f) t1)
IHt2: map (map f) (δ term G t2) =
δ term G (map (map f) t2)
map (compose (map f) ∘ Ap (A:=A)) (δ term G t1) =
(map (precompose (map f)) ∘ map (Ap (A:=B) ∘ map f))
  (δ term G t1)
      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: A -> B
t1, t2: term (G A)
IHt1: map (map f) (δ term G t1) =
δ term G (map (map f) t1)
IHt2: map (map f) (δ term G t2) =
δ term G (map (map f) t2)
map (compose (map f) ∘ Ap (A:=A)) (δ term G t1) =
map (precompose (map f) ∘ (Ap (A:=B) ∘ map f))
  (δ term G t1)
      reflexivity.
  Qed.

  #[export] Instance dist_Natural_term :
      Natural (@dist term _ _ _ _ _).G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
Natural
  (@dist term ApplicativeDist_instance_0 G Map_G
     Pure_G Mult_G)
  Proof.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
Natural
  (@dist term ApplicativeDist_instance_0 G Map_G
     Pure_G Mult_G)
    intros.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
Natural
  (@dist term ApplicativeDist_instance_0 G Map_G
     Pure_G Mult_G) constructor.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
Functor (term ○ G)
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
Functor (G ○ term)
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
forall (A B : Type) (f : A -> B),
map f ∘ δ term G = δ term G ∘ map f
    -G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
Functor (term ○ G) typeclasses eauto.
    -G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
Functor (G ○ term) typeclasses eauto.
    -G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
forall (A B : Type) (f : A -> B),
map f ∘ δ term G = δ term G ∘ map f intros.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A, B: Type
f: A -> B
map f ∘ δ term G = δ term G ∘ map f apply dist_natural_term.
  Qed.

Traversal laws

  Lemma dist_unit_term: forall (A: Type),
      dist term (fun A => A) = @id (term A).G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
forall A : Type, δ term (fun A0 : Type => A0) = id
  Proof.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
forall A : Type, δ term (fun A0 : Type => A0) = id
    intros.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
δ term (fun A : Type => A) = id ext t.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
t: term A
δ term (fun A : Type => A) t = id t induction t.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
a: A
δ term (fun A : Type => A) (Var a) = id (Var a)
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
X: typ
t: term A
IHt: δ term (fun A : Type => A) t = id t
δ term (fun A : Type => A) (λ X ⋅ t) = id (λ X ⋅ t)
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
t1, t2: term A
IHt1: δ term (fun A : Type => A) t1 = id t1
IHt2: δ term (fun A : Type => A) t2 = id t2
δ term (fun A : Type => A) ([t1][t2]) = id ([t1][t2])
    -G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
a: A
δ term (fun A : Type => A) (Var a) = id (Var a) reflexivity.
    -G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
X: typ
t: term A
IHt: δ term (fun A : Type => A) t = id t
δ term (fun A : Type => A) (λ X ⋅ t) = id (λ X ⋅ t) cbn.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
X: typ
t: term A
IHt: δ term (fun A : Type => A) t = id t
map (Lam X) (δ term (fun A : Type => A) t) =
id (λ X ⋅ t) rewrite IHt.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
X: typ
t: term A
IHt: δ term (fun A : Type => A) t = id t
map (Lam X) (id t) = id (λ X ⋅ t) reflexivity.
    -G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
t1, t2: term A
IHt1: δ term (fun A : Type => A) t1 = id t1
IHt2: δ term (fun A : Type => A) t2 = id t2
δ term (fun A : Type => A) ([t1][t2]) = id ([t1][t2]) cbn.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
t1, t2: term A
IHt1: δ term (fun A : Type => A) t1 = id t1
IHt2: δ term (fun A : Type => A) t2 = id t2
pure (Ap (A:=A)) (δ term (fun A : Type => A) t1)
  (δ term (fun A : Type => A) t2) = id ([t1][t2]) rewrite IHt1, IHt2.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
t1, t2: term A
IHt1: δ term (fun A : Type => A) t1 = id t1
IHt2: δ term (fun A : Type => A) t2 = id t2
pure (Ap (A:=A)) (id t1) (id t2) = id ([t1][t2])
      reflexivity.
  Qed.

  #[local] Set Keyed Unification.
  Lemma dist_linear_term: forall `{Applicative G1} `{Applicative G2} (A: Type),
      dist term (G1 ∘ G2) =
      map (F := G1) (dist term G2) ∘ dist term G1 (A := G2 A).G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
forall (G1 : Type -> Type) (Map_G0 : Map G1)
  (Pure_G0 : Pure G1) (Mult_G0 : Mult G1),
Applicative G1 ->
forall (G2 : Type -> Type) (Map_G1 : Map G2)
  (Pure_G1 : Pure G2) (Mult_G1 : Mult G2),
Applicative G2 ->
forall A : Type,
δ term (G1 ∘ G2) = map (δ term G2) ∘ δ term G1
  Proof.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
forall (G1 : Type -> Type) (Map_G0 : Map G1)
  (Pure_G0 : Pure G1) (Mult_G0 : Mult G1),
Applicative G1 ->
forall (G2 : Type -> Type) (Map_G1 : Map G2)
  (Pure_G1 : Pure G2) (Mult_G1 : Mult G2),
Applicative G2 ->
forall A : Type,
δ term (G1 ∘ G2) = map (δ term G2) ∘ δ term G1
    intros.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
G1: Type -> Type
Map_G0: Map G1
Pure_G0: Pure G1
Mult_G0: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G1: Map G2
Pure_G1: Pure G2
Mult_G1: Mult G2
H1: Applicative G2
A: Type
δ term (G1 ∘ G2) = map (δ term G2) ∘ δ term G1 unfold compose.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
G1: Type -> Type
Map_G0: Map G1
Pure_G0: Pure G1
Mult_G0: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G1: Map G2
Pure_G1: Pure G2
Mult_G1: Mult G2
H1: Applicative G2
A: Type
δ term (G1 ○ G2) = map (δ term G2) ○ δ term G1 ext t.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
G1: Type -> Type
Map_G0: Map G1
Pure_G0: Pure G1
Mult_G0: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G1: Map G2
Pure_G1: Pure G2
Mult_G1: Mult G2
H1: Applicative G2
A: Type
t: term (G1 (G2 A))
δ term (G1 ○ G2) t = map (δ term G2) (δ term G1 t) induction t.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
G1: Type -> Type
Map_G0: Map G1
Pure_G0: Pure G1
Mult_G0: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G1: Map G2
Pure_G1: Pure G2
Mult_G1: Mult G2
H1: Applicative G2
A: Type
a: G1 (G2 A)
δ term (G1 ○ G2) (Var a) =
map (δ term G2) (δ term G1 (Var a))
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
G1: Type -> Type
Map_G0: Map G1
Pure_G0: Pure G1
Mult_G0: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G1: Map G2
Pure_G1: Pure G2
Mult_G1: Mult G2
H1: Applicative G2
A: Type
X: typ
t: term (G1 (G2 A))
IHt: δ term (G1 ○ G2) t =
map (δ term G2) (δ term G1 t)
δ term (G1 ○ G2) (λ X ⋅ t) =
map (δ term G2) (δ term G1 (λ X ⋅ t))
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
G1: Type -> Type
Map_G0: Map G1
Pure_G0: Pure G1
Mult_G0: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G1: Map G2
Pure_G1: Pure G2
Mult_G1: Mult G2
H1: Applicative G2
A: Type
t1, t2: term (G1 (G2 A))
IHt1: δ term (G1 ○ G2) t1 =
map (δ term G2) (δ term G1 t1)
IHt2: δ term (G1 ○ G2) t2 =
map (δ term G2) (δ term G1 t2)
δ term (G1 ○ G2) ([t1][t2]) =
map (δ term G2) (δ term G1 ([t1][t2]))
    -G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
G1: Type -> Type
Map_G0: Map G1
Pure_G0: Pure G1
Mult_G0: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G1: Map G2
Pure_G1: Pure G2
Mult_G1: Mult G2
H1: Applicative G2
A: Type
a: G1 (G2 A)
δ term (G1 ○ G2) (Var a) =
map (δ term G2) (δ term G1 (Var a)) cbn.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
G1: Type -> Type
Map_G0: Map G1
Pure_G0: Pure G1
Mult_G0: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G1: Map G2
Pure_G1: Pure G2
Mult_G1: Mult G2
H1: Applicative G2
A: Type
a: G1 (G2 A)
map (Var (A:=A)) a =
map (δ term G2) (map (Var (A:=G2 A)) a) compose near a on right.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
G1: Type -> Type
Map_G0: Map G1
Pure_G0: Pure G1
Mult_G0: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G1: Map G2
Pure_G1: Pure G2
Mult_G1: Mult G2
H1: Applicative G2
A: Type
a: G1 (G2 A)
map (Var (A:=A)) a =
(map (δ term G2) ∘ map (Var (A:=G2 A))) a
      now rewrite (fun_map_map).
    -G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
G1: Type -> Type
Map_G0: Map G1
Pure_G0: Pure G1
Mult_G0: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G1: Map G2
Pure_G1: Pure G2
Mult_G1: Mult G2
H1: Applicative G2
A: Type
X: typ
t: term (G1 (G2 A))
IHt: δ term (G1 ○ G2) t =
map (δ term G2) (δ term G1 t)
δ term (G1 ○ G2) (λ X ⋅ t) =
map (δ term G2) (δ term G1 (λ X ⋅ t)) cbn.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
G1: Type -> Type
Map_G0: Map G1
Pure_G0: Pure G1
Mult_G0: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G1: Map G2
Pure_G1: Pure G2
Mult_G1: Mult G2
H1: Applicative G2
A: Type
X: typ
t: term (G1 (G2 A))
IHt: δ term (G1 ○ G2) t =
map (δ term G2) (δ term G1 t)
map (Lam X) (δ term (G1 ○ G2) t) =
map (δ term G2) (map (Lam X) (δ term G1 t)) rewrite IHt.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
G1: Type -> Type
Map_G0: Map G1
Pure_G0: Pure G1
Mult_G0: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G1: Map G2
Pure_G1: Pure G2
Mult_G1: Mult G2
H1: Applicative G2
A: Type
X: typ
t: term (G1 (G2 A))
IHt: δ term (G1 ○ G2) t =
map (δ term G2) (δ term G1 t)
map (Lam X) (map (δ term G2) (δ term G1 t)) =
map (δ term G2) (map (Lam X) (δ term G1 t)) compose near (dist term G1 t).G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
G1: Type -> Type
Map_G0: Map G1
Pure_G0: Pure G1
Mult_G0: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G1: Map G2
Pure_G1: Pure G2
Mult_G1: Mult G2
H1: Applicative G2
A: Type
X: typ
t: term (G1 (G2 A))
IHt: δ term (G1 ○ G2) t =
map (δ term G2) (δ term G1 t)
(map (Lam X) ∘ map (δ term G2)) (δ term G1 t) =
(map (δ term G2) ∘ map (Lam X)) (δ term G1 t)
      change (map (F := G1 ○ G2) (Lam X)) with (map (F := G1) (map (F := G2) (@Lam A X))).G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
G1: Type -> Type
Map_G0: Map G1
Pure_G0: Pure G1
Mult_G0: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G1: Map G2
Pure_G1: Pure G2
Mult_G1: Mult G2
H1: Applicative G2
A: Type
X: typ
t: term (G1 (G2 A))
IHt: δ term (G1 ○ G2) t =
map (δ term G2) (δ term G1 t)
(map (map (Lam X)) ∘ map (δ term G2)) (δ term G1 t) =
(map (δ term G2) ∘ map (Lam X)) (δ term G1 t)
      rewrite (fun_map_map).G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
G1: Type -> Type
Map_G0: Map G1
Pure_G0: Pure G1
Mult_G0: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G1: Map G2
Pure_G1: Pure G2
Mult_G1: Mult G2
H1: Applicative G2
A: Type
X: typ
t: term (G1 (G2 A))
IHt: δ term (G1 ○ G2) t =
map (δ term G2) (δ term G1 t)
map (map (Lam X) ∘ δ term G2) (δ term G1 t) =
(map (δ term G2) ∘ map (Lam X)) (δ term G1 t)
      now rewrite (fun_map_map).
    -G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
G1: Type -> Type
Map_G0: Map G1
Pure_G0: Pure G1
Mult_G0: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G1: Map G2
Pure_G1: Pure G2
Mult_G1: Mult G2
H1: Applicative G2
A: Type
t1, t2: term (G1 (G2 A))
IHt1: δ term (G1 ○ G2) t1 =
map (δ term G2) (δ term G1 t1)
IHt2: δ term (G1 ○ G2) t2 =
map (δ term G2) (δ term G1 t2)
δ term (G1 ○ G2) ([t1][t2]) =
map (δ term G2) (δ term G1 ([t1][t2])) rewrite dist_term_ap_2.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
G1: Type -> Type
Map_G0: Map G1
Pure_G0: Pure G1
Mult_G0: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G1: Map G2
Pure_G1: Pure G2
Mult_G1: Mult G2
H1: Applicative G2
A: Type
t1, t2: term (G1 (G2 A))
IHt1: δ term (G1 ○ G2) t1 =
map (δ term G2) (δ term G1 t1)
IHt2: δ term (G1 ○ G2) t2 =
map (δ term G2) (δ term G1 t2)
δ term (G1 ○ G2) ([t1][t2]) =
map (δ term G2)
  (map (Ap (A:=G2 A)) (δ term G1 t1) <⋆> δ term G1 t2)
      rewrite (dist_term_ap_2 (G := G1 ○ G2)).G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
G1: Type -> Type
Map_G0: Map G1
Pure_G0: Pure G1
Mult_G0: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G1: Map G2
Pure_G1: Pure G2
Mult_G1: Mult G2
H1: Applicative G2
A: Type
t1, t2: term (G1 (G2 A))
IHt1: δ term (G1 ○ G2) t1 =
map (δ term G2) (δ term G1 t1)
IHt2: δ term (G1 ○ G2) t2 =
map (δ term G2) (δ term G1 t2)
map (Ap (A:=A)) (δ term (G1 ○ G2) t1) <⋆>
δ term (G1 ○ G2) t2 =
map (δ term G2)
  (map (Ap (A:=G2 A)) (δ term G1 t1) <⋆> δ term G1 t2)
      rewrite map_ap.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
G1: Type -> Type
Map_G0: Map G1
Pure_G0: Pure G1
Mult_G0: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G1: Map G2
Pure_G1: Pure G2
Mult_G1: Mult G2
H1: Applicative G2
A: Type
t1, t2: term (G1 (G2 A))
IHt1: δ term (G1 ○ G2) t1 =
map (δ term G2) (δ term G1 t1)
IHt2: δ term (G1 ○ G2) t2 =
map (δ term G2) (δ term G1 t2)
map (Ap (A:=A)) (δ term (G1 ○ G2) t1) <⋆>
δ term (G1 ○ G2) t2 =
map (compose (δ term G2))
  (map (Ap (A:=G2 A)) (δ term G1 t1)) <⋆> δ term G1 t2
      compose near ((dist term G1 t1)).G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
G1: Type -> Type
Map_G0: Map G1
Pure_G0: Pure G1
Mult_G0: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G1: Map G2
Pure_G1: Pure G2
Mult_G1: Mult G2
H1: Applicative G2
A: Type
t1, t2: term (G1 (G2 A))
IHt1: δ term (G1 ○ G2) t1 =
map (δ term G2) (δ term G1 t1)
IHt2: δ term (G1 ○ G2) t2 =
map (δ term G2) (δ term G1 t2)
map (Ap (A:=A)) (δ term (G1 ○ G2) t1) <⋆>
δ term (G1 ○ G2) t2 =
(map (compose (δ term G2)) ∘ map (Ap (A:=G2 A)))
  (δ term G1 t1) <⋆> δ term G1 t2
      rewrite (fun_map_map).G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
G1: Type -> Type
Map_G0: Map G1
Pure_G0: Pure G1
Mult_G0: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G1: Map G2
Pure_G1: Pure G2
Mult_G1: Mult G2
H1: Applicative G2
A: Type
t1, t2: term (G1 (G2 A))
IHt1: δ term (G1 ○ G2) t1 =
map (δ term G2) (δ term G1 t1)
IHt2: δ term (G1 ○ G2) t2 =
map (δ term G2) (δ term G1 t2)
map (Ap (A:=A)) (δ term (G1 ○ G2) t1) <⋆>
δ term (G1 ○ G2) t2 =
map (compose (δ term G2) ∘ Ap (A:=G2 A))
  (δ term G1 t1) <⋆> δ term G1 t2
      rewrite (ap_compose2 G2 G1).G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
G1: Type -> Type
Map_G0: Map G1
Pure_G0: Pure G1
Mult_G0: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G1: Map G2
Pure_G1: Pure G2
Mult_G1: Mult G2
H1: Applicative G2
A: Type
t1, t2: term (G1 (G2 A))
IHt1: δ term (G1 ○ G2) t1 =
map (δ term G2) (δ term G1 t1)
IHt2: δ term (G1 ○ G2) t2 =
map (δ term G2) (δ term G1 t2)
map (ap G2) (map (Ap (A:=A)) (δ term (G1 ○ G2) t1)) <⋆>
δ term (G1 ○ G2) t2 =
map (compose (δ term G2) ∘ Ap (A:=G2 A))
  (δ term G1 t1) <⋆> δ term G1 t2
      rewrite IHt1, IHt2.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
G1: Type -> Type
Map_G0: Map G1
Pure_G0: Pure G1
Mult_G0: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G1: Map G2
Pure_G1: Pure G2
Mult_G1: Mult G2
H1: Applicative G2
A: Type
t1, t2: term (G1 (G2 A))
IHt1: δ term (G1 ○ G2) t1 =
map (δ term G2) (δ term G1 t1)
IHt2: δ term (G1 ○ G2) t2 =
map (δ term G2) (δ term G1 t2)
map (ap G2)
  (map (Ap (A:=A)) (map (δ term G2) (δ term G1 t1))) <⋆>
map (δ term G2) (δ term G1 t2) =
map (compose (δ term G2) ∘ Ap (A:=G2 A))
  (δ term G1 t1) <⋆> δ term G1 t2
      rewrite <- ap_map.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
G1: Type -> Type
Map_G0: Map G1
Pure_G0: Pure G1
Mult_G0: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G1: Map G2
Pure_G1: Pure G2
Mult_G1: Mult G2
H1: Applicative G2
A: Type
t1, t2: term (G1 (G2 A))
IHt1: δ term (G1 ○ G2) t1 =
map (δ term G2) (δ term G1 t1)
IHt2: δ term (G1 ○ G2) t2 =
map (δ term G2) (δ term G1 t2)
map (precompose (δ term G2))
  (map (ap G2)
     (map (Ap (A:=A)) (map (δ term G2) (δ term G1 t1)))) <⋆>
δ term G1 t2 =
map (compose (δ term G2) ∘ Ap (A:=G2 A))
  (δ term G1 t1) <⋆> δ term G1 t2 fequal.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
G1: Type -> Type
Map_G0: Map G1
Pure_G0: Pure G1
Mult_G0: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G1: Map G2
Pure_G1: Pure G2
Mult_G1: Mult G2
H1: Applicative G2
A: Type
t1, t2: term (G1 (G2 A))
IHt1: δ term (G1 ○ G2) t1 =
map (δ term G2) (δ term G1 t1)
IHt2: δ term (G1 ○ G2) t2 =
map (δ term G2) (δ term G1 t2)
map (precompose (δ term G2))
  (map (ap G2)
     (map (Ap (A:=A)) (map (δ term G2) (δ term G1 t1)))) =
map (compose (δ term G2) ∘ Ap (A:=G2 A))
  (δ term G1 t1)
      repeat (compose near (dist term G1 t1) on left;
              rewrite (fun_map_map (F := G1))).G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
G1: Type -> Type
Map_G0: Map G1
Pure_G0: Pure G1
Mult_G0: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G1: Map G2
Pure_G1: Pure G2
Mult_G1: Mult G2
H1: Applicative G2
A: Type
t1, t2: term (G1 (G2 A))
IHt1: δ term (G1 ○ G2) t1 =
map (δ term G2) (δ term G1 t1)
IHt2: δ term (G1 ○ G2) t2 =
map (δ term G2) (δ term G1 t2)
map
  (precompose (δ term G2)
   ∘ (ap G2 ∘ (map (Ap (A:=A)) ∘ δ term G2)))
  (δ term G1 t1) =
map (compose (δ term G2) ∘ Ap (A:=G2 A))
  (δ term G1 t1)
      fequal.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
G1: Type -> Type
Map_G0: Map G1
Pure_G0: Pure G1
Mult_G0: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G1: Map G2
Pure_G1: Pure G2
Mult_G1: Mult G2
H1: Applicative G2
A: Type
t1, t2: term (G1 (G2 A))
IHt1: δ term (G1 ○ G2) t1 =
map (δ term G2) (δ term G1 t1)
IHt2: δ term (G1 ○ G2) t2 =
map (δ term G2) (δ term G1 t2)
precompose (δ term G2)
∘ (ap G2 ∘ (map (Ap (A:=A)) ∘ δ term G2)) =
compose (δ term G2) ∘ Ap (A:=G2 A) ext s1 s2.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
G1: Type -> Type
Map_G0: Map G1
Pure_G0: Pure G1
Mult_G0: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G1: Map G2
Pure_G1: Pure G2
Mult_G1: Mult G2
H1: Applicative G2
A: Type
t1, t2: term (G1 (G2 A))
IHt1: δ term (G1 ○ G2) t1 =
map (δ term G2) (δ term G1 t1)
IHt2: δ term (G1 ○ G2) t2 =
map (δ term G2) (δ term G1 t2)
s1, s2: term (G2 A)
(precompose (δ term G2)
 ∘ (ap G2 ∘ (map (Ap (A:=A)) ∘ δ term G2))) s1 s2 =
(compose (δ term G2) ∘ Ap (A:=G2 A)) s1 s2 unfold compose; cbn.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
G1: Type -> Type
Map_G0: Map G1
Pure_G0: Pure G1
Mult_G0: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G1: Map G2
Pure_G1: Pure G2
Mult_G1: Mult G2
H1: Applicative G2
A: Type
t1, t2: term (G1 (G2 A))
IHt1: δ term (G1 ○ G2) t1 =
map (δ term G2) (δ term G1 t1)
IHt2: δ term (G1 ○ G2) t2 =
map (δ term G2) (δ term G1 t2)
s1, s2: term (G2 A)
precompose (δ term G2)
  (ap G2 (map (Ap (A:=A)) (δ term G2 s1))) s2 =
pure (Ap (A:=A)) <⋆> δ term G2 s1 <⋆> δ term G2 s2
      unfold precompose.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
G1: Type -> Type
Map_G0: Map G1
Pure_G0: Pure G1
Mult_G0: Mult G1
H0: Applicative G1
G2: Type -> Type
Map_G1: Map G2
Pure_G1: Pure G2
Mult_G1: Mult G2
H1: Applicative G2
A: Type
t1, t2: term (G1 (G2 A))
IHt1: δ term (G1 ○ G2) t1 =
map (δ term G2) (δ term G1 t1)
IHt2: δ term (G1 ○ G2) t2 =
map (δ term G2) (δ term G1 t2)
s1, s2: term (G2 A)
map (Ap (A:=A)) (δ term G2 s1) <⋆> δ term G2 s2 =
pure (Ap (A:=A)) <⋆> δ term G2 s1 <⋆> δ term G2 s2 now rewrite (map_to_ap).
  Qed.
  #[local] Unset Keyed Unification.

  Lemma dist_morph_term: forall `{ApplicativeMorphism G1 G2 ϕ} A,
      dist term G2 ∘ map (ϕ A) = ϕ (term A) ∘ dist term G1.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
forall (G1 G2 : Type -> Type) (H0 : Map G1)
  (H1 : Mult G1) (H2 : Pure G1) (H3 : Map G2)
  (H4 : Mult G2) (H5 : Pure G2)
  (ϕ : forall A : Type, G1 A -> G2 A),
ApplicativeMorphism G1 G2 ϕ ->
forall A : Type,
δ term G2 ∘ map (ϕ A) = ϕ (term A) ∘ δ term G1
  Proof.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
forall (G1 G2 : Type -> Type) (H0 : Map G1)
  (H1 : Mult G1) (H2 : Pure G1) (H3 : Map G2)
  (H4 : Mult G2) (H5 : Pure G2)
  (ϕ : forall A : Type, G1 A -> G2 A),
ApplicativeMorphism G1 G2 ϕ ->
forall A : Type,
δ term G2 ∘ map (ϕ A) = ϕ (term A) ∘ δ term G1
    intros.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
G1, G2: Type -> Type
H0: Map G1
H1: Mult G1
H2: Pure G1
H3: Map G2
H4: Mult G2
H5: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
H6: ApplicativeMorphism G1 G2 ϕ
A: Type
δ term G2 ∘ map (ϕ A) = ϕ (term A) ∘ δ term G1 ext t.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
G1, G2: Type -> Type
H0: Map G1
H1: Mult G1
H2: Pure G1
H3: Map G2
H4: Mult G2
H5: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
H6: ApplicativeMorphism G1 G2 ϕ
A: Type
t: term (G1 A)
(δ term G2 ∘ map (ϕ A)) t = (ϕ (term A) ∘ δ term G1) t unfold compose.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
G1, G2: Type -> Type
H0: Map G1
H1: Mult G1
H2: Pure G1
H3: Map G2
H4: Mult G2
H5: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
H6: ApplicativeMorphism G1 G2 ϕ
A: Type
t: term (G1 A)
δ term G2 (map (ϕ A) t) = ϕ (term A) (δ term G1 t) induction t.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
G1, G2: Type -> Type
H0: Map G1
H1: Mult G1
H2: Pure G1
H3: Map G2
H4: Mult G2
H5: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
H6: ApplicativeMorphism G1 G2 ϕ
A: Type
a: G1 A
δ term G2 (map (ϕ A) (Var a)) =
ϕ (term A) (δ term G1 (Var a))
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
G1, G2: Type -> Type
H0: Map G1
H1: Mult G1
H2: Pure G1
H3: Map G2
H4: Mult G2
H5: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
H6: ApplicativeMorphism G1 G2 ϕ
A: Type
X: typ
t: term (G1 A)
IHt: δ term G2 (map (ϕ A) t) =
ϕ (term A) (δ term G1 t)
δ term G2 (map (ϕ A) (λ X ⋅ t)) =
ϕ (term A) (δ term G1 (λ X ⋅ t))
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
G1, G2: Type -> Type
H0: Map G1
H1: Mult G1
H2: Pure G1
H3: Map G2
H4: Mult G2
H5: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
H6: ApplicativeMorphism G1 G2 ϕ
A: Type
t1, t2: term (G1 A)
IHt1: δ term G2 (map (ϕ A) t1) =
ϕ (term A) (δ term G1 t1)
IHt2: δ term G2 (map (ϕ A) t2) =
ϕ (term A) (δ term G1 t2)
δ term G2 (map (ϕ A) ([t1][t2])) =
ϕ (term A) (δ term G1 ([t1][t2]))
    -G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
G1, G2: Type -> Type
H0: Map G1
H1: Mult G1
H2: Pure G1
H3: Map G2
H4: Mult G2
H5: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
H6: ApplicativeMorphism G1 G2 ϕ
A: Type
a: G1 A
δ term G2 (map (ϕ A) (Var a)) =
ϕ (term A) (δ term G1 (Var a)) cbn.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
G1, G2: Type -> Type
H0: Map G1
H1: Mult G1
H2: Pure G1
H3: Map G2
H4: Mult G2
H5: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
H6: ApplicativeMorphism G1 G2 ϕ
A: Type
a: G1 A
map (Var (A:=A)) (ϕ A a) =
ϕ (term A) (map (Var (A:=A)) a) now rewrite <- (appmor_natural).
    -G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
G1, G2: Type -> Type
H0: Map G1
H1: Mult G1
H2: Pure G1
H3: Map G2
H4: Mult G2
H5: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
H6: ApplicativeMorphism G1 G2 ϕ
A: Type
X: typ
t: term (G1 A)
IHt: δ term G2 (map (ϕ A) t) =
ϕ (term A) (δ term G1 t)
δ term G2 (map (ϕ A) (λ X ⋅ t)) =
ϕ (term A) (δ term G1 (λ X ⋅ t)) cbn.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
G1, G2: Type -> Type
H0: Map G1
H1: Mult G1
H2: Pure G1
H3: Map G2
H4: Mult G2
H5: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
H6: ApplicativeMorphism G1 G2 ϕ
A: Type
X: typ
t: term (G1 A)
IHt: δ term G2 (map (ϕ A) t) =
ϕ (term A) (δ term G1 t)
map (Lam X) (δ term G2 (map (ϕ A) t)) =
ϕ (term A) (map (Lam X) (δ term G1 t)) rewrite IHt.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
G1, G2: Type -> Type
H0: Map G1
H1: Mult G1
H2: Pure G1
H3: Map G2
H4: Mult G2
H5: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
H6: ApplicativeMorphism G1 G2 ϕ
A: Type
X: typ
t: term (G1 A)
IHt: δ term G2 (map (ϕ A) t) =
ϕ (term A) (δ term G1 t)
map (Lam X) (ϕ (term A) (δ term G1 t)) =
ϕ (term A) (map (Lam X) (δ term G1 t))
      now rewrite (appmor_natural).
    -G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
G1, G2: Type -> Type
H0: Map G1
H1: Mult G1
H2: Pure G1
H3: Map G2
H4: Mult G2
H5: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
H6: ApplicativeMorphism G1 G2 ϕ
A: Type
t1, t2: term (G1 A)
IHt1: δ term G2 (map (ϕ A) t1) =
ϕ (term A) (δ term G1 t1)
IHt2: δ term G2 (map (ϕ A) t2) =
ϕ (term A) (δ term G1 t2)
δ term G2 (map (ϕ A) ([t1][t2])) =
ϕ (term A) (δ term G1 ([t1][t2])) rewrite map_term_ap.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
G1, G2: Type -> Type
H0: Map G1
H1: Mult G1
H2: Pure G1
H3: Map G2
H4: Mult G2
H5: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
H6: ApplicativeMorphism G1 G2 ϕ
A: Type
t1, t2: term (G1 A)
IHt1: δ term G2 (map (ϕ A) t1) =
ϕ (term A) (δ term G1 t1)
IHt2: δ term G2 (map (ϕ A) t2) =
ϕ (term A) (δ term G1 t2)
δ term G2 ([map (ϕ A) t1][map (ϕ A) t2]) =
ϕ (term A) (δ term G1 ([t1][t2]))
      infer_applicative_instances.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
G1, G2: Type -> Type
H0: Map G1
H1: Mult G1
H2: Pure G1
H3: Map G2
H4: Mult G2
H5: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
H6: ApplicativeMorphism G1 G2 ϕ
A: Type
t1, t2: term (G1 A)
IHt1: δ term G2 (map (ϕ A) t1) =
ϕ (term A) (δ term G1 t1)
IHt2: δ term G2 (map (ϕ A) t2) =
ϕ (term A) (δ term G1 t2)
app1: Applicative G1
app2: Applicative G2
δ term G2 ([map (ϕ A) t1][map (ϕ A) t2]) =
ϕ (term A) (δ term G1 ([t1][t2]))
      rewrite dist_term_ap_2.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
G1, G2: Type -> Type
H0: Map G1
H1: Mult G1
H2: Pure G1
H3: Map G2
H4: Mult G2
H5: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
H6: ApplicativeMorphism G1 G2 ϕ
A: Type
t1, t2: term (G1 A)
IHt1: δ term G2 (map (ϕ A) t1) =
ϕ (term A) (δ term G1 t1)
IHt2: δ term G2 (map (ϕ A) t2) =
ϕ (term A) (δ term G1 t2)
app1: Applicative G1
app2: Applicative G2
map (Ap (A:=A)) (δ term G2 (map (ϕ A) t1)) <⋆>
δ term G2 (map (ϕ A) t2) =
ϕ (term A) (δ term G1 ([t1][t2]))
      rewrite IHt1.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
G1, G2: Type -> Type
H0: Map G1
H1: Mult G1
H2: Pure G1
H3: Map G2
H4: Mult G2
H5: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
H6: ApplicativeMorphism G1 G2 ϕ
A: Type
t1, t2: term (G1 A)
IHt1: δ term G2 (map (ϕ A) t1) =
ϕ (term A) (δ term G1 t1)
IHt2: δ term G2 (map (ϕ A) t2) =
ϕ (term A) (δ term G1 t2)
app1: Applicative G1
app2: Applicative G2
map (Ap (A:=A)) (ϕ (term A) (δ term G1 t1)) <⋆>
δ term G2 (map (ϕ A) t2) =
ϕ (term A) (δ term G1 ([t1][t2])) rewrite IHt2.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
G1, G2: Type -> Type
H0: Map G1
H1: Mult G1
H2: Pure G1
H3: Map G2
H4: Mult G2
H5: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
H6: ApplicativeMorphism G1 G2 ϕ
A: Type
t1, t2: term (G1 A)
IHt1: δ term G2 (map (ϕ A) t1) =
ϕ (term A) (δ term G1 t1)
IHt2: δ term G2 (map (ϕ A) t2) =
ϕ (term A) (δ term G1 t2)
app1: Applicative G1
app2: Applicative G2
map (Ap (A:=A)) (ϕ (term A) (δ term G1 t1)) <⋆>
ϕ (term A) (δ term G1 t2) =
ϕ (term A) (δ term G1 ([t1][t2]))
      rewrite dist_term_ap_2.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
G1, G2: Type -> Type
H0: Map G1
H1: Mult G1
H2: Pure G1
H3: Map G2
H4: Mult G2
H5: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
H6: ApplicativeMorphism G1 G2 ϕ
A: Type
t1, t2: term (G1 A)
IHt1: δ term G2 (map (ϕ A) t1) =
ϕ (term A) (δ term G1 t1)
IHt2: δ term G2 (map (ϕ A) t2) =
ϕ (term A) (δ term G1 t2)
app1: Applicative G1
app2: Applicative G2
map (Ap (A:=A)) (ϕ (term A) (δ term G1 t1)) <⋆>
ϕ (term A) (δ term G1 t2) =
ϕ (term A)
  (map (Ap (A:=A)) (δ term G1 t1) <⋆> δ term G1 t2) rewrite (ap_morphism_1).G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
G1, G2: Type -> Type
H0: Map G1
H1: Mult G1
H2: Pure G1
H3: Map G2
H4: Mult G2
H5: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
H6: ApplicativeMorphism G1 G2 ϕ
A: Type
t1, t2: term (G1 A)
IHt1: δ term G2 (map (ϕ A) t1) =
ϕ (term A) (δ term G1 t1)
IHt2: δ term G2 (map (ϕ A) t2) =
ϕ (term A) (δ term G1 t2)
app1: Applicative G1
app2: Applicative G2
map (Ap (A:=A)) (ϕ (term A) (δ term G1 t1)) <⋆>
ϕ (term A) (δ term G1 t2) =
ϕ (term A -> term A) (map (Ap (A:=A)) (δ term G1 t1)) <⋆>
ϕ (term A) (δ term G1 t2)
      fequal.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
G1, G2: Type -> Type
H0: Map G1
H1: Mult G1
H2: Pure G1
H3: Map G2
H4: Mult G2
H5: Pure G2
ϕ: forall A : Type, G1 A -> G2 A
H6: ApplicativeMorphism G1 G2 ϕ
A: Type
t1, t2: term (G1 A)
IHt1: δ term G2 (map (ϕ A) t1) =
ϕ (term A) (δ term G1 t1)
IHt2: δ term G2 (map (ϕ A) t2) =
ϕ (term A) (δ term G1 t2)
app1: Applicative G1
app2: Applicative G2
map (Ap (A:=A)) (ϕ (term A) (δ term G1 t1)) =
ϕ (term A -> term A) (map (Ap (A:=A)) (δ term G1 t1)) now rewrite <- (appmor_natural).
  Qed.

End dist_term_properties.

#[export] Instance TraversableFunctor_term: TraversableFunctor term :=
  {| dist_natural := @dist_Natural_term;
     dist_morph := @dist_morph_term;
     dist_linear := @dist_linear_term;
     dist_unit := @dist_unit_term;
  |}.

Decorated-Traversable Functor instance

Lemma dtfun_compat_term1: forall `{Applicative G} (X: typ) {A},
    map (dec term ∘ Lam X) ∘ δ term G (A := A) =
    map (F := G) (curry (shift term) 1 ∘ Lam X) ∘ map (dec term) ∘ δ term G.forall (G : Type -> Type) (Map_G : Map G)
  (Pure_G : Pure G) (Mult_G : Mult G),
Applicative G ->
forall (X : typ) (A : Type),
map (dec term ∘ Lam X) ∘ δ term G =
map (curry (shift term) 1 ∘ Lam X) ∘ map (dec term)
∘ δ term G
Proof.forall (G : Type -> Type) (Map_G : Map G)
  (Pure_G : Pure G) (Mult_G : Mult G),
Applicative G ->
forall (X : typ) (A : Type),
map (dec term ∘ Lam X) ∘ δ term G =
map (curry (shift term) 1 ∘ Lam X) ∘ map (dec term)
∘ δ term G
  intros.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
X: typ
A: Type
map (dec term ∘ Lam X) ∘ δ term G =
map (curry (shift term) 1 ∘ Lam X) ∘ map (dec term)
∘ δ term G rewrite (fun_map_map).G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
X: typ
A: Type
map (dec term ∘ Lam X) ∘ δ term G =
map (curry (shift term) 1 ∘ Lam X ∘ dec term)
∘ δ term G reflexivity.
Qed.

Theorem dtfun_compat_term :
        `(forall `{Applicative G} {A: Type},
             dist term G ∘ map (strength) ∘ dec term (A := G A) =
             map (F := G) (dec term) ∘ dist term G).forall (G : Type -> Type) (Map_G : Map G)
  (Pure_G : Pure G) (Mult_G : Mult G),
Applicative G ->
forall A : Type,
δ term G ∘ map (σ) ∘ dec term =
map (dec term) ∘ δ term G
Proof.forall (G : Type -> Type) (Map_G : Map G)
  (Pure_G : Pure G) (Mult_G : Mult G),
Applicative G ->
forall A : Type,
δ term G ∘ map (σ) ∘ dec term =
map (dec term) ∘ δ term G
  intros.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
δ term G ∘ map (σ) ∘ dec term =
map (dec term) ∘ δ term G ext t.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
t: term (G A)
(δ term G ∘ map (σ) ∘ dec term) t =
(map (dec term) ∘ δ term G) t unfold compose.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
t: term (G A)
δ term G (map (σ) (dec term t)) =
map (dec term) (δ term G t) induction t.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
a: G A
δ term G (map (σ) (dec term (Var a))) =
map (dec term) (δ term G (Var a))
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
X: typ
t: term (G A)
IHt: δ term G (map (σ) (dec term t)) =
map (dec term) (δ term G t)
δ term G (map (σ) (dec term (λ X ⋅ t))) =
map (dec term) (δ term G (λ X ⋅ t))
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
t1, t2: term (G A)
IHt1: δ term G (map (σ) (dec term t1)) =
map (dec term) (δ term G t1)
IHt2: δ term G (map (σ) (dec term t2)) =
map (dec term) (δ term G t2)
δ term G (map (σ) (dec term ([t1][t2]))) =
map (dec term) (δ term G ([t1][t2]))
  -G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
a: G A
δ term G (map (σ) (dec term (Var a))) =
map (dec term) (δ term G (Var a)) cbn.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
a: G A
map (Var (A:=nat * A)) (map (pair Ƶ) a) =
map (dec term) (map (Var (A:=A)) a) compose near a.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
a: G A
(map (Var (A:=nat * A)) ∘ map (pair Ƶ)) a =
(map (dec term) ∘ map (Var (A:=A))) a now rewrite 2(fun_map_map).
  -G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
X: typ
t: term (G A)
IHt: δ term G (map (σ) (dec term t)) =
map (dec term) (δ term G t)
δ term G (map (σ) (dec term (λ X ⋅ t))) =
map (dec term) (δ term G (λ X ⋅ t)) cbn.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
X: typ
t: term (G A)
IHt: δ term G (map (σ) (dec term t)) =
map (dec term) (δ term G t)
map (Lam X)
  (δ term G
     (map (σ)
        (map (uncurry incr)
           (map (pair 1) (dec term t))))) =
map (dec term) (map (Lam X) (δ term G t)) do 2 (compose near (dec term t) on left;
               rewrite (fun_map_map)).G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
X: typ
t: term (G A)
IHt: δ term G (map (σ) (dec term t)) =
map (dec term) (δ term G t)
map (Lam X)
  (δ term G
     (map (σ ∘ (uncurry incr ∘ pair 1)) (dec term t))) =
map (dec term) (map (Lam X) (δ term G t))
    reassociate <-.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
X: typ
t: term (G A)
IHt: δ term G (map (σ) (dec term t)) =
map (dec term) (δ term G t)
map (Lam X)
  (δ term G
     (map (σ ∘ uncurry incr ∘ pair 1) (dec term t))) =
map (dec term) (map (Lam X) (δ term G t))
    rewrite incr_spec.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
X: typ
t: term (G A)
IHt: δ term G (map (σ) (dec term t)) =
map (dec term) (δ term G t)
map (Lam X)
  (δ term G (map (σ ∘ join ∘ pair 1) (dec term t))) =
map (dec term) (map (Lam X) (δ term G t))
    rewrite (Writer.strength_shift1 (W := nat) G).G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
X: typ
t: term (G A)
IHt: δ term G (map (σ) (dec term t)) =
map (dec term) (δ term G t)
map (Lam X)
  (δ term G
     (map (map (join ∘ pair 1) ∘ σ) (dec term t))) =
map (dec term) (map (Lam X) (δ term G t))
    rewrite <- (fun_map_map); unfold compose.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
X: typ
t: term (G A)
IHt: δ term G (map (σ) (dec term t)) =
map (dec term) (δ term G t)
map (Lam X)
  (δ term G
     (map (map (join ○ pair 1)) (map (σ) (dec term t)))) =
map (dec term) (map (Lam X) (δ term G t))
    change (map (map ?f)) with (map (F := term ∘ G) f).G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
X: typ
t: term (G A)
IHt: δ term G (map (σ) (dec term t)) =
map (dec term) (δ term G t)
map (Lam X)
  (δ term G
     (map (join ○ pair 1) (map (σ) (dec term t)))) =
map (dec term) (map (Lam X) (δ term G t))
    compose near ((map (σ (F := G)) (dec term t))).G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
X: typ
t: term (G A)
IHt: δ term G (map (σ) (dec term t)) =
map (dec term) (δ term G t)
map (Lam X)
  ((δ term G ∘ map (join ○ pair 1))
     (map (σ) (dec term t))) =
map (dec term) (map (Lam X) (δ term G t))
    unfold_compose_in_compose.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
X: typ
t: term (G A)
IHt: δ term G (map (σ) (dec term t)) =
map (dec term) (δ term G t)
map (Lam X)
  ((δ term G ∘ map (join ○ pair 1))
     (map (σ) (dec term t))) =
map (dec term) (map (Lam X) (δ term G t))
    rewrite <- (natural (ϕ := @dist term _ G _ _ _)).G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
X: typ
t: term (G A)
IHt: δ term G (map (σ) (dec term t)) =
map (dec term) (δ term G t)
map (Lam X)
  ((map (join ○ pair 1) ∘ δ term G)
     (map (σ) (dec term t))) =
map (dec term) (map (Lam X) (δ term G t))
    unfold compose.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
X: typ
t: term (G A)
IHt: δ term G (map (σ) (dec term t)) =
map (dec term) (δ term G t)
map (Lam X)
  (map (join ○ pair 1)
     (δ term G (map (σ) (dec term t)))) =
map (dec term) (map (Lam X) (δ term G t))
    rewrite IHt.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
X: typ
t: term (G A)
IHt: δ term G (map (σ) (dec term t)) =
map (dec term) (δ term G t)
map (Lam X)
  (map (join ○ pair 1) (map (dec term) (δ term G t))) =
map (dec term) (map (Lam X) (δ term G t)) compose near (δ term G t).G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
X: typ
t: term (G A)
IHt: δ term G (map (σ) (dec term t)) =
map (dec term) (δ term G t)
map (Lam X)
  ((map (join ○ pair 1) ∘ map (dec term)) (δ term G t)) =
(map (dec term) ∘ map (Lam X)) (δ term G t)
    rewrite (fun_map_map).G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
X: typ
t: term (G A)
IHt: δ term G (map (σ) (dec term t)) =
map (dec term) (δ term G t)
map (Lam X)
  ((map (join ○ pair 1) ∘ map (dec term)) (δ term G t)) =
map (dec term ∘ Lam X) (δ term G t)
    compose near (δ term G t) on left.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
X: typ
t: term (G A)
IHt: δ term G (map (σ) (dec term t)) =
map (dec term) (δ term G t)
(map (Lam X) ∘ (map (join ○ pair 1) ∘ map (dec term)))
  (δ term G t) = map (dec term ∘ Lam X) (δ term G t)
    unfold_ops @Map_compose; rewrite 2(fun_map_map).G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
X: typ
t: term (G A)
IHt: δ term G (map (σ) (dec term t)) =
map (dec term) (δ term G t)
map (Lam X ∘ (map (join ○ pair 1) ∘ dec term))
  (δ term G t) = map (dec term ∘ Lam X) (δ term G t)
    fequal.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
X: typ
t: term (G A)
IHt: δ term G (map (σ) (dec term t)) =
map (dec term) (δ term G t)
Lam X ∘ (map (join ○ pair 1) ∘ dec term) =
dec term ∘ Lam X ext t'; unfold compose; cbn.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
X: typ
t: term (G A)
IHt: δ term G (map (σ) (dec term t)) =
map (dec term) (δ term G t)
t': term A
λ X ⋅ map (join ○ pair 1) (dec term t') =
λ X ⋅ map (uncurry incr) (map (pair 1) (dec term t'))
    compose near (dec term t') on right.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
X: typ
t: term (G A)
IHt: δ term G (map (σ) (dec term t)) =
map (dec term) (δ term G t)
t': term A
λ X ⋅ map (join ○ pair 1) (dec term t') =
λ X
⋅ (map (uncurry incr) ∘ map (pair 1)) (dec term t')
    rewrite (fun_map_map (F := term)).G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
X: typ
t: term (G A)
IHt: δ term G (map (σ) (dec term t)) =
map (dec term) (δ term G t)
t': term A
λ X ⋅ map (join ○ pair 1) (dec term t') =
λ X ⋅ map (uncurry incr ∘ pair 1) (dec term t')
    now rewrite incr_spec.
  -G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
t1, t2: term (G A)
IHt1: δ term G (map (σ) (dec term t1)) =
map (dec term) (δ term G t1)
IHt2: δ term G (map (σ) (dec term t2)) =
map (dec term) (δ term G t2)
δ term G (map (σ) (dec term ([t1][t2]))) =
map (dec term) (δ term G ([t1][t2])) cbn.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
t1, t2: term (G A)
IHt1: δ term G (map (σ) (dec term t1)) =
map (dec term) (δ term G t1)
IHt2: δ term G (map (σ) (dec term t2)) =
map (dec term) (δ term G t2)
pure (Ap (A:=nat * A)) <⋆>
δ term G (map (σ) (dec term t1)) <⋆>
δ term G (map (σ) (dec term t2)) =
map (dec term)
  (pure (Ap (A:=A)) <⋆> δ term G t1 <⋆> δ term G t2) rewrite IHt1, IHt2.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
t1, t2: term (G A)
IHt1: δ term G (map (σ) (dec term t1)) =
map (dec term) (δ term G t1)
IHt2: δ term G (map (σ) (dec term t2)) =
map (dec term) (δ term G t2)
pure (Ap (A:=nat * A)) <⋆>
map (dec term) (δ term G t1) <⋆>
map (dec term) (δ term G t2) =
map (dec term)
  (pure (Ap (A:=A)) <⋆> δ term G t1 <⋆> δ term G t2) rewrite map_ap.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
t1, t2: term (G A)
IHt1: δ term G (map (σ) (dec term t1)) =
map (dec term) (δ term G t1)
IHt2: δ term G (map (σ) (dec term t2)) =
map (dec term) (δ term G t2)
pure (Ap (A:=nat * A)) <⋆>
map (dec term) (δ term G t1) <⋆>
map (dec term) (δ term G t2) =
map (compose (dec term))
  (pure (Ap (A:=A)) <⋆> δ term G t1) <⋆> 
δ term G t2 rewrite map_ap.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
t1, t2: term (G A)
IHt1: δ term G (map (σ) (dec term t1)) =
map (dec term) (δ term G t1)
IHt2: δ term G (map (σ) (dec term t2)) =
map (dec term) (δ term G t2)
pure (Ap (A:=nat * A)) <⋆>
map (dec term) (δ term G t1) <⋆>
map (dec term) (δ term G t2) =
map (compose (compose (dec term))) (pure (Ap (A:=A))) <⋆>
δ term G t1 <⋆> δ term G t2
    rewrite pure_ap_map.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
t1, t2: term (G A)
IHt1: δ term G (map (σ) (dec term t1)) =
map (dec term) (δ term G t1)
IHt2: δ term G (map (σ) (dec term t2)) =
map (dec term) (δ term G t2)
map (Ap (A:=nat * A) ∘ dec term) (δ term G t1) <⋆>
map (dec term) (δ term G t2) =
map (compose (compose (dec term))) (pure (Ap (A:=A))) <⋆>
δ term G t1 <⋆> δ term G t2 rewrite <- ap_map.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
t1, t2: term (G A)
IHt1: δ term G (map (σ) (dec term t1)) =
map (dec term) (δ term G t1)
IHt2: δ term G (map (σ) (dec term t2)) =
map (dec term) (δ term G t2)
map (precompose (dec term))
  (map (Ap (A:=nat * A) ∘ dec term) (δ term G t1)) <⋆>
δ term G t2 =
map (compose (compose (dec term))) (pure (Ap (A:=A))) <⋆>
δ term G t1 <⋆> δ term G t2
    rewrite (app_pure_natural).G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
t1, t2: term (G A)
IHt1: δ term G (map (σ) (dec term t1)) =
map (dec term) (δ term G t1)
IHt2: δ term G (map (σ) (dec term t2)) =
map (dec term) (δ term G t2)
map (precompose (dec term))
  (map (Ap (A:=nat * A) ∘ dec term) (δ term G t1)) <⋆>
δ term G t2 =
pure (compose (dec term) ∘ Ap (A:=A)) <⋆> δ term G t1 <⋆>
δ term G t2 rewrite <- (map_to_ap).G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
t1, t2: term (G A)
IHt1: δ term G (map (σ) (dec term t1)) =
map (dec term) (δ term G t1)
IHt2: δ term G (map (σ) (dec term t2)) =
map (dec term) (δ term G t2)
map (precompose (dec term))
  (map (Ap (A:=nat * A) ∘ dec term) (δ term G t1)) <⋆>
δ term G t2 =
map (compose (dec term) ∘ Ap (A:=A)) (δ term G t1) <⋆>
δ term G t2
    compose near (δ term G t1) on left.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
t1, t2: term (G A)
IHt1: δ term G (map (σ) (dec term t1)) =
map (dec term) (δ term G t1)
IHt2: δ term G (map (σ) (dec term t2)) =
map (dec term) (δ term G t2)
(map (precompose (dec term))
 ∘ map (Ap (A:=nat * A) ∘ dec term)) 
  (δ term G t1) <⋆> δ term G t2 =
map (compose (dec term) ∘ Ap (A:=A)) (δ term G t1) <⋆>
δ term G t2 rewrite (fun_map_map).G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
t1, t2: term (G A)
IHt1: δ term G (map (σ) (dec term t1)) =
map (dec term) (δ term G t1)
IHt2: δ term G (map (σ) (dec term t2)) =
map (dec term) (δ term G t2)
map
  (precompose (dec term)
   ∘ (Ap (A:=nat * A) ∘ dec term)) 
  (δ term G t1) <⋆> δ term G t2 =
map (compose (dec term) ∘ Ap (A:=A)) (δ term G t1) <⋆>
δ term G t2
    reflexivity.
Qed.

#[export] Instance: DecoratedTraversableFunctor nat term :=
  {| dtfun_compat := @dtfun_compat_term |}.

Monad instances

Plain Monad instance

Fixpoint join_term {A: Type} (t: term (term A)): term A :=
  match t with
  | Var t' => t'
  | Lam X t => Lam X (join_term t)
  | Ap t1 t2 => Ap (join_term t1) (join_term t2)
  end.

#[export] Instance Ret_term: Return term := @Var.

#[export] Instance Join_term: Join term := @join_term.

Theorem ret_natural: forall A B (f: A -> B),
    map f ∘ ret (T := term)  = ret ∘ f.forall (A B : Type) (f : A -> B),
map f ∘ ret = ret ∘ f
Proof.forall (A B : Type) (f : A -> B),
map f ∘ ret = ret ∘ f
  reflexivity.
Qed.

Theorem join_natural: forall A B (f: A -> B),
    map f ∘ join = join (T := term) ∘ map (map f).forall (A B : Type) (f : A -> B),
map f ∘ join = join ∘ map (map f)
Proof.forall (A B : Type) (f : A -> B),
map f ∘ join = join ∘ map (map f)
  intros.A, B: Type
f: A -> B
map f ∘ join = join ∘ map (map f) ext t.A, B: Type
f: A -> B
t: (term ∘ term) A
(map f ∘ join) t = (join ∘ map (map f)) t unfold transparent tcs.A, B: Type
f: A -> B
t: (term ∘ term) A
(map_term f ∘ join_term) t =
(join_term ∘ map_term (map_term f)) t
  unfold compose.A, B: Type
f: A -> B
t: (term ∘ term) A
map_term f (join_term t) =
join_term (map_term (map_term f) t) basic t.
Qed.

#[export] Instance: Natural (@ret term _).Natural (@ret term Ret_term)
Proof.Natural (@ret term Ret_term)
  constructor; try typeclasses eauto.forall (A B : Type) (f : A -> B),
map f ∘ ret = ret ∘ map f
  apply ret_natural.
Qed.

#[export] Instance: Natural (@join term _).Natural (@join term Join_term)
Proof.Natural (@join term Join_term)
  constructor.Functor (term ∘ term)
Functor term
forall (A B : Type) (f : A -> B),
map f ∘ join = join ∘ map f
  -Functor (term ∘ term) typeclasses eauto.
  -Functor term typeclasses eauto.
  -forall (A B : Type) (f : A -> B),
map f ∘ join = join ∘ map f apply join_natural.
Qed.

Theorem join_ret: forall A,
    join ∘ ret (T := term) = @id (term A).forall A : Type, join ∘ ret = id
Proof.forall A : Type, join ∘ ret = id
  reflexivity.
Qed.

Theorem join_map_ret: forall A,
    join (T := term) ∘ map (F := term) (ret (T := term)) = @id (term A).forall A : Type, join ∘ map ret = id
Proof.forall A : Type, join ∘ map ret = id
  intros.A: Type
join ∘ map ret = id unfold compose.A: Type
join ○ map ret = id
  unfold transparent tcs.A: Type
join_term ○ map_term (Var (A:=A)) = id
  ext t.A: Type
t: term A
join_term (map_term (Var (A:=A)) t) = id t basic t.
Qed.

Theorem join_join: forall A,
    join (T := term) ∘ join (T := term) = join (A := A) ∘ map (join (T := term)).forall A : Type, join ∘ join = join ∘ map join
Proof.forall A : Type, join ∘ join = join ∘ map join
  intros.A: Type
join ∘ join = join ∘ map join unfold compose.A: Type
join ○ join = join ○ map join unfold transparent tcs.A: Type
join_term ○ join_term = join_term ○ map_term join_term
  ext t.A: Type
t: term (term (term A))
join_term (join_term t) =
join_term (map_term join_term t) basic t.
Qed.

#[export] Instance Monad_term: Monad term :=
  {| mon_join_ret := join_ret;
     mon_join_map_ret := join_map_ret;
     mon_join_join := join_join |}.

Decorated Monad instance

Theorem dec_ret: forall A,
    dec term ∘ ret (A := A) = ret (T := term) ∘ pair Ƶ.forall A : Type, dec term ∘ ret = ret ∘ pair Ƶ
Proof.forall A : Type, dec term ∘ ret = ret ∘ pair Ƶ
  reflexivity.
Qed.

Theorem dec_join: forall A,
    dec term ∘ join (T := term) (A := A) =
    join (T := term) ∘ map (F := term) (shift term) ∘ dec term ∘ map (F := term) (dec term).forall A : Type,
dec term ∘ join =
join ∘ map (shift term) ∘ dec term ∘ map (dec term)
Proof.forall A : Type,
dec term ∘ join =
join ∘ map (shift term) ∘ dec term ∘ map (dec term)
  intros.A: Type
dec term ∘ join =
join ∘ map (shift term) ∘ dec term ∘ map (dec term) unfold compose.A: Type
dec term ○ join =
(fun a : term (term A) =>
 join (map (shift term) (dec term (map (dec term) a)))) ext t.A: Type
t: term (term A)
dec term (join t) =
join (map (shift term) (dec term (map (dec term) t))) induction t.A: Type
a: term A
dec term (join (Var a)) =
join
  (map (shift term)
     (dec term (map (dec term) (Var a))))
A: Type
X: typ
t: term (term A)
IHt: dec term (join t) = join (map (shift term) (dec term (map (dec term) t)))
dec term (join (λ X ⋅ t)) =
join
  (map (shift term)
     (dec term (map (dec term) (λ X ⋅ t))))
A: Type
t1, t2: term (term A)
IHt1: dec term (join t1) =
join
  (map (shift term)
     (dec term (map (dec term) t1)))
IHt2: dec term (join t2) =
join
  (map (shift term)
     (dec term (map (dec term) t2)))
dec term (join ([t1][t2])) =
join
  (map (shift term)
     (dec term (map (dec term) ([t1][t2]))))
  -A: Type
a: term A
dec term (join (Var a)) =
join
  (map (shift term)
     (dec term (map (dec term) (Var a)))) cbn -[shift].A: Type
a: term A
dec term a = shift term (Ƶ, dec term a) now rewrite (shift_zero term).
  -A: Type
X: typ
t: term (term A)
IHt: dec term (join t) =
join
  (map (shift term)
     (dec term (map (dec term) t)))
dec term (join (λ X ⋅ t)) =
join
  (map (shift term)
     (dec term (map (dec term) (λ X ⋅ t)))) cbn -[shift].A: Type
X: typ
t: term (term A)
IHt: dec term (join t) =
join
  (map (shift term)
     (dec term (map (dec term) t)))
λ X ⋅ shift term (1, dec term (join t)) =
λ X
⋅ join
    (map (shift term)
       (shift term (1, dec term (map (dec term) t)))) fequal.A: Type
X: typ
t: term (term A)
IHt: dec term (join t) =
join
  (map (shift term)
     (dec term (map (dec term) t)))
shift term (1, dec term (join t)) =
join
  (map (shift term)
     (shift term (1, dec term (map (dec term) t)))) now rewrite (dec_helper_4).
  -A: Type
t1, t2: term (term A)
IHt1: dec term (join t1) =
join
  (map (shift term)
     (dec term (map (dec term) t1)))
IHt2: dec term (join t2) =
join
  (map (shift term)
     (dec term (map (dec term) t2)))
dec term (join ([t1][t2])) =
join
  (map (shift term)
     (dec term (map (dec term) ([t1][t2])))) cbn.A: Type
t1, t2: term (term A)
IHt1: dec term (join t1) =
join
  (map (shift term)
     (dec term (map (dec term) t1)))
IHt2: dec term (join t2) =
join
  (map (shift term)
     (dec term (map (dec term) t2)))
[dec term (join t1)][dec term (join t2)] =
[join
   (map (shift term) (dec term (map (dec term) t1)))]
[join
   (map (shift term) (dec term (map (dec term) t2)))] fequal; auto.
Qed.

#[export] Instance DecoratedMonad_term: DecoratedMonad nat term.DecoratedMonad nat term
Proof.DecoratedMonad nat term
  constructor.DecoratedFunctor nat term
Monad term
Monoid nat
forall A : Type, dec term ∘ ret = ret ∘ pair Ƶ
forall A : Type,
dec term ∘ join =
join ∘ map (shift term) ∘ dec term ∘ map (dec term)
  -DecoratedFunctor nat term typeclasses eauto.
  -Monad term typeclasses eauto.
  -Monoid nat typeclasses eauto.
  -forall A : Type, dec term ∘ ret = ret ∘ pair Ƶ apply dec_ret.
  -forall A : Type,
dec term ∘ join =
join ∘ map (shift term) ∘ dec term ∘ map (dec term) apply dec_join.
Qed.

Traversable Monad instance

Theorem trvmon_ret_term `{Applicative G} :
  `(dist term G ∘ ret (T := term) (A := G A) = map (ret (T := term))).G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
forall A : Type, δ term G ∘ ret = map ret
Proof.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
forall A : Type, δ term G ∘ ret = map ret
  intros.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
δ term G ∘ ret = map ret ext x.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
x: G A
(δ term G ∘ ret) x = map ret x reflexivity.
Qed.

From Tealeaves Require Import Categories.TraversableFunctor.

#[local] Set Keyed Unification.
Theorem trvmon_join_term `{Applicative G} :
  `(dist term G ∘ join (T := term) = map (join (T := term)) ∘ dist (term ∘ term) G (A := A)).G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
forall A : Type,
δ term G ∘ join = map join ∘ δ (term ∘ term) G
Proof.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
forall A : Type,
δ term G ∘ join = map join ∘ δ (term ∘ term) G
  intros.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
δ term G ∘ join = map join ∘ δ (term ∘ term) G ext t.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
t: (term ∘ term) (G A)
(δ term G ∘ join) t = (map join ∘ δ (term ∘ term) G) t unfold compose.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
t: (term ∘ term) (G A)
δ term G (join t) = map join (δ (term ○ term) G t) induction t.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
a: term (G A)
δ term G (join (Var a)) =
map join (δ (term ○ term) G (Var a))
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
X: typ
t: term (term (G A))
IHt: δ term G (join t) =
map join (δ (term ○ term) G t)
δ term G (join (λ X ⋅ t)) =
map join (δ (term ○ term) G (λ X ⋅ t))
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
t1, t2: term (term (G A))
IHt1: δ term G (join t1) =
map join (δ (term ○ term) G t1)
IHt2: δ term G (join t2) =
map join (δ (term ○ term) G t2)
δ term G (join ([t1][t2])) =
map join (δ (term ○ term) G ([t1][t2]))
  -G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
a: term (G A)
δ term G (join (Var a)) =
map join (δ (term ○ term) G (Var a)) cbn.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
a: term (G A)
δ term G a =
map join (map (Var (A:=term A)) (δ term G a)) compose near (dist term G a).G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
a: term (G A)
δ term G a =
(map join ∘ map (Var (A:=term A))) (δ term G a)
    rewrite (fun_map_map).G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
a: term (G A)
δ term G a = map (join ∘ Var (A:=term A)) (δ term G a)
    replace (join ∘ Var (A := term A)) with (@id (term A)).G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
a: term (G A)
δ term G a = map id (δ term G a)
G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
a: term (G A)
id = join ∘ Var (A:=term A)
    now rewrite (fun_map_id).G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
a: term (G A)
id = join ∘ Var (A:=term A)
    apply (join_ret).
  -G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
X: typ
t: term (term (G A))
IHt: δ term G (join t) =
map join (δ (term ○ term) G t)
δ term G (join (λ X ⋅ t)) =
map join (δ (term ○ term) G (λ X ⋅ t)) cbn.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
X: typ
t: term (term (G A))
IHt: δ term G (join t) =
map join (δ (term ○ term) G t)
map (Lam X) (δ term G (join t)) =
map join (map (Lam X) (δ term G (map (δ term G) t))) rewrite IHt.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
X: typ
t: term (term (G A))
IHt: δ term G (join t) =
map join (δ (term ○ term) G t)
map (Lam X) (map join (δ (term ○ term) G t)) =
map join (map (Lam X) (δ term G (map (δ term G) t)))
    unfold_ops @Dist_compose.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
X: typ
t: term (term (G A))
IHt: δ term G (join t) =
map join (δ (term ○ term) G t)
map (Lam X) (map join ((δ term G ∘ map (δ term G)) t)) =
map join (map (Lam X) (δ term G (map (δ term G) t))) unfold compose.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
X: typ
t: term (term (G A))
IHt: δ term G (join t) =
map join (δ (term ○ term) G t)
map (Lam X) (map join (δ term G (map (δ term G) t))) =
map join (map (Lam X) (δ term G (map (δ term G) t)))
    compose near (dist term G (map (dist term G) t)).G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
X: typ
t: term (term (G A))
IHt: δ term G (join t) =
map join (δ (term ○ term) G t)
(map (Lam X) ∘ map join) (δ term G (map (δ term G) t)) =
(map join ∘ map (Lam X)) (δ term G (map (δ term G) t))
    rewrite (fun_map_map).G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
X: typ
t: term (term (G A))
IHt: δ term G (join t) =
map join (δ (term ○ term) G t)
map (Lam X ∘ join) (δ term G (map (δ term G) t)) =
(map join ∘ map (Lam X)) (δ term G (map (δ term G) t))
    rewrite (fun_map_map).G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
X: typ
t: term (term (G A))
IHt: δ term G (join t) =
map join (δ (term ○ term) G t)
map (Lam X ∘ join) (δ term G (map (δ term G) t)) =
map (join ∘ Lam X) (δ term G (map (δ term G) t))
    reflexivity.
  -G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
t1, t2: term (term (G A))
IHt1: δ term G (join t1) =
map join (δ (term ○ term) G t1)
IHt2: δ term G (join t2) =
map join (δ (term ○ term) G t2)
δ term G (join ([t1][t2])) =
map join (δ (term ○ term) G ([t1][t2])) cbn.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
t1, t2: term (term (G A))
IHt1: δ term G (join t1) =
map join (δ (term ○ term) G t1)
IHt2: δ term G (join t2) =
map join (δ (term ○ term) G t2)
pure (Ap (A:=A)) <⋆> δ term G (join t1) <⋆>
δ term G (join t2) =
map join
  (pure (Ap (A:=term A)) <⋆>
   δ term G (map (δ term G) t1) <⋆>
   δ term G (map (δ term G) t2)) rewrite IHt1, IHt2.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
t1, t2: term (term (G A))
IHt1: δ term G (join t1) =
map join (δ (term ○ term) G t1)
IHt2: δ term G (join t2) =
map join (δ (term ○ term) G t2)
pure (Ap (A:=A)) <⋆> map join (δ (term ○ term) G t1) <⋆>
map join (δ (term ○ term) G t2) =
map join
  (pure (Ap (A:=term A)) <⋆>
   δ term G (map (δ term G) t1) <⋆>
   δ term G (map (δ term G) t2))
    unfold_ops @Dist_compose.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
t1, t2: term (term (G A))
IHt1: δ term G (join t1) =
map join (δ (term ○ term) G t1)
IHt2: δ term G (join t2) =
map join (δ (term ○ term) G t2)
pure (Ap (A:=A)) <⋆>
map join ((δ term G ∘ map (δ term G)) t1) <⋆>
map join ((δ term G ∘ map (δ term G)) t2) =
map join
  (pure (Ap (A:=term A)) <⋆>
   δ term G (map (δ term G) t1) <⋆>
   δ term G (map (δ term G) t2)) unfold compose.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
t1, t2: term (term (G A))
IHt1: δ term G (join t1) =
map join (δ (term ○ term) G t1)
IHt2: δ term G (join t2) =
map join (δ (term ○ term) G t2)
pure (Ap (A:=A)) <⋆>
map join (δ term G (map (δ term G) t1)) <⋆>
map join (δ term G (map (δ term G) t2)) =
map join
  (pure (Ap (A:=term A)) <⋆>
   δ term G (map (δ term G) t1) <⋆>
   δ term G (map (δ term G) t2))
    rewrite <- map_to_ap.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
t1, t2: term (term (G A))
IHt1: δ term G (join t1) =
map join (δ (term ○ term) G t1)
IHt2: δ term G (join t2) =
map join (δ (term ○ term) G t2)
map (Ap (A:=A))
  (map join (δ term G (map (δ term G) t1))) <⋆>
map join (δ term G (map (δ term G) t2)) =
map join
  (pure (Ap (A:=term A)) <⋆>
   δ term G (map (δ term G) t1) <⋆>
   δ term G (map (δ term G) t2))
    rewrite <- map_to_ap.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
t1, t2: term (term (G A))
IHt1: δ term G (join t1) =
map join (δ (term ○ term) G t1)
IHt2: δ term G (join t2) =
map join (δ (term ○ term) G t2)
map (Ap (A:=A))
  (map join (δ term G (map (δ term G) t1))) <⋆>
map join (δ term G (map (δ term G) t2)) =
map join
  (map (Ap (A:=term A)) (δ term G (map (δ term G) t1)) <⋆>
   δ term G (map (δ term G) t2))
    rewrite <- ap_map.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
t1, t2: term (term (G A))
IHt1: δ term G (join t1) =
map join (δ (term ○ term) G t1)
IHt2: δ term G (join t2) =
map join (δ (term ○ term) G t2)
map (precompose join)
  (map (Ap (A:=A))
     (map join (δ term G (map (δ term G) t1)))) <⋆>
δ term G (map (δ term G) t2) =
map join
  (map (Ap (A:=term A)) (δ term G (map (δ term G) t1)) <⋆>
   δ term G (map (δ term G) t2)) rewrite map_ap.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
t1, t2: term (term (G A))
IHt1: δ term G (join t1) =
map join (δ (term ○ term) G t1)
IHt2: δ term G (join t2) =
map join (δ (term ○ term) G t2)
map (precompose join)
  (map (Ap (A:=A))
     (map join (δ term G (map (δ term G) t1)))) <⋆>
δ term G (map (δ term G) t2) =
map (compose join)
  (map (Ap (A:=term A)) (δ term G (map (δ term G) t1))) <⋆>
δ term G (map (δ term G) t2)
    fequal.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
t1, t2: term (term (G A))
IHt1: δ term G (join t1) =
map join (δ (term ○ term) G t1)
IHt2: δ term G (join t2) =
map join (δ (term ○ term) G t2)
map (precompose join)
  (map (Ap (A:=A))
     (map join (δ term G (map (δ term G) t1)))) =
map (compose join)
  (map (Ap (A:=term A)) (δ term G (map (δ term G) t1))) compose near ((dist term G (map (dist term G) t1))).G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
t1, t2: term (term (G A))
IHt1: δ term G (join t1) =
map join (δ (term ○ term) G t1)
IHt2: δ term G (join t2) =
map join (δ (term ○ term) G t2)
map (precompose join)
  ((map (Ap (A:=A)) ∘ map join)
     (δ term G (map (δ term G) t1))) =
(map (compose join) ∘ map (Ap (A:=term A)))
  (δ term G (map (δ term G) t1))
    repeat rewrite (fun_map_map).G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
t1, t2: term (term (G A))
IHt1: δ term G (join t1) =
map join (δ (term ○ term) G t1)
IHt2: δ term G (join t2) =
map join (δ (term ○ term) G t2)
map (precompose join)
  (map (Ap (A:=A) ∘ join)
     (δ term G (map (δ term G) t1))) =
map (compose join ∘ Ap (A:=term A))
  (δ term G (map (δ term G) t1))
    compose near ((dist term G (map (dist term G) t1))) on left.G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
t1, t2: term (term (G A))
IHt1: δ term G (join t1) =
map join (δ (term ○ term) G t1)
IHt2: δ term G (join t2) =
map join (δ (term ○ term) G t2)
(map (precompose join) ∘ map (Ap (A:=A) ∘ join))
  (δ term G (map (δ term G) t1)) =
map (compose join ∘ Ap (A:=term A))
  (δ term G (map (δ term G) t1))
    rewrite (fun_map_map).G: Type -> Type
Map_G: Map G
Pure_G: Pure G
Mult_G: Mult G
H: Applicative G
A: Type
t1, t2: term (term (G A))
IHt1: δ term G (join t1) =
map join (δ (term ○ term) G t1)
IHt2: δ term G (join t2) =
map join (δ (term ○ term) G t2)
map (precompose join ∘ (Ap (A:=A) ∘ join))
  (δ term G (map (δ term G) t1)) =
map (compose join ∘ Ap (A:=term A))
  (δ term G (map (δ term G) t1))
    fequal.
Qed.
#[local] Set Keyed Unification.

#[export] Instance TraversableMonad_term: TraversableMonad term :=
  {| trvmon_ret := @trvmon_ret_term;
     trvmon_join := @trvmon_join_term;
  |}.

Decorated-Traversable Monad instance

Our hard work has paid off---a DTM is defined as the combination of the typeclass instances we have given so far, so we can let Coq infer the DTM instance for us.

#[export] Instance DTM_STLC: DecoratedTraversableMonad nat term := {}.

Formalizing STLC with Tealeaves

Algebraic presentation

Imports and setup

Language Definition

Functor instances

Plain Functor instance

Rewriting rules for `map`

Decorated Functor instance

Rewriting rules for `dec`

Traversable Functor instance

Rewriting rules for `dist`

Naturality of `dist`

Traversal laws

Decorated-Traversable Functor instance

Monad instances

Plain Monad instance

Decorated Monad instance

Traversable Monad instance

Decorated-Traversable Monad instance

Formalizing STLC with Tealeaves

Algebraic presentation

Rewriting rules for map

Rewriting rules for dec

Rewriting rules for dist

Naturality of dist

Traversal laws

Rewriting rules for `map`

Rewriting rules for `dec`

Rewriting rules for `dist`

Naturality of `dist`