Composition of roofs is well defined

Ore supplies $a,b$ of the indicated types and $sa\in S$. To compare any two candidate squares, it is enough to give a common refinement of their output roofs; common refinement is an equivalence relation.

First replace $(s,f)$ by a refinement $(sr,fr)$, where $sr\in S$. Compare squares $fa=tb$ and $fr{a}^{\mathrm{\prime }}=t{b}^{\mathrm{\prime }}$, with $a,a^{\mathrm{\prime }}\in S$. Apply Ore to the denominators $sa$ and $sr{a}^{\mathrm{\prime }}$ to obtain $v\in S,w$ with $sav=sr{a}^{\mathrm{\prime }}w\in S$. Cancel $s$ by a further $e\in S$ to obtain $ave=r{a}^{\mathrm{\prime }}we$, then cancel $t$ by $k\in S$ to obtain $bvek=b^{\mathrm{\prime }}wek$. Thus the two composite roofs have equal numerator and denominator after refinement, with common denominator $savek\in S$. Taking $r=1$ proves independence of the square as well.

Next refine the second roof to $(tr,gr)$, where $tr\in S$. Compare $fa=tb$ and $f{a}^{\mathrm{\prime }}=tr{b}^{\mathrm{\prime }}$. Ore gives $v\in S,w$ with $av=a^{\mathrm{\prime }}w\in S$. Cancellation of $t$ in $tbv=tr{b}^{\mathrm{\prime }}w$ gives $e\in S$ with $bve=r{b}^{\mathrm{\prime }}we$. Hence the composites have equal numerator $gbve=gr{b}^{\mathrm{\prime }}we$ and common denominator $save\in S$. Arbitrary equivalent representatives share a refinement, so these two refinement checks and transitivity prove full representative independence.

For a third roof $(u:T\to Z,h:T\to R)$ choose $fa=tb$ as above and $ge=uk$ with $e\in S$. Ore applied to $b:W\to V$ and $e$ gives $i\in S,j$ with $bi=ej$. Then $gbi=ukj$ and $fai=tej$. The two bracketings can therefore both be computed as $(sai,hkj)$. Independence of square choices proves associativity for all choices.

Composing with an identity roof on the target uses $a=1,b=f$; composing with an identity roof on the source uses $a=s,b=1$. Both recover $(s,f)$ exactly. Thus the operation has both identity laws, including when $s$ itself is an identity.