scholarly journals On generalized algebraic theories and categories with families

2021 ◽  
pp. 1-18
Author(s):  
Marc Bezem ◽  
Thierry Coquand ◽  
Peter Dybjer ◽  
Martín Escardó
Keyword(s):  
Type Theory ◽  
Algebraic Theory ◽  
Completeness Theorem ◽  
Small Category ◽  
Equational Logic ◽  
Algebraic Theories ◽  
Semantic Notion ◽  
Finitely Presented ◽  
Extra Structure

Abstract We give a syntax independent formulation of finitely presented generalized algebraic theories as initial objects in categories of categories with families (cwfs) with extra structure. To this end, we simultaneously define the notion of a presentation Σ of a generalized algebraic theory and the associated category CwFΣ of small cwfs with a Σ-structure and cwf-morphisms that preserve Σ-structure on the nose. Our definition refers to the purely semantic notion of uniform family of contexts, types, and terms in CwFΣ. Furthermore, we show how to syntactically construct an initial cwf with a Σ-structure. This result can be viewed as a generalization of Birkhoff’s completeness theorem for equational logic. It is obtained by extending Castellan, Clairambault, and Dybjer’s construction of an initial cwf. We provide examples of generalized algebraic theories for monoids, categories, categories with families, and categories with families with extra structure for some type formers of Martin-Löf type theory. The models of these are internal monoids, internal categories, and internal categories with families (with extra structure) in a small category with families. Finally, we show how to extend our definition to some generalized algebraic theories that are not finitely presented, such as the theory of contextual cwfs.

Algebra of constructions II: an algebraic approach to Martin-Löf type theory and the calculus of constructions

1993 ◽  
Vol 3 (1) ◽  
pp. 63-92
Author(s):  
Adam Obtułowicz
Keyword(s):  
Type Theory ◽  
Algebraic Theory ◽  
Algebraic Approach ◽  
Recursive Functions ◽  
Algebraic Theories ◽  
Calculus Of Constructions ◽  
Partial Algebras

We present an algebraic approach to the syntax and semantics of Martin-Löf type theory and the calculus of constructions developed by T. Coquand and G. Huet. In our approach, models of this theory and this calculus are treated as three-sorted partial algebras, called ITSΠ-structures, described by essentially algebraic theories. We give a proof that derived statements of Martin-Löf type theory hold in appropriate ITSΠ-structures. In this proof, a formal translation from the language of terms and types into the language of terms of an appropriate essentially algebraic theory of ITSΠ-structures is used. A straightforward set-theoretic construction of ITSΠ-structures that are models of Martin-Löf type theory is demonstrated. We present a construction of a recursive ITSΠ-structure(i.e. its partial and total operations are recursive functions over some alphabet) that is a model of the calculus of constructions and demonstrates the decidability of this calculus.

scholarly journals Large algebraic theories with small algebras

1978 ◽  
Vol 19 (3) ◽  
pp. 371-380 ◽  
Author(s):  
Jan Reiterman
Keyword(s):  
Algebraic Theory ◽  
Proper Class ◽  
Algebraic Theories

The aim of the paper is to study the interrelation between several natural smallness conditions on an algebraic theory with a proper class of operations. The conditions concern the existence of sets of data determining algebras, homomorphisms, subalgebras, and congruences.

scholarly journals On the homotopy theory of monoids

1989 ◽  
Vol 47 (2) ◽  
pp. 171-185
Author(s):  
Carol M. Hurwitz
Keyword(s):  
Homotopy Type ◽  
Homotopy Theory ◽  
Small Category ◽  
Homotopy Equivalence ◽  
Classifying Spaces ◽  
Classifying Space ◽  
Finitely Presented

AbsractIn this paper, it is shown that any connected, small category can be embedded in a semi-groupoid (a category in which there is at least one isomorphism between any two elements) in such a way that the embedding includes a homotopy equivalence of classifying spaces. This immediately gives a monoid whose classifying space is of the same homotopy type as that of the small category. This construction is essentially algorithmic, and furthermore, yields a finitely presented monoid whenever the small category is finitely presented. Some of these results are generalizations of ideas of McDuff.

scholarly journals Contextual modal types for algebraic effects and handlers

2021 ◽  
Vol 5 (ICFP) ◽  
pp. 1-29
Author(s):  
Nikita Zyuzin ◽  
Aleksandar Nanevski
Keyword(s):  
Programming Languages ◽  
Type Theory ◽  
Operational Semantics ◽  
Algebraic Theory ◽  
Type System ◽  
Effect Theory ◽  
Explicit Substitutions ◽  
Type And Effect Systems ◽  
Modal Type ◽  
Modal Types

Programming languages with algebraic effects often track the computations’ effects using type-and-effect systems. In this paper, we propose to view an algebraic effect theory of a computation as a variable context; consequently, we propose to track algebraic effects of a computation with contextual modal types . We develop ECMTT, a novel calculus which tracks algebraic effects by a contextualized variant of the modal □ (necessity) operator, that it inherits from Contextual Modal Type Theory (CMTT). Whereas type-and-effect systems add effect annotations on top of a prior programming language, the effect annotations in ECMTT are inherent to the language, as they are managed by programming constructs corresponding to the logical introduction and elimination forms for the □ modality. Thus, the type-and-effect system of ECMTT is actually just a type system. Our design obtains the properties of local soundness and completeness, and determines the operational semantics solely by β-reduction, as customary in other logic-based calculi. In this view, effect handlers arise naturally as a witness that one context (i.e., algebraic theory) can be reached from another, generalizing explicit substitutions from CMTT. To the best of our knowledge, ECMTT is the first system to relate algebraic effects to modal types. We also see it as a step towards providing a correspondence in the style of Curry and Howard that may transfer a number of results from the fields of modal logic and modal type theory to that of algebraic effects.

scholarly journals The costructure–cosemantics adjunction for comodels for computational effects

2021 ◽  
pp. 1-46
Author(s):  
Richard Garner
Keyword(s):  
Dynamic Properties ◽  
Algebraic Theory ◽  
The Other ◽  
Algebraic Theories ◽  
And Mathematics ◽  
The One ◽  
Suitable Environment ◽  
The Way

Abstract It is well established that equational algebraic theories and the monads they generate can be used to encode computational effects. An important insight of Power and Shkaravska is that comodels of an algebraic theory $\mathbb{T}$ – i.e., models in the opposite category $\mathcal{S}\mathrm{et}^{\mathrm{op}}$ – provide a suitable environment for evaluating the computational effects encoded by $\mathbb{T}$ . As already noted by Power and Shkaravska, taking comodels yields a functor from accessible monads to accessible comonads on $\mathcal{S}\mathrm{et}$ . In this paper, we show that this functor is part of an adjunction – the “costructure–cosemantics adjunction” of the title – and undertake a thorough investigation of its properties. We show that, on the one hand, the cosemantics functor takes its image in what we term the presheaf comonads induced by small categories; and that, on the other, costructure takes its image in the presheaf monads induced by small categories. In particular, the cosemantics comonad of an accessible monad will be induced by an explicitly-described category called its behaviour category that encodes the static and dynamic properties of the comodels. Similarly, the costructure monad of an accessible comonad will be induced by a behaviour category encoding static and dynamic properties of the comonad coalgebras. We tie these results together by showing that the costructure–cosemantics adjunction is idempotent, with fixpoints to either side given precisely by the presheaf monads and comonads. Along the way, we illustrate the value of our results with numerous examples drawn from computation and mathematics.

scholarly journals Relationship of Algebraic Theories to Powerset Theories and Fuzzy Topological Theories for Lattice-Valued Mathematics

2007 ◽  
Vol 2007 ◽  
pp. 1-71 ◽  
Author(s):  
S. E. Rodabaugh
Keyword(s):  
Sufficient Conditions ◽  
Algebraic Theory ◽  
Fuzzy Topology ◽  
New Class ◽  
Algebraic Theories ◽  
Necessary And Sufficient ◽  
Relationship Of ◽  
Topological Theories ◽  
Fixed Basis

This paper deals with a broad question—to what extent is topology algebraic—using two specific questions: (1) what are the algebraic conditions on the underlying membership lattices which insure that categories for topology and fuzzy topology are indeed topological categories; and (2) what are the algebraic conditions which insure that algebraic theories in the sense of Manes are a foundation for the powerset theories generating topological categories for topology and fuzzy topology? This paper answers the first question by generalizing the Höhle-Šostak foundations for fixed-basis lattice-valued topology and the Rodabaugh foundations for variable-basis lattice-valued topology using semi-quantales; and it answers the second question by giving necessary and sufficient conditions under which certain theories—the very ones generating powerset theories generating (fuzzy) topological theories in the sense of this paper—are algebraic theories, and these conditions use unital quantales. The algebraic conditions answering the second question are much stronger than those answering the first question. The syntactic benefits of having an algebraic theory as a foundation for the powerset theory underlying a (fuzzy) topological theory are explored; the relationship between these two specific questions is discussed; the role of pseudo-adjoints is identified in variable-basis powerset theories which are algebraically generated; the relationships between topological theories in the sense of Adámek-Herrlich-Strecker and topological theories in the sense of this paper are fully resolved; lower-image operators introduced for fixed-basis mathematics are completely described in terms of standard image operators; certain algebraic theories are given which determine powerset theories determining a new class of variable-basis categories for topology and fuzzy topology using new preimage operators; and the theories of this paper are undergirded throughout by several extensive inventories of examples.

scholarly journals On the essentially-algebraic theory generated by a sketch

1982 ◽  
Vol 26 (1) ◽  
pp. 45-56 ◽  
Author(s):  
G.M. Kelly
Keyword(s):  
Universal Algebra ◽  
Simple Proof ◽  
Algebraic Theory ◽  
Small Category ◽  
Generic Model ◽  
Enriched Categories ◽  
Small Set

By a sketch we here mean a small category S together with a small set φ of projective cones in S, each cone φ ∈ φ being indexed by a small category Lφ. A model of S in any category B is a functor G: S → B such that each Gφ is a limit-cone. Let F be any small set of small categories containing all the Lφ. A small category T admitting all F-limits (that is, an F-complete small T ) is called an F-theory; it is considered as a sketch in which the distinguished cones are all the F-limit-cones. It is an important result of modern universal algebra, due originally to Ehresmann, that each sketch S = (S, φ) with every Lφ ∈ F determines an F-theory T, with a generic model M: S → T of S, such that composition with M induces an equivalence M* between the category of T-models in B and that of S-models in B, whenever B is F-complete. We give a simple proof of this result – one which generalizes directly to the case of enriched categories and indexed limits; and we make the new observation that the inverse to M* is given by (pointwise) right Kan extension along M.

Affine Parts of Algebraic Theories II

1978 ◽  
Vol 30 (02) ◽  
pp. 231-237
Author(s):  
J. R. Isbell ◽  
M. I. Klun ◽  
S. H. Schanuel
Keyword(s):  
Algebraic Theory ◽  
Finitely Generated ◽  
Relative Complexity ◽  
Binary Operations ◽  
Number Of Generators ◽  
Algebraic Theories ◽  
Minimum Number ◽  
Finitely Related ◽  
Affine Part

This paper concerns relative complexity of an algebraic theory T and its affine part A, primarily for theories TR of modules over a ring R. TR, AR and R itself are all, or none, finitely generated or finitely related. The minimum number of relations is the same for T R and AR. The minimum number of generators is a very crude invariant for these theories, being 1 for AR if it is finite, and 2 for TR if it is finite (and 1 ≠ 0 in R). The minimum arity of generators is barely less crude: 2 for TR} and 2 or 3 for AR (1 ≠ 0). AR is generated by binary operations if and only if R admits no homomorphism onto Z2.

scholarly journals Constructing a small category of setoids

2011 ◽  
Vol 22 (1) ◽  
pp. 103-121 ◽  
Author(s):  
OLOV WILANDER
Keyword(s):  
Type Theory ◽  
Order Theory ◽  
Small Category ◽  
First Order ◽  
First Order Theory ◽  
Unique Identity

Consider the first-order theory of a category.d It has a sort of objects, and a sort of arrows (so we may think of it as a small category). We show that, assuming the principle of unique substitutions, the setoids inside a type theoretic universe provide a model for this first-order theory. We also show that the principle of unique substitutions is not derivable in type theory, but that it is strictly weaker than the principle of unique identity proofs.

Sign in / Sign up

Export Citation Format

Share Document