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, hs]) .

Variable terminal : Terminal C.

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

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

Let hsEndC : has_homsets EndC := functor_category_has_homsets C C hs.
Let CPEndC : BinCoproducts EndC := BinCoproducts_functor_precat _ _ CC hs.
Let EndEndC := [EndC, EndC, hsEndC].
Let CPEndEndC:= BinCoproducts_functor_precat _ _ CPEndC hsEndC: BinCoproducts EndEndC.

Let one : C := @TerminalObject C terminal.

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

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


Variable Lam_Initial : Initial
     (@precategory_FunctorAlg [C, C, hs]
                             (Id_H C hs CC Lam_S) hsEndC).

Let Lam := InitialObject Lam_Initial.

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

Definition LamHSS_Initial : Initial (hss_precategory 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, hs] (App_H C hs CP) `Lam , `Lam .
Proof.
  exact (BinCoproductIn1 _ (BinCoproducts_functor_precat _ _ _ _ _ _) · (BinCoproductIn2 _ (BinCoproducts_functor_precat _ _ _ _ _ _) · alg_map _ Lam)).
Defined.

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

Definition Lam_App_Abs : [C, C, hs]
    (H C hs C hs CC (App_H C hs CP) (Abs_H C hs 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, hs] (Flat_H C hs) `Lam , `Lam .
Proof.
  exact (fbracket LamHSS (identity _ )).
Defined.

now get a LamE-algebra

Definition LamE_algebra_on_Lam : FunctorAlg (Id_H _ _ CC LamE_S) hsEndC.
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 _ hs _ _));
    apply nat_trans_eq; try (exact hs) ;
    intro c ;
    apply id_left
                   |
    apply eq_ptd_mor_precat;
    apply (invmap (eq_ptd_mor _ hs _ _)) ;
    apply nat_trans_eq; try (exact hs) ;
    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, hs]
    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 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.
    eapply pathscomp0. 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; try (exact hs).
      intro c.
      unfold functor_ptd_forget.
      apply id_left.
    }
    rewrite idness. clear idness.
    rewrite id_right.
    apply nat_trans_eq; try (exact hs).
    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; try (exact hs).
    intro c.


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


    apply BinCoproductArrowUnique.
    + eapply pathscomp0. apply assoc.
      eapply pathscomp0. apply cancel_postcomposition. apply BinCoproductIn1Commutes.
      assert (T:= nat_trans_eq_pointwise Hyp2 c).
      clear Hyp2.
      apply pathsinv0.
      assumption.


    + clear Hyp2.
      eapply pathscomp0. apply assoc.
      eapply pathscomp0. apply cancel_postcomposition. apply BinCoproductIn2Commutes.
      unfold Lam_Flatten.

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

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

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

      set ( := ptd_from_alg _ ).

      rewrite functor_id.
      rewrite functor_id.
      rewrite id_right.
      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.

      match goal with |[ T3' : _ = ?f |- _ = ?a · ?b · _ · ?d ] ⇒ transitivity (a · b · #T f · d) end.
      2: { apply cancel_postcomposition. apply maponpaths. apply maponpaths. apply (!T3'). }
      clear T3'.
      apply pathsinv0.

      assert (T3':= nat_trans_eq_pointwise T3 (T (Z c))).

      eapply pathscomp0. apply cancel_postcomposition. apply cancel_postcomposition. apply maponpaths. apply T3'.
      clear T3'.
      apply pathsinv0.
      destruct f as [f fptdmor]. simpl in ×.
      rewrite id_right.
      rewrite id_right.

      repeat rewrite assoc.

      assert (X := fptdmor (T (Z c))). clear T3 fptdmor.
      assert (X' := maponpaths (#T) X); clear X.
      rewrite functor_comp in X'.

      apply pathsinv0.
      eapply pathscomp0. apply cancel_postcomposition. apply cancel_postcomposition.
                       apply cancel_postcomposition. apply X'.
                       clear X'.

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

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

      rewrite X' in X. clear X'.

      eapply pathscomp0. apply cancel_postcomposition. apply cancel_postcomposition. apply X. clear X.

      rewrite id_left.

      assert (μ_2_nat := nat_trans_ax (μ_2 C hs CC Lam_S LamHSS)).
      assert (X := μ_2_nat _ _ (f c)).
      unfold μ_2 in X.

      eapply pathscomp0. 2: { 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'.

      eapply pathscomp0. 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, hs]
            functor_composite (U Z)
               (` LamE_algebra_on_Lam),
           `LamE_algebra_on_Lam ,
       bracket_property f h,
   t =
   tpair
     (λ h : [C, C, hs]
             functor_composite (U Z)
                (` LamE_algebra_on_Lam),
            `LamE_algebra_on_Lam ,
      bracket_property f h)
     (fbracket_for_LamE_algebra_on_Lam Z f) (bracket_property_for_LamE_algebra_on_Lam Z f).
Proof.
  intro t.
  apply subtypeEquality.
  - intro; apply isaset_nat_trans. apply hs.
  - 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; try assumption.
      intro c.
      assert (HT:=nat_trans_eq_pointwise H1 c).
      simpl.
      rewrite id_right.
      eapply pathscomp0. 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; try assumption.
      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.
            eapply pathscomp0. 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.
      eapply pathscomp0. apply assoc.
      eapply pathscomp0. apply cancel_postcomposition. apply assoc.
      eapply pathscomp0. apply cancel_postcomposition. apply cancel_postcomposition.
      apply BinCoproductIn1Commutes.

      repeat rewrite <- assoc.
      eapply pathscomp0. apply maponpaths. apply assoc.

      eapply pathscomp0. apply maponpaths. apply cancel_postcomposition. apply BinCoproductIn1Commutes.

      eapply pathscomp0. apply maponpaths. apply (!assoc _ _ _ ).
      simpl. apply maponpaths. 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 hs CC LamE_S 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 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
     (@precategory_FunctorAlg [C, C, hs]
        (Id_H C hs CC LamE_S) hsEndC).

Definition LamEHSS_Initial : Initial (hss_precategory 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