This file defines Frm, the category of frames.
The category of frames.
Construct a bundled Frm from a Frame.
An abbreviation of FrameHom that assumes Frame instead of the weaker CompleteLattice.
Necessary for the category theory machinery.
Constructs an isomorphism of frames from an order isomorphism between them.
The forgetful functor from TopCatᵒᵖ to Frm.