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!