Library UniMath.CategoryTheory.Inductives.LambdaCalculus

This file contains a direct formalization of the lambda calculus (LambdaCalculus) as the initial algebra of the lambda calculus functor. A better formalization where the lambda calculus and a substitution monad is obtained from a binding signature can be found in SubstitutionSystems/LamFromBindingSig.v.
Written by: Anders Mörtberg, 2016

Require Import UniMath.Foundations.PartD.
Require Import UniMath.Foundations.Propositions.
Require Import UniMath.Foundations.Sets.
Require Import UniMath.Foundations.NaturalNumbers.

Require Import UniMath.MoreFoundations.Tactics.

Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.FunctorCategory.
Require Import UniMath.CategoryTheory.limits.graphs.colimits.
Require Import UniMath.CategoryTheory.categories.HSET.Core.
Require Import UniMath.CategoryTheory.categories.HSET.Limits.
Require Import UniMath.CategoryTheory.categories.HSET.Colimits.
Require Import UniMath.CategoryTheory.categories.HSET.Structures.
Require Import UniMath.CategoryTheory.limits.initial.
Require Import UniMath.CategoryTheory.FunctorAlgebras.
Require Import UniMath.CategoryTheory.limits.binproducts.
Require Import UniMath.CategoryTheory.limits.bincoproducts.
Require Import UniMath.CategoryTheory.limits.terminal.
Require Import UniMath.CategoryTheory.limits.graphs.limits.
Require Import UniMath.CategoryTheory.PrecategoryBinProduct.
Require Import UniMath.CategoryTheory.Equivalences.Core.
Require Import UniMath.CategoryTheory.Adjunctions.Examples.
Require Import UniMath.CategoryTheory.Chains.All.
Require Import UniMath.CategoryTheory.exponentials.
Require Import UniMath.CategoryTheory.whiskering.

Local Open Scope cat.

Local Notation "'chain'" := (diagram nat_graph).

Section lambdacalculus.

Local Notation "'HSET2'":= [HSET, HSET].


Local Definition BinProductsHSET2 : BinProducts HSET2.
Show proof.
apply (BinProducts_functor_precat _ _ BinProductsHSET).

Local Definition BinCoproductsHSET2 : BinCoproducts HSET2.
Show proof.
apply (BinCoproducts_functor_precat _ _ BinCoproductsHSET).

Local Lemma Exponentials_HSET2 : Exponentials BinProductsHSET2.
Show proof.
apply Exponentials_functor_HSET.

Local Lemma InitialHSET2 : Initial HSET2.
Show proof.
apply (Initial_functor_precat _ _ InitialHSET).

Local Definition CCHSET : Colims_of_shape nat_graph HSET :=
  ColimsHSET_of_shape nat_graph.

Local Notation "' x" := (omega_cocont_constant_functor x)
                          (at level 10).

Local Notation "'Id'" := (omega_cocont_functor_identity _).

Local Notation "F * G" :=
  (omega_cocont_BinProduct_of_functors_alt BinProductsHSET2 _
     (is_omega_cocont_constprod_functor1 _ Exponentials_HSET2) F G).

Local Notation "F + G" :=
  (omega_cocont_BinCoproduct_of_functors BinCoproductsHSET2 F G).

Local Notation "'_' 'o' 'option'" :=
  (omega_cocont_pre_composition_functor
      (option_functor BinCoproductsHSET TerminalHSET)
      CCHSET) (at level 10).

The lambda calculus functor with one component for variables, one for application and one for abstraction/lambda
Definition lambdaOmegaFunctor : omega_cocont_functor HSET2 HSET2 :=
  omega_cocont_constant_functor (C:= [_,_]) (D:=[_,_])(functor_identity HSET) +
                                        (Id * Id + _ o option).


Let lambdaFunctor : functor HSET2 HSET2 := pr1 lambdaOmegaFunctor.
Let is_omega_cocont_lambdaFunctor : is_omega_cocont lambdaFunctor :=
  pr2 lambdaOmegaFunctor.

Lemma lambdaFunctor_Initial :
  Initial (category_FunctorAlg lambdaFunctor).
Show proof.
apply (colimAlgInitial InitialHSET2 is_omega_cocont_lambdaFunctor).
apply ColimsFunctorCategory_of_shape; apply ColimsHSET_of_shape.

The lambda calculus
Definition LambdaCalculus : HSET2 :=
  alg_carrier _ (InitialObject lambdaFunctor_Initial).

Let LambdaCalculus_mor : HSET2⟦lambdaFunctor LambdaCalculus,LambdaCalculus⟧ :=
  alg_map _ (InitialObject lambdaFunctor_Initial).

Let LambdaCalculus_alg : algebra_ob lambdaFunctor :=
  InitialObject lambdaFunctor_Initial.

Definition var_map : HSET2⟦functor_identity HSET,LambdaCalculus⟧ :=
  BinCoproductIn1 (BinCoproductsHSET2 _ _) · LambdaCalculus_mor.

Definition prod2 (x y : HSET2) : HSET2.
Show proof.
apply BinProductsHSET2; [apply x | apply y].

Definition app_map : HSET2⟦prod2 LambdaCalculus LambdaCalculus,LambdaCalculus⟧ :=
  BinCoproductIn1 (BinCoproductsHSET2 _ _) · BinCoproductIn2 (BinCoproductsHSET2 _ _) · LambdaCalculus_mor.

Definition app_map' (x : HSET) : HSET⟦(pr1 LambdaCalculus x × pr1 LambdaCalculus x)%set,pr1 LambdaCalculus x⟧.
Show proof.
apply app_map.

Let precomp_option X := (pre_composition_functor _ _ HSET
                          (option_functor BinCoproductsHSET TerminalHSET) X).

Definition lam_map : HSET2⟦precomp_option LambdaCalculus,LambdaCalculus⟧ :=
  BinCoproductIn2 (BinCoproductsHSET2 _ _) · BinCoproductIn2 (BinCoproductsHSET2 _ _) · LambdaCalculus_mor.

Definition make_lambdaAlgebra (X : HSET2) (fvar : HSET2⟦functor_identity HSET,X⟧)
  (fapp : HSET2⟦prod2 X X,X⟧) (flam : HSET2⟦precomp_option X,X⟧) : algebra_ob lambdaFunctor.
Show proof.
apply (tpair _ X).
use (BinCoproductArrow _ fvar (BinCoproductArrow _ fapp flam)).

Definition foldr_map (X : HSET2) (fvar : HSET2⟦functor_identity HSET,X⟧)
  (fapp : HSET2⟦prod2 X X,X⟧) (flam : HSET2⟦precomp_option X,X⟧) :
  algebra_mor lambdaFunctor LambdaCalculus_alg (make_lambdaAlgebra X fvar fapp flam).
Show proof.
apply (InitialArrow lambdaFunctor_Initial (make_lambdaAlgebra X fvar fapp flam)).

Definition foldr_map' (X : HSET2) (fvar : HSET2⟦functor_identity HSET,X⟧)
  (fapp : HSET2⟦prod2 X X,X⟧) (flam : HSET2⟦precomp_option X,X⟧) :
   HSET2 ⟦ pr1 LambdaCalculus_alg, pr1 (make_lambdaAlgebra X fvar fapp flam) ⟧.
Show proof.
apply (foldr_map X fvar fapp flam).

Lemma foldr_var (X : HSET2) (fvar : HSET2⟦functor_identity HSET,X⟧)
  (fapp : HSET2⟦prod2 X X,X⟧) (flam : HSET2⟦precomp_option X,X⟧) :
  var_map · foldr_map X fvar fapp flam = fvar.
Show proof.
assert (F := maponpaths (λ x, BinCoproductIn1 (BinCoproductsHSET2 _ _) · x)
                        (algebra_mor_commutes _ _ _ (foldr_map X fvar fapp flam))).
rewrite assoc in F.
eapply pathscomp0; [apply F|].
rewrite assoc.
eapply pathscomp0; [eapply cancel_postcomposition, BinCoproductOfArrowsIn1|].
rewrite <- assoc.
eapply pathscomp0; [eapply maponpaths, BinCoproductIn1Commutes|].
apply id_left.

Lemma foldr_app (X : HSET2) (fvar : HSET2⟦functor_identity HSET,X⟧)
  (fapp : HSET2⟦prod2 X X,X⟧) (flam : HSET2⟦precomp_option X,X⟧) :
  app_map · foldr_map X fvar fapp flam =
  # (pr1 (Id * Id)) (foldr_map X fvar fapp flam) · fapp.
Show proof.
assert (F := maponpaths (λ x, BinCoproductIn1 (BinCoproductsHSET2 _ _) · BinCoproductIn2 (BinCoproductsHSET2 _ _) · x)
                        (algebra_mor_commutes _ _ _ (foldr_map X fvar fapp flam))).
rewrite assoc in F.
eapply pathscomp0; [apply F|].
rewrite assoc.
eapply pathscomp0.
  eapply cancel_postcomposition.
  rewrite <- assoc.
  eapply maponpaths, BinCoproductOfArrowsIn2.
rewrite assoc.
eapply pathscomp0.
  eapply cancel_postcomposition, cancel_postcomposition, BinCoproductOfArrowsIn1.
rewrite <- assoc.
eapply pathscomp0; [eapply maponpaths, BinCoproductIn2Commutes|].
rewrite <- assoc.
now eapply pathscomp0; [eapply maponpaths, BinCoproductIn1Commutes|].

Lemma foldr_lam (X : HSET2) (fvar : HSET2⟦functor_identity HSET,X⟧)
  (fapp : HSET2⟦prod2 X X,X⟧) (flam : HSET2⟦precomp_option X,X⟧) :
  lam_map · foldr_map X fvar fapp flam =
  # (pr1 (_ o option)) (foldr_map X fvar fapp flam) · flam.
Show proof.
assert (F := maponpaths (λ x, BinCoproductIn2 (BinCoproductsHSET2 _ _) · BinCoproductIn2 (BinCoproductsHSET2 _ _) · x)
                        (algebra_mor_commutes _ _ _ (foldr_map X fvar fapp flam))).
rewrite assoc in F.
eapply pathscomp0; [apply F|].
rewrite assoc.
eapply pathscomp0.
  eapply cancel_postcomposition.
  rewrite <- assoc.
  eapply maponpaths, BinCoproductOfArrowsIn2.
rewrite assoc.
eapply pathscomp0.
  eapply cancel_postcomposition, cancel_postcomposition, BinCoproductOfArrowsIn2.
rewrite <- assoc.
eapply pathscomp0.
  eapply maponpaths, BinCoproductIn2Commutes.
rewrite <- assoc.
now eapply pathscomp0; [eapply maponpaths, BinCoproductIn2Commutes|].

End lambdacalculus.