0.1 Introduction

ETAC is the acronym for Lawvere’s ‘Elementary Theory of Abstract Categories which provides an axiomatic construction of the theory of categoriesMathworldPlanetmath and functorsMathworldPlanetmath that was extended to the axiomatic theory of supercategoriesPlanetmathPlanetmath. The following sectionPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath lists the ETAC (or ETAC) axioms.

0.2 Axioms of ETAC

The ETAC axioms viz. ([6]) are :

0. For any letters x,y,u,A,B, and unary function symbols Δ0 and Δ1, and composition law Γ, the following are defined as formulasMathworldPlanetmathPlanetmath: Δ0(x)=A, Δ1(x)=B, Γ(x,y;u), and x=y; These formulas are to be, respectively, interpreted as “A is the domain of x”, “B is the codomain, or range, of x”, “u is the composition x followed by y”, and “x equals y”.

1. If Φ and Ψ are formulas, then “[Φ] and [Ψ]” , “[Φ] or[Ψ]”, “[Φ][Ψ]”, and “[notΦ]” are also formulas.

2. If Φ is a formula and x is a letter, then “x[Φ]”, “x[Φ]” are also formulas.

3. A string of symbols is a formula in ETAC iff it follows from the above axioms 0 to 2.

A sentenceMathworldPlanetmath is then defined as any formula in which every occurrence of each letter x is within the scope of a logical quantifierMathworldPlanetmath, such as x or x. The theorems of ETAC are defined as all those sentences which can be derived through logical inference from the following ETAC axioms:

4. Δi(Δj(x))=Δj(x) for i,j=0,1.

5a. Γ(x,y;u) and Γ(x,y;u)u=u.

5b. u[Γ(x,y;u)]Δ1(x)=Δ0(y);

5c. Γ(x,y;u)Δ0(u)=Δ0(x) and Δ1(u)=Δ1(y).

6. IdentityPlanetmathPlanetmathPlanetmath axiom: Γ(Δ0(x),x;x) and Γ(x,Δ1(x);x) yield always the same result.

7. Associativity axiom: Γ(x,y;u) and Γ(y,z;w) and Γ(x,w;f) and Γ(u,z;g)f=g. With these axioms in mind, one can see that commutative diagramsMathworldPlanetmath can be now regarded as certain abbreviated formulas corresponding to systems of equations such as: Δ0(f)=Δ0(h)=A, Δ1(f)=Δ0(g)=B, Δ1(g)=Δ1(h)=C and Γ(f,g;h), instead of gf=h for the arrows f, g, and h, drawn respectively between the ‘objects’ A, B and C, thus forming a ‘triangular commutative diagram’ in the usual sense of category theoryMathworldPlanetmathPlanetmathPlanetmathPlanetmath. Compared with the ETAC formulas such diagrams have the advantage of a geometric–intuitive image of their equivalentMathworldPlanetmathPlanetmathPlanetmathPlanetmath underlying equations. The common property of A of being an object is written in shorthand as the abbreviated formula Obj(A) standing for the following three equations:

8a. A=Δ0(A)=Δ1(A),

8b. x[A=Δ0(x)]y[A=Δ1(y)],


8c. xu[Γ(x,A;u)x=u] and yv[Γ(A,y;v)]y=v .

0.3 Remarks on ETAC interpretation

Intuitively, with this terminology and axioms a category is meant to be any structureMathworldPlanetmath which is a direct interpretationMathworldPlanetmath of ETAC. A functor is then understood to be a triple consisting of two such categories and of a rule F (‘the functor’) which assigns to each arrow or morphismMathworldPlanetmath x of the first category, a unique morphism, written as ‘F(x)’ of the second category, in such a way that the usual two conditions on both objects and arrows in the standard functor definition are fulfilled (see for example [ICBM])– the functor is well behaved, it carries object identities to image object identities, and commutative diagrams to image commmutative diagrams of the corresponding image objects and image morphisms. At the next level, one then defines natural transformations or functorial morphisms between functors as metalevel abbreviated formulas and equations pertaining to commutative diagrams of the distinct images of two functors acting on both objects and morphisms. As the name indicates natural transformations are also well–behaved, in terms of the ETAC equations being always satisfied.


Title ETAC
Canonical name ETAC
Date of creation 2013-03-22 18:16:15
Last modified on 2013-03-22 18:16:15
Owner bci1 (20947)
Last modified by bci1 (20947)
Numerical id 52
Author bci1 (20947)
Entry type Topic
Classification msc 70A05
Classification msc 60A05
Classification msc 18E05
Classification msc 55N40
Classification msc 18-00
Synonym axiomatic elementary theory of categories and functors
Synonym ETAS sub-theory
Synonym special case of ETAS
Synonym axiomatic construction of the theory of categories and functors
Related topic ETAS
Related topic AxiomaticTheoryOfSupercategories
Related topic FunctorCategories
Related topic 2Category
Related topic CategoryTheory
Related topic FunctorCategory2
Related topic WilliamFrancisLawvere
Related topic NaturalTransformationsOfOrganismicStructures
Defines axiom of elementary theory of abstract categories
Defines axiomatic theory of categories and functors
Defines axiomatic construction of the theory of categories and functors
Defines ETAC sentence
Defines ETAC theorem
Defines ETAC formula
Defines Lawvere’s elementary theory of abstract categories
Defines t