Def  A =ext B == (x:A. x  B) & (x:B. x  A)

is mentioned by

Thm*  (k inj k) =ext (k bij k)	[nsub_inj_exteq_nsub_bij]
Thm*  (k onto k) =ext (k bij k)	[nsub_surj_exteq_nsub_bij]
Thm*  (k inj k) =ext (k onto k)	[nsub_inj_exteq_nsub_surj]
Thm*  (A bij B) =ext ((A inj B)(A onto B))	[bijtype_exteq_inj_isect_surjtype]
Thm*  a,a':. Thm*  a'-a = 1  (B:({a..a'}Type). (i:{a..a'}B(i)) =ext ({a:}B(a)))	[exteq_sum_family_singleton_vs_intseg]
Thm*  a,a':. Thm*  a'-a = 1  (B:({a..a'}Type). (i:{a..a'}B(i)) =ext ({a:}B(a)))	[exteq_prod_family_singleton_vs_intseg]
Thm*  a,a':. a'-a = 1  ({a..a'} =ext {a:})	[exteq_singleton_vs_intseg]

In prior sections: LogicSupplement

Try larger context: DiscrMathExt IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html