Library UniMath.SubstitutionSystems.FromBindingSigsToMonads_Summary

This file provides a stable interface to the formalization of the paper:
From binding signatures to monads in UniMath
by Benedikt Ahrens, Ralph Matthes and Anders Mörtberg.
PLEASE DO NOT RENAME THIS FILE - its name is referenced in the article about this formalization.

Require Import UniMath.Foundations.NaturalNumbers.

Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Isos.
Require Import UniMath.CategoryTheory.Core.Univalence.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.FunctorAlgebras.
Require Import UniMath.CategoryTheory.FunctorCategory.
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.Structures.
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.Chains.All.
Require Import UniMath.CategoryTheory.Adjunctions.Core.
Require Import UniMath.CategoryTheory.ProductCategory.
Require Import UniMath.CategoryTheory.exponentials.
Require Import UniMath.CategoryTheory.whiskering.
Require Import UniMath.CategoryTheory.Monads.Monads.

Require Import UniMath.SubstitutionSystems.SignatureCategory.
Require Import UniMath.SubstitutionSystems.SubstitutionSystems.
Require Import UniMath.SubstitutionSystems.BindingSigToMonad.
Require Import UniMath.SubstitutionSystems.LiftingInitial_alt.

Local Open Scope cat.

Local Notation "[ C , D , hsD ]" := (functor_precategory C D hsD).

Definition 1: Binding signature
Definition 4: Signatures with strength
Definition Signature : C : precategory, has_homsets C
                        D : precategory, has_homsets D
                        D' : precategory, has_homsets D' UU :=

Definition 5: Morphism of signatures with strength
Definition 6: Coproduct of signatures with strength
Definition 7: Binary product of signatures with strength
Problem 8: Signatures with strength from binding signatures
Definition 10 and Lemma 11 and 12: see UniMath/SubstitutionSystems/SignatureExamples.v
Definition 15: Graph
Definition 16: Diagram
Definition 17: Cocone
Definition 18: Colimiting cocone
Colimits of a specific shape
Colimits of any shape
Remark 19: Uniqueness of colimits
Definition 20: Preservation of colimits
Lemma 21: Invariance of cocontinuity under isomorphism
Lemma preserves_colimit_iso :
   (C D : precategory) (hsD : has_homsets D)
    (F G : functor C D) (α : @iso [C,D,hsD] F G)
    (g : graph) (d : diagram g C) (L : C) (cc : cocone d L),
  preserves_colimit F d L cc preserves_colimit G d L cc.
exact @UniMath.CategoryTheory.Chains.OmegaCocontFunctors.preserves_colimit_iso.

Problem 22: Colimits in functor categories
Problem 24: Initial algebras of ω-cocontinuous functors
Lemma 25: Lambek's lemma
Problem 27: Colimits in Set
Lemma 31: Left adjoints preserve colimits
Lemma 32: Examples of preservation of colimits (i): Identity functor
(ii): Constant functor
(iii): Diagonal functor
(iv): Coproduct functor
Lemma 33: Examples of preservation of cocontinuity (i): Composition of functors
(ii) Tuple functor
(iii): Families of functors
Example 35: Exponentials in Set
Lemma 36: Left and right product functors preserves colimits
Theorem 37: Binary product functor is ω-cocontinuous
Example 38: Lists of sets

Theorem 41: Precomposition functor preserves colimits
Theorem 43: Signature functor associated to a binding signature is ω-cocontinuous
Problem 45: Datatypes specified by binding signatures
Definition DatatypeOfBindingSig :
   (C : precategory) (hsC : has_homsets C)
    (BPC : BinProducts C) (BCC : BinCoproducts C)
    (_ : Initial C) (TC : Terminal C)
    (_ : Colims_of_shape nat_graph C)
    (_ : (F : functor_precategory C C hsC),
            is_omega_cocont (constprod_functor1 (BinProducts_functor_precat C C BPC hsC) F))
    (sig : BindingSig) (CC : Coproducts (BindingSigIndex sig) C),
  Initial (FunctorAlg (Id_H C hsC BCC (BindingSigToSignature hsC BPC BCC TC sig CC))
                      (BindingSigToMonad.has_homsets_C2 hsC)).
exact @UniMath.SubstitutionSystems.BindingSigToMonad.DatatypeOfBindingSig.

Theorem 48: Construction of a substitution operation on an initial algebra
Section 4.2: Binding signatures to monads
Example 50: Untyped lambda calculus

Example 51: Raw syntax of Martin-Löf type theory