quot 1 Sections StandardLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Def EquivRel x,y:T. E(x;y)
Def == Refl(T;x,y.E(x;y)) & (Sym x,y:T. E(x;y)) & (Trans x,y:T. E(x;y))

is mentioned by

Thm* E:(TTProp). 
Thm* (EquivRel x,y:T. E(x,y))
Thm* 
Thm* (x,y:T. Dec(E(x,y)))  (u,v:x,y:T//E(x,y). Dec(u = v))		[decidable__quotient_equal]
Thm* E:(TTProp). 
Thm* (EquivRel x,y:T. E(x,y))
Thm* 
Thm* (F:((x,y:T//E(x,y))Prop). 
Thm* ((w:x,y:T//E(x,y). SqStable(F(w)))
Thm* (
Thm* (((z:x,y:T//E(x,y). F(z))  (z:T. F(z))))		[all_quot_elim]
Thm* E:(TTProp). 
Thm* (EquivRel x,y:T. E(x,y))  (a,b:T. a = b  x,y:T//E(x,y)  E(a,b))		[quot_elim]
Thm* E:(TTProp). (EquivRel x,y:T. E(x,y))  T  (x,y:T//E(x,y))[quotient_qinc]
Thm* T:Type, E:(TTProp). (EquivRel x,y:T. E(x,y))  x,y:T//E(x,y)  Type[quotient_wf]

In prior sections: rel 1

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

quot 1 Sections StandardLIB Doc