[[!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? We need to define the uniqueness quantifier directly using rules. Done. Definitions using uniqueness quantification rather than equivalence types. category: redirected to nlab