Library UniMath.SubstitutionSystems.Lam

**********************************************************

Benedikt Ahrens, Ralph Matthes

SubstitutionSystems

2015

**********************************************************

Contents :

Specification of an initial morphism of substitution systems from lambda calculus with explicit flattening to lambda calculus

The category of endofunctors on C

Local Notation "'EndC'":= ([C , C ]) .

Variable terminal : Terminal C.

Variable CC : BinCoproducts C.
Variable CP : BinProducts C.

Local Notation "'Ptd'" := (category_Ptd C).

Let CPEndC : BinCoproducts EndC := BinCoproducts_functor_precat _ _ CC.
Let EndEndC := [EndC , EndC ].
Let CPEndEndC:= BinCoproducts_functor_precat _ _ CPEndC: BinCoproducts EndEndC.

Let one : C := @TerminalObject C terminal.

Variable KanExt : ∏ Z : precategory_Ptd C ,
   RightKanExtension.GlobalRightKanExtensionExists C C
     (U Z) C.

Let Lam_S : Signature _ _ _ := Lam_Sig C terminal CC CP.
Let LamE_S : Signature _ _ _ := LamE_Sig C terminal CC CP.

Variable Lam_Initial : Initial
     (@category_FunctorAlg [C , C ] (Id_H C CC Lam_S)).

Let Lam := InitialObject Lam_Initial.

bracket for Lam from the initial hss obtained via theorem 15+

Definition LamHSS_Initial : Initial (hss_category CC Lam_S).
Proof.
  apply InitialHSS.
  - apply KanExt.
  - apply Lam_Initial.
Defined.
Let LamHSS := InitialObject LamHSS_Initial.

extract constructors

Definition Lam_Var : EndC ⟦functor_identity C , `Lam ⟧.
Proof.
  exact (BinCoproductIn1 (BinCoproducts_functor_precat _ _ _ _ _) · alg_map _ Lam).
Defined.

Definition Lam_App : [C , C ] ⟦ (App_H C CP) `Lam , `Lam ⟧.
Proof.
  exact (BinCoproductIn1 (BinCoproducts_functor_precat _ _ _ _ _) · (BinCoproductIn2 (BinCoproducts_functor_precat _ _ _ _ _) · alg_map _ Lam )).
Defined.

Definition Lam_Abs : [C , C ] ⟦ (Abs_H C terminal CC) `Lam , `Lam ⟧.
Proof.
  exact (BinCoproductIn2 (BinCoproducts_functor_precat _ _ _ _ _) · (BinCoproductIn2 (BinCoproducts_functor_precat _ _ _ _ _) · alg_map _ Lam )).
Defined.

Definition Lam_App_Abs : [C , C ]
   ⟦ (H C C C CC (App_H C CP) (Abs_H C terminal CC)) `Lam , `Lam ⟧.
Proof.
  exact (BinCoproductIn2 (BinCoproducts_functor_precat _ _ _ _ _) · alg_map _ Lam).
Defined.

Definition of a "model" of the flattening arity in pure lambda calculus

we need a flattening in order to get a model for LamE

Definition Lam_Flatten :
[C , C ] ⟦ (Flat_H C) `Lam , `Lam ⟧.
Proof.
exact (prejoin_from_hetsubst (hetsubst_from_hss _ _ _ LamHSS)).
Defined.

now get a LamE-algebra

Definition LamE_algebra_on_Lam : FunctorAlg (Id_H _ CC LamE_S).
Proof.
  ∃ ( `Lam).
  use (BinCoproductArrow (CPEndC _ _ )).
  + exact Lam_Var.
  + use (BinCoproductArrow (CPEndC _ _ )).
    × apply Lam_App_Abs.     × apply Lam_Flatten.
Defined.

Lemma τ _LamE_algebra_on_Lam : τ LamE_algebra_on_Lam =
                              BinCoproductArrow (CPEndC _ _ ) Lam_App_Abs Lam_Flatten.
Proof.
  apply BinCoproductIn2Commutes.
Defined.

now define bracket operation for a given Z and f

preparations for typedness

Local Definition bla': (ptd_from_alg_functor CC LamE_S LamE_algebra_on_Lam ) --> (ptd_from_alg_functor CC _ Lam ).
Proof.
  use tpair.
    + apply (nat_trans_id _ ).
    + abstract
        (intro c; rewrite id_right
         ; apply BinCoproductIn1Commutes_left_dir;
         apply idpath).
Defined.

Local Definition bla'_inv: (ptd_from_alg_functor CC _ Lam ) --> (ptd_from_alg_functor CC LamE_S LamE_algebra_on_Lam ).
Proof.
  use tpair.
    + apply (nat_trans_id _ ).
    + abstract
        (intro c; rewrite id_right ;
         apply BinCoproductIn1Commutes_right_dir;
         apply idpath) .
Defined.

this iso does nothing, but is needed to make the argument to fbracket below well-typed

Local Definition bla : iso (ptd_from_alg_functor CC LamE_S LamE_algebra_on_Lam) (ptd_from_alg_functor CC _ Lam).
Proof.
  unfold iso.
  ∃ bla'.
  apply is_iso_from_is_z_iso.
  ∃ bla'_inv.
  abstract (
   split; [
    apply (invmap (eq_ptd_mor _ _));
    apply nat_trans_eq; [apply homset_property |] ;
    intro c ;
    apply id_left
                   |
    apply eq_ptd_mor_cat;
    apply (invmap (eq_ptd_mor _ _)) ;
    apply nat_trans_eq; [apply homset_property |];
    intro c ;
    apply id_left ]
           ).
Defined.

Definition fbracket_for_LamE_algebra_on_Lam (Z : Ptd)
   (f : Ptd ⟦ Z , ptd_from_alg_functor CC LamE_S LamE_algebra_on_Lam ⟧ ) :
   [C , C ]⟦ functor_composite (U Z) `LamE_algebra_on_Lam , `LamE_algebra_on_Lam ⟧ .
Proof.
  exact (fbracket LamHSS (f · bla)).
Defined.

Main lemma: our "model" for the flatten arity in pure lambda calculus is compatible with substitution

Lemma bracket_property_for_LamE_algebra_on_Lam (Z : Ptd)
  (f : Ptd ⟦ Z , ptd_from_alg LamE_algebra_on_Lam ⟧)
:
   bracket_property (nat_trans_fix_snd_arg _ _ _ _ _ (theta LamE_S) Z) _ f (fbracket_for_LamE_algebra_on_Lam Z f).
Proof.
  assert (Hyp := pr2 (pr1 (pr2 LamHSS _ (f · bla)))).
  apply parts_from_whole in Hyp.
  apply whole_from_parts.
  split.
  -
    apply pr1 in Hyp.
    apply (maponpaths (λ x , x · #U (inv_from_iso bla ))) in Hyp.
    rewrite <- functor_comp in Hyp.
    rewrite <- assoc in Hyp.
    rewrite iso_inv_after_iso in Hyp.
    rewrite id_right in Hyp.
    etrans; [ exact Hyp |].
    clear Hyp.
    fold (fbracket LamHSS (f · bla)).
    unfold fbracket_for_LamE_algebra_on_Lam.
    match goal with |[ |- _· _ · ?h = _ ] ⇒
         assert (idness : h = nat_trans_id _) end.
    { apply nat_trans_eq_alt.
      intro c.
      unfold functor_ptd_forget.
      apply id_left.
    }
    rewrite idness. clear idness.
    rewrite id_right.
    apply nat_trans_eq_alt.
    intro c.
    apply cancel_postcomposition.
    apply BinCoproductIn1Commutes_right_dir.
    apply idpath.
  -
    destruct Hyp as [_ Hyp2].
    fold (fbracket LamHSS (f · bla)) in Hyp2.
    unfold fbracket_for_LamE_algebra_on_Lam.
    apply nat_trans_eq_alt.
    intro c.

    rewrite τ _LamE_algebra_on_Lam.
    etrans; [ apply cancel_postcomposition ; apply BinCoproductOfArrows_comp |].
    etrans; [ apply precompWithBinCoproductArrow |].
    apply pathsinv0.

    apply BinCoproductArrowUnique.
    + etrans; [ apply assoc |].
      etrans. { apply cancel_postcomposition. apply BinCoproductIn1Commutes. }
      assert (T:= nat_trans_eq_pointwise Hyp2 c).
      clear Hyp2.
      apply pathsinv0.
      assumption.

    + clear Hyp2.
      etrans; [ apply assoc |].
      etrans. { apply cancel_postcomposition. apply BinCoproductIn2Commutes. }
      unfold Lam_Flatten.

      Opaque fbracket.
      Opaque LamHSS.
      set (X := f · bla).

      assert (TT := compute_fbracket C CC Lam_S LamHSS(Z:=Z)).
      simpl in ×.
      assert (T3 := TT X); clear TT.
      unfold X; unfold X in T3; clear X.
      do 2 rewrite id_left.

      Local Notation "⦃ f ⦄" := (fbracket _ f)(at level 0).

      set (Tη := ptd_from_alg _ ).

      destruct Z as [Z e]. simpl in ×.
      set (T := ` Lam).

      assert (T3' := nat_trans_eq_pointwise T3 c).
      simpl in ×.
      match goal with |[ T3' : _ = ?f |- ?a · _ = _ ] ⇒ transitivity (a · f) end.
      { apply maponpaths. apply T3'. }

      repeat rewrite assoc.
      etrans.
      2: { do 2 apply cancel_postcomposition. do 3 apply maponpaths. apply pathsinv0, T3'. }
      clear T3'.
      apply pathsinv0.

      assert (T3':= nat_trans_eq_pointwise T3 (T c)).
      simpl in T3'. rewrite id_right in T3'.
      etrans. { apply cancel_postcomposition. apply maponpaths. exact T3'. }
      clear T3'.

      apply pathsinv0.
      destruct f as [f fptdmor]. simpl in ×.

      repeat rewrite assoc.

      rewrite <- (functor_comp T).
      repeat rewrite <- assoc.
      etrans.
      2: { apply cancel_postcomposition. apply maponpaths. apply (nat_trans_ax e). }
      repeat rewrite assoc.
      rewrite <- (functor_comp T).

      assert (X := fptdmor (T c)). clear T3 fptdmor.
      unfold functor_identity_data. simpl.

      apply pathsinv0.
      etrans. { do 2 apply cancel_postcomposition. apply maponpaths. repeat rewrite <- assoc.
      do 2 apply maponpaths. apply X. }
      clear X.

      assert (X := Monad_law_2_from_hss _ CC Lam_S LamHSS (T c)).
      unfold μ_0 in X. unfold μ_2 in X.

      change (pr1 ⦃ identity (ptd_from_alg (pr1 LamHSS)) ⦄ c) with (prejoin_from_hetsubst LamHSS c).

      etrans.
      { do 2 apply cancel_postcomposition. apply maponpaths. apply assoc. }
      rewrite (functor_comp T).
      repeat rewrite <- assoc.

      match goal with |[ X : ?e = _ |- _ · (?a · (?b · _)) = _ ] ⇒
                         assert (X' : e = a · b) end.
      { apply cancel_postcomposition. apply maponpaths.
        cbn. apply pathsinv0, BinCoproductIn1Commutes. }
      rewrite X' in X. clear X'.

      etrans. { apply maponpaths. rewrite assoc. apply cancel_postcomposition. apply X. }
      clear X.

      rewrite id_left.

      assert (μ_2_nat := nat_trans_ax (μ_2 C CC Lam_S LamHSS)).
      assert (X := μ_2_nat _ _ (f c · identity (pr1 `Lam c))).
      unfold μ_2 in X.

      etrans. 2: { rewrite assoc. apply cancel_postcomposition. apply X. }
      clear X.

      rewrite functor_comp.
      repeat rewrite <- assoc.
      apply maponpaths.

      assert (X := third_monad_law_from_hss _ CC Lam_S LamHSS).
      assert (X' := nat_trans_eq_pointwise X). clear X.
      simpl in X'.

      etrans; [ apply X' |].
      clear X'. apply cancel_postcomposition. apply id_left.
Qed.

Uniqueness of the bracket operation

That is a consequence of uniqueness of that operation for a larger signature, namely for that of lambda calculus with flattening. We thus only have to extract the relevant parts, which is still a bit cumbersome.

Lemma bracket_for_LamE_algebra_on_Lam_unique (Z : Ptd)
  (f : Ptd ⟦ Z , ptd_from_alg LamE_algebra_on_Lam ⟧)
:
   ∏
   t : ∑
       h : [C , C ]
           ⟦ functor_composite (U Z)
               (` LamE_algebra_on_Lam),
           `LamE_algebra_on_Lam ⟧,
       bracket_property (nat_trans_fix_snd_arg _ _ _ _ _ (theta LamE_S) Z) _ f h ,
   t =
   tpair
     (λ h : [C , C ]
            ⟦ functor_composite (U Z)
                (` LamE_algebra_on_Lam),
            `LamE_algebra_on_Lam ⟧,
      bracket_property (nat_trans_fix_snd_arg _ _ _ _ _ (theta LamE_S) Z) _ f h)
     (fbracket_for_LamE_algebra_on_Lam Z f) (bracket_property_for_LamE_algebra_on_Lam Z f).
Proof.
  intro t.
  apply subtypePath.
  - intro; apply (isaset_nat_trans (homset_property C)).
  - simpl.
    destruct t as [t Ht]; simpl.
    unfold fbracket_for_LamE_algebra_on_Lam.
    apply (fbracket_unique LamHSS).
    split.
    + apply parts_from_whole in Ht. destruct Ht as [H1 _].
      apply nat_trans_eq_alt.
      intro c.
      assert (HT := nat_trans_eq_pointwise H1 c).
      simpl.
      rewrite id_right.
      etrans; [ apply HT |].
      simpl. repeat rewrite assoc. apply cancel_postcomposition.
      apply BinCoproductIn1Commutes.
    + apply parts_from_whole in Ht. destruct Ht as [_ H2].
      apply nat_trans_eq_alt.
      intro c.
      assert (HT := nat_trans_eq_pointwise H2 c).
      match goal with |[H2 : ?e = ?f |- _ ] ⇒
                         assert (X: BinCoproductIn1 _ · e = BinCoproductIn1 _ · f) end.
      { apply maponpaths . assumption. }
      clear HT. clear H2.

      match goal with |[X : _ = ?f |- _ ] ⇒ transitivity f end.
       2: { rewrite τ _LamE_algebra_on_Lam.
            etrans; [apply assoc |].
            apply cancel_postcomposition. apply BinCoproductIn1Commutes.
       }
      match goal with |[X : ?e = _ |- _ ] ⇒ transitivity e end.
       2: apply X.

      rewrite τ _LamE_algebra_on_Lam.

      apply pathsinv0.
      etrans; [ apply assoc |].
      etrans. { apply cancel_postcomposition. apply assoc. }
      etrans. { apply cancel_postcomposition. apply cancel_postcomposition.
                apply BinCoproductIn1Commutes. }

      repeat rewrite <- assoc.
      etrans. { apply maponpaths. apply assoc. }

      etrans. { apply maponpaths. apply cancel_postcomposition. apply BinCoproductIn1Commutes. }

      etrans. { apply maponpaths. apply assoc'. }
      simpl. do 2 apply maponpaths.
      apply BinCoproductIn1Commutes.
Qed.

Definition bracket_for_LamE_algebra_on_Lam_at (Z : Ptd)
  (f : Ptd ⟦ Z , ptd_from_alg LamE_algebra_on_Lam ⟧)
  :
    bracket_at C CC LamE_S (nat_trans_fix_snd_arg _ _ _ _ _ (theta LamE_S) Z) LamE_algebra_on_Lam f.
Proof.
  use tpair.
  - ∃ (fbracket_for_LamE_algebra_on_Lam Z f).
    apply (bracket_property_for_LamE_algebra_on_Lam Z f).
  - simpl; apply bracket_for_LamE_algebra_on_Lam_unique.
Defined.

Definition bracket_for_LamE_algebra_on_Lam : bracket (theta LamE_S) LamE_algebra_on_Lam.
Proof.
  intros Z f.
  simpl.
  apply bracket_for_LamE_algebra_on_Lam_at.
Defined.

Definition LamE_model_on_Lam : hss CC LamE_S.
Proof.
  ∃ LamE_algebra_on_Lam.
  exact bracket_for_LamE_algebra_on_Lam.
Defined.

Variable LamE_Initial : Initial
     (@category_FunctorAlg [C , C ]
        (Id_H C CC LamE_S)).

Definition LamEHSS_Initial : Initial (hss_category CC LamE_S).
Proof.
  apply InitialHSS.
  - apply KanExt.
  - apply LamE_Initial.
Defined.
Let LamEHSS := InitialObject LamEHSS_Initial.

Specification of a morphism from lambda calculus with flattening to pure lambda calculus

Definition FLATTEN : (hss_category CC LamE_S ) ⟦LamEHSS , LamE_model_on_Lam ⟧
:= InitialArrow _ _ .

End Lambda.