Prototype: where the free coproduct completion sits inside presheaves

Throwaway exploration, not upstream-eligible content. Every declaration here is Classical.choice-free.

Fam(C), the free set-indexed coproduct completion of C (Remarks 2.3 of [GhaniNordvallForsbergMalatesta2015]), embeds into PSh(C) as the coproducts of representables. Geb/Prototypes/FinCardUniverse/ works over PSh(C), so the question is which presheaf polynomial functors carry Fam(C) into itself — whether a universe built over presheaves can be read back as a family of codes.

This module answers it, and the answer is not the one the value computation of FinCardUniverse might suggest. Membership in Fam(C) is closed under set-indexed coproducts, so a representable times a constant is still in Fam(C): isFamPsh_praPsh shows that the shape of the p.r.a. formula's value — a sum over shapes of a representable times the set of arity homs — is a family presheaf whatever that set of arity homs is. So the functors do restrict, and the coercion multiplicity the finite model exhibits is not an obstruction to restricting: it lands in the code type, not in the decoding.

What does obstruct is the shape presheaf. Since T₁ = T(1), a functor restricts only if the terminal presheaf's image does, and the terminal presheaf need not itself lie in Fam(C): isFamPsh_topPsh_of_terminal shows it does when C has a terminal object, and not_isFamPsh_topPsh shows it does not over the walking parallel pair, which has none. The category of elements of the terminal presheaf is C itself, so this is the general criterion — a presheaf lies in Fam(C) exactly when every connected component of its category of elements has a terminal object — read at the terminal presheaf. That general criterion is not formalized here; the two brackets are.

Main definitions

famPsh — a family of objects as a presheaf, the coproduct of representables Σ_u y(d u).

IsFamPsh — membership in the image, as an unbundled natural isomorphism.

praPsh — the shape of the p.r.a. formula's value: a sum over shapes of a representable times a set.

topPsh — the terminal presheaf.

Main statements

isFamPsh_praPsh — the p.r.a. formula's value is a family presheaf, with the codes the shapes paired with their arity homs and the decoding read off the shape alone.

isFamPsh_topPsh_of_terminal — the terminal presheaf is a family presheaf when the base has a terminal object.

not_isFamPsh_topPsh — and is not, over the walking parallel pair.

References

[GhaniNordvallForsbergMalatesta2015]

[Weber2007]

Tags

prototype, presheaf, free coproduct completion, parametric right adjoint, inductive-recursive

Family presheaves

A family of objects as a presheaf: the coproduct of representables Σ_u y(d u). This is the embedding of Fam(C) into PSh(C).

A presheaf lies in the image of Fam(C): it is naturally isomorphic to a family presheaf. The isomorphism is unbundled — a family of equivalences with the naturality equation — so that no hom of a functor category is named and the statement stays Classical.choice-free.

The p.r.a. formula's value

At a shape presheaf that is itself a family presheaf, and an arity assignment depending only on the shape's index, the p.r.a. formula T(Z)(j) = Σ_{a ∈ T₁(j)} Hom(E_a, Z) takes the form below: a sum over shapes of a representable times the set of arity homs.

The p.r.a. formula's value: shapes S lying over objects o s, each carrying a set A s of arity homs.

The p.r.a. formula's value is a family presheaf: the codes are the shapes paired with their arity homs, and the decoding is read off the shape alone.

This is why the multiplicity of arity homs is no obstruction to restricting to Fam(C): it is absorbed into the code type, the coproduct completion being closed under set-indexed coproducts. It is also why restricting does not recover an inductive-recursive interpretation — the decoding o s does not mention the arity hom, so it does not depend on the codes the shape binds.

The terminal presheaf

T₁ = T(1), so a functor restricts only if the terminal presheaf's image does. Whether the terminal presheaf is itself a family presheaf is a property of the base.

The terminal presheaf.

Over a base with a terminal object, the terminal presheaf is the representable it represents, hence a family presheaf.

A base where it fails

The walking parallel pair has no terminal object: zero is not terminal because nothing maps from one to it, and one is not because two morphisms map into it from zero.

Nothing maps from one to zero.

The two parallel morphisms are distinct.

Over the walking parallel pair the terminal presheaf is not a family presheaf. A code would have to decode to one, since nothing maps from one to zero; but then the two parallel morphisms give two elements over zero, where a family presheaf isomorphic to the terminal one has exactly one.

Universal elements

A family presheaf's category of elements is a coproduct of slices, and a code is recovered as the terminal object of its component: the element carrying the identity — the universal element of that representable summand, in the sense of the Yoneda correspondence, and Lawvere's generic figure.

The word "generic" is avoided here. In the parametric-right-adjoint literature this repository cites ([Weber2007], [nLabParametricRightAdjoint]) a morphism f : B ⟶ T A is T-generic when every commuting square over it has a unique T-fill, and T is a parametric right adjoint exactly when every map into a T-value factors as a generic followed by a T-image. Under that factorization it is the coercion that is the generic part and the universal element that is the trivially-factoring one, so calling the latter generic would invert the established usage in the one setting where it is in play.

The universal element is what an inductive-recursive constraint on a direction would ask for — asking for it says d u = i on the nose, where asking for an arbitrary element says only i ⟶ d u.

The constraint cannot be imposed while keeping every morphism of families, because universality is not stable: a morphism sends the universal element of u to its own decoding map, which is universal only when that map is a transport. isUniversalElement_famMorApp is the stability on the morphisms that do preserve it — the split cartesian fragment, which is Dybjer and Setzer's setting.

IsSplitCoercion weakens the constraint from "the coercion is a transport" to "the coercion is a split epimorphism", and isSplitCoercion_famMorApp is the corresponding stability: it holds on the morphisms whose decoding maps are split epimorphisms. So there is a constraint strictly weaker than universality that survives non-invertible morphisms, which is the setting Geb/Prototypes/UniverseVariance/ shows both type formers act over.

The universal element of a code's component: the code with the identity.

An element is universal when its coercion is a transport: the object it lies over is the code's decoding, on the nose.

A morphism of families: a map of codes and, for each code, a morphism of decodings.

The map of codes.

The comparison of decodings.

The action of a morphism of families on the family presheaves.

The action is natural.

A morphism preserves universal elements when every decoding comparison is a transport. These are the split cartesian morphisms, and Dybjer and Setzer's Fam |C| is the fragment they span.

Genericity is stable under the morphisms that preserve it.