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.CategoryTheory.FreeCoprodCompDisc
public import Geb.Mathlib.Logic.Equiv.Basic
public import Mathlib.Data.PFunctor.Univariate.BasicCodes for positive inductive-recursive definitions
IR I O is the type of codes for inductive-recursive definitions with
input index type I and output index type O, presented as the W-type
of a polynomial functor IR.pFunctor I O whose shapes are the three
code constructors — constant (iota), dependent sum (sigma), and
dependent product (delta) — and whose directions are their subcode
arities. A code is interpreted as a functor from the free coproduct
completion of I to that of O (both treated as discrete categories,
CategoryTheory.FreeCoprodCompDisc, the category of families of
elements of the index type): this file constructs the object map and
morphism map of the interpretation.
It follows [GhaniNordvallForsbergMalatesta2015], Section 2
(Definitions 2.1–2.2 and Theorem 2.4), which presents the codes of
[DybjerSetzer1999] and the functorial semantics of [DybjerSetzer2003].
The split into separate input and output index types — generalizing
the single shared index type of [DybjerSetzer1999] and
[DybjerSetzer2003] — follows Definition 3 of
[HancockMcBrideGhaniMalatestaAltenkirch2013], whose footnote observes
that the generalization allows the construction of partial fixed
points.
Main definitions
IR.pFunctor — the polynomial functor whose W-type defines codes:
shapes IR.Shape, directions IR.Direction.
IR.Dest, IR.Dest.elim, IR.Dest.elimInv, IR.destEquiv — the
pattern-matched destructor for morphisms out of IR.Obj, its
conversions to and from such morphisms, and the equivalence they
form.
IR.DepDest, IR.DepDest.elim, IR.DepDest.elimInv,
IR.depDestEquiv — the dependent counterparts.
IR.objIota, IR.objSigma, IR.objDelta — the element
constructors of IR.Obj, one per shape.
IR, IR.mk — the type of codes and its constructor.
IR.iota, IR.sigma, IR.delta — the code constructors, one per
shape.
IR.elim, IR.rec — the eliminator and the dependent recursor,
the latter with step arguments of type IR.RecStep (the Type
specialization, alongside IR.InductionStep for Prop, of the
Sort-valued IR.Step).
IR.interpObj, IR.interpMor — the object map and morphism map of
the interpretation of an IR code as a FreeCoprodCompDisc.Map (a
functor between the free coproduct completions of I and O).
IR.precomp — precomposition of a code along a coproduct (the γ^i
of [HancockMcBrideGhaniMalatestaAltenkirch2013], Lemma 4, which
asserts existence only; this construction is the project's),
computed by the algebra IR.precompAlg, which merges assignments
through IR.precompMerge.
IR.PrecompIsoMotive — the statement schema of Lemma 4 of
[HancockMcBrideGhaniMalatestaAltenkirch2013]: interpreting a
precomposed code at an object is isomorphic to interpreting the
original code at the coproduct of that object with the
precomposition data.
Main statements
IR.ext, IR.snd_eq_of_eq — extensionality for codes.
IR.induction — the induction principle, the recursor restricted to
Prop-valued motives.
IR.precomp_iota, IR.precomp_sigma, IR.precomp_delta —
computation rules for IR.precomp at each code constructor
([HancockMcBrideGhaniMalatestaAltenkirch2013], Lemma 4).
IR.interpPrecompIso — Lemma 4 of
[HancockMcBrideGhaniMalatestaAltenkirch2013], generated by IR.rec
from the per-shape steps IR.precompIsoIota, IR.precompIsoSigma,
and IR.precompIsoDelta.
IR.interpDeltaIso — Lemma 3 of
[HancockMcBrideGhaniMalatestaAltenkirch2013]: the dependent product
(delta) interpretation at an object is isomorphic to the indexed
coproduct, over its direction assignments, of copowers of the
subcode interpretations by the morphisms into that object.
IR.elim_mk, IR.rec_mk (with IR.rec_iota, IR.rec_sigma,
IR.rec_delta) — the computation rules of IR.elim
(definitional, pinned) and IR.rec (propositional), the latter
from the transport congruence IR.recStep_congr.
Implementation notes
The interpretation is given by its object map (IR.interpObj) and
its morphism map (IR.interpMor). The propositional computation
rule of IR.rec is IR.rec_mk. The functor laws (preservation of
identities and composition, completing Theorem 2.4 of
[GhaniNordvallForsbergMalatesta2015]) are IR.interpMor_id and
IR.interpMor_comp in
Geb/Mathlib/Data/PFunctor/IndRec/Functor.lean. The initial
algebras of the interpreted endofunctors — the universes the codes
describe, in the endofunctor case IR I I — are constructed in
Geb/Mathlib/Data/PFunctor/IndRec/W.lean, through the translation
of a code to a slice polynomial functor in
Geb/Mathlib/Data/PFunctor/IndRec/Slice.lean. For the general —
not necessarily small — inductive-recursive definitions of
[DybjerSetzer2003], where no such translation is available, the
set-theoretic model given there justifies their existence using a
Mahlo cardinal.
The sigma arities of IR.Shape live at the universe uA and the
delta arities at uB, generalizing the single Set of
Definition 2.1 (recovered as the case uA = uB). The output index
type O parameterizes the iota shapes (a code IR.iota I O o
decodes to o : O); the input index type I parameterizes the
delta directions (a code IR.delta I O B c receives the decodings
of its recursive arguments as assignments B → I).
The linter.checkUnivs false option suppresses the checkUnivs
warning on the separated arity universes uA/uB: in the suppressed
declarations' types they appear only together under max, so the
linter flags them as a pair that could be unified; keeping them
distinct is the point of the separation.
The whole file is exposed (@[expose] public section): downstream
modules, in particular the tests, rely on definitional reduction
through every definition here.
IR.precomp introduces a fresh universe uQ for the coproduct's
index type: the resulting code's sigma-arity universe becomes
max uA uB uQ, generalizing the argument code's uA, while the
delta-arity universe uB is unchanged. Two deviations from
[HancockMcBrideGhaniMalatestaAltenkirch2013] are recorded at the
affected declarations: Lemma 4 states an equality between the
precomposed and direct interpretations, but IR.interpPrecompIso
supplies only the pointwise isomorphism IR.PrecompIsoMotive, since
equality is not the natural comparison between general objects here;
the naturality upgrade is IR.interpPrecompIso_natural. Lemma 3
states a natural isomorphism, but IR.interpDeltaIso states it
pointwise at a fixed object; the naturality upgrade is
IR.natDeltaEquiv. The delta case of both
IR.precomp and IR.interpPrecompIso inserts ULifts to align the
classifier sigma's index universe with the code's ambient arity
universes, and IR.interpDeltaIso inserts FreeCoprodCompDisc.lift
(through homLiftEquiv) to align a direction assignment's morphism
type with the fixed object.
References
[DybjerSetzer1999]
[DybjerSetzer2003]
[GhaniNordvallForsbergMalatesta2015]
[HancockMcBrideGhaniMalatestaAltenkirch2013]
Tags
inductive-recursive, polynomial functor, W-type
@[expose] public sectionuniverse uA uB uI uOnamespace IndRecopen CategoryTheoryvariable (I : Type uI) (O : Type uO)namespace IRThe shape type of the polynomial functor whose W-type defines codes for positive inductive-recursive types.
set_option linter.checkUnivs false indef Shape : Type (max (uA + 1) (uB + 1) uO) :=
O ⊕ Type uA ⊕ Type uBThe direction type of the polynomial functor whose W-type defines codes for positive inductive-recursive types.
def Direction : Shape.{uA, uB, uO} O → Type (max uA uB uI) :=
Sum.elim (fun _ ↦ PEmpty)
(Sum.elim (fun A ↦ ULift.{max uB uI} A) (fun B ↦ ULift.{uA} (B → I)))
Simplification for the constant (iota) case of IR.Direction.
@[simp]
theorem direction_iota (o : O) : Direction.{uA, uB, uI, uO} I O (Sum.inl o) = PEmpty := rfl
Simplification for the dependent sum (sigma) case of
IR.Direction.
@[simp]
theorem direction_sigma (A : Type uA) :
Direction.{uA, uB, uI, uO} I O (Sum.inr (Sum.inl A)) = ULift.{max uB uI} A := rfl
Simplification for the dependent product (delta) case of
IR.Direction.
@[simp]
theorem direction_delta (B : Type uB) :
Direction.{uA, uB, uI, uO} I O (Sum.inr (Sum.inr B)) = ULift.{uA} (B → I) := rflRewrite the direction type along a shape-type equality.
def directionOfEq {s s' : Shape.{uA, uB, uO} O} : s = s' → Direction I O s → Direction I O s'
| rfl => id
Elimination rule for IR.Direction.
def directionElim.{v} (V : Type v) (σ : (A : Type uA) → A → V)
(δ : (B : Type uB) → (B → I) → V) (s : Shape O) (ds : Direction I O s) : V :=
match s with
| Sum.inl _ => PEmpty.elim ds
| Sum.inr (Sum.inl (A : Type uA)) => σ A (ULift.down ds)
| Sum.inr (Sum.inr (B : Type uB)) => δ B (ULift.down ds)The polynomial functor whose W-type defines codes for positive inductive-recursive types.
set_option linter.checkUnivs false indef pFunctor : PFunctor.{max (uA + 1) (uB + 1) uO, max uA uB uI} :=
⟨Shape.{uA, uB, uO} O, Direction.{uA, uB, uI, uO} I O⟩
The value at V of the interpretation of IR.pFunctor as an
endofunctor on Type.
set_option linter.checkUnivs false indef Obj.{v} (V : Type v) : Type (max (uA + 1) (uB + 1) uI uO v) :=
PFunctor.Obj.{v, max (uA + 1) (uB + 1) uO, max uA uB uI}
(pFunctor.{uA, uB, uI, uO} I O) V
The first component of IR.Obj.
set_option linter.checkUnivs false indef ObjFst : Type (max (uA + 1) (uB + 1) uO) :=
Shape.{uA, uB, uO} O
The second component of IR.Obj.
def ObjSnd.{v} (V : Type v) : ObjFst O → Type (max uA uB uI v) :=
fun s ↦ Direction.{uA, uB, uI, uO} I O s → V
Rewrite the second component of IR.Obj along a shape-type
equality.
def objSndOfEq.{v} (V : Type v) {s s' : ObjFst.{uA, uB, uO} O} :
s = s' → ObjSnd I O V s → ObjSnd I O V s'
| rfl => id
The constant (iota) element constructor of IR.Obj: shape o,
no directions.
def objIota.{v} (V : Type v) (o : O) : Obj.{uA, uB, uI, uO, v} I O V :=
⟨Sum.inl o, PEmpty.elim⟩
The dependent sum (sigma) element constructor of IR.Obj: shape
A, directions assigned by f (through the lifted direction type
ULift A).
def objSigma.{v} (V : Type v) (A : Type uA) (f : A → V) :
Obj.{uA, uB, uI, uO, v} I O V :=
⟨Sum.inr (Sum.inl A), f ∘ ULift.down⟩
The dependent product (delta) element constructor of IR.Obj:
shape B, directions assigned by f (through the lifted direction
type ULift (B → I)).
def objDelta.{v} (V : Type v) (B : Type uB) (f : (B → I) → V) :
Obj.{uA, uB, uI, uO, v} I O V :=
⟨Sum.inr (Sum.inr B), f ∘ ULift.down⟩
Every element of IR.Obj with an iota shape equals the
IR.objIota element: direction assignments out of the empty direction
type are all equal.
theorem objIota_eq_mk.{v} (V : Type v) (o : O)
(ds : Direction.{uA, uB, uI, uO} I O (Sum.inl o) → V) :
objIota I O V o = (⟨Sum.inl o, ds⟩ : Obj.{uA, uB, uI, uO, v} I O V) :=
congrArg (Sigma.mk (Sum.inl o)) (funext (fun x ↦ PEmpty.elim x))
A destructor for IR.Obj — a pattern-matched form of
elimination.
set_option linter.checkUnivs false indef Dest.{v, w} (V : Type v) (W : Type w) :
Type (max (uA + 1) (uB + 1) uI uO v w) :=
(O → W) × ((A : Type uA) → (A → V) → W) ×
((B : Type uB) → ((B → I) → V) → W)
Convert IR.Dest to a morphism out of IR.Obj (an eliminator).
def Dest.elim.{v, w} (V : Type v) (W : Type w)
(dest : Dest.{uA, uB, uI, uO, v, w} I O V W) : Obj I O V → W :=
fun ⟨s, ds⟩ ↦ match s with
| Sum.inl o => dest.1 o
| Sum.inr (Sum.inl (A : Type uA)) => dest.2.1 A (ds ∘ ULift.up)
| Sum.inr (Sum.inr (B : Type uB)) => dest.2.2 B (ds ∘ ULift.up)
The inverse of IR.Dest.elim.
def Dest.elimInv.{v, w} (V : Type v) (W : Type w) (m : Obj I O V → W) :
Dest.{uA, uB, uI, uO, v, w} I O V W :=
⟨fun o ↦ m (objIota I O V o),
fun A f ↦ m (objSigma I O V A f),
fun B f ↦ m (objDelta I O V B f)⟩
IR.Dest.elimInv is a left inverse of IR.Dest.elim.
theorem Dest.elimInv_elim.{v, w} (V : Type v) (W : Type w)
(dest : Dest.{uA, uB, uI, uO, v, w} I O V W) :
Dest.elimInv.{uA, uB, uI, uO, v, w} I O V W (Dest.elim.{uA, uB, uI, uO, v, w} I O V W dest) =
dest :=
rfl
IR.Dest.elimInv is a right inverse of IR.Dest.elim.
theorem Dest.elim_elimInv.{v, w} (V : Type v) (W : Type w)
(m : Obj I O V → W) :
Dest.elim.{uA, uB, uI, uO, v, w} I O V W (Dest.elimInv.{uA, uB, uI, uO, v, w} I O V W m) = m :=
funext <| fun ⟨s, ds⟩ ↦ match s with
| Sum.inl o => congrArg m (objIota_eq_mk.{uA, uB, uI, uO, v} I O V o ds)
| Sum.inr (Sum.inl _) => rfl
| Sum.inr (Sum.inr _) => rfl
IR.Dest is equivalent to the morphisms out of IR.Obj.
def destEquiv.{v, w} (V : Type v) (W : Type w) :
Dest.{uA, uB, uI, uO, v, w} I O V W ≃ (Obj I O V → W) where
toFun := Dest.elim I O V W
invFun := Dest.elimInv I O V W
left_inv := Dest.elimInv_elim I O V W
right_inv := Dest.elim_elimInv I O V W
A dependent destructor for IR.Obj — a pattern-matched form of
elimination.
def DepDest.{v, w} (V : Type v) (W : Obj I O V → Type w) :
Type (max (uA + 1) (uB + 1) uI uO v w) :=
((o : O) → W (objIota I O V o)) ×
((A : Type uA) → (f : A → V) → W (objSigma I O V A f)) ×
((B : Type uB) → (f : (B → I) → V) → W (objDelta I O V B f))
Convert IR.DepDest to a destructor into a sigma type.
def sigmaDest.{v, w} (V : Type v) (W : Obj I O V → Type w) :
DepDest.{uA, uB, uI, uO, v, w} I O V W →
Dest.{uA, uB, uI, uO, v, max (uA + 1) (uB + 1) uI uO v w} I O V (Σ e, W e) :=
fun dest ↦
⟨fun o ↦ ⟨objIota I O V o, dest.1 o⟩,
fun A f ↦ ⟨objSigma I O V A f, dest.2.1 A f⟩,
fun B f ↦ ⟨objDelta I O V B f, dest.2.2 B f⟩⟩
Convert IR.DepDest to a morphism into a sigma type.
def sigmaElim.{v, w} (V : Type v) (W : Obj I O V → Type w) :
DepDest.{uA, uB, uI, uO, v, w} I O V W → Obj I O V → Σ e, W e :=
Dest.elim.{uA, uB, uI, uO, v, max (uA + 1) (uB + 1) uI uO v w} I O V (Σ e, W e) ∘
sigmaDest.{uA, uB, uI, uO, v, w} I O V W
IR.sigmaElim is a section of the first projection.
theorem sigmaElim_fst.{v, w} (V : Type v) (W : Obj I O V → Type w)
(dest : DepDest.{uA, uB, uI, uO, v, w} I O V W) (e : Obj I O V) :
(sigmaElim I O V W dest e).1 = e :=
match e with
| ⟨s, ds⟩ => match s with
| Sum.inl o => objIota_eq_mk.{uA, uB, uI, uO, v} I O V o ds
| Sum.inr (Sum.inl _) => rfl
| Sum.inr (Sum.inr _) => rfl
Convert IR.DepDest to a dependent eliminator for IR.Obj.
def DepDest.elim.{v, w} (V : Type v) (W : Obj I O V → Type w) :
DepDest.{uA, uB, uI, uO, v, w} I O V W → (e : Obj I O V) → W e :=
fun dest ↦
sigmaFstSectionElim (sigmaElim I O V W dest) (sigmaElim_fst I O V W dest)
The inverse of IR.DepDest.elim.
def DepDest.elimInv.{v, w} (V : Type v) (W : Obj I O V → Type w) :
((e : Obj I O V) → W e) → DepDest.{uA, uB, uI, uO, v, w} I O V W :=
fun m ↦
⟨fun o ↦ m (objIota I O V o),
fun A f ↦ m (objSigma I O V A f),
fun B f ↦ m (objDelta I O V B f)⟩
IR.DepDest.elimInv is a left inverse of IR.DepDest.elim.
theorem DepDest.elimInv_elim.{v, w} (V : Type v) (W : Obj I O V → Type w)
(dest : DepDest.{uA, uB, uI, uO, v, w} I O V W) :
DepDest.elimInv.{uA, uB, uI, uO, v, w} I O V W
(DepDest.elim.{uA, uB, uI, uO, v, w} I O V W dest) = dest :=
rfl
IR.DepDest.elimInv is a right inverse of IR.DepDest.elim.
theorem DepDest.elim_elimInv.{v, w} (V : Type v) (W : Obj I O V → Type w)
(m : (e : Obj I O V) → W e) :
DepDest.elim.{uA, uB, uI, uO, v, w} I O V W
(DepDest.elimInv.{uA, uB, uI, uO, v, w} I O V W m) = m :=
funext <| fun ⟨s, ds⟩ ↦ match s with
| Sum.inl o => objIota_eq_mk.{uA, uB, uI, uO, v} I O V o ds ▸ rfl
| Sum.inr (Sum.inl _) => rfl
| Sum.inr (Sum.inr _) => rfl
IR.DepDest is equivalent to the dependent eliminators of
IR.Obj.
def depDestEquiv.{v, w} (V : Type v) (W : Obj I O V → Type w) :
DepDest.{uA, uB, uI, uO, v, w} I O V W ≃ ((e : Obj I O V) → W e) where
toFun := DepDest.elim I O V W
invFun := DepDest.elimInv I O V W
left_inv := DepDest.elimInv_elim I O V W
right_inv := DepDest.elim_elimInv I O V W
A pattern-matched form of an algebra of IR.pFunctor.
set_option linter.checkUnivs false indef Alg.{v} (V : Type v) : Type (max (uA + 1) (uB + 1) uI uO v) :=
Dest.{uA, uB, uI, uO, v, v} I O V V
Convert IR.Alg to the morphism form of an algebra of
IR.pFunctor.
def Alg.toHom.{v} (V : Type v) (alg : Alg.{uA, uB, uI, uO, v} I O V) : Obj I O V → V :=
Dest.elim.{uA, uB, uI, uO, v, v} I O V V algend IR
The type of codes for positive inductive-recursive definitions:
the W-type of IR.pFunctor.
set_option linter.checkUnivs false indef IR : Type (max (uA + 1) (uB + 1) uI uO) :=
PFunctor.W.{max (uA + 1) (uB + 1) uO, max uA uB uI}
(IR.pFunctor.{uA, uB, uI, uO} I O)namespace IR
The constructor for IR.
def mk (s : Shape O) (d : Direction I O s → IR.{uA, uB, uI, uO} I O) :
IR.{uA, uB, uI, uO} I O :=
WType.mk.{max (uA + 1) (uB + 1) uO, max uA uB uI} s d
The constant (iota) code: no subcodes; its interpretation is the
constant functor at the object with one name decoding to o.
The dependent sum (sigma) code: subcodes c indexed by A; its
interpretation is the pointwise indexed coproduct over A of the
interpretations of the subcodes.
def sigma (A : Type uA) (c : A → IR.{uA, uB, uI, uO} I O) : IR I O :=
mk I O (Sum.inr (Sum.inl A)) (c ∘ ULift.down)
The dependent product (delta) code: subcodes c indexed by the
assignments of decodings to B; its interpretation takes recursive
arguments indexed by B and passes their decodings to c.
def delta (B : Type uB) (c : (B → I) → IR.{uA, uB, uI, uO} I O) : IR I O :=
mk I O (Sum.inr (Sum.inr B)) (c ∘ ULift.down)
Congruence for IR.mk in the direction assignment.
theorem mk_congr (s : Shape O) {ds ds' : Direction I O s → IR I O} :
ds = ds' → mk.{uA, uB, uI, uO} I O s ds = mk.{uA, uB, uI, uO} I O s ds'
| rfl => rfl
The motive of the proof of IR.ext.
def ExtMotive (s : Shape.{uA, uB, uO} O) (d : Direction I O s → IR I O)
(s' : Shape O) (eq1 : s = s') : Prop :=
∀ d' : Direction I O s' → IR I O, d = d' ∘ directionOfEq I O eq1 → mk I O s d = mk I O s' d'
Extensionality for IR (equality is determined by equality of
shapes and pointwise equality of directions).
theorem ext {ir ir' : IR.{uA, uB, uI, uO} I O} (eq1 : ir.1 = ir'.1)
(eq2 : ir.2 = ir'.2 ∘ directionOfEq I O eq1) : ir = ir' :=
match ir, ir' with
| ⟨s, d⟩, ⟨_, d'⟩ =>
Eq.rec (motive := ExtMotive I O s d) (fun _ ↦ mk_congr I O s) eq1 d' eq2
The converse of IR.ext: an equality in IR determines a
pointwise equality of directions (transported along the shape equality
induced by the first projection).
theorem snd_eq_of_eq {ir ir' : IR.{uA, uB, uI, uO} I O} :
(eq : ir = ir') → ir.2 = ir'.2 ∘ directionOfEq I O (congrArg (fun t ↦ t.1) eq)
| rfl => rfl
The eliminator (the algebra morphism from the initial algebra) for
IR, taking the algebra in morphism form.
def elim.{v} (V : Type v) (alg : Obj.{uA, uB, uI, uO, v} I O V → V) : IR I O → V :=
WType.elim.{max (uA + 1) (uB + 1) uO, max uA uB uI, v} V alg
The eliminator for IR, taking the algebra in the IR.Alg form.
def elimAlg.{v} (V : Type v) (alg : Alg.{uA, uB, uI, uO, v} I O V) : IR I O → V :=
elim I O V (Alg.toHom I O V alg)
The computation rule of IR.elim at IR.mk. It holds
definitionally; the named statement pins the definitional-unfolding
chain through WType.elim at one site, so that any change to that
chain localizes here.
theorem elim_mk.{v} (V : Type v) (alg : Obj.{uA, uB, uI, uO, v} I O V → V)
(s : Shape O) (d : Direction I O s → IR I O) :
elim I O V alg (mk I O s d) = alg ⟨s, fun x ↦ elim I O V alg (d x)⟩ :=
rfl
The type of the step argument of IR's recursors at a
Sort-valued motive: from a shape, a subcode assignment, and results
for the subcodes, produce the result for the constructed code. The
result sort (an imax expression) is left to inference; the
specializations IR.RecStep and IR.InductionStep carry the explicit
ascriptions.
def Step.{v} (motive : IR.{uA, uB, uI, uO} I O → Sort v) :=
(a : Shape O) → (f : Direction I O a → IR I O) →
((d : Direction I O a) → motive (f d)) → motive (mk I O a f)
The step argument type at a Type-valued motive (for IR.rec,
IR.sigmaRec, and their companions).
def RecStep.{v} (motive : IR.{uA, uB, uI, uO} I O → Type v) :
Type (max (uA + 1) (uB + 1) uI uO v) :=
Step I O motive
The step argument type at a Prop-valued motive (for IR.induction).
The induction principle — the recursor restricted to Prop-valued
motives. (The compiler does not generate code for WType.rec
applications, so WType.rec is used only here, where propositions
need no code.)
theorem induction (motive : IR I O → Prop) :
InductionStep.{uA, uB, uI, uO} I O motive → ∀ t : IR I O, motive t :=
WType.rec.{0, max (uA + 1) (uB + 1) uO, max uA uB uI}
(α := Shape O) (β := Direction I O) (motive := motive)
The IR.pFunctor algebra over a sigma type generated by a
recursor step.
def sigmaRecAlg.{v} (motive : IR I O → Type v)
(mk' : RecStep.{uA, uB, uI, uO, v} I O motive) :
Obj I O (Σ e, motive e) → Σ e, motive e :=
fun ⟨s, f⟩ ↦
⟨mk I O s (Sigma.fst ∘ f), mk' s (Sigma.fst ∘ f) (fun d ↦ (f d).2)⟩
IR.sigmaRecAlg preserves the shape component.
theorem sigmaRecAlg_fst_fst.{v} (motive : IR I O → Type v)
(mk' : RecStep.{uA, uB, uI, uO, v} I O motive) (t : Obj I O (Σ e, motive e)) :
(sigmaRecAlg I O motive mk' t).1.1 = t.1 :=
rfl
IR.sigmaRecAlg preserves the direction component.
theorem sigmaRecAlg_fst_snd.{v} (motive : IR I O → Type v)
(mk' : RecStep.{uA, uB, uI, uO, v} I O motive) (t : Obj I O (Σ e, motive e)) :
(sigmaRecAlg I O motive mk' t).1.2 = Sigma.fst ∘ t.2 :=
rflThe recursor's auxiliary fold into a sigma type.
def sigmaRec.{v} (motive : IR I O → Type v)
(mk' : RecStep.{uA, uB, uI, uO, v} I O motive) : IR I O → Σ e, motive e :=
elim I O (Σ e, motive e) (sigmaRecAlg I O motive mk')
The inductive step of the proof that IR.sigmaRec is a section of
the first projection.
theorem sigmaRec_fst_step.{v} (motive : IR I O → Type v)
(mk' : RecStep.{uA, uB, uI, uO, v} I O motive) :
InductionStep.{uA, uB, uI, uO} I O (fun t ↦ (sigmaRec I O motive mk' t).1 = t) :=
fun _ _ ih ↦ ext I O rfl (funext ih)
IR.sigmaRec is a section of the first projection.
theorem sigmaRec_fst.{v} (motive : IR I O → Type v)
(mk' : RecStep.{uA, uB, uI, uO, v} I O motive) :
∀ t : IR I O, (sigmaRec I O motive mk' t).1 = t :=
induction I O (motive := fun t ↦ (sigmaRec I O motive mk' t).1 = t)
(sigmaRec_fst_step I O motive mk')
The shape component of IR.sigmaRec agrees with the shape
component of the argument.
theorem sigmaRec_fst_fst.{v} (motive : IR I O → Type v)
(mk' : RecStep.{uA, uB, uI, uO, v} I O motive) (t : IR I O) :
(sigmaRec I O motive mk' t).1.1 = t.1 :=
match t with
| ⟨_, _⟩ => rfl
The direction component of IR.sigmaRec agrees with the direction
component of the argument, transported along IR.sigmaRec_fst_fst.
theorem sigmaRec_fst_snd.{v} (motive : IR I O → Type v)
(mk' : RecStep.{uA, uB, uI, uO, v} I O motive) (t : IR I O) :
(sigmaRec I O motive mk' t).1.2 =
t.2 ∘ directionOfEq I O (sigmaRec_fst_fst I O motive mk' t) :=
snd_eq_of_eq I O (sigmaRec_fst I O motive mk' t)
The recursor — the dependent eliminator for IR.
def rec.{v} {motive : IR I O → Type v} (mk' : RecStep.{uA, uB, uI, uO, v} I O motive) :
(t : IR I O) → motive t :=
sigmaFstSectionElim (sigmaRec I O motive mk') (sigmaRec_fst I O motive mk')
The motive of the proof of IR.recStep_congr: transporting a
recursor-step application along an equality of constructed codes
agrees with applying the step to the pointwise-transported
results.
def RecStepCongrMotive.{v} {motive : IR.{uA, uB, uI, uO} I O → Type v}
(mk' : RecStep I O motive) (s : Shape O)
(f : Direction I O s → IR I O) (m : (x : Direction I O s) → motive (f x))
(g : Direction I O s → IR I O) (e : f = g) : Prop :=
∀ h : mk I O s f = mk I O s g,
Eq.ndrec (motive := motive) (mk' s f m) h =
mk' s g (fun x ↦ Eq.ndrec (motive := motive) (m x) (congrFun e x))
Transporting a recursor-step application along an equality of
constructed codes agrees with applying the step to the
pointwise-transported results. The base case is definitional:
proof irrelevance identifies the transport proof with rfl.
theorem recStep_congr.{v} {motive : IR.{uA, uB, uI, uO} I O → Type v}
(mk' : RecStep I O motive) (s : Shape O)
(f : Direction I O s → IR I O) (m : (x : Direction I O s) → motive (f x))
(g : Direction I O s → IR I O) (e : f = g) :
RecStepCongrMotive I O mk' s f m g e :=
Eq.rec (motive := fun g' e' ↦ RecStepCongrMotive I O mk' s f m g' e')
(fun _ ↦ rfl) e
The propositional computation rule of IR.rec at IR.mk.
IR.rec does not satisfy a definitional computation rule (it is
built from IR.elim through a propositional first-projection
section), so the rule holds propositionally, by IR.recStep_congr
along the pointwise section proofs.
theorem rec_mk.{v} {motive : IR.{uA, uB, uI, uO} I O → Type v}
(mk' : RecStep I O motive) (s : Shape O)
(d : Direction I O s → IR I O) :
rec I O mk' (mk I O s d) = mk' s d (fun x ↦ rec I O mk' (d x)) :=
recStep_congr I O mk' s
(fun x ↦ (sigmaRec I O motive mk' (d x)).1)
(fun x ↦ (sigmaRec I O motive mk' (d x)).2)
d
(funext (fun x ↦ sigmaRec_fst I O motive mk' (d x)))
(sigmaRec_fst I O motive mk' (mk I O s d))
The computation rule of IR.rec at IR.iota.
theorem rec_iota.{v} {motive : IR.{uA, uB, uI, uO} I O → Type v}
(mk' : RecStep I O motive) (o : O) :
rec I O mk' (iota I O o) =
mk' (Sum.inl o) PEmpty.elim (fun x ↦ rec I O mk' (PEmpty.elim x)) :=
rec_mk I O mk' (Sum.inl o) PEmpty.elim
The computation rule of IR.rec at IR.sigma.
theorem rec_sigma.{v} {motive : IR.{uA, uB, uI, uO} I O → Type v}
(mk' : RecStep I O motive) (A : Type uA) (c : A → IR I O) :
rec I O mk' (sigma I O A c) =
mk' (Sum.inr (Sum.inl A)) (c ∘ ULift.down)
(fun x ↦ rec I O mk' (c x.down)) :=
rec_mk I O mk' (Sum.inr (Sum.inl A)) (c ∘ ULift.down)
The computation rule of IR.rec at IR.delta.
theorem rec_delta.{v} {motive : IR.{uA, uB, uI, uO} I O → Type v}
(mk' : RecStep I O motive) (B : Type uB) (c : (B → I) → IR I O) :
rec I O mk' (delta I O B c) =
mk' (Sum.inr (Sum.inr B)) (c ∘ ULift.down)
(fun x ↦ rec I O mk' (c x.down)) :=
rec_mk I O mk' (Sum.inr (Sum.inr B)) (c ∘ ULift.down)end IRnamespace IR
The constant (iota) case of the interpretation of an IR code
as a FreeCoprodCompDisc.Map: the constant object map at the
singleton family decoding to o.
set_option linter.checkUnivs false indef interpObjIota (o : O) : FreeCoprodCompDisc.Map.{max uA uB, uI, uO} I O :=
fun _ ↦ ⟨ULift Unit, fun _ ↦ o⟩
The dependent sum (sigma) case of the interpretation of an IR
code as a FreeCoprodCompDisc.Map: the pointwise indexed coproduct
over A of the interpretations α of the subcodes.
def interpObjSigma (A : Type uA)
(α : A → FreeCoprodCompDisc.Map.{max uA uB, uI, uO} I O) :
FreeCoprodCompDisc.Map.{max uA uB, uI, uO} I O :=
fun X ↦ FreeCoprodCompDisc.coprod.{max uA uB, uO, uA} O A (fun a ↦ α a X)
The dependent product (delta) case of the interpretation of an
IR code as a FreeCoprodCompDisc.Map: at an object X, the
indexed coproduct over B → X.1 of the interpretations α of the
subcodes at the directions induced by X.
def interpObjDelta (B : Type uB)
(α : (B → I) → FreeCoprodCompDisc.Map.{max uA uB, uI, uO} I O) :
FreeCoprodCompDisc.Map.{max uA uB, uI, uO} I O :=
fun X ↦
FreeCoprodCompDisc.coprod.{max uA uB, uO, max uA uB} O (B → X.1)
(fun g ↦ α (X.2 ∘ g) X)
The algebra which computes one step of the interpretation of an
IR code as a FreeCoprodCompDisc.Map.
def interpObjAlg :
Alg.{uA, uB, uI, uO, max (uA + 1) (uB + 1) uI uO} I O
(FreeCoprodCompDisc.Map.{max uA uB, uI, uO} I O) :=
⟨interpObjIota.{uA, uB, uI, uO} I O, interpObjSigma I O, interpObjDelta I O⟩
The object map of the interpretation of an IR code as a
FreeCoprodCompDisc.Map.
def interpObj : IR.{uA, uB, uI, uO} I O → FreeCoprodCompDisc.Map.{max uA uB, uI, uO} I O :=
elimAlg I O (FreeCoprodCompDisc.Map.{max uA uB, uI, uO} I O) (interpObjAlg I O)
The signature of the morphism map accompanying IR.interpObj.
def MorMapSig (ir : IR.{uA, uB, uI, uO} I O) : Type (max (uA + 1) (uB + 1) uI) :=
FreeCoprodCompDisc.MapMor I O (interpObj I O ir)
The morphism-map component of the constant (iota) interpretation
IR.interpObjIota: every morphism maps to the identity.
def interpMorIota (o : O) :
FreeCoprodCompDisc.MapMor I O (interpObjIota.{uA, uB, uI, uO} I O o) :=
fun _ _ _ ↦ ⟨id, rfl⟩
The morphism-map component of the dependent sum (sigma)
interpretation IR.interpObjSigma: the indexed coproduct of the
componentwise morphism maps μ.
def interpMorSigma (A : Type uA)
(α : A → FreeCoprodCompDisc.Map.{max uA uB, uI, uO} I O)
(μ : (a : A) → FreeCoprodCompDisc.MapMor I O (α a)) :
FreeCoprodCompDisc.MapMor I O (interpObjSigma I O A α) :=
fun X Y h ↦
FreeCoprodCompDisc.coprodMor O A A id
(fun a ↦ α a X)
(fun a ↦ α a Y)
(fun a ↦ μ a X Y h)
The morphism-map component of the dependent product (delta)
interpretation IR.interpObjDelta: reindex along postcomposition with
the morphism, transporting each componentwise morphism map μ along
the morphism's commutation equality.
def interpMorDelta (B : Type uB)
(α : (B → I) → FreeCoprodCompDisc.Map.{max uA uB, uI, uO} I O)
(μ : (f : B → I) → FreeCoprodCompDisc.MapMor I O (α f)) :
FreeCoprodCompDisc.MapMor I O (interpObjDelta I O B α) :=
fun X Y h ↦
FreeCoprodCompDisc.coprodMor O (B → X.1) (B → Y.1) (fun g ↦ h.1 ∘ g)
(fun g ↦ α (X.2 ∘ g) X)
(fun g ↦ α (Y.2 ∘ g) Y)
(fun g ↦
FreeCoprodCompDisc.homOfEq O
(congrArg (fun t ↦ α (t ∘ g) Y) h.2.symm)
(μ (X.2 ∘ g) X Y h))
The step argument to the recursor which generates the morphism map
of the interpretation of an IR code as a FreeCoprodCompDisc.Map
(the object map is IR.interpObj).
def interpMorStep :
RecStep.{uA, uB, uI, uO, max (uA + 1) (uB + 1) uI} I O (MorMapSig I O) :=
fun s c m ↦ match s with
| Sum.inl o => interpMorIota.{uA, uB, uI, uO} I O o
| Sum.inr (Sum.inl A) =>
interpMorSigma I O A
(fun a ↦ interpObj I O (c (ULift.up a)))
(fun a ↦ m (ULift.up a))
| Sum.inr (Sum.inr B) =>
interpMorDelta I O B
(fun f ↦ interpObj I O (c (ULift.up f)))
(fun f ↦ m (ULift.up f))
The morphism map of the interpretation of an IR code as a
FreeCoprodCompDisc.Map (the object map is IR.interpObj).
def interpMor (ir : IR.{uA, uB, uI, uO} I O) : MorMapSig I O ir :=
rec I O (interpMorStep I O) irend IRnamespace IRPrecomposition on codes
Precomposition of an IR code along a coproduct (the γ^i of
[HancockMcBrideGhaniMalatestaAltenkirch2013], Lemma 4, which
asserts existence only; the construction here is the project's):
precomp Q i transports a code from I to a code over the
same I, replacing every recursive-argument decoding by its
image under i when resolved, or leaving it as a fresh
recursive argument otherwise. iota and sigma subcodes push
through unchanged (up to ULift); a delta B c subcode becomes
a sigma over classifiers B → Q ⊕ PUnit followed by a delta
over the classifier's unresolved elements, recursing into c at
the assignment merging i-images with the fresh decodings.
universe uQ
The assignment merging, along a classifier c of B into
Q ⊕ PUnit, the i-images of the resolved (Q-classified)
elements with the decodings j of the unresolved elements.
def precompMerge (Q : Type uQ) (i : Q → I) {B : Type uB}
(c : ArrowSumClassifier.{uB, uQ, uQ} B Q)
(j : ArrowSumUnresolved c → I) : B → I :=
Sum.elim i _root_.id ∘ arrowSumMerge c j
The algebra computing one step of IR.precomp: iota and
sigma push through (up to ULift); delta becomes a sigma
over classifiers followed by a delta over the unresolved
arity elements.
def precompAlg (Q : Type uQ) (i : Q → I) :
Alg.{uA, uB, uI, uO, max (max uA uB uQ + 1) (uB + 1) uI uO}
I O (IR.{max uA uB uQ, uB, uI, uO} I O) :=
⟨fun o ↦ iota I O o,
fun A f ↦ sigma I O (ULift.{max uB uQ} A) (f ∘ ULift.down),
fun B f ↦
sigma I O (ULift.{uA} (B → Q ⊕ PUnit.{uQ + 1})) (fun cl ↦
delta I O {b : B // cl.down b = Sum.inr PUnit.unit} (fun j ↦
f (precompMerge I Q i cl.down j)))⟩
Precomposition on codes (the γ^i of
[HancockMcBrideGhaniMalatestaAltenkirch2013], Lemma 4, which
asserts existence only; this construction is the project's):
⟦precomp Q i γ⟧ k is isomorphic to ⟦γ⟧ at the coproduct of
⟨Q, i⟩ with k.
def precomp (Q : Type uQ) (i : Q → I) :
IR.{uA, uB, uI, uO} I O → IR.{max uA uB uQ, uB, uI, uO} I O :=
elimAlg I O (IR.{max uA uB uQ, uB, uI, uO} I O) (precompAlg I O Q i)
Computation rule for IR.precomp at IR.iota: unchanged
(part of Lemma 4 of [HancockMcBrideGhaniMalatestaAltenkirch2013]).
theorem precomp_iota (Q : Type uQ) (i : Q → I) (o : O) :
precomp I O Q i (iota I O o) = iota I O o :=
rfl
Computation rule for IR.precomp at IR.sigma: the arity is
lifted (ULift), and precomp recurses into each subcode (part of
Lemma 4 of [HancockMcBrideGhaniMalatestaAltenkirch2013]).
theorem precomp_sigma (Q : Type uQ) (i : Q → I) (A : Type uA)
(c : A → IR.{uA, uB, uI, uO} I O) :
precomp I O Q i (sigma I O A c) =
sigma I O (ULift.{max uB uQ} A)
(fun a ↦ precomp I O Q i (c a.down)) :=
rfl
Computation rule for IR.precomp at IR.delta: a sigma over
classifiers B → Q ⊕ PUnit, then a delta over the unresolved
arity elements, recursing into the subcode at the merged
assignment (part of Lemma 4 of
[HancockMcBrideGhaniMalatestaAltenkirch2013]).
theorem precomp_delta (Q : Type uQ) (i : Q → I) (B : Type uB)
(c : (B → I) → IR.{uA, uB, uI, uO} I O) :
precomp I O Q i (delta I O B c) =
sigma I O (ULift.{uA} (ArrowSumClassifier.{uB, uQ, uQ} B Q))
(fun cl ↦ delta I O (ArrowSumUnresolved cl.down)
(fun j ↦ precomp I O Q i (c (precompMerge I Q i cl.down j)))) :=
rfl
The per-code statement of Lemma 4
([HancockMcBrideGhaniMalatestaAltenkirch2013]): interpreting a code
precomposed along Q, i is isomorphic to interpreting the code
directly at the coproduct object FreeCoprodCompDisc.plus ⟨Q, i⟩ k.
def PrecompIsoMotive (γ : IR.{max uA uB, uB, uI, uO} I O) :
Type (max (max uA uB + 1) uI) :=
(Q : Type uB) → (i : Q → I) →
(k : FreeCoprodCompDisc.{max uA uB, uI} I) →
FreeCoprodCompDisc.Iso O
(interpObj I O (precomp I O Q i γ) k)
(interpObj I O γ (FreeCoprodCompDisc.plus I ⟨Q, i⟩ k))
PrecompIsoMotive at the constant (iota) code: interpObj
ignores its argument at an iota code, so both sides are the same
object and the identity isomorphism suffices.
def precompIsoIota (o : O) : PrecompIsoMotive I O (iota I O o) :=
fun _ _ k ↦ FreeCoprodCompDisc.Iso.refl O (interpObj I O (iota I O o) k)
PrecompIsoMotive at the dependent sum (sigma) code: by
precomp_sigma, both sides are indexed coproducts of subcode
interpretations, related componentwise by the inductive hypotheses
ih via coprodIso over the equivalence stripping the ULift that
precomp_sigma introduces.
def precompIsoSigma (A : Type (max uA uB))
(c : A → IR.{max uA uB, uB, uI, uO} I O)
(ih : (a : A) → PrecompIsoMotive I O (c a)) :
PrecompIsoMotive I O (sigma I O A c) :=
fun Q i k ↦
FreeCoprodCompDisc.coprodIso O (ULift.{uB} A) A Equiv.ulift
(fun a ↦ interpObj I O (precomp I O Q i (c a.down)) k)
(fun a ↦ interpObj I O (c a) (FreeCoprodCompDisc.plus I ⟨Q, i⟩ k))
(fun a ↦ ih a.down Q i k)
The merged assignment precompMerge, taking the resolved elements
of c from the i-images and the unresolved elements from the
k-decodings of a direction assignment j, equals the cotuple
Sum.elim i k.2 reindexed along the reassembled function
arrowSumMerge c j. This aligns the delta subcode argument used on
the precomposed side with the one used on the direct side.
theorem precompMerge_elim (Q : Type uB) (i : Q → I)
(k : FreeCoprodCompDisc.{max uA uB, uI} I) (B : Type uB)
(c : ArrowSumClassifier.{uB, uB, uB} B Q)
(j : ArrowSumUnresolved c → k.1) :
precompMerge I Q i c (k.2 ∘ j) = Sum.elim i k.2 ∘ arrowSumMerge c j :=
funext (fun b ↦
Sum.casesOn (motive := fun t ↦ c b = t →
(precompMerge I Q i c (k.2 ∘ j) b = (Sum.elim i k.2 ∘ arrowSumMerge c j) b))
(c b)
(fun q h ↦
(congrArg (Sum.elim i _root_.id) (arrowSumMerge_eq c (k.2 ∘ j) b (Sum.inl q) h)).trans
(congrArg (Sum.elim i k.2) (arrowSumMerge_eq c j b (Sum.inl q) h)).symm)
(fun u h ↦
(congrArg (Sum.elim i _root_.id) (arrowSumMerge_eq c (k.2 ∘ j) b (Sum.inr u) h)).trans
(congrArg (Sum.elim i k.2) (arrowSumMerge_eq c j b (Sum.inr u) h)).symm)
rfl)
The delta-case inner isomorphism at a fixed classifier cl: over
the unresolved-arity coproduct, each precomposed subcode interpretation
is related, by the inductive hypothesis ih, to the direct
interpretation at the merged assignment, whose subcode argument
precompMerge_elim then rewrites to Sum.elim i k.2 ∘ arrowSumMerge cl g.
def precompIsoDeltaInner (B : Type uB)
(c : (B → I) → IR.{max uA uB, uB, uI, uO} I O)
(ih : (m : B → I) → PrecompIsoMotive I O (c m)) (Q : Type uB) (i : Q → I)
(k : FreeCoprodCompDisc.{max uA uB, uI} I) (cl : ArrowSumClassifier.{uB, uB, uB} B Q) :
FreeCoprodCompDisc.Iso O
(FreeCoprodCompDisc.coprod O (ArrowSumUnresolved cl → k.1)
(fun g ↦ interpObj I O (precomp I O Q i (c (precompMerge I Q i cl (k.2 ∘ g)))) k))
(FreeCoprodCompDisc.coprod O (ArrowSumUnresolved cl → k.1)
(fun g ↦ interpObj I O (c (Sum.elim i k.2 ∘ arrowSumMerge cl g))
(FreeCoprodCompDisc.plus I ⟨Q, i⟩ k))) :=
FreeCoprodCompDisc.coprodIso O ({b // cl b = Sum.inr PUnit.unit} → k.1)
({b // cl b = Sum.inr PUnit.unit} → k.1) (Equiv.refl _)
(fun g ↦ interpObj I O (precomp I O Q i (c (precompMerge I Q i cl (k.2 ∘ g)))) k)
(fun g ↦ interpObj I O (c (Sum.elim i k.2 ∘ arrowSumMerge cl g))
(FreeCoprodCompDisc.plus I ⟨Q, i⟩ k))
(fun g ↦ FreeCoprodCompDisc.Iso.trans O (ih (precompMerge I Q i cl (k.2 ∘ g)) Q i k)
(FreeCoprodCompDisc.isoOfEq O
(congrArg (fun m ↦ interpObj I O (c m) (FreeCoprodCompDisc.plus I ⟨Q, i⟩ k))
(precompMerge_elim I Q i k B cl g))))
The delta interpretation reshuffled as a coproduct, over the
direction classifiers cl : B → Q ⊕ PUnit, of coproducts, over the
k-assignments of each classifier's unresolved elements, of the
interpretations of the direct subcodes at the coproduct object
FreeCoprodCompDisc.plus ⟨Q, i⟩ k. This is the common endpoint of
precompIsoDeltaStrip and precompIsoDeltaReshuffle.
abbrev precompDeltaCoprod (B : Type uB)
(c : (B → I) → IR.{max uA uB, uB, uI, uO} I O) (Q : Type uB) (i : Q → I)
(k : FreeCoprodCompDisc.{max uA uB, uI} I) :
FreeCoprodCompDisc.{max uA uB, uO} O :=
FreeCoprodCompDisc.coprod O (ArrowSumClassifier.{uB, uB, uB} B Q)
(fun cl ↦ FreeCoprodCompDisc.coprod O (ArrowSumUnresolved cl → k.1)
(fun g ↦ interpObj I O (c (Sum.elim i k.2 ∘ arrowSumMerge cl g))
(FreeCoprodCompDisc.plus I ⟨Q, i⟩ k)))
The delta-case classifier-stripping isomorphism: strips the
ULift on the sigma-over-classifiers index introduced by
precomp_delta (via Equiv.ulift) and, componentwise, applies
precompIsoDeltaInner. The source is definitionally the precomposed
delta interpretation.
def precompIsoDeltaStrip (B : Type uB)
(c : (B → I) → IR.{max uA uB, uB, uI, uO} I O)
(ih : (m : B → I) → PrecompIsoMotive I O (c m)) (Q : Type uB) (i : Q → I)
(k : FreeCoprodCompDisc.{max uA uB, uI} I) :
FreeCoprodCompDisc.Iso O
(interpObj I O (precomp I O Q i (delta I O B c)) k)
(precompDeltaCoprod I O B c Q i k) :=
FreeCoprodCompDisc.coprodIso O (ULift.{max uA uB} (B → Q ⊕ PUnit.{uB + 1}))
(B → Q ⊕ PUnit.{uB + 1}) Equiv.ulift
(fun cl ↦ interpObj I O (delta I O {b // cl.down b = Sum.inr PUnit.unit}
(fun j ↦ precomp I O Q i (c (precompMerge I Q i cl.down j)))) k)
(fun cl ↦ FreeCoprodCompDisc.coprod O ({b // cl b = Sum.inr PUnit.unit} → k.1)
(fun g ↦ interpObj I O (c (Sum.elim i k.2 ∘ arrowSumMerge cl g))
(FreeCoprodCompDisc.plus I ⟨Q, i⟩ k)))
(fun cl ↦ precompIsoDeltaInner I O B c ih Q i k cl.down)
The delta-case reshuffling isomorphism: the double coproduct over
classifiers and their unresolved assignments is regrouped, via the
sigma-associativity equivalence and arrowSumEquivSigma, into the
single coproduct over assignments B → Q ⊕ k.1 that is definitionally
the direct delta interpretation at the coproduct object.
def precompIsoDeltaReshuffle (B : Type uB)
(c : (B → I) → IR.{max uA uB, uB, uI, uO} I O) (Q : Type uB) (i : Q → I)
(k : FreeCoprodCompDisc.{max uA uB, uI} I) :
FreeCoprodCompDisc.Iso O
(precompDeltaCoprod I O B c Q i k)
(interpObj I O (delta I O B c) (FreeCoprodCompDisc.plus I ⟨Q, i⟩ k)) :=
⟨(Equiv.sigmaAssoc (fun (cl : B → Q ⊕ PUnit.{uB + 1})
(g : {b // cl b = Sum.inr PUnit.unit} → k.1) ↦
(interpObj I O (c (Sum.elim i k.2 ∘ arrowSumMerge cl g))
(FreeCoprodCompDisc.plus I ⟨Q, i⟩ k)).1)).symm.trans
(Equiv.sigmaCongrLeft
(β := fun (g' : B → Q ⊕ k.1) ↦
(interpObj I O (c (Sum.elim i k.2 ∘ g')) (FreeCoprodCompDisc.plus I ⟨Q, i⟩ k)).1)
(arrowSumEquivSigma B Q k.1).symm),
funext (fun _ ↦ rfl)⟩
PrecompIsoMotive at the dependent product (delta) code (the
delta case of Lemma 4 of [HancockMcBrideGhaniMalatestaAltenkirch2013]):
by precomp_delta the precomposed side is a sigma over classifiers of
a delta over their unresolved elements; precompIsoDeltaStrip relates
it (using ih) to the double coproduct at the merged assignments, and
precompIsoDeltaReshuffle regroups that into the direct delta
interpretation at the coproduct object.
def precompIsoDelta (B : Type uB)
(c : (B → I) → IR.{max uA uB, uB, uI, uO} I O)
(ih : (m : B → I) → PrecompIsoMotive I O (c m)) :
PrecompIsoMotive I O (delta I O B c) :=
fun Q i k ↦
FreeCoprodCompDisc.Iso.trans O (precompIsoDeltaStrip I O B c ih Q i k)
(precompIsoDeltaReshuffle I O B c Q i k)
The step argument to the recursor which generates the family of
isomorphisms of Lemma 4, dispatching on the shape to the constant,
dependent sum, and dependent product cases, as interpMorStep does for
the morphism map.
def interpPrecompIsoStep :
RecStep.{max uA uB, uB, uI, uO, max (max uA uB + 1) uI} I O
(PrecompIsoMotive I O) :=
fun s c m ↦ match s with
| Sum.inl o => precompIsoIota I O o
| Sum.inr (Sum.inl A) =>
precompIsoSigma I O A (fun a ↦ c (ULift.up a)) (fun a ↦ m (ULift.up a))
| Sum.inr (Sum.inr B) =>
precompIsoDelta I O B (fun f ↦ c (ULift.up f)) (fun f ↦ m (ULift.up f))
Lemma 4 of [HancockMcBrideGhaniMalatestaAltenkirch2013]: interpreting
a code precomposed along Q, i is isomorphic to interpreting the code
directly at the coproduct object FreeCoprodCompDisc.plus ⟨Q, i⟩ k. The
paper asserts an equality; the recorded deviation replaces it with the
isomorphism PrecompIsoMotive, obtained by IR.rec from the per-shape
steps.
def interpPrecompIso (γ : IR.{max uA uB, uB, uI, uO} I O) :
PrecompIsoMotive I O γ :=
rec I O (interpPrecompIsoStep I O) γ
The name type of the delta interpretation regrouped by the
fibers of the direction-decoding composite k.2 ∘ g: over each
direction assignment i : B → I, the fiber {g : B → k.1 // k.2 ∘ g = i} paired with the name type of the subcode interpretation c i at
k.
abbrev InterpDeltaFiberSigma (B : Type uB)
(c : (B → I) → IR.{max uA uB, uB, uI, uO} I O)
(k : FreeCoprodCompDisc.{max uA uB, uI} I) :=
Σ i : B → I, Σ _ : {g : B → k.1 // k.2 ∘ g = i}, (interpObj I O (c i) k).1
The grouping equivalence underlying Lemma 3 of
[HancockMcBrideGhaniMalatestaAltenkirch2013]: the directions
g : B → k.1 of the delta interpretation are grouped by their
composite k.2 ∘ g : B → I with the decoding of k, presenting each
group as a fiber of that composite.
def interpDeltaIsoGroup (B : Type uB)
(c : (B → I) → IR.{max uA uB, uB, uI, uO} I O)
(k : FreeCoprodCompDisc.{max uA uB, uI} I) :
(interpObj I O (delta I O B c) k).1 ≃ InterpDeltaFiberSigma I O B c k :=
sigmaCompEquivSigmaFiber (f := (k.2 ∘ ·)) (N := fun i ↦ (interpObj I O (c i) k).1)
The direction-replacement equivalence underlying Lemma 3 of
[HancockMcBrideGhaniMalatestaAltenkirch2013]: per composite i : B → I,
the fiber {g : B → k.1 // k.2 ∘ g = i} is the morphism type
Hom I (lift ⟨B, i⟩) k (by homLiftEquiv), so each grouped summand
becomes the name type of the copower. The projection-based form (rather
than Equiv.sigmaCongrLeft') keeps the second component untransported,
so the decodings agree definitionally.
def interpDeltaIsoHom (B : Type uB)
(c : (B → I) → IR.{max uA uB, uB, uI, uO} I O)
(k : FreeCoprodCompDisc.{max uA uB, uI} I) :
InterpDeltaFiberSigma I O B c k ≃
Σ i : B → I, Σ _ : FreeCoprodCompDisc.Hom I
(FreeCoprodCompDisc.lift.{uB, uI, max uA uB} I ⟨B, i⟩) k,
(interpObj I O (c i) k).1 :=
sigmaCongrRight' (fun i ↦
{ toFun := fun q ↦ ⟨(FreeCoprodCompDisc.homLiftEquiv I ⟨B, i⟩ k).symm q.1, q.2⟩,
invFun := fun q ↦ ⟨FreeCoprodCompDisc.homLiftEquiv I ⟨B, i⟩ k q.1, q.2⟩,
left_inv := fun q ↦
congrArg (fun s ↦ (⟨s, q.2⟩ : Σ _ : {g : B → k.1 // k.2 ∘ g = i},
(interpObj I O (c i) k).1))
((FreeCoprodCompDisc.homLiftEquiv I ⟨B, i⟩ k).apply_symm_apply q.1),
right_inv := fun q ↦
congrArg (fun s ↦ (⟨s, q.2⟩ : Σ _ : FreeCoprodCompDisc.Hom I
(FreeCoprodCompDisc.lift.{uB, uI, max uA uB} I ⟨B, i⟩) k,
(interpObj I O (c i) k).1))
((FreeCoprodCompDisc.homLiftEquiv I ⟨B, i⟩ k).symm_apply_apply q.1) })
Lemma 3 of [HancockMcBrideGhaniMalatestaAltenkirch2013]:
interpreting the dependent product (delta) code at k is isomorphic
to the indexed coproduct, over the direction assignments i : B → I,
of the copower of the interpretation of the subcode c i by the
morphisms Hom I (lift ⟨B, i⟩) k. The paper states a natural
isomorphism; the recorded deviation states it pointwise at k; the
naturality upgrade is IR.natDeltaEquiv.
The isomorphism composes interpDeltaIsoGroup and interpDeltaIsoHom;
its decodings agree definitionally.
def interpDeltaIso (B : Type uB)
(c : (B → I) → IR.{max uA uB, uB, uI, uO} I O)
(k : FreeCoprodCompDisc.{max uA uB, uI} I) :
FreeCoprodCompDisc.Iso O
(interpObj I O (delta I O B c) k)
(FreeCoprodCompDisc.coprod O (B → I) (fun i ↦
FreeCoprodCompDisc.copower O
(FreeCoprodCompDisc.Hom I
(FreeCoprodCompDisc.lift.{uB, uI, max uA uB} I ⟨B, i⟩) k)
(interpObj I O (c i) k))) :=
⟨(interpDeltaIsoGroup I O B c k).trans (interpDeltaIsoHom I O B c k),
funext (fun _ ↦ rfl)⟩end IRend IndRec