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.total2_paths.
Require Import UniMath.CategoryTheory.Categories.
Require Import UniMath.CategoryTheory.functor_categories.
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.EquivalencesExamples.
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, has_homsets_HSET].

Local Definition has_homsets_HSET2 : has_homsets HSET2.
Proof.
apply functor_category_has_homsets.
Defined.

Local Definition BinProductsHSET2 : BinProducts HSET2.
Proof.
apply (BinProducts_functor_precat _ _ BinProductsHSET).
Defined.

Local Definition BinCoproductsHSET2 : BinCoproducts HSET2.
Proof.
apply (BinCoproducts_functor_precat _ _ BinCoproductsHSET).
Defined.

Local Lemma Exponentials_HSET2 : Exponentials BinProductsHSET2.
Proof.
apply Exponentials_functor_HSET, has_homsets_HSET.
Defined.

Local Lemma InitialHSET2 : Initial HSET2.
Proof.
apply (Initial_functor_precat _ _ InitialHSET).
Defined.

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

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

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

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

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

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

The lambda calculus functor with one component for variables, one for application and one for abstraction/lambda
The lambda calculus
Definition LambdaCalculus : HSET2 :=
  alg_carrier _ (InitialObject lambdaFunctor_Initial).

Let LambdaCalculus_mor : HSET2lambdaFunctor LambdaCalculus,LambdaCalculus :=
  alg_map _ (InitialObject lambdaFunctor_Initial).

Let LambdaCalculus_alg : algebra_ob lambdaFunctor :=
  InitialObject lambdaFunctor_Initial.

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

Definition prod2 (x y : HSET2) : HSET2.
Proof.
apply BinProductsHSET2; [apply x | apply y].
Defined.

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

Definition app_map' (x : HSET) : HSET(pr1 LambdaCalculus x × pr1 LambdaCalculus x)%set,pr1 LambdaCalculus x.
Proof.
apply app_map.
Defined.

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

Definition lam_map : HSET2precomp_option LambdaCalculus,LambdaCalculus :=
  BinCoproductIn2 HSET2 (BinCoproductsHSET2 _ _) · BinCoproductIn2 HSET2 (BinCoproductsHSET2 _ _) · LambdaCalculus_mor.

Definition mk_lambdaAlgebra (X : HSET2) (fvar : HSET2functor_identity HSET,X)
  (fapp : HSET2prod2 X X,X) (flam : HSET2precomp_option X,X) : algebra_ob lambdaFunctor.
Proof.
apply (tpair _ X).
use (BinCoproductArrow _ _ fvar (BinCoproductArrow _ _ fapp flam)).
Defined.

Definition foldr_map (X : HSET2) (fvar : HSET2functor_identity HSET,X)
  (fapp : HSET2prod2 X X,X) (flam : HSET2precomp_option X,X) :
  algebra_mor lambdaFunctor LambdaCalculus_alg (mk_lambdaAlgebra X fvar fapp flam).
Proof.
apply (InitialArrow lambdaFunctor_Initial (mk_lambdaAlgebra X fvar fapp flam)).
Defined.

Definition foldr_map' (X : HSET2) (fvar : HSET2functor_identity HSET,X)
  (fapp : HSET2prod2 X X,X) (flam : HSET2precomp_option X,X) :
   HSET2 pr1 LambdaCalculus_alg, pr1 (mk_lambdaAlgebra X fvar fapp flam) .
Proof.
apply (foldr_map X fvar fapp flam).
Defined.

Lemma foldr_var (X : HSET2) (fvar : HSET2functor_identity HSET,X)
  (fapp : HSET2prod2 X X,X) (flam : HSET2precomp_option X,X) :
  var_map · foldr_map X fvar fapp flam = fvar.
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.
Defined.

Lemma foldr_app (X : HSET2) (fvar : HSET2functor_identity HSET,X)
  (fapp : HSET2prod2 X X,X) (flam : HSET2precomp_option X,X) :
  app_map · foldr_map X fvar fapp flam =
  # (pr1 (Id × Id)) (foldr_map X fvar fapp flam) · fapp.
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|].
Defined.

Lemma foldr_lam (X : HSET2) (fvar : HSET2functor_identity HSET,X)
  (fapp : HSET2prod2 X X,X) (flam : HSET2precomp_option X,X) :
  lam_map · foldr_map X fvar fapp flam =
  # (pr1 (_ o option)) (foldr_map X fvar fapp flam) · flam.
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|].
Defined.

End lambdacalculus.