Local reflexivity versus left quasi reflexivity versus right quasi reflexivity versus pure reflexivity

[cjheath]

Reflexivity is currently formalised as local reflexivity or pure reflexivity (core reflexivity).

Local reflexivity seems to be only left quasi reflexivity, that x1x2 implies x1x1. Why left and not right, that is, x1x2 implies x2x2? Should local reflexivity be (bi)quasi reflexivity, that is, x1x2 implies x1x1 && x2x2?

Per group email 2024-10-17

[cjheath]

Enrico's answer is that left quasi reflexivity may be used twice (with the role order swapped) for bi-reflexivity, and so is sufficient for formalisation.