 Constructions, and the entities they construct, are organized into a ramified type theory incorporating a simple type theory.The semantics is tailored to the hardest case, as constituted by hyperintensional contexts, and generalized from there to intensional and extensional contexts.The underlying logic is a Frege-style function/argument one, treating functions, rather than relations or sets, as primitive, together with a Church-style logic, centred on the operations of functional abstraction and application.