Library UniMath.SubstitutionSystems.SimplifiedHSS.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
version for simplified notion of HSS by Ralph Matthes (2022, 2023) the file is identical to the homonymous file in the parent directory, except for importing files from the present directory and WARNING: a big part of the previous development is commented out since the adaptation does to seem to be smooth here

Set Kernel Term Sharing.

Require Import UniMath.Foundations.PartD.

Require Import UniMath.MoreFoundations.Tactics.

Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Isos.
Require Import UniMath.CategoryTheory.Core.NaturalTransformations.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.FunctorCategory.
Require Import UniMath.CategoryTheory.whiskering.
Require Import UniMath.CategoryTheory.Limits.BinProducts.
Require Import UniMath.CategoryTheory.Limits.BinCoproducts.
Require Import UniMath.CategoryTheory.Limits.Terminal.
Require Import UniMath.CategoryTheory.Limits.Initial.
Require Import UniMath.CategoryTheory.FunctorAlgebras.
Require Import UniMath.CategoryTheory.PointedFunctors.
Require Import UniMath.CategoryTheory.PrecategoryBinProduct.
Require Import UniMath.SubstitutionSystems.Signatures.
Require Import UniMath.SubstitutionSystems.BinSumOfSignatures.
Require Import UniMath.SubstitutionSystems.SubstitutionSystems.
Require Import UniMath.SubstitutionSystems.LamSignature.
Require Import UniMath.SubstitutionSystems.LiftingInitial.
Require Import UniMath.SubstitutionSystems.MonadsFromSubstitutionSystems.
Require Import UniMath.SubstitutionSystems.Notation.
Local Open Scope subsys.

Local Open Scope cat.

Section Lambda.

Context (C : category).

The category of endofunctors on C
Local Notation "'EndC'":= ([C, C]) .

Context (terminal : Terminal C) (CC : BinCoproducts C) (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.

Context (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.


Context (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 (η (pr1 LamHSS)).
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 (τ (pr1 LamHSS)).
Defined.

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

Definition Lam_Abs : [C, C] ⟦ (Abs_H C terminal CC) `Lam, `Lam ⟧.
Proof.
  exact (BinCoproductIn2 (BinCoproducts_functor_precat _ _ _ _ _) · Lam_App_Abs).
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.
  exists ( `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 helper_to: (ptd_from_alg_functor CC LamE_S LamE_algebra_on_Lam) --> (ptd_from_alg_functor CC Lam_S Lam).
Proof.
  use tpair.
    + apply (nat_trans_id _ ).
    + abstract
        (intro c; rewrite id_right
         ; apply BinCoproductIn1Commutes_left_dir;
         apply idpath).
Defined.

Local Definition helper_from: (ptd_from_alg_functor CC Lam_S 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 bracket_property_for_LamE_algebra_on_Lam_helper : iso (ptd_from_alg_functor CC LamE_S LamE_algebra_on_Lam) (ptd_from_alg_functor CC Lam_S Lam).
Proof.
  unfold iso.
  exists helper_to.
  apply is_iso_from_is_z_iso.
  exists helper_from.
  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.

WARNING: the rest is commented out since the adaptation to SimplifiedHSS is not yet clear

End Lambda.