[[!redirects Sandbox > history]] [[!redirects Sandbox]] < [[nlab:Sandbox]] Dependent type theory is first and foremost a logic with equality. It differs from first-order logic with equality, but it is still a logic with equality. And indeed one could implement higher-order logic as a dependent type theory. One could also implement different kinds of mathematical foundations such as set theory, topos theory, and univalent type theory by postulating different kinds of universes via axioms and axiom schemata to work in. But that is irrelevant to the primary purpose of dependent type theory as a logic with equality. I am a pluralist and an agnostic when it comes to which foundations of mathematics to use. I don't really care how people view sets and the collection of all sets. However, I am monist when it comes to which ambient logic to use. ---- The important thing about impredicative types, such as function types, dependent function types, or the type of all propositions, is not that they satisfy universal properties, but rather that they allow non-element things, such as families of elements or types with at most one element, to be represented as elements of types. Are universal properties overrated? Only needed for the natural numbers... ---- Judgmental equality is useless to me. Cubical type theory is useless to me because it has judgmental equality. Similarly (higher) objective type theory is useless to me because it has judgmental equality. ---- Instead, we should be focusing upon using typal equality and equivalence for the definition of the type of propositions Formation rules for the type of all propositions: $$\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathrm{Prop} \; \mathrm{type}}$$ Introduction rules for the type of all propositions: $$\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma \vdash \mathrm{toProp}_A:\mathrm{isProp}(A) \to \mathrm{Prop}}$$ Elimination rules for the type of all propositions: $$\frac{\Gamma \vdash A:\mathrm{Prop}}{\Gamma \vdash \mathrm{El}(A) \; \mathrm{type}} \qquad \frac{\Gamma \vdash A:\mathrm{Prop}}{\Gamma \vdash \mathrm{proptrunc}(A):\mathrm{isProp}(\mathrm{El}(A))}$$ Computation rules for the type of all propositions: $$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash p:\mathrm{isProp}(A)}{\Gamma \vdash \beta_\mathrm{Prop}^{\mathrm{El}, A}(p):\mathrm{El}(\mathrm{toProp}_A(p)) \simeq A \; \mathrm{type}}$$ * Judgmental computation rules: $$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash p:\mathrm{isProp}(A)}{\Gamma \vdash \mathrm{congform}_\mathrm{isProp}(\beta_\mathrm{Prop}^{\mathrm{El}, A}(p))(\mathrm{proptrunc}(\mathrm{toProp}_A(p))) \equiv p:\mathrm{isProp}(A)}$$ * Typal computation rules: $$\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash p:\mathrm{isProp}(A)}{\Gamma \vdash \beta_\mathrm{Prop}^{\mathrm{proptrunc},A}(p):\mathrm{congform}_\mathrm{isProp}(\beta_\mathrm{Prop}^{\mathrm{El}, A}(p))(\mathrm{proptrunc}(\mathrm{toProp}_A(p))) =_{\mathrm{isProp}(A)} p}$$ where the equivalence $$\mathrm{congform}_\mathrm{isProp}(\beta_\mathrm{Prop}^{\mathrm{El}, A}(p)):\mathrm{isProp}(\mathrm{El}(\mathrm{toProp}_A(p))) \simeq \mathrm{isProp}(A)$$ can always be constructed in a type theory with [[dependent product types]], [[dependent sum types]], and [[identity types]], and [[function extensionality]], as given types $A$ and $B$ and an equivalence $e:A \simeq B$, it is always possible to form the equivalence $$\mathrm{congform}_\mathrm{isProp}(e):\mathrm{isProp}(A) \simeq \mathrm{isProp}(B)$$ For example, for $\mathrm{isProp}$ defined as the dependent product type $\prod_{x:A} \prod_{y:A} x =_A y$, we have that the [[function application to identifications|application]] of the equivalence $e:A \simeq B$ to identifications is itself an equivalence: $$\mathrm{ap}_e(x, y):(x =_A y) \simeq (e(x) =_B e(y))$$ Then by the [[typal congruence rules]] of [[dependent function types]], there is an equivalence $$\mathrm{congform}_\mathrm{isProp}(e) \equiv \mathrm{congform}_{\prod}(e, \lambda x:A.\mathrm{congform}_{\prod}(e, \lambda y:A.\mathrm{ap}_e(x, y))):\left(\prod_{x:A} \prod_{y:A} x =_A y\right) \simeq \left(\prod_{x:B} \prod_{y:B} x =_B y\right)$$ And for any other definition of $\mathrm{isProp}$, we have an equivalence $\delta_{\mathrm{isProp}(A)}:\mathrm{isProp}(A) \simeq \prod_{x:A} \prod_{y:A} x =_A y$ for type $A$, and so there is an equivalence $$\mathrm{congform}_\mathrm{isProp}(e) \equiv \delta_{\mathrm{isProp}(B)}^{-1} \circ \mathrm{congform}_{\prod}(e, \lambda x:A.\mathrm{congform}_{\prod}(e, \lambda y:A.\mathrm{ap}_e(x, y))) \circ \delta_{\mathrm{isProp}(A)}:\mathrm{isProp}(A) \simeq \mathrm{isProp}(B)$$ Uniqueness rules for the type of all propositions: * Judgmental computation rules: $$\frac{\Gamma \vdash A:\mathrm{Prop}}{\Gamma \vdash A \equiv \mathrm{toProp}_{\mathrm{El}(A)}(\mathrm{proptrunc}(A)):\mathrm{Prop}}$$ * Typal computation rules: $$\frac{\Gamma \vdash A:\mathrm{Prop}}{\Gamma \vdash \eta_{\mathrm{Prop}}(A):A =_{\mathrm{Prop}} \mathrm{toProp}_{\mathrm{El}(A)}(\mathrm{proptrunc}(A))}$$ Extensionality principle of the type of all propositions: $$\frac{\Gamma \vdash A:\mathrm{Prop} \quad \Gamma \vdash B:\mathrm{Prop}} {\Gamma \vdash \mathrm{ext}_\mathrm{Prop}(A, B):\mathrm{isEquiv}(\mathrm{transport}^\mathrm{El}(A, B))}$$ ---- I would rather define these complicated types and functions than use judgmental equality. However this would first involve proving the typal congruence rule for dependent function types, which hasn't been proven yet. Only for strict dependent function types has it been proven, but we don't have strict dependent function types because we don't have judgmental equality. ---- ... category: redirected to nlab