QUOTIENT

>> E[y,x/x,y]
* x:A,y:A,z:A,E[x,y/x,y] ,\ E[y,z/x,y] >> E[x,z/x,y]

. H >> (u,v):A//E in by intro new x,y,z
* >> A in
* x:A,y:A >> E[x,y/u,v] in
* x:A >> E[x,x/u,v]
* x:A,y:A,E[x,y/u,v]

>> E[y,x/u,v]
* x:A,y:A,z:A,E[x,y/u,v] ,\ E[y,z/u,v] >> E[x,z/u,v]

rulesubsection23.25ex plus 1ex minus .2ex1.5ex plus .2ex

* canonical  . H >> (x,y):A//E ext a by intro at
* >> (x,y):A//E in
* >> A ext a

. H >> a in (x,y):A//E by intro at
* >> (x,y):A//E in
* >> a in A

rulesubsection23.25ex plus 1ex minus .2ex1.5ex plus .2ex

* noncanonical  . H,u:(x,y):A//E, >> t= in T by elim u at [new v,w]
* v:A,w:A >> E[v,w/x,y] in
* >> T in
* v:A,w:A,E[v,w/x,y] >>
* t[v/u] = [w/u] in T[v/u]

rulesubsection23.25ex plus 1ex minus .2ex1.5ex plus .2ex

* equality  . H >> (x,y):A//E = (u,v):B//F in by intro [new r,s]
* >> (x,y):A//E in
* >> (u,v):B//F in
* >> A = B in
* A=B in ,r:A,s:A >> E[r,s/x,y] -> F[r,s/u,v]
* A=B in ,r:A,s:A >> F[r,s/u,v] -> E[r,s/x,y]

. H >> t = in (x,y):A//E by intro at
* >> (x,y):A//E in
* >> t in A
* >> in A
* >> E[/x,y]

---

Richard Eaton
Thu Sep 14 08:45:18 EDT 1995