Prototype: the finite-type universe over a non-discrete base

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

The universe of [GhaniNordvallForsbergMalatesta2015], Examples 2.5 and 2.6, with the decoding taking values in a category of finite sets — a genuine category, not a discrete one. Geb/Mathlib/Data/PFunctor/IndRec/Universes.lean writes the same universe over Type treated as discrete, which is what the inductive-recursive presentation requires; this module asks what a presheaf polynomial functor over a base with its morphisms restored computes instead. The answer is in the sibling Value module.

The shape presheaf and the arities are coproducts of representables, which is the presentation a family of objects acquires under the embedding of the free coproduct completion Fam(C) into PSh(C) (Fam(C) is the free set-indexed coproduct completion, Remarks 2.3 of [GhaniNordvallForsbergMalatesta2015]). The type former is a parameter, so the dependent-sum and dependent-product universes are two instances of one functor differing only in the shape-output map q.

Main definitions

Card / El — the base category's objects (the finite cardinals, with functions as morphisms) and their elements.

Code / Former / out — the code formers, a type former, and the object a code former's output decodes to.

Idx / bound — the representable summands of a code former's arity and the object each is indexed by: bind's are the code being bound and the family under the binder.

Shp / Dir — the shapes and directions: the total spaces of the shape presheaf Σ_c y(out c) and of the arity presheaf Σ_k y(bound c k).

universeData / universeFunctor — the operations and the functor with its seven functor laws, both parameterized by the type former.

sigmaFormer / piFormer / sigmaUniverse / piUniverse — the dependent-sum and dependent-product formers and the two functors they give.

Main statements

directionRestr_id_law through reindex_comp_law — the seven functor laws.

Implementation notes

The base is defined here rather than taken to be Geb/Mathlib/CategoryTheory/FinSetSkel, which has the same objects. That category seals FinSetSkel.Hom irreducible so that morphism equality is decidable without Classical.choice; the seal blocks the definitional reasoning this construction runs on. The p.r.a. laws ReindexId and ReindexComp compare directions over shapes whose morphism components are different composites, and the arity reindexing here is the identity map because the arity depends on the shape only through its code former. Both rely on composition being definitionally associative and unital, which holds for functions and not past the seal: unfolding a sealed composite reaches a projection out of the irreducible Hom and the elaborator fails rather than getting stuck. FinSetSkel.toIdxFun and FinSetSkel.ofIdxFun exhibit the two bases' correspondence.

Shp and Dir are the total spaces of presheaves of the form Σ_k y(bound k), so every restriction map — directionRestr, shapeRestr — is precomposition. The shape restriction is written by projection and eqToHom rather than by matching on the shape, which keeps (shapeRestr g a).1.1 definitionally equal to a.1.1; since Dir mentions only that component, the arity reindexing is the identity.

References

[GhaniNordvallForsbergMalatesta2015]

[HancockMcBrideGhaniMalatestaAltenkirch2013]

[Weber2007]

Tags

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

The base category

An object of the base: a finite cardinal.

The number of elements.

The elements of an object.

The base category: finite cardinals and functions between their elements. Composition is function composition, so the category laws hold definitionally.

Codes

The code formers: one nullary former per object of the base, and one binder former taking an object and a family of objects indexed by its elements.

The code of the object c.

The binder former at the object S and the family T.

A type former: what the binder does to an object and a family of objects indexed by its elements.

The object a code former's output decodes to.

The representable summands of a code former's arity: iota has none, bind has the code it binds and one code per element of the bound object.

The object a summand is indexed by.

Shapes and directions

The shapes: the total space of the shape presheaf Σ_c y(out c). A shape is a code former together with a morphism into the object its output decodes to.

The directions of a shape: the total space of the arity presheaf Σ_k y(bound c k). Only the shape's code former is used, so shapes sharing a code former have the same directions.

The functor

The operations of the universe endofunctor at a type former. Every restriction map is precomposition.

The functor laws

Every restriction map is precomposition, so the laws are the category laws, which hold definitionally for functions. They are stated separately rather than inline because reindex_comp_law needs shapeRestr_comp_law by name: the law is stated relative to it.

directionRestr preserves identities.

directionRestr reverses composition.

shapeRestr preserves identities.

shapeRestr reverses composition.

The arity reindexing is a morphism of arity presheaves. It is the identity map, the arity depending on the shape only through its code former.

The arity reindexing along an identity is the identity.

The arity reindexing along a composite is the composite of the reindexings.

The universe endofunctor at a type former: the operations with the seven functor laws.

The two type formers

The dependent-sum former: the object of pairs.

The dependent-product former: the object of sections.

The universe closed under dependent sums.

The universe closed under dependent products.