In the mathematical vernacular (Section 1.6), let and suppose introduce hypothetical things and properties. Formally, they expand the context in the sequent style, or open nested boxes in the box presentation. Things introduced by ``let'' are denoted by typed variables. Hypothetical properties may of course depend on entities which have already been introduced in the argument; now the types of the variables may also be dependent on what has gone before. This means that, as a precondition of opening the box or expanding the context, these types must themselves be shown to be well formed.
DEFINITION 8.1.1 The steps in an argument are called judgements. Amongst the direct algebraic steps (those within a fixed context G), we distinguish the following forms:
G\vdash f = y): that these propositions or types are intensionally equal.
For the postulates at the beginning of an argument we need

We discuss context formation in the next section, where it will become clear that we must also say when two contexts are equal, using equality of their types. The provision of arguments of types and operationsymbols also needs formation and equality rules for substitutions.
The idioms which close boxes or make the contexts smaller arise from the quantifiers (Remark 9.1.6 and the whole of the final chapter). For the time being, therefore, boxes never get closed. Despite the boxes and sequents, this chapter generalises, not the predicate calculus as we saw it in Sections 1.4 1.5, but just resolution of Horn clauses involving atomic predicates, as in PROLOG (Remark 1.7.2ff).
At the algebraic level the only distinction between the behaviour of types and propositions is that elements (terms) of the same set (type) are distinguished , but proofs are anonymous. By giving names to the Horn clauses, proofterms may be assigned to propositions (Remark 6.2.10); the main point of Section 2.4 was to do the same for implicational logic, using lterms. Alternatively, we may simply assert that any two proofs of the same proposition in the same context are equal.
The classification of judgements also applies to the rules which justify them. These are the subject of the rest of this section.
Terms In this chapter, a term is an algebraic expression: just as in Definition 1.1.3, it is either a variable x belonging to the context, or an operationsymbol r applied to (zero or more) subterms.
REMARK 8.1.2 Let r be an operationsymbol, from the objecttheory. It is applied to arguments,

omitted proofbox environment
and so on (with intermediate steps). The operationsymbol r might for example be composition, the types being the set of objects and homsets of a category. For propositions r names a Horn clause:



A lot of work remains to be done in the next section to define general substitutions u and their action u^{*}t on terms  the calculus is highly recursive, and we have to break into the circle somewhere  but, in anticipation of this, here are the first of the formal rules.
DEFINITION 8.1.3 The termformation rules are as follows:


Both of these rules incorporate weakening, cf Definition 1.4.8 and Remark 2.3.8. We study the structural rules in the next section.
Equality of terms The notion of equality needed in the foundations of dependent type theory is that from algebra: congruence. The judgement G\vdash a = b means that, for any valid judgement G,Y\vdash J in which a is a subexpression, replacing it with b gives another valid judgement.
DEFINITION 8.1.4 The intensional termequality rules are:



The anonymity of proofs is expressed by an indiscriminate equality rule:

REMARK 8.1.5 Intensional equality G\vdash a = b:X remains at the level of judgements: it does not (within the basic calculus) provide us with a term of some propositional type eq[a,b]. We discuss extensional equality briefly in Section 8.3. If we want to do something conditionally on the equality of a and b, it is extensional equality that we need.
Dependent types The dependency of types on terms (in predicates, homsets, arities, etc ) is expressed in a similar way to the application of operationsymbols to arguments, but there are no type variables.
DEFINITION 8.1.6 The direct type formation rule is


Equality of types The instantiation of a dependent type Y[[(x)\vec]] at equal terms [(a)\vec] = [(b)\vec] gives rise to equal types. We have not addressed this phenomenon before  indeed we have gone to some lengths to exclude it  but how can we deny that Factors[9×4] = Factors[6×6]? There must at least be a canonical isomorphism between the two, but if we chose to make this explicit we would be obliged to introduce formation and equality rules for it, which would have to obey further coherence rules with respect to other substitutions. Predicates at equal subjects also give rise to equal types; again there is a canonical way of translating a proof of one into a proof of the other, which must also obey coherence.
Rather than enter this labyrinth, we accept that types can be intensionally equal, ie if they have a common history of formation. Whereas set theory allows independently given types to be tested for equality or inequality, we do not. Section 9.2, however, does look at some of the categorical consequences of replacing equality by isomorphism .
DEFINITION 8.1.7 The type equality rules are




For the sake of giving a little more thought to the allimportant coercion rule, we pause to consider its oneway version.
REMARK 8.1.8 Subtyping generalises equality between types to a non symmetric relation(judgement) G\vdash U Ì X satisfying


Subtyping also arises in objectoriented programming languages, in which complex types are developed from simpler ones by the addition of constructors and properties. As a mathematical analogy to this style, we may define a field as an Abelian group, with multiplication as an extra operation and the field axioms as extra conditions.
Terms of the narrower type inherit the covariant properties (positive, in the sense of Remark 1.5.9) associated with the wider one to which we coerce them; negative properties pass the other way. The coercion functions, like forgetful functors, need not be injective, but if they are suppressed from the notation then there must be at most one between any two types. (This has nontrivial consequences for functiontypes.)
REMARK 8.1.9 Some authors allow axioms stating equality of types, so that Heyting semilattices can be treated in the same framework. We forbid them, because interchangeability of objects should be expressed as isomorphisms, ie by means of two operationsymbols and two laws between their composites ( cf Section 7.6). See Exercise 4.7 regarding the quotient of a category by a system of canonical isomorphisms. As we commented before Proposition 3.2.11, the antisymmetry law for posets is a sideeffect of the imposition of algebraic notation (Ù, Ú, Þ ), and is not an intrinsic feature of logic.
The restriction drastically simplifies the issue of type equality, as type expressions can be equal only as a result of making equal substitutions into the same ``outermost'' typesymbol. This is essential to the validity of the structural recursion used in the interpretation (Section 8.4).
Definitional equality need not be excluded: it is of course very useful to define R = {(L,U):P(Q)¼} as in Remark 2.1.1. This is harmless to the interpretation of dependent type theory, as we may simply replace the left hand side of the definition by the right. Interprovability as a notion of equality of propositions will be discussed in Remark 9.5.6.
The objectlanguage The pure theory cannot prove the existence of anything apart from the empty context [ ], so an objecttheory is needed. As in simply typed algebra, it has types, operationsymbols and laws.
DEFINITION 8.1.10 A generalised algebraic theory L is given by
In order to give meaning to the ``contexts'' which occur in these data, we have to generate a small part of the language  as we did to state laws for an algebraic theory in Section 4.6. However, the ubiquitous dependencies must not be allowed to become circular, so we require that
the types and operationsymbols which occur in D must have been declared in advance.
Abstractly, the presentation defines a relation between each new symbol being defined and the typesymbols and operationsymbols that are used in the formation of its defining context D (there are operation symbols in the terms that are the arguments of the typeexpressions). This relation must be well founded.
DEFINITION 8.1.11 A stratified algebraic theory is one which obeys a stronger well foundedness condition, that all of the operationsymbols r:X and laws a = b:X must be declared before variables x:X may be used as arguments of further typesymbols Y[x]. We shall not impose this condition in this chapter, as it is violated by the canonical language in Definition 8.4.6. See Exercises 8.1 8.5 and Examples 9.2.4.
EXAMPLE 8.1.12 The theory of categories, with cm(f,g) for f;g.
omitted eqnarray* environment
In Remark 4.1.10 we said that the maps of a category C with O = obC could be collected together and presented by src,tgt:(mor C)® OxO instead of using the dependent type H[x,y]. In fact src,tgt will serve as the display map [^(f)] that corresponds to this dependent type, which we introduce syntactically and semantically in the next two sections.
omitted diagram environment
Before composition can be defined, its support  the set of composable pairs (f,g) with tgt(f) = src(g)  must be constructed. There is a natural syntactic description of this set, namely the context of the rule which introduces c. It is also the pullback of tgt and src, as marked in the diagram above, cf transitivity of a kernel pair (Proposition 5.6.4).
This chapter shows how to translate between the symbolic and diagrammatic idioms. The next section constructs the classifying category for L, ie the category in which this diagram is drawn, and shows that squares like the one marked really are pullbacks. In fact pullback performs all of the substitutions u^{*} in Definitions 8.1.3(a), 8.1.4(c), 8.1.6 and elsewhere. In Section 8.4 we shall give the interpretation of the language, for which we shall need a sharper form of the induction which generates it.