Tealeaves.Adapters.CategoricalToKleisli.DecoratedFunctorPoly

From Tealeaves Require Import
  Classes.Categorical.DecoratedFunctorPoly
  Classes.Kleisli.DecoratedFunctorPoly
  Functors.List.

#[local] Generalizable Variables T.

Import Functor2.Notations.

Kleisli DTMs from Categorical DTMs

Derived Operations

Module DerivedOperations.

  #[export] Instance Mapdp_Categorical
    (T: Type Type Type)
    `{Map2 T}
    `{DecoratePoly T}: MapdPoly T :=
    fun (B1 B2 V1 V2: Type)
      (ρ: list × ) (* rename binders *)
      (σ: list × ) (* insert subtrees *)
    ⇒ ρ σ decp (F := T) (B := ) (V := ).

End DerivedOperations.

Class Compat_Mapdp_Categorical
    (T: Type Type Type)
    `{Map_T: Map2 T}
    `{Decorate_T: DecoratePoly T}
    `{Mapdp_T: MapdPoly T} :=
  compat_mapdp_categorical:
    Mapdp_T = @DerivedOperations.Mapdp_Categorical T Map_T Decorate_T.

#[export] Instance Mapdp_Categorical_Self
  (T: Type Type Type)
  `{Map2 T}
  `{DecoratePoly T}:
  @Compat_Mapdp_Categorical T _ _ (@DerivedOperations.Mapdp_Categorical T _ _).
Proof.
  reflexivity.
Qed.


Lemma mapdp_to_categorical {T}
    `{Map_T: Map2 T}
    `{Decorate_T: DecoratePoly T}
    `{Mapdp_T: MapdPoly T}
    `{Compat: Compat_Mapdp_Categorical T}:
   (B1 B2 V1 V2: Type)
      (ρ: list × )
      (σ: list × )
      (t: T ),
      mapdp ρ σ t = ρ σ (decp t).
Proof.
  now rewrite compat_mapdp_categorical.
Qed.


Module DerivedInstances.

  Import DerivedOperations.

  Section context.

    Context
      `{Categorical.DecoratedFunctorPoly.DecoratedFunctorPoly T}.

    #[export] Instance: Kleisli.DecoratedFunctorPoly.DecoratedFunctorPoly T.
    Proof.
      constructor; intros.
      - unfold mapdp, Mapdp_Categorical.
        rewrite dfunp_dec_extract.
        reflexivity.
      - unfold mapdp, Mapdp_Categorical.
        reassociate on left.
        reassociatenear ( ρ1 σ1).
        rewrite polydecnat.
        repeat reassociate on left.
        rewrite (fun2_map_map).
        reassociateon left.
        rewrite dfunp_dec_dec.
        reassociate on left.
        rewrite fun2_map_map.
        unfold kc_dz.
        unfold kc_dfunp.
        reassociateon left.
        rewrite cobind_Z_spec.
        reflexivity.
    Qed.

  End context.

End DerivedInstances.