]      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGH I J K L M N O P Q R S T U V W X Y Z [ \  ]^_`a]^_`aPair of types of kind  ((((* -> *) -> *) -> *) -> *)  Pair of types of kind  (((* -> *) -> *) -> *)  Pair of types of kind  ((* -> *) -> *)  Pair of types of kind  (* -> *)  " Kind-cast"  ((((* -> *) -> *) -> *) -> *)  to  (((* -> *) -> *) -> *) . Also lower elements using . " Kind-cast"  (((* -> *) -> *) -> *)  to  ((* -> *) -> *) . Also lower elements using  . " Kind-cast"  ((* -> *) -> *)  to  (* -> *) . Also lower elements using  . " Kind-cast"  (* -> *)  to *      Unique existence Universal quantification TExistential quantification ;This class collects lemmas. It plays no foundational role.   !"  !"  !"#V s is the sum of all types x such that s x is provable. %Unique existence, unlowered ) Powerset +8Membership of a set in a set representing a set of sets RSet of all types of kind * T!Empty set (barring cheating with b ) WBinary products YSet difference \ Complement ^Intersection of a family aDependent sum cUnion of a family fBinary intersection i Binary union lExtensional equality of sets oRepresents a proof that set1 is a subset of set2 r!Coercion from subset to superset sCoercion using a set equality t(Coercion using a set equality (flipped) +Product is monotonic wrt. subset inclusion Example application #$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~qoprnlmstuvwxykijzh{|}~fgecdab`^_\][YZWXVTURSPQNOLMJKHIFGDEBC@A>?<=:;8967452301./,-+)*'(%&#$#$$%&&'(()**+,--.//011233455677899:;;<==>??@AABCCDEEFGGHIIJKKLMMNOOPQQRSSTUUVWXXYZZ[\]]^__`abbcddefgghijjklmmnoppqrstuvwxyz{|}~7Expresses that f is a section of  bundleMap NB: famm must be a function mapping some set to a set of sets, or the second condition in the constructor is vacuous  Graph of a  (* -> * -> *) type constructor  Graph of a (* -> *) type constructor The type-level function: KleisliHom(a,b) = (a -> m b) The type-level function: HaskFun(a,b) = (a -> b)  Analogous to c  Injective functions ?(NB: Surjectivity is meaningless here because our functions don'#t know their codomain, but we have ) EInclusion of the equaliser into the domain of the parallel functions Equalisers :D 9In our category, the equaliser of two parallel functions f1 and f2 is the set of types on which f1 and f2 agree; that is: %Equaliser f1 f2 = { x | f1 x = f2 x }  Composition Identity function on dom Inclusion function of a subset  Inclusions do: know their codomain (somewhat arbitrary design decision) "Image of a set under the function .Kind-casted variant (function space as a set) Convention: Instances of  should always prove ':~>:' rather than this type. ZFunctions are encoded as functional relations; the three arguments to the construcor are:  Is a relation  Totality ' Single-valuedness (CPS-encoded; using ':=:'t would work just as well. I hope that the CPS variant makes the optimizer more happy, but this is pure speculation) Single-valuedness (CPS)  Totality >Existential quantification over the first component of a pair Functions are relations Functions are total 6The detailed type variable names help debugging proofs 7Functions are single-valued (reified equality version) -Perform coercion using the single-valuedness *Functions are single-valued (CPS version) Shortcut for unpacking  If f a = b, then a is in the domain of f If f a = b, then b is in the codomain of f 0The domain of a function is uniquely determined This is stronger than ( since it introduces the knowledge that lf is of the form Lower f, rather than assuming it. 3Every image is a subset of every possible codomain The full image is a codomain SChange the codomain by proving that the full image is included in the new codomain Enlargen the codomain @Image distributes over union (in general not over intersection) 5Very useful lemma for proving equality of functions. =Given the properties of functions, it is enough to show that f is a subset of f' to prove f = f'. % with the inclusion argument flipped Expresses the fact that f = f' ==> f x = f' x +Perform coercion using a function equality Inclusion is a function Id is a function The composition is a function @ is a left identity for composition < is a right identity for composition CThe equaliser is a subset of the domain of the parallel functions &The equaliser inclusion is a function "Universal property of equalisers: f1 . g = f2 . g ==> g factors uniquely through Equaliser f1 f2 MUniqueness is trivial in our case because the function into the equaliser is  identical to g (our functions don't know their codomain)  Type constructors are injective  eNB: this is stronger than the straightforward unpacking function -- we can use the single-valuedness   Type constructors are injective 5Example of an extensional equation between functions 3Lemma for proving a function equal to the identity Is section ==> composition is id Composition is id ==> is section <An injective function has an inverse, with domain the image u     u     u     Either Typeable d s, or e s A Map9 whose keys are taken from any type which is a member of set    !The unique morphism from an & to any .- NB: s is a type constructor, but succ2 is a Function () $6Successor function made from a unary type constructor &`Actually any pair of (nullary type, unary type constructor) gives us a copy of the naturals; let' s call these TNats )Expresses that (set1,z1,succ1) is initial in the cat of .-@s, in other words, that it is isomorphic to the natural numbers +Structure-preserving maps of .-s -7Sets equipped with a constant and a function to itself !"#$%&'()*+,-./01-.+,)*&('$%/0!#"1!#""#$%%&(''()**+,,-../0188Existential wrapping of the composition for types a,b,c :3Existential wrapping of the identity function on a <7Category with type-level set of objects and type-level homY function, but value-level composition and value-level definition of identity functions. @ Composition DJLemma for constructing categories; abstracts the usage of the hom function's  23456789:;<=>?@ABCDEFG<=>?@:;89ABCDEF456723G2334567567899:;;<=>?@=>?@ABCDEFG WN  in terms of K  and I  XL  in terms of K  and I  HIJKLMNOPQRSTUVWXYZ[\MNJKLHIOPQRSTUVWXYZ[\HIIJKLKLMNNOPQRSTUVWXYZ[\f !!""#$%&'())*+,-..//0011233445566778899::;;<<==>>??@@AABBCCDDEEFFGGHIIJJKLLMMNOOPPQRQSTSUVWXYXZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~                    ! " # $ % & ' ( ) * + , - . /0 1 23 456type-settheory-0.1.2Data.Typeable.Extras Type.Dummies Type.LogicType.Set Type.FunctionType.Set.ExampleType.Nat Data.CategoryControl.SMonadDefsHelperbasePrelude Control.Arrow Data.ChardynEq dynComparePAIR3PAIR2PAIR1PAIRLower3 Lower2ElementLower2 Lower1ElementLower1 LowerElementLowerCOrExUniqAllallElimEx DecidabledecideFactautoNotTruth TruthProofFalsity elimFalsityexElimlemelimCorVExUniq1ProofSetPowerset::∈:ApplicativeType MonadPlusType MonadType FunctorTypeDataType TypeableTypeFractionalType MonoidType IntegralTypeNumType BoundedTypeEnumTypeOrdTypeEqTypeReadTypeShowType CoKleisliType KleisliType FunctionTypeUnivEmptyProd:×:DiffDisjoint ComplementInters DependentSumΣUnionsInter:∩:Union:∪: Singleton:==:SetEqSubset:⊆::∈:scoerceecoerce ecoerceFlip subsetRefl subsetTrans setEqReflsetEqSym setEqTrans elimUnionunionLunionR unionMinimalunionIdempotent elimInterinterFstinterSnd interMaximalinterIdempotent elimUnions elimInterselimComplementcomplContradiction complEmpty complMaximalelimDifffstPrfsndPrf prodMonotonic elimEmpty emptySubset univSubset functionType kleisliType coKleisliTypegetShowgetEq getComparegetFmappowersetWholeset powersetEmpty powersetUnion powersetInterpowersetMonotonicpowersetClosedDownwards autosubset autoequalityliftEq liftCompare liftShowsPrecInvSectionΠConstBiGraphToTyConGraph KleisliHomHaskFun:***:SndFstPreimage Injective EqualiserIncl Equaliser:○:CompoIdInclImage:~~>::~>:IsFunSvalTotalExSndrelationtotaltotalCPSsval svalCoercesvalCPSsvalCPS'relrelCPSinDominCoddomUniqlowerFunraiseFun raiseFunCPSimageCod setCodToImage adjustCod extendCodimageMonotonic imageEmptyimageOfInclusionfullImageOfInclusion imageUnionfunEqfunEq'equal_fequal_f_coerceisFun_congruenceinclusionIsFunidIsFun compoIsFun compo_idl compo_idr compo_assocequaliserSubsetequaliserIsFun equaliserUni injectiveinclusion_Injectivepreimage_Imageimage_PreimagefstIsFunsndIsFuntargetTuplingIsFun fst_tupling snd_tupling tupling_eta haskFunIsFunhaskFunInjectivekleisliHomIsFunkleisliHomInjective graphIsFungraphCPSgraphInjectiveimageGraphList introToTyCon elimToTyContoTCGfromTCG biGraphIsFunbiGraphInjectivebiGraph_eq_HaskFun constIsFunconstEqidLemmasection_CompoIdcompoId_SectioninvInv0invInv injective_InvinvId ExampleSetSMap singletoninsertlookupstringInExampleSetintInExampleSettestInitorInitorSInitorZSuccTNatIsSIsZNInitial NMorphism NStructuresuccFun tyconNStruct initorFunExFmapGFunctor omapIsFungetfmapExCExIdCathomIsFungetidgetchaskkleislifromControlCategorymakeCatidautocauto fromFunctorSMonadsbind' SApplicativespure'sap'SFunctorsfmap'sfmapspuresapsreturn'sreturnsbindsjoin'sjoin sfmap'Default sap'DefaultsliftA2'sliftA2 ssequence' ssequencedecomposeForallTlemma unmangleName unmangleNameslemmataGHC.Err undefined***GHC.RealIntegralGHC.BaseString