DanielFilan comments on Multiplicative Operations on Cartesian Frames

[DanielFilan]

Claim: For all Cartesian Frames C, C≃1⊸C and C∗≃C⊸⊥.

These should be isomorphisms, not biextensional equivalences, right? The proofs establish isomorphism.

[Scott Garrabrant]

Yep, fixed, thanks.