Library UniMath.SubstitutionSystems.LamSignature

**********************************************************
Benedikt Ahrens, Ralph Matthes
SubstitutionSystems
2015
**********************************************************
Contents :
  • Definition of the arities of the constructors of lambda calculus
  • Definition of the signatures of lambda calculus and lambda calculus with explicit flattening

Require Import UniMath.Foundations.PartD.
Require Import UniMath.MoreFoundations.All.

Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.Core.NaturalTransformations.
Local Open Scope cat.
Require Import UniMath.CategoryTheory.FunctorCategory.
Require Import UniMath.CategoryTheory.Limits.BinProducts.
Require Import UniMath.CategoryTheory.Limits.BinCoproducts.
Require Import UniMath.CategoryTheory.Limits.Terminal.
Require Import UniMath.CategoryTheory.PointedFunctors.
Require Import UniMath.CategoryTheory.HorizontalComposition.
Require Import UniMath.CategoryTheory.PointedFunctorsComposition.
Require Import UniMath.CategoryTheory.PrecategoryBinProduct.
Require Import UniMath.SubstitutionSystems.Signatures.
Require Import UniMath.CategoryTheory.BicatOfCatsElementary.
Require Import UniMath.SubstitutionSystems.BinSumOfSignatures.
Require Import UniMath.SubstitutionSystems.Notation.
Local Open Scope subsys.
Require Import UniMath.CategoryTheory.Chains.Chains.
Require Import UniMath.CategoryTheory.Chains.OmegaCocontFunctors.
Require Import UniMath.CategoryTheory.Exponentials.
Require Import UniMath.CategoryTheory.whiskering.
Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits.

Section Preparations.

Context (C : category) (CP : BinProducts C) (CC : BinCoproducts C).

Definition square_functor := BinProduct_of_functors C C CP (functor_identity C) (functor_identity C).

End Preparations.

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).

Let one : C := @TerminalObject C terminal.

App_H (X) (A) := X(A) × X(A)
Definition App_H : functor EndC EndC.
Show proof.
  apply square_functor.
  apply BinProducts_functor_precat.
  exact CP.

Lemma is_omega_cocont_App_H
  (hE : ∏ x, is_omega_cocont (constprod_functor1 (BinProducts_functor_precat C C CP) x)) :
  is_omega_cocont App_H.
Show proof.
  unfold App_H, square_functor.
  apply is_omega_cocont_BinProduct_of_functors; try assumption.
  - apply (BinProducts_functor_precat _ _ CP).
  - apply is_omega_cocont_functor_identity.
  - apply is_omega_cocont_functor_identity.

Abs_H (X) := X o option








Definition Abs_H : functor [C, C] [C, C] :=
 
  pre_composition_functor _ _ _ (option_functor CC terminal).

Lemma is_omega_cocont_Abs_H (CLC : Colims_of_shape nat_graph C) : is_omega_cocont Abs_H.
Show proof.
  unfold Abs_H.
  apply (is_omega_cocont_pre_composition_functor _ CLC).

Flat_H (X) := X o X
free in two arguments, then precomposed with diagonal

Definition Flat_H : functor [C, C] [C, C] := functor_composite (bindelta_functor [C, C]) (functorial_composition _ _ _).

here definition of suitable θ's together with their strength laws

Definition App_θ_data: ∏ XZ, (θ_source App_H) XZ --> (θ_target App_H) XZ.
Show proof.
  intro XZ.
  apply nat_trans_id.

Lemma is_nat_trans_App_θ_data: is_nat_trans _ _ App_θ_data.
Show proof.
  red.
  unfold App_θ_data.
  intros XZ XZ' αβ.
  apply nat_trans_eq_alt.
  intro c.
  simpl.
  rewrite id_left.
  rewrite id_right.
  unfold binproduct_nat_trans_data, BinProduct_of_functors_mor.
  unfold BinProductOfArrows.
  etrans; [ apply precompWithBinProductArrow |].
  simpl.
  unfold binproduct_nat_trans_pr1_data. unfold binproduct_nat_trans_pr2_data.
  simpl.
  apply BinProductArrowUnique.
  + rewrite BinProductPr1Commutes.
    repeat rewrite assoc.
    etrans.
    { apply cancel_postcomposition.
      apply BinProductPr1Commutes. }
    apply idpath.
  + rewrite BinProductPr2Commutes.
    repeat rewrite assoc.
    etrans.
    { apply cancel_postcomposition.
      apply BinProductPr2Commutes. }
    apply idpath.

Definition App_θ: PrestrengthForSignature App_H :=
  tpair _ _ is_nat_trans_App_θ_data.

Lemma App_θ_strength1_int: θ_Strength1_int App_θ.
Show proof.
  red.
  intro.
  unfold App_θ, App_H.
  simpl.
  unfold App_θ_data.
  apply nat_trans_eq; [apply homset_property |].
  intro c.
  simpl.
  rewrite id_left.
  unfold binproduct_nat_trans_data.
  apply pathsinv0.
  apply BinProductArrowUnique.
  + rewrite id_left.
    simpl.
    rewrite id_right.
    apply idpath.
  + rewrite id_left.
    simpl.
    rewrite id_right.
    apply idpath.

Lemma App_θ_strength2_int: θ_Strength2_int App_θ.
Show proof.
  red.
  intros.
  unfold App_θ, App_H.
  simpl.
  unfold App_θ_data.
  apply nat_trans_eq; [apply homset_property |].
  intro c.
  simpl.
  do 3 rewrite id_left.
  unfold binproduct_nat_trans_data.
  apply pathsinv0.
  apply BinProductArrowUnique.
  + rewrite id_left.
    simpl.
    rewrite id_right.
    apply idpath.
  + rewrite id_left.
    simpl.
    rewrite id_right.
    apply idpath.

Definition Abs_θ_data_data: ∏ XZ c, pr1 (θ_source Abs_H XZ) c --> pr1 (θ_target Abs_H XZ) c.
Show proof.
  intros XZ c.
  simpl.
  apply (functor_on_morphisms (functor_data_from_functor _ _ (pr1 XZ))).
  unfold constant_functor.
  simpl.
  apply BinCoproductArrow.
  + exact (BinCoproductIn1 _ ·
           nat_trans_data_from_nat_trans (pr2 (pr2 XZ)) (BinCoproductObject (CC (TerminalObject terminal) c))).
  + exact (# (pr1 (pr2 XZ)) (BinCoproductIn2 (CC (TerminalObject terminal) c))).

Lemma is_nat_trans_Abs_θ_data_data (XZ: [C, C] ⊠ category_Ptd C): is_nat_trans _ _ (Abs_θ_data_data XZ).
Show proof.
  intros c c' f.
  unfold Abs_θ_data_data.
  simpl.
  rewrite <- functor_comp.
  rewrite <- functor_comp.
  apply maponpaths.
  etrans.
  { apply precompWithBinCoproductArrow. }
  etrans; [| apply (!(postcompWithBinCoproductArrow _ _ _ _ _)) ].
  simpl.
  rewrite id_left.
  rewrite <- assoc.
  rewrite <- functor_comp.
  rewrite <- functor_comp.
  apply maponpaths_12.
  + assert (NN := nat_trans_ax (pr2 (pr2 XZ)) _ _ (BinCoproductOfArrows C (CC (TerminalObject terminal) c) (CC (TerminalObject terminal) c')
         (identity (TerminalObject terminal)) f)).
    match goal with |[ H1: _ = ?f·?g |- _ = ?h · _ ] =>
         intermediate_path (h·(f·g)) end.
    * rewrite <- NN.
      clear NN.
      unfold functor_identity.
      simpl.
      rewrite assoc.
      rewrite BinCoproductOfArrowsIn1.
      rewrite id_left.
      apply idpath.
    * apply idpath.
  + apply maponpaths.
    etrans; [| apply (!(BinCoproductOfArrowsIn2 _ _ _ _ _ )) ].
    apply idpath.


Definition Abs_θ_data (XZ: [C, C] ⊠ category_Ptd C): (θ_source Abs_H) XZ --> (θ_target Abs_H) XZ.
Show proof.
  exact (tpair _ _ (is_nat_trans_Abs_θ_data_data XZ)).

Lemma is_nat_trans_Abs_θ_data: is_nat_trans _ _ Abs_θ_data.
Show proof.
  red.
  intros XZ XZ' αβ.
  destruct XZ as [X [Z e]].
  destruct XZ' as [X' [Z' e']].
  destruct αβ as [α β].
  simpl in *.
  apply nat_trans_eq; [apply homset_property |].
  intro c.
  simpl.
  unfold constant_functor.
  simpl.
  rewrite assoc.
  unfold Abs_θ_data_data. simpl.
  rewrite (nat_trans_ax α).
  etrans.
  2: { apply cancel_postcomposition.
       apply functor_comp. }
  rewrite (nat_trans_ax α).
  rewrite <- assoc.
  apply maponpaths.
  etrans.
  { apply pathsinv0, functor_comp. }
  apply maponpaths.
  unfold constant_functor_data.
  simpl.
  etrans; [ apply precompWithBinCoproductArrow |].
  rewrite id_left.
  etrans.
  2: { eapply pathsinv0.
       apply postcompWithBinCoproductArrow. }
  apply BinCoproductArrowUnique.
  - rewrite BinCoproductIn1Commutes.
     rewrite <- assoc.
     apply maponpaths.
     apply pathsinv0, (ptd_mor_commutes _ β).
  - rewrite BinCoproductIn2Commutes.
    apply pathsinv0, (nat_trans_ax β).

Definition Abs_θ: PrestrengthForSignature Abs_H :=
  tpair _ _ is_nat_trans_Abs_θ_data.

Lemma Abs_θ_strength1_int: θ_Strength1_int Abs_θ.
Show proof.
  intro X.
  unfold Abs_θ, Abs_H, Abs_θ_data.
  apply nat_trans_eq_alt.
  intro c.
  simpl.
  rewrite id_right.
  apply functor_id_id.
  apply pathsinv0.
  apply BinCoproductArrowUnique.
  + apply idpath.
  + apply id_right.

Lemma Abs_θ_strength2_int: θ_Strength2_int Abs_θ.
Show proof.
  intros X Z Z'.
  unfold Abs_θ, Abs_H, Abs_θ_data.
  apply nat_trans_eq_alt.
  intro c.
  simpl.
  rewrite id_left.
  rewrite id_right.
  unfold Abs_θ_data_data. simpl. unfold horcomp_data; simpl.
  rewrite <- functor_comp.
  apply maponpaths.
  clear X.
  destruct Z as [Z e]; destruct Z' as [Z' e']; etrans.
  2: { eapply pathsinv0.
       apply postcompWithBinCoproductArrow. }
  simpl.
  apply maponpaths_12.
  + rewrite <- assoc.
    assert (NN := nat_trans_ax e' _ _ (e (BinCoproductObject (CC (TerminalObject terminal) c)))).
    simpl in NN.     match goal with |[ H1: _ = ?f·?g |- ?h · _ = _ ] =>
         intermediate_path (h·(f·g)) end.
    * apply maponpaths, NN.
    * assert (NNN := nat_trans_ax e' _ _ (BinCoproductArrow (CC (TerminalObject terminal) (Z c))
         (BinCoproductIn1 (CC (TerminalObject terminal) c)·
          e (BinCoproductObject (CC (TerminalObject terminal) c)))
         (# Z (BinCoproductIn2 (CC (TerminalObject terminal) c))))).
      simpl in NNN.
      match goal with |[ H1: _ = ?f·?g |- _ = ?h · _] =>
         intermediate_path (h·(f·g)) end.
      - simpl. rewrite <- NNN.
        clear NNN.
        do 2 rewrite assoc.
        rewrite BinCoproductIn1Commutes.
        do 2 rewrite <- assoc.
        apply maponpaths, pathsinv0, NN.
      - apply idpath.
  + rewrite <- functor_comp.
    apply maponpaths.
    etrans.
    2: { eapply pathsinv0.
         apply BinCoproductIn2Commutes. }
    apply idpath.

Definition Flat_θ_data (XZ: [C, C] ⊠ category_Ptd C): [C, C] ⟦θ_source Flat_H XZ, θ_target Flat_H XZ⟧.
Show proof.
  set (h:= nat_trans_comp (linvunitor_CAT (pr1 XZ)) ((nat_trans_id _) ⋆ (pr2 (pr2 XZ)))).
  set (F1' := pr1 (pr2 (left_unit_as_nat_z_iso _ _) (pr1 XZ))).
  set (F2' := # (post_comp_functor (pr1 XZ)) (pr2 (pr2 XZ))).
  set (h' := F1' · F2').
  set (obsolete := nat_trans_comp (lassociator_CAT (pr1 (pr2 XZ)) (pr1 XZ) (pr1 XZ)) (h ⋆ (nat_trans_id (functor_composite (pr1 (pr2 XZ)) (pr1 XZ))))).
  set (F3' := rassociator_CAT (pr12 XZ) (pr1 XZ) (pr1 XZ)).
  set (F4' := # (pre_comp_functor (functor_compose (pr1 (pr2 XZ)) (pr1 XZ))) h').
  exact (F3' · F4').

Lemma is_nat_trans_Flat_θ_data: is_nat_trans _ _ Flat_θ_data.
Show proof.
  intros XZ XZ' αβ.
  apply nat_trans_eq_alt.
  intro c.
  simpl.
  destruct XZ as [X [Z e]];
  destruct XZ' as [X' [Z' e']];
  destruct αβ as [α β];
  simpl in *.
  repeat rewrite id_left.
  rewrite (functor_comp Z).
  rewrite (functor_comp X).
  repeat rewrite assoc.
  do 4 rewrite <- functor_comp.
  rewrite (nat_trans_ax α).
  repeat rewrite <- assoc.
  rewrite <- functor_comp.
  do 2 rewrite (nat_trans_ax α).
  do 2 apply maponpaths.
  repeat rewrite assoc.
  etrans.
  2: { do 2 apply cancel_postcomposition.
       apply (nat_trans_ax e). }
  cbn.
  assert (β_is_pointed := ptd_mor_commutes _ β).
  simpl in β_is_pointed.
  rewrite <- (nat_trans_ax α).
  repeat rewrite <- assoc.
  apply maponpaths.
  rewrite assoc.
  etrans.
  2: { apply cancel_postcomposition.
       apply (nat_trans_ax e). }
  cbn.
  rewrite <- assoc.
  rewrite β_is_pointed.
  apply idpath.

Definition Flat_θ: PrestrengthForSignature Flat_H :=
  tpair _ _ is_nat_trans_Flat_θ_data.

Lemma Flat_θ_strength1_int: θ_Strength1_int Flat_θ.
Show proof.
  intro.
  unfold Flat_θ, Flat_H.
  apply nat_trans_eq_alt.
  intro c.
  simpl.
  do 2 rewrite id_left.
  rewrite functor_id.
  rewrite id_left.
  rewrite id_right.
  apply functor_id.

Lemma Flat_θ_strength2_int: θ_Strength2_int Flat_θ.
Show proof.
  intros ? ? ?.
  apply nat_trans_eq_alt.
  intro c.
  cbn.
  repeat rewrite id_left.
  rewrite id_right.
  repeat rewrite <- functor_comp.
  apply maponpaths.
  repeat rewrite functor_id.
  rewrite id_right.
  set (c' := pr1 X (pr1 Z' (pr1 Z c))).
  change (pr1 (ptd_pt C Z) c' · pr1 (ptd_pt C Z') (pr1 (pr1 (pr1 Z)) c') =
            pr1 (pr2 Z') c' · # (pr1 Z') (pr1 (pr2 Z) c')).
  etrans.
  2: { apply (nat_trans_ax (pr2 Z')). }
  apply idpath.

finally, constitute the 3 signatures

Definition App_Sig: Signature C C C.
Show proof.
  exists App_H.
  exists App_θ.
  split.
  + exact App_θ_strength1_int.
  + exact App_θ_strength2_int.

Definition Abs_Sig: Signature C C C.
Show proof.
  exists Abs_H.
  exists Abs_θ.
  split.
  + exact Abs_θ_strength1_int.
  + exact Abs_θ_strength2_int.

Definition Flat_Sig: Signature C C C.
Show proof.
  exists Flat_H.
  exists Flat_θ.
  split.
  + exact Flat_θ_strength1_int.
  + exact Flat_θ_strength2_int.

Definition Lam_Sig: Signature C C C :=
  BinSum_of_Signatures C C C CC App_Sig Abs_Sig.

Lemma is_omega_cocont_Lam
  (hE : ∏ x, is_omega_cocont (constprod_functor1 (BinProducts_functor_precat C C CP) x))
  (LC : Colims_of_shape nat_graph C) : is_omega_cocont (Signature_Functor Lam_Sig).
Show proof.
  apply is_omega_cocont_BinCoproduct_of_functors.
  - apply (is_omega_cocont_App_H hE).
  - apply (is_omega_cocont_Abs_H LC).

Definition LamE_Sig: Signature C C C :=
  BinSum_of_Signatures C C C CC Lam_Sig Flat_Sig.

End Lambda.