The reflexive-transitive closure of any relation is a poset.

Given A, define B inductively by

(i) B(x,x)

(ii) if B(x, y) and A(y, z) then B(x, z).

The transpose of any poset is a poset.

Given A, define B explicitly by

B(x, y) = A(y, x).

Adding to David's product construction, more generally the function type A -> S can be made dependent.

Given an "index set" A and for each a in A a poset S(a), the set (a:A)->S(a) of functions which to each a in A arrange a unique s in S(a), can be ordered by defining f <= g to mean, as before, for all a, f(a) <= g(a).

Given A, define B inductively by

(i) B(x,x)

(ii) if B(x, y) and A(y, z) then B(x, z).

The transpose of any poset is a poset.

Given A, define B explicitly by

B(x, y) = A(y, x).

Adding to David's product construction, more generally the function type A -> S can be made dependent.

Given an "index set" A and for each a in A a poset S(a), the set (a:A)->S(a) of functions which to each a in A arrange a unique s in S(a), can be ordered by defining f <= g to mean, as before, for all a, f(a) <= g(a).