% transitivity:
defFoAs(isTrans(P),subseteq(circ(P,P),P)).

% symmetry:
defFoAs(isSymm(P),is_rev(P)).

% reflexivity:
defFoAs(isRefl(P),subseteq(un(P,rev(P)),rA(int(id,P)))).

% strictness:
defFoAs(isStrict(P),z_diag(P)).

% antisymmetry:
defFoAs(isAntisymm(P),subseteq(int(P,rev(P)),id)).

% trichotomy:
defFoAs(isTrich(P),u_un([P,id,rev(P)])).

% asymmetry (=isAntisymm+isStrict):
defFoAs(isAsymm(P),z_int(P,rev(P))).

% total reflexivity (=isRefl+Tot):
defFoAs(isTotRefl(P),subseteq(id,P)).

% connexity (=isTotRefl+isTrich):
defFoAs(isConnex(P),u_un(P,rev(P))). % (cf. [SS93], p.12)

% preorder relation:
defThAs(isPreord(P),[isRefl(P),isTrans(P)]).

% equivalence relation (a special case of preorder):
defThAs(isEquiv(P),[isSymm(P),isTrans(P)]).

% single-valuedness (property of a partial function)
defFoAs('isFunc'(P),subseteq(bros(P),id)).

% an equivalence relation is often characterized via 
%	a choice of representatives:
defThAs(isEquiv(P,Ch),
	['isFunc'(Ch),is_circ(Ch,Ch),equiv(circ(Ch,rev(Ch)),P)]).

% Galois' connection:
defThAs(isGaloisCorr(F), [
	subseteq( circ(F,F), id ),
	isStrict(F),
	subseteq( rev(F), rA( F ) )
]).

%=======

% density (of a reflexive ordering):
defFoAs( isDense(Le),
	subseteq( arcs(Le),
		circ(arcs(Le), arcs(Le)) )).

% lack of endpoints:
defFoAs( isWithoutEndPoints(Le),
	subseteq( id,
		link(arcs(Le), rev(arcs(Le))) )).

% (Non-decreasing) monotonicity:
defFoAs( isNDMonotonic( F, Le ),
	z_int( circ( Le, F ), circ( F, opp( Le ) ) )).


% Bisimulation:
defFoAs( isBisim( Bis, Oss ),
	z_un( lA( setminus( Bis, rev(Bis) ) ),
		setminus( circ( Oss, Bis ), circ( Bis, Oss ) ) ) ).