This is a proposal to solve #31 and related issues by introducing one last (!?) abstraction in the Respects realm for binary relations, using an idea which appears in:
Definition: given U : REL A B _, K : REL B D _ as the 'left-vertical' and 'bottom-horizontal' edges in a square, with H : REL A C _ as the 'top-horizontal' and V : REL C D _ as the 'right-vertical' edges, one can consider the property that U ; K ⇒ H ; V for the two 'diagonal' compositions of relations of type REL A D _.
Cf. #2303 which in some sense this issue blocks on: I'd like a better way to state the property, both to name it, but also to depict it as syntax (or otherwise). Semicolons are just... yuk, to me at least.
Properties: given a square satisfying such a property, then they may be composed horizontally and vertically in the 'obvious' way, using left- and right- monotonicity of relational composition wrt _⇒_, and transitivity of the latter notion.
Correspondingly, the property considered in #31 and similar can be expressed as a such a square, subject to suitable flipping of the edges to conform to the particular details of such properties.
Proposal: we add this 4-place property of heterogeneous relations as a definition (where though? the dependency graph for this definition is already quite complex), and establish its composition properties (cf. recent work on left- and right- associativity of Appending on lists... etc.), as well as perhaps additional specialisation of the concept to Rel, and to the case(s) where some of the edges are in fact the graph of a function (cf. actual lax naturality, definitions of HalfLeftAdjoint etc.).
As noted on #31 suggest closing that issue in favour of this one.
This is a proposal to solve #31 and related issues by introducing one last (!?) abstraction in the
Respectsrealm for binary relations, using an idea which appears in:theya special case of this notion is referred to as a 'Reynolds square' https://www.cambridge.org/core/services/aop-cambridge-core/content/view/F48258008F47DC9F53AA2E61B4E511A7/S0956796825000012a.pdf/how_much_is_in_a_square_calculating_functional_programs_with_squares.pdfDefinition: given
U : REL A B _,K : REL B D _as the 'left-vertical' and 'bottom-horizontal' edges in a square, withH : REL A C _as the 'top-horizontal' andV : REL C D _as the 'right-vertical' edges, one can consider the property thatU ; K ⇒ H ; Vfor the two 'diagonal' compositions of relations of typeREL A D _.Cf. #2303 which in some sense this issue blocks on: I'd like a better way to state the property, both to name it, but also to depict it as
syntax(or otherwise). Semicolons are just... yuk, to me at least.Properties: given a square satisfying such a property, then they may be composed horizontally and vertically in the 'obvious' way, using left- and right- monotonicity of relational composition wrt
_⇒_, and transitivity of the latter notion.Correspondingly, the property considered in #31 and similar can be expressed as a such a square, subject to suitable
flipping of the edges to conform to the particular details of such properties.Proposal: we add this 4-place property of heterogeneous relations as a definition (where though? the dependency graph for this definition is already quite complex), and establish its composition properties (cf. recent work on left- and right- associativity of
Appendingon lists... etc.), as well as perhaps additional specialisation of the concept toRel, and to the case(s) where some of the edges are in fact the graph of a function (cf. actual lax naturality, definitions ofHalfLeftAdjointetc.).As noted on #31 suggest closing that issue in favour of this one.