Find better new symbol for `;` (relational composition)

[jamesmckinna]

Responding to my query on #2301 , @Taneb wrote:

`;` is (according to agda-mode's "Information about the character at point" tool) a Greek question mark, which is written with `\;`, but there's a dozen characters with that and it's the 11th in the list.

I don't think we should be using that character, it's identical to the semicolon graphically (it's even normalized to the semicolon by Unicode) and bound to cause confusion. But I don't have a suggestion for what to use instead. EDIT: `⨾` (first in the list of `\;` but also \z;`) is "Z NOTATION RELATION COMPOSITION" per the Unicode standard. So it's at least semantically appropriate

Originally posted by @Taneb in https://github.com/agda/agda-stdlib/issues/2301#issuecomment-1965933649

I too had queried that info, finding that the symbol is written with \;, but not as far as finding it's the 11th in the list.

I would prefer to use the symbol which exhibits REL as the prototypical bicategory, namely $\otimes$, but I have had push back for suggesting that usage in other settings in the past... but here I think it does make sense, and ushers in the use of the left- and right- linear lollipops for the corresponding adjoints...

[silentstormm]

⨾ U+2A3E : Z NOTATION RELATIONAL COMPOSITION shows up as the first suggestion for \;, doesn't seem to be used anywhere else and is intended for this exact purpose, is there any reason not to use it here?

[Taneb]

Yes, that's the symbol I suggested in the linked PR

[JacquesCarette]

Personally I much prefer U+02A1F , i.e.

02A1F ⨟ # \zcmp mathop oz = \semi (oz), = \fatsemi (stmaryrd), Z NOTATION SCHEMA COMPOSITION

which I believe is also available in newer agdas.

[MatthewDaggitt]

@JacquesCarette what do you see as the difference between your symbol and the one suggested by @silentstormm above?

[JacquesCarette]

U+02A1F is larger than U+2A3E which I've found to act as a nice visual delimiter. It also has the advantage of having been in a standard latex package for longer.

[jamesmckinna]

What are the 'natural' symbols for the right adjoints to these candidate 'semicolon' symbols for composition? (Maybe de Moor and Bird came up with 'reasonable' names for them in Algebra of Programming?)

(otherwise, giving in to the temptation to repeat myself: why not \otimes, which has the advantage of having been in standard LaTeX packages for a lot longer... I'm not sure that Z notation is necessarily a good guide to choices we might commit to in stdlib? especially if such notation doesn't then lend itself to the additional structure/operations associated with relational composition)

UPDATED: we've stalled on this, but I found in Relation.Unary, L308-L311:

-- Composition.

_⟨∘⟩_ : Pred (A × B) ℓ₁ → Pred (B × C) ℓ₂ → Pred (A × C) _
(P ⟨∘⟩ Q) (x , z) = ∃ λ y → (x , y) ∈ P × (y , z) ∈ Q

Can we adopt this notation as is for Relation.Binary, and make sure that the imports get fixed so that the Unary and Binary versions never occur in the same scope?