Ramana Kumar comments on Committing, Assuming, Externalizing, and Internalizing

[Ramana Kumar]

Claim: For any Cartesian frame $C=(A,E,\cdot )$ over $W$ and partition $V$ of $W$, let $v:W\to V$ send each element of $W$ to its part in $V$. If for all $a_0,a_1\in A$ and $e\in E\text{,}$ we have $v(a_0\cdot e)=v(a_1\cdot e)$, then ${\text{External}}_V\left(C\right)\cong C$.

I think this may also need to assume that $A$ is non-empty.

[Scott Garrabrant]

Fixed, Thanks