% inclusion, disjointness:
defFoAs( subseteq(P,Q), z_setminus(P,Q)).
defFoAs( supseteq(P,Q), subseteq(Q,P)).
defFoAs( 'Disj'(P,Q),	z_int(P,Q) ).

% right-totality, right-absoluteness, left-absoluteness,
%	diagonality, functionality, left-uniqueness:
defFoAs( 'Tot'(  R ), u_rA(R) ).
defFoAs( 'RAbs'( R ), is_rA(R) ).   % "row-constant" characterization of collection
defFoAs( 'LAbs'( R),  is_lA(R) ).   % "column-constant" characterization of collection
defFoAs( 'Coll'( R ), is_diag(R) ). % "subdiagonal" characterization of collection
defFoAs( 'RUniq'( R ), z_mult(R) ). % "P is a function"
% Alternatively: defFoAs( 'RUniq'( R ), 'Coll'( bros(R) ) ).
defFoAs( 'LUniq'( R ), 'Coll'( sibs(R,R) ) ). % "P is the converse of a function"
% Alternatively: defFoAs( 'LUniq'( R ), 'RUniq'( rev(R) ) ).

% relativization of the above "uniqueness" notions to a domain P:
defFoAs( 'RUniq'( P, R ), 'Disj'(mult(R),rA(P)) ).
defFoAs( 'LUniq'( P, R ), 'RUniq'(P,rev(R)) ).

% "sends-to" and surjectivity properties:
defFoAs(sends( R, E, F ),
	subseteq( circ( E, R ), lA( F ) ) ).

defFoAs(isSurj( R, F, E ),
	subseteq( F, img( circ( E, R ) ) ) ).


defThAs(isSurj( R, F ), [% equivalent to isSurj( R, F, id )
	'Coll'( F ),
	subseteq( F, lA( R ) )
]).

%=== three useful variadic constructs ==========

defThAs( equiv([P]), [true(P)] ).
defThAs( equiv([P,Q|T]), [equiv(P,Q)|equiv([P|T])]).

defThAs( subseteq([P]), [true(P)] ).
defThAs( subseteq([P,Q|T]), [subseteq(P,Q)|subseteq([Q|T])]).

defThAs( nameLets([]), [] ).
defThAs( nameLets([LN,L|T]), [defAs(@(LN),L)|nameLets(T)] ).

%=== useful parametric constructs ==========

% Two maps, L[eft] and R[ight], are used to navigate "tuples":

defAs(th((L,_;one)),L).
defAs(th((L,R;incr(I))),circ(th(R,R,I),L)).

defAs(succth((L,R;decr(H))),th(L,R,H)).
defAs(tuples((R;H)),
	setminus(int(img(R),dom(th(R,R,H))),dom(succth(R,R,H)))).

defAs(sibs((L,R;nil)),u).
defAs(sibs((L,R;sng(H))),sibs([succth(L,R,H)])).
defAs(sibs((L,R;cons(H,B))),int(sibs([succth(L,R,H)]),sibs(L,R,B))).