Not signed in (Sign In)

Not signed in

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

  • Sign in using OpenID

Discussion Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • CommentRowNumber1.
    • CommentAuthorjustin
    • CommentTimeDec 25th 2020
    • (edited Dec 25th 2020)


    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 AEA\subseteq E. For all n:n:\mathbb{N}, I define I nI_n the set {1,,n}\{1,\dots,n\} and Assoc(n)proj 1( a:I nA(i:I n,j:I n)(i=j)+(a| ia| j=))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 nI_n to AA that where constructed from programs with an additional specification that either it is proved that i=ji=j, or it is proved that the valued of the program are disjoint sets.

    Next I define the type F c:E a:Assoc(n)(c=a| 1a| n).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 x,y:A f:F(xy=proj 1(f))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 xyx\setminus y.

    Now I assume the judgment d:Dd: 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) x:A(x=)(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)(A)(a:A)\to (\emptyset\in A) ? For this, I’m going to use the element dd assumed to exist. I define the program as f(a:A)proj 1(proj 2(proj 2(d(a,a))))f(a:A) \equiv proj_1(proj_2(proj_2(d(a,a)))), that is: I evaluate the program dd at (a,a)(a,a), yielding some e: f:F(aa=proj 1(f))e: \sum_{f:F}(a\setminus a = proj_1(f)). Now I project this ee to extract the proof (aa=a| 1a| n)(a\setminus a = a|_1\cup\dots\cup a|_n) as above.

    To me, this formally defines a program (a:A) a:Assoc(n)(aa=a| 1a| n)(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 (aa=a| 1a| n)(a\setminus a = a|_1\cup\dots\cup a|_n) is the same as (=a| 1)(\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) x:A(x=)(a:A) \to \sum_{x:A}(x = \emptyset) and (a:A)(A)(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.



    • CommentRowNumber2.
    • CommentAuthorNikolajK
    • CommentTimeDec 25th 2020

    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.

    • CommentRowNumber3.
    • CommentAuthorjustin
    • CommentTimeDec 26th 2020
    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