I believe a counter-model to "there is a specified set that covers
Set" is presheaves on the 2-category X with two objects a and b,
X(b,a)=0, X(a,a)=1, and X(b,b) = X(a,b) = Bℤ.
Thanks for the hint! Let me see if I can work it out:
We let G = Bℤ, considered as a 2-group with delooping BG = B²ℤ. Write * for the basepoint.
Take ∂ : BG → U, ∂ t = (* = t). We get the direct category X by attaching to the terminal category 1 a new level of objects BG along the boundary operator ∂.
(We could make another direct category using ∂ t = (t = t); this also works!)
The object a is the unique object at level 0; write b(t), t : BG, for the objects at level 1.
Contexts Γ ⊢ :
Γ₀ : U
Γ₁ : (t : BG) → (∂ t → Γ₀) → U
Representable contexts a and b(t), t : BG :
a₀ = 1
a₀ t u = 0
b(t)₀ = ∂ t = (* = t)
b(t)₁ t' u = (q : t' = t) × (u =_q id)
Evaluation of Γ at a is Γ₀, evaluation at b(t), t : BG, is
Γ(t) = (u : ∂ t → Γ₀) × Γ₁ t u
(So Γ evaluates to sets iff Γ₀ and Γ₁ are Set-valued)
Substitutions σ : Γ → Δ :
σ₀ : Γ₀ → Δ₀
σ₁ : (t : BG) → (u : ∂ t → Γ₀) → Γ₁ t u → Δ₁ t (σ₀ ∘ u)
Action of σ on values at b(t), t : BG :
σ(t) : Γ(t) → Δ(t)
σ(t) (u , γ) = (σ₀ ∘ u , σ₁ t u γ)
Families Γ ⊢ A :
A₀ : Γ₀ → U
A₁ : (t : BG) → (u : ∂ t → Γ₀) → Γ₁ t u → ((x : ∂ t) → A₀ (u x)) → U
Universe of sets, Set ⊢ :
Set₀ = Set
Set₁ t u = ((x : ∂ t) → u x) → Set
hence value over b(t) is:
Set(t) = (u : ∂ t → Set) × (((x : ∂ t) → u x) → Set)
(I think this is correct; I'm skipping the entire calculation of the interpretation of (A : U) × is-set A. We really only need the level zero component, and that's definitely Set.)
Now assume there is a set context Γ and a levelwise surjection σ : Γ → Set :
σ₀ : Γ₀ → Set (i.e., a cover of Set at the meta-level)
σ₁ : (t : BG) → (u : ∂ t → Γ₀) → Γ₁ t u → ((x : ∂ t) → σ₀ (u x)) → Set
so we assume that
σ(t) : Γ(t) → (v : ∂ t → Set) × (((x : ∂ t) → v x) → Set)
σ(t) (u , γ) = (σ₀ ∘ u , σ₁ t u γ)
is surjective for each t : BG.
This is a proposition, so it holds iff it holds at the basepoint * : BG.
We have ∂ * = (* = *) = G = Bℤ, so v : Bℤ → Set amounts to a set with an automorphism.
However, any u : Bℤ → Γ₀ is constant, since Γ₀ is a set, so a non-trivial v cannot be written as σ₀ ∘ u for any such u. Nice!
One can then get a
counter-model to "there merely exists a set that covers Set" with
presheaves on X * 1.
This I didn't check. But couldn't we here instead appeal to homotopy canonicity? Since Set is a closed type, if there is a proof of the mere existence of a set cover of Set, we could extract a specific term for one, and then obtain a contradiction in the above model.
Cheers,
Ulrik