[[!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 quantificaiton 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. Quantifiers: * existential quantifier - there is at least one element $x:T$ for which $P(x)$ holds $\exists x:T.P(x)$ * uniqueness quantifier - there is exactly one element $x:T$ for which $P(x)$ holds $\exists! x:T.P(x)$ * (?) quantifier - there is at most one element $x:T$ for which $P(x)$ holds $\exists? x:T.P(x) \coloneqq \exists x:T.P(x) \implies \exists! x:T.P(x)$ $$x:\exists x:T.P(x) \vdash p(x):\exists! x:T.P(x)$$ category: redirected to nlab