@user21820 (1) This is explained by the Wadler paper I referred to, it is not related to having one more universe. (2) CoC cannot have any more universes without deleting some typing rules, this is seen if you write down the typing rules of universes for CoC, system U and the system that Coq uses.

@user21820 I don't use sized types. People put it into Agda because Agda is a place for experimentation, not development. So when somebody wrote a paper on some new type theory, they may choose to addit into Agda. Note that this will never happen unless you explicitly turn it on with options. So if you don't care about these new features, they won't bite you.

> experimentation, not development

I meant "experimentation and development".

@Couchy No don't be sorry; it's great to have more people chiming in! Could you say more about your opinion on predicativity and on what you think impredicativity might be useful for? In my opinion, true impredicativity is actually unnecessary for anything meaningful, but I would of course love to see contrary examples.

@Trebor Ah okay thanks. I didn't know that sized types was just an experimental option; I had the impression that it was something people thought was both correct and useful, since many people (including on ProofAssist SE) have had no qualms claiming proofs of various theorems in Agda using sized types, as if such proofs held much more weight than informal mathematical arguments. Do you think most people using sized types would still have done so if they knew about the inconsistency?

To clarify what I just asked, I'm asking about your impression of the user base of sized types as a whole, rather than of just people who know all the underlying technical details.

@Trebor (1) I'll take a look at the paper, thanks. (2) Do you know of a modern reference with a comparison of the systems you intend to refer to by CoC and Coq and U? I find many online sources hard to read, partly because there seems to be an incredible plethora of variants, and partly because most of those sources seem to be experts talking to themselves, and I'm not an expert...

@user21820 The current version of Agda has a dozen sources of inconsistencies (with or without experimental options), one of which I discovered. They will probably be fixed in the next version. So does Coq, so does Lean. So does every single software that is more complex than a beginner's program.

I think the sized type issue is not that it is inherently unsafe, but that we haven't figured out the exact conditions (actually we do, but the known conditions are too restrictive, so we now allow some unsafe cases).

@Trebor Oh haha.. isn't having a dozen inconsistencies even without experimental options a bad thing, in your opinion?

Once somebody figures out a set of reasonably restrictive rules, we can all be happy with sized types. Of course, it might be the case that somebody figures out that all the consistent rules are too restrictive, which will be sad.

It is a bad thing, and that's why we are fixing these bugs. But it is not the reason to abandon Agda or anything.

@Trebor What about Mizar? I've read that it is based on ZFC plus Grothendieck universes, which so far is not known to be inconsistent (even though I don't even buy plain ZFC).

@user21820 Although ZFC is probably consistent, you still got the problem of whether the Mizar system honestly reflects ZFC + Grothendieck universes. And the answer of that is probably "no".

@Trebor Yea I get that issue. I don't use Mizar or follow the development, so I don't know. I just read about it.

As for the systems CoC and U, you can read about it in Barendregt's book titled something like "typed lambda calculus", IIRC.

@Trebor Ok thanks for the reference.

@user21820 If you take 2 to be the set with two elements, then the CoC type T = forall X. ((X -> 2) -> 2) -> X has the property that T is isomorphic to its double power set.

@Trebor By the way, I also read that HOL Light was supposed to be a minimal kernel that was quite certainly safe. Though I know the whole point of a complex system is that generally user-friendly systems are complex.

@Trebor Wait, what?

In ZFC, you can take the product of all the function spaces with the same domain and codomain. This gives you a proper class including functions like x^2 : R -> R etc.

But in CoC, the set forall X. X -> X has exactly one element.

@Trebor Oh, what I meant was, is there really no counterpart to Cantor's proof in CoC?

There's a few difficulties. You can't really express equality in CoC (and if you try to you will see that it doesn't behave as you expected).

Hmm. That's a bit disappointing. In the past I had just assumed that everything I can do in predicative mathematics can be done in CoC.

CoC enjoys (or suffers?) from a property called parametricity. Meaning that you can't do weird things to types like "if this is the type of real numbers then do this, otherwise default to that".

You can only do everything uniformly and parametrically.

This is good as a programming language, but I'm not sure whether it is good for maths.

Anyway, CoC is way too weak. Its proof theoretic ordinal is something like omega^omega. Nowhere near epsilon_0.

@Trebor But if we add universes, it's supposedly crazily high strength? And yet I presume that it still cannot express Cantor's theorem well?

I understand that you cannot perform 'type-inspection', but Cantor's theorem in itself seems completely sound, and for reference here is the version I am referring to: ∀S∈set ¬∃f∈S→(S→bool) ∀g∈S→bool ∃x∈S ∀y∈S ( f(x)(y) ⇔ g(y) ).

The reason it is completely predicative is that we can predicatively prove "¬∃f∈S→(S→bool) ∀g∈S→bool ∃x∈S ∀y∈S ( f(x)(y) ⇔ g(y) )" with S and bool as mere sorts, so representing this fact by adding the quantifier "∀S∈set" is predicatively fine, just like the fact that ACA (which is completely predicative) can prove various Π[1,1]-sentences. Do you get what I'm saying, and is there any relevance to CoC?

@user21820 No, adding one more universe will allow you to embed system U. It is inconsistent. We must give up some impredicativity. Also, it is not very efficient to add universes. Adding inductive types and familys quickly blows up the strength without getting inconsistent.

@user21820 Yes and you can construct the actual diagonal thing. But you can't use it to reason that such an isomorphism cannot exist (P(X) cannot be isomorphic to X, but P(P(X)) can!).

Oh and also, although you can construct, in CoC, two functions witnessing that P(P(X)) is isomorphic to X, you can't prove (or even state) that it is isomorphic, because we lack equality.

@Trebor Oh interesting. That's very discomfiting.

Is there any (computational?) interpretation that makes it sensible for X ≅ P(P(X))?

I can't see any.

They are both meta-theoretically countable, because computable functions are countable. So there is no size issue.

It is actually saying that "there are very few functions that can be described within CoC, so few that no paradox arise".

@Trebor I know there's no size issue, but the congruence doesn't make sense even from any computational viewpoint that I can think of, because Cantor's theorem has a computable counterpart.

Well, remember that I'm not saying that it holds for all X. I'm just saying that such a fixpoint exists.

CoC has all fixpoints for functors. The least fixpoint X=X+1 is the natural numbers (+1 means adjoining one more element). The greatest fixpoint is the natural numbers extended with infinity.

I don't think that type is particularly useful. It behaves weird, and I haven't found any use of it in practice.

@Trebor Oh just existence of a fixed-point. That's not a problem then if we allow non-termination. But I presume the fixed-point you are referring to in CoC is actually 'terminating'.

Yes, they are terminating. If you allow non-termination then we can even construct P(X) \cong X

In Coq though, if X:Set you can't construct any of these, and you do have cantor's paradox if you could.

So that's a bit of a problem then, because I don't believe there is a good computational interpretation of a fixed point of ( X ↦ X→(X→bool) ) that is 'terminating' in a natural sense. Is the proof of "the CoC type T = forall X. ((X -> 2) -> 2) -> X has the property that T is isomorphic to its double power set." short?

Yes, it's in Wadler's paper.

Ok good I'm really going to have to go through that (later).

Actually it is just Lambek's theorem that initial algebras are isomorphisms.

Thanks a lot! Do you mind if I ping you later for further questions?

@Trebor I don't know anything about those, unfortunately.

No problem. But I might not be able to answer all of them, of course ;)

@Trebor Sure, thank you. And I agree with your moderator self-nomination that you're "working towards making professional knowledge more accessible to newcomers.". =)

@Trebor Hmm I can't find anything in Wadler's paper that talks about "forall X. ((X -> 2) -> 2) -> X" or "double power set". Do you mind explaining it explicitly?

What would you like to know? He explains the general case. I have nothing more to add apart from simply specializing to this.

As long as F is a functor (i.e. for functions a -> b, you naturally have F a -> F b which preserves composition), Wadler can construct its least and greatest fixpoint.

The power set operation is almost a functor, except it reverses the direction of the arrows (inverse image). If you try to use the direct image to make the directions right, you need some sort of classical logic. But the double power set is then again a functor.

@Trebor That's the problem; I do not understand how Pow is anything like a functor. If you can explain in ZFC terms, I would surely get it.

Inverse image is the usual term, right?

If there's a function f : A -> B, and we have a subset b : B -> Bool (i.e. the characteristic function), then a(x) = b(f(x)) is the inverse image.

So you have the way to turn any function from A to B into a function from Pow(B) to Pow(A). And doing it again, you have a function from Pow(Pow(A)) to Pow(Pow(B)).

@Trebor Oh. I think I know what I was missing. I was interpreting the webpage's definition in ZFC terms as follows: A functor F is a definable function such that ∀S,T∈set ∀g∈S→T ( F(g)∈F(S)→F(T) ) (and ...). But that isn't what it intended; the F acts differently on terms than on types. Is that right?

A functor is a term in category theory. If you got a bunch of objects (e.g. groups) and a bunch of morphisms (e.g. group homomorphisms), it is called a category. In CoC, types are the objects and functions are the morphisms. A functor is two things, one acts on the objects and one acts on the morphisms.

And we refer to the whole functor by the former part. This is maybe a bad practice, like how we refer to the topological space of the standard real line with R, which is supposed to be the underlying set.

@Trebor I see. That functor thing makes sense now. So to get the fixed-point of Pow^2, I see you used the least fixed-point. But I have one question; why does that webpage say "Lfix X. F X = All X. (F X -> X) -> X." instead of just "Lfix F = All X. (F X -> X) -> X."?

Ah, I think I know; because they want to impose syntactic restrictions on the defining expression, so Lfix can't be a black-box term. Correct?

I still don't know why ( ∀X . ( F X → X ) → X ) works, but at least I know where you got what you wrote from.

It is most helpful to consider more elementary examples.

Do you have any recommended easier example?

Maybe try F(X) = X+1 which gives you natural numbers, or F(X) = 1 + A*X where A is any constant type, and * is the cartesian product. This gives you finite lists.

What is "+"? Disjoint sum-type?

Wadler is writing more from a programmer's perspective. These were well-discussed, especially among the Haskell community at that time.

@user21820 Yeah.

Yea I get that it's well discussed in a certain community, but honestly I don't like the abstruseness of their syntax.

@Trebor: Oh and here's an unrelated question: The author of this PDF on CIC said "Impredicative systems are powerful but also very fragile in the sense that impredicativity does not interact very well with other features leading rapidly to inconsistent systems.". Do you agree, or do you actually think there is absolutely nothing wrong with impredicative Prop?

@user21820 Syntax is made to suit the need. So when you tend to have a plethora of function calls, you will embrace the syntax that doesn't require parentheses for function calls. And when you use cartesian product / disjoint union more than arithmetic operations, you tend to use + and * for the former.

@user21820 Maybe there's something wrong. That's debatable. But there's nothing wrong to claim that impredicative Set and Prop is dangerous.

Personally I am very slightly in favor of predicative Prop.

I see. Lol I got the opposite impression because in your second comment to me you said "propositional inpredicativity is just fine" haha.

But I felt that it was similar to the impredicativity in full ZFC as opposed to bounded ZFC.

The interesting thing is that bounded ZFC is enough for practically all modern mathematics outside of set theory and higher logic.

@user21820 Well that's because people like the familiar stuff ;) I work with Agda more than all the other PAs added together.

Aha...

@user21820 Since systems based off first order logic make the distinctions of terms and propositions very clear, it's not very comparable.

We don't care about stuff like proof irrelevance, because they can't even be stated in first order logic.

But with CoC, terms, types, proofs, propositions all starts to mix up and interact.

@Trebor Why is it not the same? The common claim that ZFC can be given an ontology based on the cumulative hierarchy is broken precisely in that aspect, even after granting full power-sets as an assumed primitive. Full specification/replacement requires the universe to be fixed in order for the unbounded quantifiers to make sense, which is impredicative and unjustifiable because if one cannot build a level without the entire universe then one cannot get the universe!

Ah so you are talking about Prop impredicativity.

Yup that's what I meant.