Prototype: what the universe functor computes over a non-discrete base

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

Basic builds the universe endofunctor over a base of finite sets with all functions between them as morphisms. This module computes its value on a family of codes and records what the computation shows.

A family of codes (U, d : U → Card) — an object of the free coproduct completion Fam(Card) — becomes the presheaf famPresheaf U d, the coproduct of representables Σ_u y(d u). The p.r.a. formula then reads the functor's value at that presheaf off the arity homs, and arityHomEquiv computes them: an arity hom for the shape at a code former is a choice, for each summand k of its arity, of a code u together with a morphism bound k ⟶ d u.

That morphism is where the two presentations part. The inductive-recursive presentation of the same universe (Geb/Mathlib/Data/PFunctor/IndRec/Universes.lean) works over Type treated as discrete, so its corresponding datum is an equality: the bound code's decoding is the declared object. Over a base with morphisms the equality relaxes to a coercion, and junkArity exhibits a consequence: a binder shape declaring the empty object accepts a code denoting the singleton. Since a shape's output index is fixed by the shape (out_emptyBind), the code so formed decodes by its declaration rather than by its children — the recursion of induction-recursion is decoupled.

The relaxation is not a defect of the encoding but the price of functoriality. piFormer_not_covariant reproduces, at this scale, the obstruction of Example 3.6 of [GhaniNordvallForsbergMalatesta2015]: the dependent-product former admits no covariant action on the base's morphisms, while sigmaFormer_covariant shows the dependent-sum former does at the same instance. The universe functor of Basic is nonetheless total in the type former — sigmaUniverse and piUniverse differ only in the shape-output map — precisely because the declared decoding it carries is not required to match the decodings of its children.

Main definitions

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

arityHomEquiv — the arity homs into such a presheaf: one code and one coercion per arity summand.

oneFam / emptyBindCode / junkShape / junkArity / junkObj — the family with one code denoting the singleton, the binder code declaring the empty object, and the element of the functor's value that binds the one against the other.

counterFam / counterMap / counterFamReindexed — the data of Example 3.6.

Main statements

junk_decoding_ne — the bound code's decoding differs from the object the shape declares, so the arity hom has no inductive-recursive counterpart.

out_emptyBind — the shape's output object is fixed by the declaration.

sigmaFormer_covariant / piFormer_not_covariant — Example 3.6 at this scale.

References

[GhaniNordvallForsbergMalatesta2015]

[Weber2007]

Tags

prototype, inductive-recursive, presheaf, universe, parametric right adjoint, finite set

Families as presheaves

A family of codes as a presheaf: the coproduct of representables Σ_u y(d u). This is the embedding of the free coproduct completion Fam(Card) into PSh(Card); its fiber over c is not the codes decoding to c but the codes admitting a morphism from c.

The arity homs

The arity homs into a family presheaf: an arity hom for the shape a is a choice, for each arity summand k, of a code u together with a morphism bound k ⟶ d u. Forward is evaluation at the summands' universal directions and backward is precomposition, the two round trips being Yoneda.

The morphism is the point of the computation. The inductive-recursive presentation over a discrete base has an equality bound k = d u here; over a base with morphisms no arity can ask for that, since a direction constrains the index of the value it receives and the index of a value in a family presheaf is not its code's decoding.

A code with no inductive-recursive counterpart

The family with one code, denoting the singleton.

The binder code declaring the empty object as the object it binds.

The shape at that code, over the object its dependent-sum output decodes to.

An arity hom for junkShape binding the single code of oneFam: the summand asks for a morphism ⟨0⟩ ⟶ ⟨1⟩, which the empty function supplies, where the inductive-recursive presentation would demand ⟨1⟩ = ⟨0⟩. The second summand family is empty.

The bound code's decoding is not the object the shape declares.

The shape's output object is fixed by its declaration, whatever code the binder is applied to: the dependent sum over the declared empty object is the empty object.

The arity hom as an element of the functor's value at the family presheaf, through the p.r.a. formula.

Example 3.6 at this scale

The obstruction to interpreting the dependent-product universe over a base with morphisms: reindexing the family along a morphism of the bound object must act covariantly on the former's output.

The family of the counterexample: the singleton indexes the empty object.

The morphism of the counterexample: the unique map from the empty object to the singleton.

The counterexample's family reindexed along that morphism.

The dependent-sum former acts covariantly at the counterexample: both sides are the empty object.

The dependent-product former does not: the empty product is the singleton and the product of the counterexample family is empty, and there is no map from the singleton to the empty object. This is Example 3.6 of [GhaniNordvallForsbergMalatesta2015] at the smallest scale that hosts it.

The counterexample's morphism admits no section: a section would be a map from the singleton to the empty object. What the dependent-product former's action needs is exactly such a section, which is the subject of Geb/Prototypes/UniverseVariance.lean.