Imports
/-
Copyright (c) 2026 Terence Rokop. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Terence Rokop
-/
module
public import Geb.Mathlib.Data.PFunctor.IndRec.Basic
public import Geb.Mathlib.Data.PFunctor.Slice.BasicCodes for slice polynomial functors as IR codes, and back
Section 4 of [HancockMcBrideGhaniMalatestaAltenkirch2013] establishes that
small inductive-recursive definitions (IR codes) and dependent polynomials
(indexed containers) define the same class of functors. This file implements
the two code-level translations: IR.sliceCode translates a
SlicePFunctor to an IR code (Lemma 1), and IR.toSlicePFunctor
translates an IR code to a SlicePFunctor (Lemma 2 / Definition 5),
the latter via IR.elimAlg.
Main definitions
IR.sliceCode — the IR code for a slice polynomial functor (Lemma 1
of [HancockMcBrideGhaniMalatestaAltenkirch2013]).
IR.toSlicePFunctorIota, IR.toSlicePFunctorSigma,
IR.toSlicePFunctorDelta — the per-case components of the recursive
translation (Definition 5).
IR.toSlicePFunctorAlg — the Alg assembling the three components.
IR.toSlicePFunctor — the slice polynomial functor for an IR code
(Lemma 2 / Definition 5), generated by IR.elimAlg.
Main statements
IR.toSlicePFunctor_iota, IR.toSlicePFunctor_sigma,
IR.toSlicePFunctor_delta — the computation rules of
IR.toSlicePFunctor at each code constructor, via IR.elim_mk.
Implementation notes
Definition 5's sigma and delta clauses are both coproducts of slice
polynomial functors, so both are expressed through SlicePFunctor.coprod;
the delta clause differs only in its summand, the product of the
sub-polynomial with the functor SliceDomPFunctor.representable
represents. Since the representable has one shape, the summand's shapes are
PUnit × (sub i).A rather than (sub i).A; the two are isomorphic, and
the clause is stated up to that isomorphism.
The summand is equally the O-way product, over SlicePFunctor.ofFamily's
equivalence of Type/O with O-indexed families, of the products of the
representable with each member of the sub-polynomial's family. It is formed
here as SliceDomPFunctor.prodSlice instead, because transporting a
SlicePFunctor out to its family and back introduces a Σ over O and so
raises the shape universe by uO, which the fixed carrier of
IR.toSlicePFunctorAlg does not admit.
The recursive translation stabilizes the universe parameters: shapes at
max uA uB uI (the delta case introduces shapes indexed by B → I at
Type (max uB uI)), directions at uB. The constraint in
IR.sliceCode embeds the Prop-valued compatibility condition into
Type uA via ULift.{uA} (PLift (...)), following the pattern of
IR.InnerHom (IndRec/Hom.lean). The delta-case direction structure
follows the indexed-container presentation (proof of Lemma 2) rather than
the dependent-polynomial diagram (Definition 5); the two are equivalent
via the fiber construction of Definition 2.
References
[HancockMcBrideGhaniMalatestaAltenkirch2013]
Tags
inductive-recursive, polynomial functor, slice category, container, indexed container
@[expose] public sectionuniverse uA uB uI uOnamespace IndRecopen CategoryTheoryvariable (I : Type uI) (O : Type uO)namespace IR
The IR code for a slice polynomial functor F (Lemma 1 of
[HancockMcBrideGhaniMalatestaAltenkirch2013]): a sigma over the
shapes, then for each shape a delta over its directions, then a
sigma over the compatibility constraint, terminating in iota at the
output index.
set_option linter.checkUnivs false indef sliceCode (F : SlicePFunctor.{uA, uB, uI, uO} I O) :
IR.{uA, uB, uI, uO} I O :=
sigma I O F.toPFunctor.A fun a ↦
delta I O (F.toPFunctor.B a) fun assign ↦
sigma I O (ULift.{uA} (PLift (∀ b, assign b = F.rCurried a b))) fun _ ↦
iota I O (F.q a)
The constant (iota) case of the translation from IR codes to
SlicePFunctors (Definition 5, clause 1 of
[HancockMcBrideGhaniMalatestaAltenkirch2013]): one shape, no directions,
output index o.
set_option linter.checkUnivs false indef toSlicePFunctorIota (o : O) :
SlicePFunctor.{max uA uB uI, uB, uI, uO} I O :=
{ toPFunctor := ⟨PUnit, fun _ ↦ PEmpty⟩
, r := fun ⟨_, b⟩ ↦ PEmpty.elim b
, q := fun _ ↦ o }
The dependent sum (sigma) case of the translation (Definition 5,
clause 2): the coproduct of the sub-polynomials over the arity.
set_option linter.checkUnivs false indef toSlicePFunctorSigma (A : Type uA)
(sub : A → SlicePFunctor.{max uA uB uI, uB, uI, uO} I O) :
SlicePFunctor.{max uA uB uI, uB, uI, uO} I O :=
SlicePFunctor.coprod A sub
The dependent product (delta) case of the translation (Definition 5,
clause 3): the coproduct, over the assignments i : B → I, of the product
of the sub-polynomial at i with the functor represented by i read as an
object (B, i) of Type/I. The representable contributes the one shape
and the B directions carrying i as their direction-input map, so the
summand's input map is the cotuple [i, (sub i).r].
set_option linter.checkUnivs false indef toSlicePFunctorDelta (B : Type uB)
(sub : (B → I) → SlicePFunctor.{max uA uB uI, uB, uI, uO} I O) :
SlicePFunctor.{max uA uB uI, uB, uI, uO} I O :=
SlicePFunctor.coprod (B → I) fun i ↦
(SliceDomPFunctor.representable B i).prodSlice (sub i)
The algebra computing one step of the translation from IR codes to
SlicePFunctors (Definition 5 of
[HancockMcBrideGhaniMalatestaAltenkirch2013]), assembling the iota,
sigma, and delta cases.
set_option linter.checkUnivs false indef toSlicePFunctorAlg :
Alg.{uA, uB, uI, uO, max (max uA uB uI + 1) (uB + 1) uI uO} I O
(SlicePFunctor.{max uA uB uI, uB, uI, uO} I O) :=
⟨toSlicePFunctorIota.{uA, uB, uI, uO} I O,
toSlicePFunctorSigma.{uA, uB, uI, uO} I O,
toSlicePFunctorDelta.{uA, uB, uI, uO} I O⟩
The slice polynomial functor for an IR code (Lemma 2 / Definition 5
of [HancockMcBrideGhaniMalatestaAltenkirch2013]), generated by IR.elimAlg
from IR.toSlicePFunctorAlg.
def toSlicePFunctor (γ : IR.{uA, uB, uI, uO} I O) :
SlicePFunctor.{max uA uB uI, uB, uI, uO} I O :=
elimAlg I O (SlicePFunctor.{max uA uB uI, uB, uI, uO} I O)
(toSlicePFunctorAlg.{uA, uB, uI, uO} I O) γ
Computation rule for IR.toSlicePFunctor at IR.iota (definitional,
via IR.elim_mk).
theorem toSlicePFunctor_iota (o : O) :
toSlicePFunctor I O (iota.{uA, uB, uI, uO} I O o) =
toSlicePFunctorIota.{uA, uB, uI, uO} I O o := rfl
Computation rule for IR.toSlicePFunctor at IR.sigma (definitional,
via IR.elim_mk).
theorem toSlicePFunctor_sigma (A : Type uA) (c : A → IR.{uA, uB, uI, uO} I O) :
toSlicePFunctor I O (sigma I O A c) =
toSlicePFunctorSigma I O A fun a ↦ toSlicePFunctor I O (c a) := rfl
Computation rule for IR.toSlicePFunctor at IR.delta (definitional,
via IR.elim_mk).
theorem toSlicePFunctor_delta (B : Type uB) (c : (B → I) → IR.{uA, uB, uI, uO} I O) :
toSlicePFunctor I O (delta I O B c) =
toSlicePFunctorDelta.{uA, uB, uI, uO} I O B
fun i ↦ toSlicePFunctor I O (c i) := rflend IRend IndRec