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

]]>