Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

• Forgot your password?
• Apply for membership

1. • CommentRowNumber1.
   • CommentAuthorjustin
   • CommentTimeDec 25th 2020
   • (edited Dec 25th 2020)
   • PermaLink
   Author: justin
   Format: MarkdownItexHello, 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

   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

2. • CommentRowNumber2.
   • CommentAuthorNikolajK
   • CommentTimeDec 25th 2020
   • PermaLink
   Author: NikolajK
   Format: MarkdownItexAs 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](https://github.com/leanprover-community/mathlib/blob/master/src/set_theory/zfc.lean) and corresponding [docs](https://leanprover-community.github.io/mathlib_docs/set_theory/zfc.html).

   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.

3. • CommentRowNumber3.
   • CommentAuthorjustin
   • CommentTimeDec 26th 2020
   • PermaLink
   Author: justin
   Format: TextThank you for your message, Indeed, I've seen that kind of code during my resource researches, and I feel like it could be useful to invest some time to learn to read that. From an IT point of view, as shown in the link, it seems to me (although I don't know much on the topic) that the zfc materials is grouped in a package and then included for later use, in other packages. My approach is actually kind of similar, but instead of implementing zfc using type theory, I assume zfc is already constructed as "the usual theory of sets I know about". Maybe what I have in mind is similar more similar to the exposition made in https://www.sciencedirect.com/science/article/pii/S157086830700081X Regards, Justin

   Thank you for your message,
   
   Indeed, I've seen that kind of code during my resource researches, and I feel like it could be useful to invest some time to learn to read that.
   
   From an IT point of view, as shown in the link, it seems to me (although I don't know much on the topic) that the zfc materials is grouped in a package and then included for later use, in other packages.
   My approach is actually kind of similar, but instead of implementing zfc using type theory, I assume zfc is already constructed as "the usual theory of sets I know about".
   
   Maybe what I have in mind is similar more similar to the exposition made in https://www.sciencedirect.com/science/article/pii/S157086830700081X
   
   Regards,
   
   Justin