Computational Category Theory

abstract adjunctions apply arrow f binary coproducts blue pink bool Burstall cartesian closed categories category theory Chapter cocomplete cocontinuous coequalizers colimiting cocone comma category comma_arrow complete_cat components composition consider datatype defined definition denote described diagram dual duality edges elements encode example Exercise exponentials expressed F-algebras finite colimits finite sets FinSet free algebras functional programming functor categories functor F Goguen identity initial object integers isomorphisms labelled left adjoint let val limits and colimits LNCS logic mathematics monic monoid natural numbers natural transformations nodes objects and arrows operations pair of arrows parallel pair polymorphism Proc programming language proof pullback pushout recursive right adjoint semantics set of equations signature slice category sorts source and target Standard ML structure subobject classifier theorem theory arrow tions topos toposes transitive closure truth-values truvals unification algorithms unifier unique arrow values variables