Definition PCF_Consts : MultiSortedSig type. Proof. use make_MultiSortedSig. - exact ((nat,,isasetnat) + (stn 6,,isasetstn 6))%set. - induction 1 as [n|i]. + exact ([],,Nat). + apply (six_rec i). * exact ([],,Bool). * exact ([],,Bool). * exact ([],,arr Nat Nat). * exact ([],,arr Nat Bool). * exact ([],,arr Bool (arr Nat (arr Nat Nat))). * exact ([],,arr Bool (arr Bool (arr Bool Bool))). Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.Combinatorics.Lists. Require Import UniMath.Combinatorics.StandardFiniteSets. Require Import UniMath.CategoryTheory.Core.Categories. 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.Categories.HSET.Core. Require Import UniMath.SubstitutionSystems.BindingSigToMonad. Section MultiSortedSigFromBindingSig. Definition arFromBindingSig : I → list (list sort × sort) × sort. Definition MultiSortedSigFromBindingSig : MultiSortedSig := I ,, arFromBindingSig. End MultiSortedSigFromBindingSig.