[[!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. What is transport in the context of strongly predicative mathematics? 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