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.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.PrecategoryBinProduct.
Require Import UniMath.SubstitutionSystems.Signatures.
Require Import UniMath.CategoryTheory.UnitorsAndAssociatorsForEndofunctors.
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.

Variable C : precategory.
Variable hs : has_homsets C.
Variable CP : BinProducts C.
Variable CC : BinCoproducts C.

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

End Preparations.

Section Lambda.

Variable C : precategory.
Variable hs : has_homsets C.

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

Variable terminal : Terminal C.

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

Let one : C := @TerminalObject C terminal.

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

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

Abs_H (X) := X o option








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

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

Flat_H (X) := X o X
ingredients:
  • functor_composite in CategoryTheory.functor_categories
  • map given by horizontal composition in Substsystems.HorizontalComposition
Alternatively : free in two arguments, then precomposed with diagonal
Definition Flat_H_ob (X: EndC): functor C C := functor_composite X X.
Definition Flat_H_mor (X X': EndC)(α: X --> X'): (Flat_H_ob X: EndC) --> Flat_H_ob X' := α ∙∙ α.
Definition Flat_H_functor_data: functor_data EndC EndC.
Proof.
  ∃ Flat_H_ob.
  exact Flat_H_mor.
Defined.

Lemma is_functor_Flat_H_data: is_functor Flat_H_functor_data.
Proof.
  red.
  split; red.
  + intros X.
    unfold Flat_H_functor_data.
    simpl.
    unfold Flat_H_mor.
    apply nat_trans_eq; try assumption.
    intro c.
    simpl.
    rewrite id_left.
    apply functor_id.
  + intros X X' X'' α β.
    unfold Flat_H_functor_data.
    simpl.
    unfold Flat_H_mor.
    apply nat_trans_eq; try assumption.
    intro c.
    simpl.
    rewrite functor_comp.
    repeat rewrite <- assoc.
    apply maponpaths.
    repeat rewrite assoc.
    rewrite (nat_trans_ax β).
    apply idpath.
Qed.

Definition Flat_H : functor [C, C, hs] [C, C, hs] := tpair _ _ is_functor_Flat_H_data.

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

Definition App_θ_data: ∏ XZ, (θ_source(hs := hs) App_H)XZ --> (θ_target App_H)XZ.
Proof.
  intro XZ.
  apply nat_trans_id.
Defined.

Lemma is_nat_trans_App_θ_data: is_nat_trans _ _ App_θ_data.
Proof.
  red.
  unfold App_θ_data.
  intros XZ XZ' αβ.
  apply nat_trans_eq; try assumption.
  intro c.
  simpl.
  rewrite id_left.
  rewrite id_right.
  unfold binproduct_nat_trans_data, BinProduct_of_functors_mor.
  unfold BinProductOfArrows.
  eapply pathscomp0.
  apply precompWithBinProductArrow.
  simpl.
  unfold binproduct_nat_trans_pr1_data. unfold binproduct_nat_trans_pr2_data.
  simpl.
  apply BinProductArrowUnique.
  + rewrite BinProductPr1Commutes.
    repeat rewrite assoc.
    rewrite BinProductPr1Commutes.
    apply idpath.
  + rewrite BinProductPr2Commutes.
    repeat rewrite assoc.
    rewrite BinProductPr2Commutes.
    apply idpath.
Qed.

Definition App_θ: nat_trans (θ_source App_H) (θ_target App_H) :=
  tpair _ _ is_nat_trans_App_θ_data.

Lemma App_θ_strength1_int: θ_Strength1_int App_θ.
Proof.
  red.
  intro.
  unfold App_θ, App_H.
  simpl.
  unfold App_θ_data.
  apply nat_trans_eq; try assumption.
  intro c.
  simpl.
  rewrite id_left.
  unfold binproduct_nat_trans_data.
  apply pathsinv0.
  apply BinProductArrowUnique.
  + rewrite id_left.
    unfold UnitorsAndAssociatorsForEndofunctors.λ_functor.
    unfold UnitorsAndAssociatorsForEndofunctors.ρ_functor.
    simpl.
    rewrite id_right.
    apply idpath.
  + rewrite id_left.
    unfold UnitorsAndAssociatorsForEndofunctors.λ_functor.
    unfold UnitorsAndAssociatorsForEndofunctors.ρ_functor.
    simpl.
    rewrite id_right.
    apply idpath.
Qed.

Lemma App_θ_strength2_int: θ_Strength2_int App_θ.
Proof.
  red.
  intros.
  unfold App_θ, App_H.
  simpl.
  unfold App_θ_data.
  apply nat_trans_eq; try assumption.
  intro c.
  simpl.
  do 3 rewrite id_left.
  unfold binproduct_nat_trans_data.
  apply pathsinv0.
  apply BinProductArrowUnique.
  + rewrite id_left.
    unfold UnitorsAndAssociatorsForEndofunctors.α_functor.
    simpl.
    rewrite id_right.
    apply idpath.
  + rewrite id_left.
    unfold UnitorsAndAssociatorsForEndofunctors.α_functor.
    simpl.
    rewrite id_right.
    apply idpath.
Qed.

Definition Abs_θ_data_data: ∏ XZ A, ((θ_source(hs := hs) Abs_H)XZ: functor C C) A --> ((θ_target Abs_H)XZ: functor C C) A.
Proof.
  intro XZ.
  simpl.
  intro A.
  apply (functor_on_morphisms (functor_data_from_functor _ _ (pr1 XZ))).
  unfold BinCoproduct_of_functors_ob.
  unfold constant_functor.
  simpl.
  simpl.
  apply BinCoproductArrow.
  + exact (BinCoproductIn1 _ _ ·
           nat_trans_data_from_nat_trans (pr2 (pr2 XZ)) (BinCoproductObject C (CC (TerminalObject terminal) A))).
  + exact (# (pr1 (pr2 XZ)) (BinCoproductIn2 _ (CC (TerminalObject terminal) A))).
Defined.

Lemma is_nat_trans_Abs_θ_data_data: ∏ XZ, is_nat_trans _ _ (Abs_θ_data_data XZ).
Proof.

  intro XZ.
  intros c c' f.
  unfold Abs_θ_data_data.
  simpl.
  rewrite <- functor_comp.
  rewrite <- functor_comp.
  apply maponpaths.
  unfold BinCoproduct_of_functors_mor.
  eapply pathscomp0.
  apply precompWithBinCoproductArrow.
  eapply pathscomp0.
  2: apply (!(postcompWithBinCoproductArrow _ _ _ _ _)).
  simpl.
  rewrite id_left.
  rewrite <- assoc.
  rewrite <- functor_comp.
  rewrite <- functor_comp.
  simpl.
  apply BinCoproductArrow_eq.
  + 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.
    eapply pathscomp0.
    2: apply (!(BinCoproductOfArrowsIn2 _ _ _ _ _ )).
    apply idpath.

Qed.

Definition Abs_θ_data: ∏ XZ, (θ_source(hs := hs) Abs_H)XZ --> (θ_target Abs_H)XZ.
Proof.
  intro XZ.
  exact (tpair _ _ (is_nat_trans_Abs_θ_data_data XZ)).
Defined.

Lemma is_nat_trans_Abs_θ_data: is_nat_trans _ _ Abs_θ_data.
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; try assumption.
  intro c.
  simpl.
  simpl in ×.
  unfold constant_functor.
  unfold BinCoproduct_of_functors_ob.
  simpl.
  rewrite assoc.
  unfold Abs_θ_data_data. simpl.
  rewrite (nat_trans_ax α).
  do 2 rewrite <- assoc.
  apply maponpaths.
  do 2 rewrite <- functor_comp.
  apply maponpaths.
  unfold BinCoproduct_of_functors_mor, constant_functor_data.
  simpl.
  eapply pathscomp0. apply precompWithBinCoproductArrow.
  eapply pathscomp0.
  2: { eapply pathsinv0.
       apply postcompWithBinCoproductArrow. }


  apply BinCoproductArrow_eq.
  + rewrite id_left.
    rewrite <- assoc.
    rewrite <- (ptd_mor_commutes _ β).
    apply idpath.
  + simpl in ×.
    apply pathsinv0.
    apply (nat_trans_ax β).
Qed.

Definition Abs_θ: nat_trans (θ_source Abs_H) (θ_target Abs_H) :=
  tpair _ _ is_nat_trans_Abs_θ_data.

Lemma Abs_θ_strength1_int: θ_Strength1_int Abs_θ.
Proof.
  red.
  intro.
  unfold Abs_θ, Abs_H.
  simpl.
  unfold Abs_θ_data.
  apply nat_trans_eq; try assumption.
  intro c.
  simpl.
  rewrite id_right.
  apply functor_id_id.
  apply pathsinv0.
  apply BinCoproductArrowUnique.
  + apply idpath.
  + apply id_right.
Qed.

Lemma Abs_θ_strength2_int: θ_Strength2_int Abs_θ.
Proof.
  red.
  intros.
  unfold Abs_θ, Abs_H.
  simpl.
  unfold Abs_θ_data.
  apply nat_trans_eq; try assumption.
  intro c.
  simpl.
  rewrite id_left.
  rewrite id_right.
  unfold Abs_θ_data_data. simpl.
  rewrite <- functor_comp.
  apply maponpaths.
  clear X.
  destruct Z as [Z e];
  destruct Z' as [Z' e'];
  simpl.
  eapply pathscomp0.
  2: { eapply pathsinv0.
       apply postcompWithBinCoproductArrow. }
  simpl in ×.
  apply BinCoproductArrow_eq.
  + rewrite <- assoc.
    assert (NN := nat_trans_ax e' _ _ (e (BinCoproductObject C (CC (TerminalObject terminal) c)))).
    simpl in NN.     match goal with |[ H1: _ = ?f·?g |- ?h · _ = _ ] ⇒
         intermediate_path (h·(f·g)) end.
    × apply idpath.
    × simpl. rewrite <- NN.
      clear NN.
      assert (NNN := nat_trans_ax e' _ _ (BinCoproductArrow C (CC (TerminalObject terminal) (Z c))
         (BinCoproductIn1 C (CC (TerminalObject terminal) c)·
          e (BinCoproductObject C (CC (TerminalObject terminal) c)))
         (# Z (BinCoproductIn2 C (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.
        apply idpath.
      - apply idpath.
  + rewrite <- functor_comp.
    apply maponpaths.
    eapply pathscomp0.
    2: { eapply pathsinv0.
         apply BinCoproductIn2Commutes. }
    apply idpath.
Qed.

Definition Flat_θ_data: ∏ XZ, (θ_source(hs := hs) Flat_H)XZ --> (θ_target Flat_H)XZ.
Proof.
  intro XZ.
  set (h:= nat_trans_comp (λ_functor_inv (pr1 XZ)) ((nat_trans_id _) ∙∙ (pr2 (pr2 XZ)))).
  exact (nat_trans_comp (α_functor_inv (pr1 (pr2 XZ)) (pr1 XZ) (pr1 XZ)) (h ∙∙ (nat_trans_id (functor_composite (pr1 (pr2 XZ)) (pr1 XZ))))).
Defined.

Lemma is_nat_trans_Flat_θ_data: is_nat_trans _ _ Flat_θ_data.
Proof.
  red.
  intros XZ XZ' αβ.
  apply nat_trans_eq; try assumption.
  intro c.
  simpl.
  destruct XZ as [X [Z e]];
  destruct XZ' as [X' [Z' e']];
  destruct αβ as [α β];
  simpl in ×.
  repeat rewrite id_left.
  do 4 rewrite functor_id.
  do 2 rewrite id_right.
  repeat rewrite <- assoc.
  do 3 rewrite <- functor_comp.
  repeat rewrite assoc.
  rewrite (nat_trans_ax α).
  repeat rewrite <- assoc.
  apply maponpaths.
  rewrite <- functor_comp.
  apply maponpaths.
  repeat rewrite assoc.
  assert (β_is_pointed := ptd_mor_commutes _ β).
  simpl in β_is_pointed.
  rewrite β_is_pointed.
  simpl.
  eapply pathscomp0.
  2: apply (nat_trans_ax e').
  apply idpath.
Qed.

Definition Flat_θ: nat_trans (θ_source Flat_H) (θ_target Flat_H) :=
  tpair _ _ is_nat_trans_Flat_θ_data.

Lemma Flat_θ_strength1_int: θ_Strength1_int Flat_θ.
Proof.
  red.
  intro.
  unfold Flat_θ, Flat_H.
  simpl.
  apply nat_trans_eq; try assumption.
  intro c.
  simpl.
  repeat rewrite id_left.
  repeat rewrite functor_id.
  repeat rewrite id_left.
  apply idpath.
Qed.

Lemma Flat_θ_strength2_int: θ_Strength2_int Flat_θ.
Proof.
  red.
  intros.
  destruct Z as [Z e];
  destruct Z' as [Z' e'];
  simpl.
  apply nat_trans_eq; try assumption.
  intro c.
  simpl.
  repeat rewrite id_left.
  repeat rewrite <- functor_comp.
  apply maponpaths.
  repeat rewrite functor_id.
  repeat rewrite id_right.
  apply idpath.
Qed.

finally, constitute the 3 signatures

Definition App_Sig: Signature C hs C hs C hs.
Proof.
  ∃ App_H.
  ∃ App_θ.
  split.
  + exact App_θ_strength1_int.
  + exact App_θ_strength2_int.
Defined.

Definition Abs_Sig: Signature C hs C hs C hs.
Proof.
  ∃ Abs_H.
  ∃ Abs_θ.
  split.
  + exact Abs_θ_strength1_int.
  + exact Abs_θ_strength2_int.
Defined.

Definition Flat_Sig: Signature C hs C hs C hs.
Proof.
  ∃ Flat_H.
  ∃ Flat_θ.
  split.
  + exact Flat_θ_strength1_int.
  + exact Flat_θ_strength2_int.
Defined.

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

Lemma is_omega_cocont_Lam
  (hE : ∏ x, is_omega_cocont (constprod_functor1 (BinProducts_functor_precat C C CP hs) x))
  (LC : Colims_of_shape nat_graph C) : is_omega_cocont (Signature_Functor _ _ _ _ _ _ Lam_Sig).
Proof.
apply is_omega_cocont_BinCoproduct_of_functors.
- apply functor_category_has_homsets.
- apply (is_omega_cocont_App_H hE).
- apply (is_omega_cocont_Abs_H LC).
Defined.

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

End Lambda.