Selected Objects

def	hone	hone == Unit
def	hone_el	one_el ==
THM	hone_ty_def	exists(rep:hone  hbool. type_definition((b:hbool. b),rep))
THM	hone_def	equal(one_el,select(x:hone. t))
THM	hone_axiom	'a:S. all(f:'a  hone. all(g:'a  hone. equal(f,g)))
THM	hone_wd	all(v:hone. equal(v,one_el))
THM	hone_axiom_2	'a:S. all(e:'a. exists_unique(fn:hone  'a. equal(fn(one_el),e)))
THM	one_axiom	'a:S, f,g:('aUnit). f = g
THM	one_wd	v:Unit. v =
THM	one_axiom_2	'a:S, e:'a. (fn:(Unit'a). fn() = e) & (fn,y:(Unit'a). fn() = e & y() = e  fn = y)

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html