Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
Hello,
I’m starting to learn about type theory (in HoTT or articles on the net) after having been “passively” using it for years in programming languages. My question may certainly be a bit simple but I couldn’t find a resource on the net, so better ask it!
Let’s say I take as granted usual set-theory (ZFC let’say), with its standard notion of set, function and real numbers. Then I would like to “inject” those objects in type theory formalism. My goal is to exploit the type theory expression system for constructive proofs without having “constructively-obtained objects”. In other words, I don’t really care about constructive sets, reals, measures, or anything. I’m more interested in expression theorems and structures in type theory, and using this language for object manipulation.
So I started an easy example or semi-ring of parts (from measure theory). So far, it goes at follows: (1) I use “set” to talk abut ZFC sets, “function” for function in the usual ZFC sense, and “program” for arrows from type theory (2) for any set E, I abuse notation by writing x:E when an object (set) x belongs to E, in the usual sense (judgment)
Fix two sets $A\subseteq E$. For all $n:\mathbb{N}$, I define $I_n$ the set $\{1,\dots,n\}$ and $Assoc(n) \equiv proj_1\bigg(\sum_{a:I_n\to A}(i:I_n,j:I_n)\to (i=j) + (a|_i \cap a|_j = \emptyset) \bigg)$ So if I don’t mistake, this consists of programs from $I_n$ to $A$ that where constructed from programs with an additional specification that either it is proved that $i=j$, or it is proved that the valued of the program are disjoint sets.
Next I define the type $F \equiv \sum_{c: E}\sum_{a:Assoc(n)} (c = a|_1 \cup \dots \cup a|_n) .$ If I don’t mistake, this type consists of (dependent) programs that provide a proof that c (in E) may be written as a disjoint finite union of elements in A.
Next I define the type $D \equiv \prod_{x,y:A}\sum_{f:F}(x\setminus y = proj_1(f))$ If I don’t mistake, this consists of programs that prove that for all x,y: A, there is a writing of the difference $x\setminus y$.
Now I assume the judgment $d: D$ is true (think of A as being a semi-ring in E, but that won’t be important for the remaining part), and I’m interested in constructing a program for $(a:A) \to \sum_{x:A}(x = \emptyset)$, that is: as soon as there exists an element in A, the empty set belongs to A. First, is that indeed equivalent to $(a:A)\to (\emptyset\in A)$ ? For this, I’m going to use the element $d$ assumed to exist. I define the program as $f(a:A) \equiv proj_1(proj_2(proj_2(d(a,a))))$, that is: I evaluate the program $d$ at $(a,a)$, yielding some $e: \sum_{f:F}(a\setminus a = proj_1(f))$. Now I project this $e$ to extract the proof $(a\setminus a = a|_1\cup\dots\cup a|_n)$ as above.
To me, this formally defines a program $(a:A) \to \sum_{a:Assoc(n)}(a\setminus a = a|_1\cup\dots\cup a|_n)$. In my eyes, this is enough to conclude, because the type $(a\setminus a = a|_1\cup\dots\cup a|_n)$ is the same as $(\emptyset=a|_1)$. But here I’m not sure how I should justify the argument. I’m ok to “inject” standard set-theoretic logic, so to me, it is sufficient to have a lemma proving this somewhere, which is kind of trivial. In the same spirit, is it ok to “assume” that $(a:A) \to \sum_{x:A}(x = \emptyset)$ and $(a:A)\to (\emptyset\in A)$ are equivalent programs?
Could someone, somehow validate my approach here?
I emphasize on the idea that I would like to exploit the formalism of type theory without committing to constructive analysis. I like my usual non-constructive analysis objects and I wouldn’t be happy in facing hard and touchy constructivist problems.
Regards,
Justin
As a pointer (independent of your approach and type theoretical framework), maybe it’s interesting to see other implementations.
E.g. there’s that model in Lean, see the zfc
-github page and corresponding docs.
1 to 3 of 3