Mateusz Bagiński comments on Subagents of Cartesian Frames

[Mateusz Bagiński]

Proof: We use the categorical definition. That $\top ◃C$ is vacuous, since there is no morphism from $\top$ to $\perp$. That $C◃\perp$ is also trivial, since any $\varphi :C◃\perp$ is equal to $\varphi \circ {\text{id}}_{\perp }$. $\square$

Shouldn’t this be “any $\varphi :C\to \perp$ is equal to ${\text{id}}_{\perp }\circ \varphi$”? (two mistakes, triangle instead of arrow and wrong composition order)