Library UniMath.SubstitutionSystems.MultiSorted

This file contains a fomalization of multisorted binding signatures:
  • Definition of multisorted binding signatures (MultiSortedSig)
  • Construction of a functor from a multisorted binding signature (MultiSortedSigToFunctor)
  • Construction of signature with strength from a multisorted binding signature (MultiSortedSigToSignature)
  • Proof that the functor obtained from a multisorted binding signature is omega-cocontinuous (is_omega_cocont_MultiSortedSigToFunctor)
  • Construction of a monad on Set/sort from a multisorterd signature (MultiSortedSigToMonad)
Written by: Anders Mörtberg, 2016. The formalization follows a note written by Benedikt Ahrens and Ralph Matthes, and is also inspired by discussions with them and Vladimir Voevodsky.
Strength calculation added by Ralph Matthes, 2017.
In the end of the file there is a module with an alternative version using X,SET instead of SET/X. There is no proof that the functor we obtain using this approach is omega-cocontinuous yet.

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

Require Import UniMath.MoreFoundations.Tactics.

Require Import UniMath.Combinatorics.Lists.

Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Isos.
Require Import UniMath.CategoryTheory.Core.NaturalTransformations.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.FunctorCategory.
Require Import UniMath.CategoryTheory.whiskering.
Require Import UniMath.CategoryTheory.limits.graphs.limits.
Require Import UniMath.CategoryTheory.limits.graphs.colimits.
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.limits.initial.
Require Import UniMath.CategoryTheory.limits.pullbacks.
Require Import UniMath.CategoryTheory.FunctorAlgebras.
Require Import UniMath.CategoryTheory.exponentials.
Require Import UniMath.CategoryTheory.Adjunctions.Core.
Require Import UniMath.CategoryTheory.Chains.All.
Require Import UniMath.CategoryTheory.Monads.Monads.
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.categories.HSET.Structures.
Require Import UniMath.CategoryTheory.HorizontalComposition.
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.

Local Open Scope cat.

Local Notation "C / X" := (slicecat_ob C X).
Local Notation "C / X" := (slice_precat_data C X).
Local Notation "C / X" := (slice_precat C X (homset_property C)).
Local Notation "C / X ⟦ a , b ⟧" := (slicecat_mor C X a b) (at level 50, format "C / X ⟦ a , b ⟧").

Arguments post_composition_functor {_ _ _} _ _ _.
Arguments pre_composition_functor {_ _ _} _ _ _.
Arguments Gθ_Signature {_ _ _ _ _ _} _ _.
Arguments Signature_Functor {_ _ _ _} _.
Arguments BinProduct_of_functors {_ _} _ _ _.
Arguments DL_comp {_ _ _} _ {_} _.
Arguments θ_from_δ_Signature {_ _ _} _.
Arguments BinProduct_of_Signatures {_ _ _ _} _ _ _.
Arguments Sum_of_Signatures _ {_ _ _ _} _ _.

Definition of multisorted binding signatures

Section MBindingSig.

Variables (sort : hSet).

Local Definition SET_over_sort : category.
Show proof.
exists (SET / sort).
now apply has_homsets_slice_precat.

Let hs : has_homsets (SET / sort) := homset_property SET_over_sort.

Let BC := BinCoproducts_slice_precat has_homsets_HSET BinCoproductsHSET sort: BinCoproducts (SET / sort).

Definition of multi sorted signatures
Definition MultiSortedSig : UU :=
  ∑ (I : hSet), I → list (list sort × sort) × sort.

Definition ops (M : MultiSortedSig) : hSet := pr1 M.
Definition arity (M : MultiSortedSig) : ops M → list (list sort × sort) × sort :=
  λ x, pr2 M x.

Definition mkMultiSortedSig {I : hSet}
  (ar : I → list (list sort × sort) × sort) : MultiSortedSig := (I,,ar).

Construction of an endofunctor on SET/sort,SET/sort from a multisorted signature

Section functor.

Local Definition proj_fun (s : sort) : SET / sort -> SET :=
  λ p, hfiber_hSet (pr2 p) s.

Definition proj_functor (s : sort) : functor (SET / sort) SET.
Show proof.
use tpair.
- exists (proj_fun s).
  intros X Y f p.
  exists (pr1 f (pr1 p)).
  abstract (now induction f as [h hh]; induction p as [x hx]; simpl in *; rewrite <- hx, hh).
- abstract (split; [intros X|intros X Y Z f g];
            apply funextsec; intro p; apply subtypeEquality; trivial;
            intros x; apply setproperty).

The left adjoint to the proj_functor
Definition hat_functor (t : sort) : functor SET (SET / sort).
Show proof.
use tpair.
- use tpair.
  + intro A; apply (A,,λ _, t).
  + intros A B f; apply (tpair _ f), idpath.
- abstract (now split; [intros A|intros A B C f g];
            apply subtypeEquality; try (intro x; apply has_homsets_HSET)).

Local Definition constHSET_slice := constHSET_slice sort.

Local Definition sorted_option_functor := sorted_option_functor sort.

Sorted option functor for lists (also called option in the note)
Local Definition option_list (xs : list sort) : functor (SET / sort) (SET / sort).
Show proof.
use (foldr1 (λ F G, F ∙ G) (functor_identity _) (map sorted_option_functor xs)).

Define a functor
F^(l,t)(X) := proj_functor(t) ∘ X ∘ option_functor(l)
if l is nonempty and
F^(l,t)(X) := proj_functor(t) ∘ X
otherwise
Definition exp_functor (lt : list sort × sort) :
  functor [SET_over_sort,SET_over_sort] [SET_over_sort,SET].
Show proof.
induction lt as [l t].
use (list_ind _ _ _ l); clear l.
- exact (post_composition_functor _ _ (proj_functor t)).
- intros s l _; simpl.
  eapply functor_composite.
  + exact (pre_composition_functor hs hs (option_list (cons s l))).
  + exact (post_composition_functor _ has_homsets_HSET (proj_functor t)).

This defines F^lts where lts is a list of (l,t). Outputs a product of functors if the list is nonempty and otherwise the constant functor.
Local Definition exp_functor_list (xs : list (list sort × sort)) :
  functor [SET_over_sort,SET_over_sort] [SET_over_sort,SET].
Show proof.
set (T := constant_functor [SET_over_sort,SET_over_sort] [SET_over_sort,SET]
                           (constant_functor SET_over_sort HSET TerminalHSET)).
set (XS := map exp_functor xs).
use (foldr1 (λ F G, BinProduct_of_functors _ F G) T XS).
apply BinProducts_functor_precat, BinProductsHSET.

Local Definition hat_exp_functor_list (xst : list (list sort × sort) × sort) :
  functor [SET_over_sort,SET_over_sort] [SET_over_sort,SET_over_sort] :=
    exp_functor_list (pr1 xst) ∙ post_composition_functor _ _ (hat_functor (pr2 xst)).

The function from multisorted signatures to functors
Definition MultiSortedSigToFunctor (M : MultiSortedSig) :
  functor [SET_over_sort,SET_over_sort] [SET_over_sort,SET_over_sort].
Show proof.
use (coproduct_of_functors (ops M)).
+ apply Coproducts_functor_precat, Coproducts_slice_precat, CoproductsHSET, setproperty.
+ intros op.
  exact (hat_exp_functor_list (arity M op)).

End functor.

Construction of the strength for the endofunctor on SET/sort,SET/sort derived from a

multisorted signature
Section strength.

Local Definition DL_sorted_option_functor (s : sort) :
  DistributiveLaw _ hs (sorted_option_functor s) :=
    genoption_DistributiveLaw _ hs (constHSET_slice s)(BinCoproducts_HSET_slice sort).

Local Definition DL_option_list (xs : list sort) :
  DistributiveLaw _ hs (option_list xs).
Show proof.
induction xs as [[|n] xs].
+ induction xs.
  apply DL_id.
+ induction n as [|n IH].
  * induction xs as [m []].
    apply DL_sorted_option_functor.
  * induction xs as [m [k xs]].
    apply (DL_comp (DL_sorted_option_functor m) (IH (k,,xs))).

Local Definition Sig_exp_functor (lt : list sort × sort) :
  Signature _ hs _ has_homsets_HSET.
Show proof.
exists (exp_functor lt).
induction lt as [l t].
induction l as [[|n] xs].
+ induction xs.
  exact (pr2 (Gθ_Signature (IdSignature _ _) (proj_functor t))).
+ induction n as [|n IH].
  * induction xs as [m []].
    set (Sig_option_list := θ_from_δ_Signature (DL_option_list (cons m (0,,tt)))).
    exact (pr2 (Gθ_Signature Sig_option_list (proj_functor t))).
  * induction xs as [m xs].
    set (Sig_option_list := θ_from_δ_Signature (DL_option_list (cons m (S n,,xs)))).
    exact (pr2 (Gθ_Signature Sig_option_list (proj_functor t))).

Local Lemma functor_in_Sig_exp_functor_ok (lt : list sort × sort) :
  Signature_Functor (Sig_exp_functor lt) = exp_functor lt.
Show proof.
apply idpath.

Local Definition Sig_exp_functor_list (xs : list (list sort × sort)) :
  Signature _ hs _ has_homsets_HSET.
Show proof.
exists (exp_functor_list xs).
induction xs as [[|n] xs].
- induction xs.
  exact (pr2 (ConstConstSignature SET_over_sort SET TerminalHSET)).
- induction n as [|n IH].
  + induction xs as [m []].
    exact (pr2 (Sig_exp_functor m)).
  + induction xs as [m [k xs]].
    exact (pr2 (BinProduct_of_Signatures _ (Sig_exp_functor _) (tpair _ _ (IH (k,,xs))))).

Local Lemma functor_in_Sig_exp_functor_list_ok (xs : list (list sort × sort)) :
  Signature_Functor (Sig_exp_functor_list xs) = exp_functor_list xs.
Show proof.
apply idpath.

Local Definition Sig_hat_exp_functor_list (xst : list (list sort × sort) × sort) :
  Signature _ hs _ hs.
Show proof.
apply (Gθ_Signature (Sig_exp_functor_list (pr1 xst)) (hat_functor (pr2 xst))).

Local Lemma functor_in_Sig_hat_exp_functor_list_ok (xst : list (list sort × sort) × sort) :
  Signature_Functor (Sig_hat_exp_functor_list xst) = hat_exp_functor_list xst.
Show proof.
apply idpath.

Definition MultiSortedSigToSignature (M : MultiSortedSig) : Signature _ hs _ hs.
Show proof.
set (Hyps := λ (op : ops M), Sig_hat_exp_functor_list (arity M op)).
use (Sum_of_Signatures (ops M) _ Hyps).
apply Coproducts_slice_precat, CoproductsHSET, setproperty.

Local Lemma functor_in_MultiSortedSigToSignature_ok (M : MultiSortedSig) :
  Signature_Functor (MultiSortedSigToSignature M) = MultiSortedSigToFunctor M.
Show proof.
apply idpath.

End strength.

Proof that the functor obtained from a multisorted signature is omega-cocontinuous

Section omega_cocont.

The proj functor is naturally isomorphic to the following functor which is a left adjoint:
Local Definition proj_functor' (s : sort) : functor (SET / sort) SET :=
  functor_composite
     (constprod_functor1 (BinProducts_HSET_slice sort) (constHSET_slice s))
     (slicecat_to_cat has_homsets_HSET sort).

Local Lemma nat_trans_proj_functor (s : sort) : nat_trans (proj_functor' s) (proj_functor s).
Show proof.
use mk_nat_trans.
- simpl; intros x H.
  exists (pr2 (pr1 H)).
  apply (!pr2 H).
- intros x y f.
  apply funextsec; intro w.
  apply subtypeEquality; trivial.
  intro z; apply setproperty.

Local Lemma is_iso_nat_trans_proj_functor (s : sort) :
  @is_iso [SET/sort,SET] _ _ (nat_trans_proj_functor s).
Show proof.
use is_iso_qinv.
+ use mk_nat_trans.
  - simpl; intros x xy.
    exists (tt,,pr1 xy).
    apply (!pr2 xy).
  - abstract (intros X Y f; apply funextsec; intros x;
              apply subtypeEquality; trivial; intros w; apply setproperty).
+ abstract (split;
  [ apply subtypeEquality; [intros x; apply isaprop_is_nat_trans, has_homsets_HSET|];
    apply funextsec; intro x; apply funextsec; intro y; cbn;
    now rewrite pathsinv0inv0; induction y as [y' y3]; induction y' as [y'' y2]; induction y''
  | apply (nat_trans_eq has_homsets_HSET); simpl; intros x;
    apply funextsec; intros z; simpl in *;
    now apply subtypeEquality; trivial; intros w; apply setproperty]).

Local Lemma is_left_adjoint_proj_functor' (s : sort) : is_left_adjoint (proj_functor' s).
Show proof.
use is_left_adjoint_functor_composite.
- apply Exponentials_HSET_slice.
- apply is_left_adjoint_slicecat_to_cat_HSET.

Local Lemma is_left_adjoint_proj_functor (s : sort) : is_left_adjoint (proj_functor s).
Show proof.
apply (is_left_adjoint_iso _ _ _ (_,,is_iso_nat_trans_proj_functor s)).
apply is_left_adjoint_proj_functor'.

Local Lemma is_omega_cocont_post_comp_proj (s : sort) :
  is_omega_cocont (@post_composition_functor (SET/sort) _ _ hs has_homsets_HSET (proj_functor s)).
Show proof.
apply is_omega_cocont_post_composition_functor.
apply is_left_adjoint_proj_functor.

The hat_functor is left adjoint to proj_functor
Local Lemma is_left_adjoint_hat (s : sort) : is_left_adjoint (hat_functor s).
Show proof.
exists (proj_functor s).
use mk_are_adjoints.
+ use mk_nat_trans.
  - intros X; simpl; intros x; apply (x,,idpath s).
  - intros X Y f; simpl; apply funextsec; intro x; cbn.
    now apply subtypeEquality; trivial; intros y; apply setproperty.
+ use mk_nat_trans.
  - intros X; simpl in *.
    use tpair; simpl.
    * intros H; apply (pr1 H).
    * abstract (apply funextsec; intro x; apply (! pr2 x)).
  - now intros X Y f; apply (eq_mor_slicecat has_homsets_HSET).
+ split.
  - now intros X; apply (eq_mor_slicecat has_homsets_HSET).
  - intros X; apply funextsec; intro x.
    now apply subtypeEquality; trivial; intros x'; apply setproperty.

Local Lemma is_omega_cocont_exp_functor (a : list sort × sort)
  (H : Colims_of_shape nat_graph SET_over_sort) :
  is_omega_cocont (exp_functor a).
Show proof.
induction a as [xs t].
induction xs as [[|n] xs].
- induction xs.
  apply is_omega_cocont_post_comp_proj.
- induction n as [|n].
  + induction xs as [m []].
    use is_omega_cocont_functor_composite.
    * apply functor_category_has_homsets.
    * apply is_omega_cocont_pre_composition_functor, H.
    * apply is_omega_cocont_post_comp_proj.
  + induction xs as [m k]; simpl.
    use (@is_omega_cocont_functor_composite _ _ _ _ (ℓ (option_list _))).
    * apply (functor_category_has_homsets (SET / sort) HSET has_homsets_HSET).
    * apply is_omega_cocont_pre_composition_functor, H.
    * apply is_omega_cocont_post_comp_proj.

Local Lemma is_omega_cocont_exp_functor_list (xs : list (list sort × sort))
  (H : Colims_of_shape nat_graph SET_over_sort) :
  is_omega_cocont (exp_functor_list xs).
Show proof.
induction xs as [[|n] xs].
- induction xs.
  apply is_omega_cocont_constant_functor, functor_category_has_homsets.
- induction n as [|n IHn].
  + induction xs as [m []].
    apply is_omega_cocont_exp_functor, H.
  + induction xs as [m [k xs]].
    apply is_omega_cocont_BinProduct_of_functors; try apply homset_property.
    * apply BinProducts_functor_precat, BinProducts_slice_precat, PullbacksHSET.
    * apply is_omega_cocont_constprod_functor1; try apply functor_category_has_homsets.
      apply Exponentials_functor_HSET, homset_property.
    * apply is_omega_cocont_exp_functor, H.
    * apply (IHn (k,,xs)).

Local Lemma is_omega_cocont_post_comp_hat_functor (s : sort) :
  is_omega_cocont (@post_composition_functor SET_over_sort _ _
       (homset_property SET) hs (hat_functor s)).
Show proof.
apply is_omega_cocont_post_composition_functor, is_left_adjoint_hat.

Local Lemma is_omega_cocont_hat_exp_functor_list (xst : list (list sort × sort) × sort)
  (H : Colims_of_shape nat_graph SET_over_sort) :
  is_omega_cocont (hat_exp_functor_list xst).
Show proof.
apply is_omega_cocont_functor_composite.
+ apply functor_category_has_homsets.
+ apply is_omega_cocont_exp_functor_list, H.
+ apply is_omega_cocont_post_comp_hat_functor.

The functor obtained from a multisorted binding signature is omega-cocontinuous
Lemma is_omega_cocont_MultiSortedSigToFunctor (M : MultiSortedSig)
  (H : Colims_of_shape nat_graph SET_over_sort) :
  is_omega_cocont (MultiSortedSigToFunctor M).
Show proof.
apply is_omega_cocont_coproduct_of_functors; try apply homset_property.
intros op; apply is_omega_cocont_hat_exp_functor_list, H.

Lemma is_omega_cocont_MultiSortedSigToSignature
  (M : MultiSortedSig) (H : Colims_of_shape nat_graph SET_over_sort) :
  is_omega_cocont (MultiSortedSigToSignature M).
Show proof.
apply is_omega_cocont_MultiSortedSigToFunctor, H.

End omega_cocont.

Construction of a monad from a multisorted signature

Section monad.

Let Id_H := Id_H (SET / sort) hs (BinCoproducts_HSET_slice sort).

Local Lemma has_homsets_SetSort2 : has_homsets [SET/sort,(SET/sort,,hs)].
Show proof.
apply homset_property.

Let FunctorAlg F := FunctorAlg F has_homsets_SetSort2.

Definition SignatureInitialAlgebraSetSort
  (H : Signature _ hs _ hs) (Hs : is_omega_cocont H) :
  Initial (FunctorAlg (Id_H H)).
Show proof.
use colimAlgInitial.
- apply Initial_functor_precat, Initial_slice_precat, InitialHSET.
- apply (is_omega_cocont_Id_H), Hs.
- apply ColimsFunctorCategory_of_shape, slice_precat_colims_of_shape,
        ColimsHSET_of_shape.

Let HSS := @hss_precategory _ hs (BinCoproducts_HSET_slice sort).

Definition MultiSortedSigToHSS (sig : MultiSortedSig) :
  HSS (MultiSortedSigToSignature sig).
Show proof.
apply SignatureToHSS.
+ apply Initial_slice_precat, InitialHSET.
+ apply slice_precat_colims_of_shape, ColimsHSET_of_shape.
+ apply is_omega_cocont_MultiSortedSigToSignature.
  apply slice_precat_colims_of_shape, ColimsHSET_of_shape.

Definition MultiSortedSigToHSSisInitial (sig : MultiSortedSig) :
  isInitial _ (MultiSortedSigToHSS sig).
Show proof.
now unfold MultiSortedSigToHSS, SignatureToHSS; destruct InitialHSS.

Function from multisorted binding signatures to monads

Definition MultiSortedSigToMonad (sig : MultiSortedSig) : Monad (SET / sort).
Show proof.
use Monad_from_hss.
- apply hs.
- apply BinCoproducts_HSET_slice.
- apply (MultiSortedSigToSignature sig).
- apply MultiSortedSigToHSS.

End monad.
End MBindingSig.

Alternative version using X,SET instead of SET/X below. There is no proof that the functor we obtain using this approach is omega-cocontinuous yet.
Require UniMath.CategoryTheory.categories.StandardCategories.
Require UniMath.CategoryTheory.Adjunctions.Examples.

Module alt.

Import UniMath.CategoryTheory.Groupoids.
Import UniMath.CategoryTheory.categories.StandardCategories.
Import UniMath.CategoryTheory.Adjunctions.Examples.

Definition of multisorted binding signatures

Section MBindingSig.

Variables (sort : UU) (eq : isdeceq sort). Variables (C : category) (BP : BinProducts C) (BC : BinCoproducts C) (TC : Terminal C).

Define the discrete category of sorts
Let sort_cat : precategory := path_pregroupoid sort.

Let hsC : has_homsets C := homset_property C.

This represents "sort → C"
Let sortToC : category := [sort_cat,C].

Local Lemma has_homsets_sortToC : has_homsets sortToC.
Show proof.
apply homset_property.

Local Definition BinProductsSortToCToC : BinProducts [sortToC,C].
Show proof.
apply (BinProducts_functor_precat _ _ BP).

Local Definition mk_sortToC (f : sort → C) : sortToC := functor_path_pregroupoid f.

Local Definition proj_gen_fun (D : precategory) (E : category) (d : D) : functor [D,E] E.
Show proof.
use tpair.
+ use tpair.
  - intro f; apply (pr1 f d).
  - simpl; intros a b f; apply (f d).
+ abstract (split; [intro f; apply idpath|intros f g h fg gh; apply idpath]).

Local Definition proj_gen {D : precategory} {E : category} : functor D [[D,E],E].
Show proof.
use tpair.
+ use tpair.
  - apply proj_gen_fun.
  - intros d1 d2 f.
    use tpair.
    * red; simpl; intro F; apply (# F f).
    * abstract (intros F G α; simpl in *; apply pathsinv0, (nat_trans_ax α d1 d2 f)).
+ abstract (split;
  [ intros F; simpl; apply nat_trans_eq; [apply homset_property|]; intro G; simpl; apply functor_id
  | intros F G H α β; simpl; apply nat_trans_eq; [apply homset_property|];
    intro γ; simpl; apply functor_comp ]).

Given a sort s this applies the sortToC to s and returns C
Definition projSortToC (s : sort) : functor sortToC C.
Show proof.
apply proj_gen_fun.
apply s.

Definition of multi sorted signatures
Definition MultiSortedSig : UU :=
  ∏ (s : sort), ∑ (I : UU), (I → list (list sort × sort)).
Definition indices (M : MultiSortedSig) : sort → UU := λ s, pr1 (M s).

Definition args (M : MultiSortedSig) (s : sort) : indices M s → list (list sort × sort) :=
  pr2 (M s).

Local Notation "'1'" := (TerminalObject TC).
Local Notation "a ⊕ b" := (BinCoproductObject _ (BC a b)).

Local Definition option_fun : sort -> sortToC -> sortToC.
Show proof.
intros s f.
apply mk_sortToC; intro t.
induction (eq s t) as [H|H].
- apply (pr1 f t ⊕ 1).
- apply (pr1 f t).

Local Definition option_functor_data (s : sort) : functor_data sortToC sortToC.
Show proof.
use tpair.
+ apply (option_fun s).
+ cbn. intros F G α.
  use tpair.
  * red; simpl; intro t.
    induction (eq s t) as [p|p]; simpl; clear p.
    { apply (BinCoproductOfArrows _ _ _ (α t) (identity _)). }
    { apply α. }
  * abstract (now intros t1 t2 []; cbn; induction (eq s t1); simpl; rewrite id_left, id_right).

Local Lemma is_functor_option_functor s : is_functor (option_functor_data s).
Show proof.
split.
+ intros F; apply (nat_trans_eq hsC); intro t; simpl.
  induction (eq s t) as [p|p]; trivial; simpl; clear p.
  now apply pathsinv0, BinCoproductArrowUnique; rewrite id_left, id_right.
+ intros F G H αFG αGH; apply (nat_trans_eq hsC); intro t; simpl.
  induction (eq s t) as [p|p]; trivial; simpl; clear p.
  apply pathsinv0; eapply pathscomp0; [apply precompWithBinCoproductArrow|].
  rewrite !id_left; apply BinCoproductArrowUnique.
  * now rewrite BinCoproductIn1Commutes, assoc.
  * now rewrite BinCoproductIn2Commutes, id_left.

Local Definition option_functor (s : sort) : functor sortToC sortToC :=
  tpair _ _ (is_functor_option_functor s).

Local Definition option_list (xs : list sort) : functor sortToC sortToC.
Show proof.
use (foldr _ _ xs).
+ intros s F.
  apply (functor_composite (option_functor s) F).
+ apply functor_identity.

Local Lemma exp_functor (a : list sort × sort) : functor [sortToC,sortToC] [sortToC,C].
Show proof.
eapply functor_composite.
- apply (pre_composition_functor has_homsets_sortToC _ (option_list (pr1 a))).
- apply post_composition_functor, (projSortToC (pr2 a)).


Local Definition exp_functors (xs : list (list sort × sort)) :
  functor [sortToC,sortToC] [sortToC,C].
Show proof.
set (XS := map exp_functor xs).
set (T := constant_functor [sortToC,sortToC] [sortToC,C]
                           (constant_functor sortToC C TC)).
apply (foldr1 (λ F G, BinProduct_of_functors BinProductsSortToCToC F G) T XS).


Local Definition MultiSortedSigToFunctor_helper1 (C1 D E1 : precategory) (E2 : category)
  : functor [E1,[C1,[D,E2]]] [E1,[D,[C1,E2]]].
Show proof.
eapply post_composition_functor.
apply functor_cat_swap.

Local Definition MultiSortedSigToFunctor_helper (C1 D E1 : precategory) (E2 : category) :
  functor [E1,[C1,[D,E2]]] [C1,[D,[E1,E2]]].
Show proof.
eapply (functor_composite (functor_cat_swap _ _ _)).
apply MultiSortedSigToFunctor_helper1.





Local Definition MultiSortedSigToFunctor_fun (M : MultiSortedSig) (CC : ∏ s, Coproducts (indices M s) C)
  : [sort_cat, [[sortToC, sortToC], [sortToC, C]]].
Show proof.
  apply functor_path_pregroupoid; intro s.
  use (coproduct_of_functors (indices M s)).
  + apply Coproducts_functor_precat, CC.
  + intros y; apply (exp_functors (args M s y)).


The functor constructed from a multisorted binding signature

Definition MultiSortedSigToFunctor (M : MultiSortedSig) (CC : ∏ s, Coproducts (indices M s) C) :
  functor [sortToC,sortToC] [sortToC,sortToC].
Show proof.
set (F := MultiSortedSigToFunctor_helper [sortToC,sortToC] sortToC sort_cat C).
set (x := MultiSortedSigToFunctor_fun M CC).
apply (F x).


End MBindingSig.
End alt.