is mentioned by

Thm* eq:{T}. eq TT	[equivalence_bool_function]
Thm* f:{T}. (x,y,z:T. f(x,y) f(y,z) f(x,z)) & (x,y:T. f(x,y) f(y,x)) & (x:T. f(x,x)) & f TT	[equivalence_properties]
Thm* eq:{T}. eq TT	[equivalence_type]
Thm* {T} (TT)	[equivalence_inc]
Thm* P:(TZProp). (x:T, y:Z. Dec(P(x,y))) (f_p:(TZ). x:T, y:Z. P(x,y) f_p(x,y))	[decidable_iff_exists_bool_function_2]
Thm* P:(TProp). (x:T. Dec(P(x))) (f_p:(T). x:T. P(x) f_p(x))	[decidable_iff_exists_bool_function]
Def {T} == {f:(TT)| (x:T. (f(x,x))) & (x,y:T. (f(x,y)) (f(y,x))) & (x,y,z:T. (f(x,y)) (f(y,z)) (f(x,z))) }	[equivalence]

In prior sections: bool 1 bool 2 jlc discrete jlc