Library UniMath.SubstitutionSystems.STLC

Syntax of the simply typed lambda calculus as a multisorted signature.
Written by: Anders Mörtberg, 2017

Require Import UniMath.Foundations.PartD.
Require Import UniMath.Foundations.Sets.

Require Import UniMath.MoreFoundations.Tactics.

Require Import UniMath.Combinatorics.Lists.

Require Import UniMath.CategoryTheory.Categories.
Require Import UniMath.CategoryTheory.functor_categories.
Require Import UniMath.CategoryTheory.categories.HSET.Core.
Require Import UniMath.CategoryTheory.categories.HSET.Colimits.
Require Import UniMath.CategoryTheory.categories.HSET.Limits.
Require Import UniMath.CategoryTheory.categories.HSET.Slice.
Require Import UniMath.CategoryTheory.Chains.Chains.
Require Import UniMath.CategoryTheory.Chains.OmegaCocontFunctors.
Require Import UniMath.CategoryTheory.limits.graphs.limits.
Require Import UniMath.CategoryTheory.limits.graphs.colimits.
Require Import UniMath.CategoryTheory.limits.initial.
Require Import UniMath.CategoryTheory.limits.binproducts.
Require Import UniMath.CategoryTheory.limits.products.
Require Import UniMath.CategoryTheory.limits.bincoproducts.
Require Import UniMath.CategoryTheory.limits.coproducts.
Require Import UniMath.CategoryTheory.limits.terminal.
Require Import UniMath.CategoryTheory.FunctorAlgebras.
Require Import UniMath.CategoryTheory.exponentials.
Require Import UniMath.CategoryTheory.whiskering.
Require Import UniMath.CategoryTheory.Monads.Monads.
Require Import UniMath.CategoryTheory.slicecat.

Require Import UniMath.SubstitutionSystems.Signatures.
Require Import UniMath.SubstitutionSystems.SumOfSignatures.
Require Import UniMath.SubstitutionSystems.BinProductOfSignatures.
Require Import UniMath.SubstitutionSystems.SubstitutionSystems.
Require Import UniMath.SubstitutionSystems.LiftingInitial_alt.
Require Import UniMath.SubstitutionSystems.MonadsFromSubstitutionSystems.
Require Import UniMath.SubstitutionSystems.Notation.
Local Open Scope subsys.
Require Import UniMath.SubstitutionSystems.SignatureExamples.
Require Import UniMath.SubstitutionSystems.BindingSigToMonad.
Require Import UniMath.SubstitutionSystems.MonadsMultiSorted.
Require Import UniMath.SubstitutionSystems.MultiSorted.

Local Open Scope cat.

The simply typed lambda calculus from a multisorted binding signature

Section Lam.

Variable (sort : hSet) (arr : sort sort sort).

A lot of notations, upstream?
Local Infix "::" := (@cons _).
Local Notation "[]" := (@nil _) (at level 0, format "[]").
Local Notation "C / X" := (slice_precat C X (homset_property C)).
Local Notation "a + b" := (setcoprod a b) : set.

Local Definition SET_over_sort : category.
Proof.
(SET / sort).
now apply has_homsets_slice_precat.
Defined.

Let hs : has_homsets (SET / sort) := homset_property SET_over_sort.
Let SET_over_sort2 := [SET/sort,SET_over_sort].

Local Lemma hs2 : has_homsets SET_over_sort2.
Proof.
apply functor_category_has_homsets.
Qed.

Local Lemma BinProducts_SET_over_sort2 : BinProducts SET_over_sort2.
Proof.
apply BinProducts_functor_precat, BinProducts_slice_precat, PullbacksHSET.
Defined.

Local Lemma Coproducts_SET_over_sort2 : Coproducts ((sort × sort) + (sort × sort))%set SET_over_sort2.
Proof.
apply Coproducts_functor_precat, Coproducts_slice_precat, CoproductsHSET.
apply setproperty.
Defined.

The signature of the simply typed lambda calculus
Definition STLC_Sig : MultiSortedSig sort.
Proof.
use mkMultiSortedSig.
- apply ((sort × sort) + (sort × sort))%set. - intros H; induction H as [st|st]; induction st as [s t].
  + exact ((([],,arr s t) :: ([],,s) :: nil),,t).
  + exact (((cons s [],,t) :: []),,arr s t).
Defined.

The signature with strength for the simply typed lambda calculus
Extract the constructors of the stlc from the initial algebra
The variables
The source of the application constructor
The application constructor
The source of the lambda constructor
Definition lam_source (s t : sort) (X : SET_over_sort2) : SET_over_sort2 :=
  (sorted_option_functor sort s X proj_functor sort t) hat_functor sort (arr s t).

Definition lam_map (s t : sort) : SET_over_sort2lam_source s t STLC,STLC :=
  (CoproductIn _ _ (Coproducts_functor_precat _ _ _ _ _ _) (ii2 (s,,t)))
    · BinCoproductIn2 _ (BinCoproducts_functor_precat _ _ _ _ _ _)
    · STLC_mor.

Definition mk_STLC_Algebra X (fvar : SET_over_sort21,X)
  (fapp : s t, SET_over_sort2app_source s t X,X)
  (flam : s t, SET_over_sort2lam_source s t X,X) :
    algebra_ob STLC_Functor.
Proof.
apply (tpair _ X).
use (BinCoproductArrow _ _ fvar).
use CoproductArrow.
intro b; induction b as [st|st]; induction st as [s t].
- apply (fapp s t).
- apply (flam s t).
Defined.

The recursor for the stlc
The equation for variables
Lemma foldr_var X (fvar : SET_over_sort21,X)
  (fapp : s t, SET_over_sort2app_source s t X,X)
  (flam : s t, SET_over_sort2lam_source s t X,X) :
  var_map · foldr_map X fvar fapp flam = fvar.
Proof.
assert (F := maponpaths (λ x, BinCoproductIn1 _ (BinCoproducts_functor_precat _ _ _ _ _ _) · 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.


End Lam.