Categorical Semantics of First-Order Functional

Type Theories

Krzysztof Worytkiewicz

February 28, 1995

Abstract

A study of the categorical semantics of the simply typed >=-calculus and two relevant extensions of the latter.

1 Inroduction

The calculi under investigation are

ffl the simply typed >=-calculus with constants and products called >=?.

ffl the simply typed >=-calculus with constants, products and fixpoint operators called >= ? Y

ffl the recursively typed >=-calculus called Y>=?

They are treated in the general framework of type theories, i.e they decompose into

ffl syntax

ffl typing rules

ffl equational rules

1.1 Syntax

The description of the syntax consists of two sets of BNF-productions, one for the syntax of the types and the other for the syntax of the terms.

1.2 Typing rules

For each calculus there is a enumerable set of variables V, a enumerable set of constants C and a collection of types T which may be a proper class. A typing context H consists of two partial functions

HV : V ! T

and

HC : C ! T

Hv and Hc have finite domains and often written as lists. At a first glance it seems artificial to split a typing context in a variable and a constant part. However, the latter come from a different syntax class and, in particular, cannot be bound by abstractions like the former. A typing judgement H ` M : t means that the term M has the type t relative to the typing context H. A typing rules consist of a finite number of typing judgements as premisses and a conclusion, often written

H1 ` M1 : t1; : : : ; H1 ` Mn : tn
H ` M : t

The typing rules define an inference system. where a proof of H ` M : t is called a typing derivation. It certifies that a term is well-typed and only welltyped terms are given a meaning in a semantic model.

1.3 Equational Rules

An equation H oe M = N : t means that terms M and N are equal and of type t relative to the typing context H. An equational judgement T ` (H oe M = N : t) means that the equation is provable relative to the equational theory T 1.

Equational rules have a premisses-conclusion structure much alike the typing ones and also define an inference system where a proof is sometimes called equation derivation. The categorical models the heart of the study are required to be sound w.r.t the equational rules.

2 >=?: The Simply Typed >=-Calculus with Constants

and Products

Itself a variation of the simply typed >=-calculus, it is the basic case on which the other two calculi under study are built. There is the well-known CurryHoward correspondence between this calculus and the natural deduction. It can be characterised by the double slogan:

proof = term
proposition = type

2.1 Type Theory

2.1.1 Syntax

Let Tc be the set of type constants. The types are given by the syntax

t ::= c j t ! t j t ? t

where c 2 Tc. It is the set of finite terms over the signature

? = hTc; !;?i

where

8c 2 Tc:ar(c) = ; ar(!) = ar(?) = 2:

The terms are given by the syntax

M ::= c j x j >=x : t: M j MM j (M; M ) j fst(M ) j snd(M )

2.1.2 Typing Rules

i. k2dom(HC )
H ` k:HC(k)

ii. H; x:t; H0 ` x:t

1an equational theory is a set of equations

iii. H; x:s ` M :t
H ` >=x : s: M :s ! t

iv. H ` M :s ! t H ` N :s
H ` M(N):t

v. H ` M :s H ` N :t
H ` (M;N):s?t

vi. H ` M :s?t
H ` fst(M):s

vii. H ` M :s?t
H ` snd(M):t

2.1.3 Equational Rules

i. (HoeM=N :t)2T
T ` (HoeM=N :t)

ii. T ` (HoeM=N :t) x62dom(HV )
T ` (H; x:soeM=N :t)

iii. T ` (H; x:soeM=N :t) x62FV (M)[FV (N)
T ` (HoeM=N :t)

iv. H ` M :t
T ` (HoeM=N :t)

v. T ` (HoeM=N :t)
T ` (HoeN=M :t)

vi. T ` (HoeL=M :t) T ` (HoeM=N :t)
T ` (HoeL=M :t)

vii. T ` (HoeM=M :s!t) T ` (HoeN=N :s
T ` (HoeM(N)=M (N ):t)

viii. T ` (H; x:soeM=N :t)
T ` (Hoe>=x : s: M=>=x : s: N :s!t

ix. H; x:s ` M :t H ` N :s
T ` (Hoe(>=x : s: M)(N)=[N=x]M :t

x. H ` M :s!t x62FV (M)
T ` (Hoe>=x : s: M(x)=M :s!t

xi. H ` M :s H ` N :t
T ` (Hoefst(M;N)=M :s

xii. H ` M :s H ` N :t
T ` (Hoesnd(M;N)=N :t

xiii. H ` M :s?t
T ` (Hoe(fst(M);snd(N))=M :s?t

Rules vii and viii assert that abstraction and application are congruence relations relative to a fixed theory while rules ix and x are respectively the reduction and extensionality rules.

2.2 Semantics

The main idea here is to interpret types as objects of a category, terms as morphisms thereof and substitution by composition of morphisms. It turns out that, in order to model functional types, a certain property of the category is required, namely cartesian closedeness. Such a category is routinely abbreviated CCC and bears the categorical counterparts of application and currying.

2.2.1 CCC' s

Definition 2.1 Let C be a category. C is cartesian iff it has

1. a terminal object 1

2. all binary products

|

Proposition 2.1 A cartesian category C has all finite products.

|

Proposition 2.2 Let C be a cartesian category and 1 it' s terminal object. For all objects b of C we have

b ' 1 ? b ' b ? 1

|
Clearly, most of the concrete categories like Set, Grp or Top occuring in the daily life of the working mathematician are cartesian.

Definition 2.2 Let C be cartesian and b; c 2 Ob(C). The exponent of b and c is an object cb together with a morphism ev, such that, for any object a and morphism f : a ? b ! c there is a unique arrow ?f making the diagram

cb ? b oe?f ? 1b a ? b

??????
f

c

ev

?

commute.|

Definition 2.3 A cartesian closed category (CCC) is a cartesian category with all exponents. |

The most simple example is Set.

2.2.2 Categorical Models of >=?

Let C be a CCC. The types of >=? are interpreted as objects in C by the inductive definition:

i. an object [[c]] for every type constant c

ii. [[s ! t]] = [[s]] ! [[t]]

iii. [[s ? t]] = [[s]] ? [[t]]

Let H = x1 : t1; : : : ; xn : tn a type assignment and H ` M : t. The interpretation of H ` M : t is a morphism

[[H oe M : t]] = [[t1]] ? ? ? ? [[tn]]? ! [[t]]

defined inductively by:

i. [[H oe k : t]] = [[k]]ffi!tH where k a term constant, [[k]] 2 C[1; HC(k)] and !tH the unique morphism !tH : [[t1]] ? ? ? ? [[tn]] ! 1

ii. [[H oe xi : ti]] = ssi]]

iii. [[H oe (>=x : u: N ) : u ! v]] = ?[[H; x : u oe N : v]]

iv. [[H oe L(N ) : s]] = ev ffi h[[H oe L : t ! s]]; [[H oe N : t]]i

v. [[H oe (L; N ) : s ? t]] = h[[H oe L : s]]; [[H oe N : t]]i

vi. [[H oe fst(N ) : s]] = fst ffi [[H oe N : s ? t]]

vii. [[H oe snd(N ) : s]] = snd ffi [[H oe N : s ? t]]

As an example

[[; oe >=x : s: >=f : s!t: f(x) : s!(s!t)!t]] =

?[[x : s oe >=f : s!t: f(x) : (s!t)!t]] =

??[[x : s; f : s!t oe f(x) : t]] =

??ev ffi h[[x : s; f : s!t oe f : s!t]]; [[x : s; f : s!t oe x : s]]i =

??ev ffi hss2; ss1i

where ss1 and ss2 are the projections belonging to the product [[s]] ? ([[s!t]]) = [[s]] ? ([[t]][[s]]). Let f be defined by the diagram

[[s]] ? [[t]][[s]] hss2; ss1i- [[t]][[s]] ? [[s]]

@@@@@
f R
[[t]]
?

ev

Then by definition of ?:

[[t]][[t]][[s]] ? [[t]][[s]] oe?f ? 1[[t]][[s]] [[s]] ? [[t]][[s]]

??????

f

[[t]]

ev

?

hence

?ev ffi hss2; ss1i : [s]]![[t]][[t]][[s]]

The following theorem ensures that this interpretation is sound w.r.t the equational rules of the calculus:

Theorem 2.1 Let C be a CCC. If

` H oe M = N : t

then

[[H oe M : t]] = [[H oe N : t]]

|

When looking for a model of >=?, e.g an abstract interpretation, this leaves several degrees of freedom while retaining the same formal machinery.

3 >= ? Y: The Simply Typed >=-Calculus with Constants,

Products and Fixpoint Operators

The calculus treated in this section an extension of the previous one by fixpoint operators and other (more unproblematic) pieces enabling the definition of recursive functions. The price to pay is to blurr the correspondence with natural deduction. Indeed, in the case of >=?, a constructive proof of a formula has a closed term as counterpart. The bottom line is that a formula is provable in the logic if and only if the corresponding type is inhabited. The introduction of fixpoint operators makes all types inhabited so there is no non-trivial correspondence ?a la Curry-Howard for this calculus. However, the calculus is not equationally inconsistent.

3.1 Type Theory

3.1.1 Syntax

The type theory of this sections is a variation of Plotkin' s FPC. The types are those of section 2.1 where TC = fbool; numg. The syntax of the terms has additionally to those of section 2.1 the following productions

M ::= j true j false j succ(M ) j pred(M ) j zero?(M ) j if M then M else M j ?x : t: M

3.1.2 Typing Rules

All the rules in section 2.1 and additionally:

i. H`0:num

ii. H`true:bool

iii. H`false:bool

iv. H`M :num
H`pred(M):num

v. H`M :num
H`O(M):num

vi. H`M :num
H`zero?(M):bool

vii. H`L:bool H`M :t H`N :t
H`if L then M else N :t

viii. H;x:t`M :t
H`?x : t: M :t

3.1.3 Equational Rules

All the rules in section 2.1 and additionally:

i. Hoepred(0)=0:num

ii. Hoepred(succ(n))=n:num

iii. Hoezero?(0)=true:bool

iv. Hoezero?(succ(n))=false:bool

v. H`M :t H`N :t
`(if true then M else N=M :t)

vi. H`M :t H`N :t
`(if false then M else N=N :t)

vii. H;x:t`M :t
`(Hoe?x : t: M=[?x : t: M=x]M :t)

viii. `(HoeM=N :num)
`(Hoepred(M)=pred(N):num)

ix. `(HoeM=N :num)
`(Hoesucc(M)=succ(N):num)

x. `(HoeM=N :num)
`(Hoezero?(M)=zero?(N):bool)

xi. `(H;x:toeM=N :t
`(H;x:toe?x : t: M=?x : t: N :t

xii. `(HoeL=L0:bool `(HoeM=M0:t `(HoeN=N0:t
`(Hoeif L then M else N=if L0 then M else N :t

3.2 Semantics

3.2.1 Fixpoint Operators in CCC' s

Definition 3.1 Let C be a CCC and b 2 Ob(b). A fixpoint operator for b is a morphism F ixb : bb!b such that the diagram

bb ? b oehid; F ixbi bb

??????

F ixb

b

ev

?

commutes. A CCC with all fixpoint operators is called CCC with fixpoint operators. |

One of the best known examples of CCC' s with fixpoint operators is Cpo, the category of complete partial orders and continous functions:

Definition-Proposition 3.1 Let d be a cpo and f : d!d a continous function. Then [!fn(?d) is the least fixed point of f . Define F ixd as

F ixd : dd ! d
f 7! [!fn(?d)

for every continous f : d!d. F ixd is continous. |

3.2.2 Categorical Models of >= ? Y

>= ? Ycan be modelled in any CCC with fixpoint operators.

4 Y>=?: The Recursively Typed >=-Calculus

Y>=? is a calculus with a computational power similar to that of >= ? Y. However, there is no fixpoint operator which means that all the recursion has been moved at the level of types. Another particularity of the calculus is that, despite a type system equipped with type variables, there are no type constants. It is in fact possible to unroll all types from the void one 2 using the function space operator, a construction similar in spirit to that of defining the natural numbers in set theory.

2i.e a type which is not inhabited

4.1 Type Theory

4.1.1 Syntax

There are two syntactic classes of variables: type variables belonging to the enumerable set typeV ar and term variables belonging to the enumerable set termV ar.

x 2 termV ar

a 2 typeV ar

t ::= a j t!t j t ? t j ?a:t

M ::= x j >=x : t: M j MM j (M; M ) j intro[?a:t]M j elim[?a:t]M j

4.1.2 Typing Rules

In addition to the typing rules for >=?in section 2.1, there are

i. H ` M :[?a:t=a]t

H ` intro[?a:t]M :?a:t

ii. H ` M :[?a:t]t
H ` elim[?a:t]M :[?a:t=a]t

Definition-Proposition 4.1 The recursive type ?a:a is called void and is not inhabited.

Proof. By contradiction on the length of the type derivation. Assume the derivation of ` N : ?a:a at least as short as that of any other typing judgment involving this type. As it stands, N must be of the form intro(M ) for some term M . Hence ` M : ?a:a by the rule i. The derivation of must ` M : ?a:a be shorter than that of ` N : ?a:a which is a contradiction. diamondsuit

Let C be a CCC and 1C the terminal object. It is possible to code up the numerals like follows:

[[0]] = void; [[1]] = void!void; [[2]] = (void!void)!void!void; : : :

and henceforth any concrete data structure.

4.1.3 Equational Rules

Again addition to the typing rules for >=?in section 2.1, there are

i. ` (HoeM=N :[?a:t=a]t)
` (Hoeintro[?a:t]M=intro[?a:t]N :?a:t)

ii. ` (HoeM=N :[?a:t])
` (Hoeelim[?a:t]M=elim[?a:t]N :[?a:t=a]t)

4.2 Semantics

Types are modelled by objects of a semantic CCC. Thus, The construction required to model ?x:t must involve some sort of functorial fixpoint. The following sections make this notion precise.

4.2.1 Colimits

Colimits are the categorical generalization of a l.u.b of a directed set.

Definition 4.1 Let I be a poset and C a category. An I-diagram over C is a functor ? : I!C where I is considered as a (small) category. Such a diagram is also called indexed by I and written

? = (Di; fij)i;j 2 I

where Di = ?i and fij = ?(ivj). |

Clearly, fik = fjk ffi fij for ivjvk.

Definition 4.2 Let C be a category and ? an I-diagram over C. A cocone over ? is a pair hD; ?i, where D is an object of C and ? a family of morphisms ? = (?i)i2I indexed by I such that, for each i; j 2 I; ?i : Di!D. Moreover, the diagram

Dj ?j - D

?????
?i
?

Di

fij

6

commutes for each i; j 2 I such that ivj. A cocone mu is often written

? : ?!D

|

Cocones over a diagram are objects of a category:

Definition 4.3 Let C be a category and ? a diagram over C indexed by the poset I. The objects of the category Cocone(?) are the cocones over ?. Let ?; ? 2 Ob(Cocone(?)) where ? = hD; ?i and ? = hE; ?i. A morphism Mor(Cocone(?)) 3 f : ?!? is a morphism Mor(C) 3 f : D!E such that the diagram

D f - E

?????
?i
?

Di

?i

6

commutes for each i 2 I. In particular, an !-chain over C is a diagram indexed by a total order. |

Definition 4.4 Let C be a category and ? a diagram over C indexed by the poset I. A colimit of ? is an initial object in Cocone(?). |

In particular, a colimit is unique up to iso. Let I be the poset above and ? : I!I the identity functor. A cocone over ? is an upper bound while a colimit is a l:u:b. The notions of cone and limit are dual.

Definition 4.5 Let C be a category and F : C!C an endofunctor. An F- algebra is a morphism f : F (A)!A. The F-Algebras are the objects of the category Falg(F ). Let Ob(Falg(F )) 3 f : F (A)!A and Ob(Falg(F )) 3 g : F (B)!B be two F-algebras. A morphism Mor(Falg(F )) 3 h : f!g is a morphism Mor(C) 3 h : A!B such that the diagram

F (A) F (h)- F (B)

A

f

? h - B

g

?

An initial F-algebra is an initial object in Falg(F ) |

Proposition 4.1 Let f : F (A)!A be an initial F-algebra. The f is iso. |

Definition-Proposition 4.2 Let ? : ?!D be an !-chain over the category C, F : C!C an endofunctor and ? : ?!A a cocone over ?.

1. F (?) : F(?)!F (A) is a cocone.

2. there is an !-chain ??n with Di? = Di+1 and fi? = fi+1

3. there is a cone ?? : ??!D with ?i? = ?i+1

|

Theorem 4.1 Let C be a category with initial object , F : C!C an endofunctor
C!C, ? = (Fn(0); Fn(!i))i2! be an !-chain over C where !i is the unique morphism !i : !F (0) and ? : ?!A a colimit of ?. If F (?) is a colimit
of F(?) then the cocone morphism a : F (?)!?? is an initial F-algebra a : F (A)!A. |

In particular, under the assumptions of the theorem, a is iso by proposition 4.1. In order to exploit this in practice, two problems arise:

1. it is difficult to determine from the definition if a functor is continous or not

2. it is not possible to compose functors of different variance

The next section makes precise how to circumvent this difficulty.

4.2.2 Continous Functors and Fixed Points Thereof

Definition 4.6 An O-category has a cpo-structure on the homsets. Moreover, the composition of morphisms is required to be continous.

Definition 4.7 Let C be an O-category. An embedding i : D ! E in C is a morphism with a right adjoint iR : E ! D called projection:

ffl iR ffi i = idD

ffl i ffi iR v idE

w.r.t order on the homsets. |

As an example, Cpo is an O-category with the pointwise ordering of the continous functions. The next definition introduces some notation:

Definition 4.8 Let C be an O-category and h : D ! E an embedding. An embedding-projection pair or ep-pair is the pair

h = hhe; hpi

where he = h and hp = hR. |

It is easy to see that the ep-pairs are the morphisms of a category with the same objects as C:

Definition 4.9 Let C be an O-category. The category Cep is the category with the same objects as C and ep-pairs as morphisms. The composition of eppairs is given componentwise while hidd; iddi is the identity morphism for any d 2 Ob(Cep). |

The next theorem gives a continuity criterion for endofunctors on Cep:

Theorem 4.2 Let C be an O-category and ? a diagram over Cep indexed by poset I. The cocone ? : ?!D is a colimit of ? if
G

i2I
?ei ffi ?pi = idD

Definition 4.10 An O-category C has locally determined colimits if, for every diagram ? over Cep indexed by poset I and every cocone ? : ?!D the following are equivalent:

1. ? is a colimit

2. F
i2I ?ei ffi ?pi = idD

Only the implication from 1 to 2 needs to be checked because of theorem 4.2. Clearly, a cone ? is a colimit in a O-category C with locally determined colimits if and only if F
i2I ?ei ffi ?pi = idD. Cpo is an example of such a category.

Definition 4.11 Let C and D be O-categories and F : C!D a functor. F is locally monotone if f v g implies F (f) v F (g). A locally monotone functor is locally continous if F (FM ) = FF (M ) for any directed M ? C[D; E].

Proposition 4.2 Let C and D be O-categories with locally determined colimits and F : C!D a locally continous functor. Then the functor F induces between Cep and Dep is continous.

By the means exposed above it is easy to check that almost all functors on Cpo and other relevant categories are continous. Remains to see how the composability problem can be solved:

Theorem 4.3 Let C be an O-category and Let T : Cm+n ! C, m;n >= be contravariant in the first m arguments and covariant in the following n arguments, T locally continous. Let D0; : : : ; Dm?1;E0; : : : ; En?1 cpo' s and fi : D0i ! Di; (i < m), gi : Ei ! E0i; (i < n) ep-pairs. Then

TE : (Eep)m+n ! Eep

defined by

TE(D0; : : : ; Dm?1;E0; : : : ; En?1) = T (D0; : : : ; Dm?1;E0; : : : ; En?1)

and

TE(f0; : : : ; fm?1; g0; : : : ; gn?1) = T (fp0 ; : : : ; fpm?1; g0; : : : ; gn?1)

is (m + n)-covariant. |

4.2.3 Categorical Models of Y>=?

Since operators like ?, ! or + can be extended into functors, the machinery developped in the previous section allows to define the meaning of recursive types as intial F -Algebras of such functors since it guarantees the existence of the later and gives an effective construction. For example, the meaning of the type ?a:a + (a!a) is the intial algebra of the functor ( + ( ! ))E

A Elements of the proof of theorem 2.1

Proposition A.1 Let C a CCC and H : a ! cb an arrow in C. Then

h = ?(ev ffi (h ? 1b))

|

Proof. Consider the diagram

cb ? b oeh ffi 1b a ? b

??????

ev ffi (h ? 1b)

c

ev

?

It commutes by composition, hence the proposition is true by unicity of currying. diamondsuit

Proposition A.2 Let C a CCC, f : a ! b, g : b ? c ! d arrows. Then

?(g) ffi f = ?(g ffi (f ? 1c))

|

Proof. Consider the diagram

a ? c f ? 1c - b ? c g - d

@@@@@
(?(g) ffi f) ? 1c R ?????

ev

?

dc ? c

?(g) ? 1c

?

The left triangle commutes by composition and the right one by definition of the exponential, hence the outer diagram commutes too. The assertion follows then by unicity of currying. diamondsuit

Definition A.1 Let C a CC and the products

a = a1 ? ? ? ? ? ak ? ak+1 ? ? ? ? ? an

a? = a1 ? ? ? ? ? ak+1 ? ak ? ? ? ? ? an

for

1 <= k < n

We define recurrently the arrow onk : a ! a0 as

onk =

ae hh?1 ffi ?1; ?2i; ?2 ffi ?1i k + 1 = n
on?1
k k + 1 < n

|

Lemma A.1 Given the type environments

H = x1 : t1; : : : ; xk : tk; xk+1 : tk+1; : : : ; xn : tn

and

H0 = x1 : t1; : : : ; xk+1 : tk+1; xk : tk; : : : ; xn : tn

and the type judgment

H ` M : t

we have

[[H oe M : t]] = [[H0 oe M : t]] ffi onk

|

Lemma A.2 Let M be a term and x 62 FV (M ). Then

[[H; x : s oe M : t]] = [[H oe M : t]] ffi ?1

|

Proof. Structural induction on M . Let [[s]] = b, [[t]] = c and [[H; x : s oe M : t]] : a ? b ! c. We treat only the case M ? >=y : u: M : there is a v s.t
t = u ! v. Let o = hh?1 ffi ?1; ?2i; ?2 ffi ?1i : (a ? b) ? u ! (a ? u) ? b where u = [[v]] and a = H.

[[H; x : s oe >=y : u: M : u ! v
= ?([[H; x : s; y : u oe M : v]]) CCC-model
= ?([[H; y : u; x : s oe M : v]] ffi tau) lemma A.1
= ?([[H; y : u oe M : v]] ffi ?1 ffi tau) CCC-model
= ?([[H; y : u oe M : v]] ffi (?1 ? u)) (?)
= ?([[H; y : u oe M : v]]) ffi ?1 prop. A.2
= ?([[H oe M >=y : u: M : u ! v]]) ffi ?1 CCC-model

Let h = [[H; y : u oe M : v]]. It is easy to see (?) with a simple diagram chase:

(a ? b) ? u o- (a ? u) ? b

@@@@@

?1

R
a ? u

??????

h

a ? u

?1 ? 1u

?

h
- [[v]]

}

Lemma A.3 (?)

[[H oe >=x : s: M (x) : s ! t]] = [[H oe M : s ! t]]

|

Proof.

[[H oe >=x : s: M (x) : s ! t]]
= ?([[H; x : s oe M (x) : t]]) CCC-model = ?(ev ffi h[[H; x : s oe M : s ! t]]; [[H; x : s oe x : s]]i) CCC-model = ?(ev ffi h[[H oe M : s ! t]] ffi ?1; ?2 by lemma A.2 and def. = ?(ev ffi ([[H oe M : s ! t]] ? 1[[s]] )) CCC-model and easy diagram chase = [[H oe M : s ! t]] by prop. A.1

}

Lemma A.4 (Substitution) Let

f = [[H; x : s oe M : t]] : a ? b ! c

and

g = [[H oe N : s]] : a ! b

Then

[[H oe [N=x]M : t]] = f ffi h1a; gi : a ! c

a h1a; gi- a ? b

@@@@@R
c?

f

|

Lemma A.5 ( )

[[H oe >=x : s: M (N ) : t]] = [[H oe [N=x]M : t]]

|

Proof. Let H : x1 : t1; : : : ; xn : tn be a type assignment. In the following, we abbreviate H = [[t1]] ? ? ? ? ? [[tn]].

[[H oe >=x : s: M (N ) : t]]
= ev ffi h[[H oe >=x : s: M : s ! t]]; [[H oe N : s]]i CCC-model = ev ffi h?([[H; x : s oe M : t]]); [[H oe N : s]]i CCC-model = ev ffi (?([[H; x : s oe M : t]]) ? 1[[s]] ) ffi h1H ; [[H oe N : s]]i easy diagram chase = [[H; x : s oe M : t]] ffi h1H ; [[H oe N : s]]i prop. A.1 = [[H oe [N=x]M : t]] lemma A.4

|