[[!redirects Sandbox > history]] [[!redirects Sandbox]] < [[nlab:Sandbox]] Implication is represented by a function into a proposition, rather than an embedding, and function extensionality is represented by the fact that every function type into a proposition is a proposition. Universal quantification is represented by the dependent product of a family of propositions, and dependent function extensionality then becomes the statement that universal quantification is closed under propositions: the dependent product type of a family of propositions is a proposition. One really needs to get into the habit of using equivalences for equality of types, and embeddings for subtyping and supertyping of types. category: redirected to nlab