Prototype: the dependent-type universe as a presheaf over the walking arrow

Throwaway exploration, not upstream-eligible content. This is a Lean port of the IRCode/IRdecode example of the Idris-2 file src/LanguageDef/Test/PolyIndTypesTest.idr — the universe closed under dependent sums and dependent products — in the inductive-inductive (arrow) formulation of that file, on top of the presheaf inductive-inductive types of Geb.Mathlib.Data.PFunctor.Presheaf.W (the W-types of presheaf polynomial endofunctors), with the walking arrow as the underlying category.

The construction

The walking arrow is Fin 2 as a preorder (the unique non-identity morphism 0 ⟶ 1). A presheaf on it is a pair of types with a map, so the presheaf initial algebra of an endofunctor F : PresheafPFunctor (Fin 2) (Fin 2) is a pair of mutually-defined types together with a fibration — the presheaf inductive-inductive reading of an inductive-recursive definition: one fibre plays the role of the data type and the other the role of the decoding, with the restriction map as the decoder.

univPsh K is the endofunctor of the Idris example: the shapes are the constructors — the starting-type codes iota k (k : K), the dependent-sum code sigma, the dependent-product code pi, and the two term shapes termSigma, termPi — and the directions are their recursive fields: no fields for iota, the bound code for sigma/pi, and for the terms the code together with a payload. Every shape and direction is a finite type (the sigma/pi code directions are a point and the term directions are two points).

The W-type univW K := (univPsh K).W is a presheaf over the walking arrow: Codes := (univW K).obj ⟨0⟩ is the type of codes, Terms := (univW K).obj ⟨1⟩ the type of terms, and fib : Terms → Codes — the restriction map of the presheaf along 0 ⟶ 1 — the decoding of a term into its code. A term termSigma p d decodes to the sigma code at p, discarding the payload d; dually termPi p d decodes to the pi code at p. The fibre of fib over a code — the type of its terms — is therefore the payload type: over a sigma or pi code it is (isomorphic to) the codes themselves, and over a starting-type code it is empty.

Relationship to the Idris-2 formulation

The Idris-2 file defines the same universe twice: once by explicit induction-recursion (IRCode, IRdecode — the family formulation, which the Lean port Geb.Mathlib.Data.PFunctor.IndRec.Universes follows) and once inductively-inductively over arrows (IRCode', IRTerm, IRfib — the arrow formulation, a presheaf over the walking arrow, whose domain is the terms and whose codomain the codes). This module follows the arrow formulation. Two deviations are forced by the W-type machinery, and both are recorded here for the review this prototype is intended for:

In the Idris-2 arrow formulation a code constructor carries its recursive data in its shape: IRCsigma' u v is a node whose constructor argument is the pair (u, v) with u : IRCode' and v : IRfib u → IRCode'. A W-type of a polynomial functor has a fixed shape type, so the data of a code cannot live in its shape; it lives in its children. Here the bound code u is a child, and the family v — a function, and so not a well-founded tree — is dropped, the term payload taking its place. The dependent-sum and dependent-product formers are consequently binary: sigma (u, v) with v : Fib u → Code is not representable; the code former at u is.

In the Idris-2 formulation the terms' payloads are elements of the decodings, which may be arbitrary types. A W-type's children are trees, so a leaf payload cannot be carried; the payload here is itself a code.

Both deviations make the types smaller than the Idris-2 types: every code and term is a well-founded tree built from finite shapes and directions, and the decoding of a code — the fibre of fib — is a subtype of the terms, not an arbitrary type. What is preserved is the shape of the example: a universe generated by starting types, closed under dependent sums and products, whose terms decode to their codes by the walking-arrow fibration, obtained as the presheaf initial algebra rather than by explicit induction-recursion.

Main definitions

waHom — the unique non-identity morphism 0 ⟶ 1 of the walking arrow.

univShape / univDir / univR / univQ — the shapes (the constructor tags), directions (the recursive fields), the direction-input map, and the shape-output map of univPsh.

univPsh — the presheaf polynomial endofunctor over the walking arrow.

univW — its W-type, a presheaf over the walking arrow.

Codes / Terms / fib — the two fibres and the fibration.

univIota / univSigma / univPi — the code constructors.

univTermSigma / univTermPi — the term constructors.

Main statements

univShapeRestr_over — the restricted shape lies over the target index.

univDirection_empty — every shape has no directions over 1; all recursion is over the code fibre.

univPshLaws — the seven functor laws of univPsh; the whole construction is Classical.choice-free, depending only on propext and Quot.sound.

The decoding theorems — fib (univTermSigma p d) = univSigma p and the fibre statement fib_eq_iff — go through the root-restriction wRestrTree of the presheaf W-type, whose computation is too deep for this prototype; they are deferred to the review below ("Decoding").

Tags

prototype, inductive-inductive, presheaf, walking arrow, W-type, universe, dependent sum, dependent product

The unique non-identity morphism of the walking arrow (Fin 2 as a preorder), 0 ⟶ 1.

The presheaf endofunctor

The shapes of univPsh: the starting-type code iota k for each k : K, the dependent-sum code sigma, the dependent-product code pi, and the two term shapes termSigma, termPi.

The directions of univPsh: none for iota; the bound code (a point) for sigma and pi; and the code-and-payload pair (two points) for the two term shapes.

The direction-input map: every direction lies over the code fibre 0, so the recursion of the W-type runs through the codes.

The shape-output map: iota, sigma, and pi are codes (fibre 0); termSigma and termPi are terms (fibre 1).

The slice polynomial functor underlying univPsh.

Every shape has no directions over 1: all recursion is over the code fibre, which is what makes the W-type's hereditary naturality over the single non-identity morphism vacuous at every node.

The direction-restriction of univPsh: morphisms into 0 are identities, so the restriction is the identity on the directions over 0; there are no directions over 1 to restrict.

The shape-restriction of univPsh to a target index t: the code shapes are fixed, and the term shapes are sent to the code shape of the same former (termSigma to sigma, termPi to pi).

The restricted shape lies over the target index.

The shape-restriction of univPsh.

The raw direction map of the reindexing: on the code shapes the identity, and on the term shapes the code component (Sum.inl) when restricting along 0 ⟶ 1, the identity otherwise.

The arity reindexing of univPsh along a walking-arrow morphism.

The operations of the presheaf polynomial endofunctor of the universe.

The identity law for shapeRestr, as a standalone theorem.