Library UniMath.SubstitutionSystems.CCS

Syntax of the calculus of constructions as in Streicher "Semantics of Type Theory" formalized as a multisorted binding 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.StandardFiniteSets.
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.

Section ccs.

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.

Definition six_rec {A : UU} (a b c d e f : A) : stn 6 A.
Proof.
induction 1 as [n p].
induction n as [|n _]; [apply a|].
induction n as [|n _]; [apply b|].
induction n as [|n _]; [apply c|].
induction n as [|n _]; [apply d|].
induction n as [|n _]; [apply e|].
induction n as [|n _]; [apply f|].
induction (nopathsfalsetotrue p).
Defined.

We assume a two element set of sorts
Definition sort : hSet := @tpair _ (λ X, isaset X) bool isasetbool.

Definition ty : sort := true.
Definition el : sort := false.

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.

The grammar of expressions and objects from page 157:
E ::= (Πx:E) E                product of types
    | Prop                    type of propositions
    | Proof(t)                type of proofs of proposition t

t ::= x                       variable
    | (λx:E) t                function abstraction
    | App([x:E] E, t, t)      function application
    | (∀x:E) t                universal quantification
We refer to the first syntactic class as ty and the second as el. We first reformulate the rules as follows:
A,B ::= Π(A,x.B)              product of types
      | Prop                  type of propositions
      | Proof(t)              type of proofs of proposition t

t,u ::= x                     variable
      | λ(A,x.t)              function abstraction
      | App(A,x.B,t,u)        function application
      | ∀(A,x.t)              universal quantification
This grammar then gives 6 operations, to the left as Vladimir's restricted 2-sorted signature (where el is 0 and ty is 1) and to the right as a multisorted signature:
((0, 1), (1, 1), 1) = ((,ty), (el, ty), ty) (1) = (,ty) ((0, 0), 1) = ((, el), ty) ((0, 1), (1, 0), 0) = ((, ty), (el, el), el) ((0, 1), (1, 1), (0, 0), (0, 0), 0) = ((, ty), (el, ty), (, el), (, el), el) ((0, 1), (1, 0), 0) = ((, ty), (el, el), el)
The multisorted signature of CC-S
Extract the constructors from the initial algebra
The variables
The Pi constructor
The Proof constructor
The lambda constructor
The app constructor
The ∀ constructor
Definition forall_map : SET_over_sort2forall_source CCS,CCS :=
  (CoproductIn _ _ (Coproducts_functor_precat _ _ _ _ _ _) ( 5)%stn)
    · (BinCoproductIn2 _ (BinCoproducts_functor_precat _ _ _ _ _ _))
    · CCS_mor.

Definition mk_CCS_Algebra X
  (fvar : SET_over_sort2Id,X)
  (fPi : SET_over_sort2Pi_source X,X)
  (fProp : SET_over_sort2Prop_source X,X)
  (fProof : SET_over_sort2Proof_source X,X)
  (flam : SET_over_sort2lam_source X,X)
  (fapp : SET_over_sort2app_source X,X)
  (fforall : SET_over_sort2forall_source X,X) : algebra_ob CCS_Functor.
Proof.
apply (tpair _ X).
use (BinCoproductArrow _ _ fvar).
use CoproductArrow.
intros i.
induction i as [n p].
repeat (induction n as [|n _]; try induction (nopathsfalsetotrue p)).
- exact fPi.
- exact fProp.
- exact fProof.
- exact flam.
- simpl in fapp.
  exact fapp.
- exact fforall.
Defined.
The recursor for ccs