% Assuming the function *:U x U -> U  to be injective,
% where U is the domain of discourse,
% the fork operator 'frk' has the following meaning:
% frk^I(P,Q)={[x,y*z]: x P^I y, x Q^I z},
% where I is any interpretation.
 
defAs(frk(P,Q),frk(P,Q)). % we take frk as primitive

[defAs0B,defAs1,defFoAs0]. % we adopt all constructs of map algebra

defAs(cross(P,Q),frk(circ(rev(frk(id,u)),P),circ(rev(frk(u,id)),Q))).

defAs(left,rev(frk(id,u))). % first projection of non-urelements

defAs(right,rev(frk(u,id))). % second projection of non-urelements

defAs(idUr,diag(bros(frk(u,u)))). % identity map restricted to urelements