Commuting lift and dependent sums

Stream: Type theory

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

I believe that they following proposition is not provable in Lean (though I'd be very interested to be proven wrong):

example (A : Type 0) (B : A → Type 0) :
    ULift.{1} (@Sigma.{0,0} A B) = @Sigma.{1,1} (ULift.{1} A) (fun a => ULift.{1} (B a.down)) := by
  sorry

Does anyone know if there is a model of Lean in which it is actually false?

[Kevin Buzzard]

Do you know the status of this simpler question:

example (A B : Type 0) : ULift.{1} (A × B) = (ULift.{1} A × ULift.{1} B) := sorry

?

[Kevin Buzzard]

And an even dumber question on my part: do you know if there is a model of Lean and two types X and Y in the same universe which can be put into bijection with each other but for which it is "false" that they are equal? By "false" I mean "false as in the sense of your question" but I don't really know what that means. Do you mean "provably false in Lean"?

[Mario Carneiro]

Yes, both of these two are false in a model that tags types with the names of the inductive types that are used to build them

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

By "false" I mean "false as in the sense of your question" but I don't really know what that means.

There are numerous notions of "model of type theory", so the original question really is ambiguous. But if we restrict "model" to mean something of the same shape as #leantt, we'd expect that it comes with an interpretation function taking every (closed/variable-free) type $A$ to some set $⟦A⟧$. If it can also interpret any (closed) term $e : A$ as another set $⟦e⟧ ∈ ⟦A⟧$, then the question of whether the original equality is true in that model is asking whether $⟦\texttt{ULift.{1} (@Sigma.{0,0} A B) = @Sigma.{1,1} (ULift.{1} A) (fun a => ULift.{1} (B a.down))}⟧$ is nonempty.

Do you mean "provably false in Lean"?

I do not mean that; a provably false proposition would be false in every (sound) model, whereas I was just looking for one counterexample.

do you know if there is a model of Lean and two types X and Y in the same universe which can be put into bijection with each other but for which it is "false" that they are equal?

This sounds like univalence, and I think it might already be false in the "intended model" of #leantt? The interpretation of $=$ is very strong, requiring both sides to be literally equal as sets. Then α + (β + γ) ≃ (α + β) + γ, but the two sets $⟦α⟧ ⊔ (⟦β⟧ ⊔ ⟦γ⟧)$ and $(⟦α⟧ ⊔ ⟦β⟧) ⊔ ⟦γ⟧$ need not be equal (maybe depending on the specific encoding of disjoint unions).

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Yes, both of these two are false in a model that tags types with the names of the inductive types that are used to build them

Do you mean something like section 6.4 of #leantt? Indeed I guess we'd have different sequences of ulift/Σ tags then.

But maybe a more interesting question: are the two ulift commutation equations consistent? It seems that they are; in #leantt they interpret as literally the same set because ulift is interpreted as nothing/the identity map.

[Kevin Buzzard]

They're true in the cardinality model right? So they're consistent? I barely know what I'm talking about here as is probably clear

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

I guess so, I've just never seen the mythical 'cardinality model' written down :)