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.Prototypes.LargeIR.Basic
public import Geb.Mathlib.Data.PFunctor.IndRec.Basic
meta import GebMeta  -- shake: keep; supplies the cite docstring role

set_option doc.verso true

Prototype: the transcription read back as a large inductive-recursive code

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

GebProto.LargeIR.objEquiv computes the value of the transcription GebProto.LargeIR.arrowPsh of a slice polynomial functor P : Type/X → Type/Y at a walking-arrow presheaf Z as a level 0 of Y × (X → Z 0) and a level 1 over (y, f₀) of P at the pullback along f₀. This module reads that computation back as the interpretation of an inductive-recursive code on Fam(Type), the free coproduct completion of Type, in the repository's code system IndRec.IR at input and output index type Type: the code code P is σ Y (fun y ↦ δ X (fun A ↦ ι (fibreValue P y A))), whose σ contributes the Y, whose δ contributes the base map X → Z 0 as the assignment g : X → U of the δ rule, and whose ι decodes to the slice functor's fibre at y applied to the decoded family T ∘ g. The interpretation IndRec.IR.interpObj of code P at the family (U, T) of Z — U := Z 0 and T u the fibre of Z 1 → Z 0 over u — is isomorphic, as a walking-arrow presheaf, to the transcription's value. That is arrowPshCodeEquiv, and it confirms the reading of the transcription as a large-IR δ code rather than as the slice functor.

The comparison is stated between walking-arrow presheaves, a family being turned into one by GebProto.LargeIR.ofSlice of the projection of its total space, and an isomorphism of walking-arrow presheaves is a pair of equivalences commuting with the restriction map, PshEquiv. Two choices are forced by what is available choice-free. A functor-category isomorphism would name the functor category, which depends on Classical.choice, so the isomorphism is unbundled. And the repository's CategoryTheory.FreeCoprodCompDisc is the completion of Type as a discrete category, whose morphisms compare decodings by equality, so the agreement is stated at the level of objects: the morphism action of large inductive-recursive definitions, which compares decodings by functions T u → T' (h u) and is what the positivity of

[GhaniNordvallForsbergMalatesta2015]

Neil Ghani, Fredrik Nordvall Forsberg, Lorenzo Malatesta (2015). “Positive Inductive-Recursive Definitions”. Logical Methods in Computer Science 11(1). https://doi.org/10.2168/LMCS-11(1:13)2015.

provides, is outside what that completion expresses, and is not compared here.

Main definitions

fibreValue — the slice functor's fibre at an output index, applied to a family X → Type.
code — the code σ Y (fun y ↦ δ X (fun A ↦ ι (fibreValue P y A))).
famOfPsh — the family (U, T) of a walking-arrow presheaf; pshOfFam — the walking-arrow presheaf of a family.
PshEquiv — an isomorphism of walking-arrow presheaves, unbundled; PshEquiv.trans its composition.
levelsPsh — GebProto.LargeIR.Levels as a walking-arrow presheaf.
levelZeroEquiv, levelOneEquiv — the level-0 and level-1 elements of the transcription's value as the two summands of GebProto.LargeIR.Levels.

Main statements

objPresheafEquiv — the transcription's output presheaf is levelsPsh.
levelsCodeEquiv — levelsPsh is the presheaf of the code's interpretation at the family of the input.
arrowPshCodeEquiv — their composite: the transcription's output presheaf is the presheaf of the code's interpretation.

References

[DybjerSetzer2003]
Peter Dybjer, Anton Setzer (2003). “Induction--recursion and initial algebras”. Annals of Pure and Applied Logic 124(1--3), pp. 1–47. https://doi.org/10.1016/S0168-0072(02)00096-9.
[GhaniNordvallForsbergMalatesta2015]
Neil Ghani, Fredrik Nordvall Forsberg, Lorenzo Malatesta (2015). “Positive Inductive-Recursive Definitions”. Logical Methods in Computer Science 11(1). https://doi.org/10.2168/LMCS-11(1:13)2015.

The code

The slice functor's fibre at the output index y, applied to a family A : X → Type: a shape over y with an element of the family at each direction's input index.

def fibreValue (y : Y) (A : X → Type) : Type :=
  Σ a : P.Shape y, ∀ b : P.B a.1, A (P.r ⟨a.1, b⟩)

The code σ Y (fun y ↦ δ X (fun A ↦ ι (fibreValue P y A))): a constructor for each output index, whose recursive arguments are indexed by X and whose decoding is the slice functor's fibre applied to the decodings of those arguments.

def code : IR.{0, 0, 1, 1} Type Type :=
  IR.sigma Type Type Y fun y ↦ IR.delta Type Type X fun A ↦ IR.iota Type Type (fibreValue P y A)

Families and walking-arrow presheaves

The family (U, T) of a walking-arrow presheaf: U := Z 0 and T u the fibre of the restriction Z 1 → Z 0 over u.

def famOfPsh (Z : (Fin 2)ᵒᵖ ⥤ Type) : FreeCoprodCompDisc.{0, 1} Type :=
  ⟨Z.obj ⟨0⟩, fun u ↦ { z : Z.obj ⟨1⟩ // Z.map waHom.op z = u }⟩

The walking-arrow presheaf of a family: the projection of its total space as an object of Type/U.

def pshOfFam (F : FreeCoprodCompDisc.{0, 1} Type) : (Fin 2)ᵒᵖ ⥤ Type :=
  ofSlice (Sigma.fst : (Σ u : F.1, F.2 u) → F.1)

An isomorphism of walking-arrow presheaves, unbundled: equivalences at the two levels commuting with the restriction map.

The equivalence at level 0.

The equivalence at level 1.

The equivalences commute with the restriction along 0 ⟶ 1.

              structure PshEquiv (Z Z' : (Fin 2)ᵒᵖ ⥤ Type) where  base : Z.obj ⟨0⟩ ≃ Z'.obj ⟨0⟩  total : Z.obj ⟨1⟩ ≃ Z'.obj ⟨1⟩  map_total : ∀ z, Z'.map waHom.op (total z) = base (Z.map waHom.op z)

Composition of isomorphisms of walking-arrow presheaves.

def PshEquiv.trans {Z Z' Z'' : (Fin 2)ᵒᵖ ⥤ Type} (e : PshEquiv Z Z') (e' : PshEquiv Z' Z'') :
    PshEquiv Z Z'' where
  base := e.base.trans e'.base
  total := e.total.trans e'.total
  map_total z := (e'.map_total (e.total z)).trans (congrArg e'.base (e.map_total z))

The transcription's output presheaf as a family

variable (Z : (Fin 2)ᵒᵖ ⥤ Type)

The level of a summand of GebProto.LargeIR.Levels.

def levelOf : Levels P Z → Fin 2 :=
  Sum.elim (fun _ ↦ 0) (fun _ ↦ 1)

The level of an element of the transcription's value is the level of its image in GebProto.LargeIR.Levels.

theorem q_shape_eq_levelOf (x : (arrowPsh P).obj Z) :
    (arrowPsh P).q x.shape = levelOf P Z (toLevels P Z x) :=
  match x with
  | ⟨⟨⟨.inl _, _⟩, _⟩, _⟩ => rfl
  | ⟨⟨⟨.inr _, _⟩, _⟩, _⟩ => rfl

GebProto.LargeIR.toLevels inverts GebProto.LargeIR.ofLevels.

theorem toLevels_ofLevels (l : Levels P Z) : toLevels P Z (ofLevels P Z l) = l := byX:TypeY:TypeP:SlicePFunctor X YZ:(Fin 2)ᵒᵖ ⥤ Typel:Levels P Z⊢ toLevels P Z (ofLevels P Z l) = l
  exact (objEquiv P Z).right_inv lAll goals completed! 🐙

GebProto.LargeIR.ofLevels inverts GebProto.LargeIR.toLevels.

theorem ofLevels_toLevels (x : (arrowPsh P).obj Z) : ofLevels P Z (toLevels P Z x) = x := byX:TypeY:TypeP:SlicePFunctor X YZ:(Fin 2)ᵒᵖ ⥤ Typex:(arrowPsh P).obj Z⊢ ofLevels P Z (toLevels P Z x) = x
  exact (objEquiv P Z).left_inv xAll goals completed! 🐙

The elements of the transcription's value over j are the summands of GebProto.LargeIR.Levels at level j.

def objLevelEquiv (j : Fin 2) :
    { x : (arrowPsh P).obj Z // (arrowPsh P).q x.shape = j } ≃
      { l : Levels P Z // levelOf P Z l = j } where
  toFun x := ⟨toLevels P Z x.1, (q_shape_eq_levelOf P Z x.1).symm.trans x.2⟩
  invFun l := ⟨ofLevels P Z l.1,
    (q_shape_eq_levelOf P Z _).trans
      ((congrArg (levelOf P Z) (toLevels_ofLevels P Z l.1)).trans l.2)⟩
  left_inv x := Subtype.ext (ofLevels_toLevels P Z x.1)
  right_inv l := Subtype.ext (toLevels_ofLevels P Z l.1)

The elements of a sum at level 0 are its left summand.

def sumLeftEquiv {α β : Type} :
    { s : α ⊕ β // Sum.elim (fun _ ↦ 0) (fun _ ↦ 1) s = (0 : Fin 2) } ≃ α where
  toFun s :=
    match s with
    | ⟨.inl a, _⟩ => a
    | ⟨.inr _, h⟩ => absurd h Fin.zero_ne_one.symm
  invFun a := ⟨.inl a, rfl⟩
  left_inv s :=
    match s with
    | ⟨.inl _, _⟩ => rfl
    | ⟨.inr _, h⟩ => absurd h Fin.zero_ne_one.symm
  right_inv _ := rfl

The elements of a sum at level 1 are its right summand.

def sumRightEquiv {α β : Type} :
    { s : α ⊕ β // Sum.elim (fun _ ↦ 0) (fun _ ↦ 1) s = (1 : Fin 2) } ≃ β where
  toFun s :=
    match s with
    | ⟨.inl _, h⟩ => absurd h Fin.zero_ne_one
    | ⟨.inr b, _⟩ => b
  invFun b := ⟨.inr b, rfl⟩
  left_inv s :=
    match s with
    | ⟨.inl _, h⟩ => absurd h Fin.zero_ne_one
    | ⟨.inr _, _⟩ => rfl
  right_inv _ := rfl

The level-0 elements of the transcription's value are Y × (X → Z 0).

def levelZeroEquiv :
    { x : (arrowPsh P).obj Z // (arrowPsh P).q x.shape = 0 } ≃ (Y × (X → Z.obj ⟨0⟩)) :=
  (objLevelEquiv P Z 0).trans sumLeftEquiv

The level-1 elements of the transcription's value are the sum over the base maps of the slice functor's values at the pullbacks.

def levelOneEquiv :
    { x : (arrowPsh P).obj Z // (arrowPsh P).q x.shape = 1 } ≃
      (Σ f₀ : X → Z.obj ⟨0⟩, P.toSliceDomPFunctor.Obj (pullbackProj Z f₀)) :=
  (objLevelEquiv P Z 1).trans sumRightEquiv

The level-1 part of GebProto.LargeIR.Levels regrouped over the level-0 part: over (y, f₀), the slice functor's values at the pullback along f₀ whose output index is y.

def levelsFibre (yf : Y × (X → Z.obj ⟨0⟩)) : Type :=
  { o : P.toSliceDomPFunctor.Obj (pullbackProj Z yf.2) // P.obj (pullbackProj Z yf.2) o = yf.1 }

An element of the regrouped level-1 part reassembled from its components along an equation of its output index is the original element.

theorem levelsFibre_ext {f₀ : X → Z.obj ⟨0⟩} {y : Y}
    (o : P.toSliceDomPFunctor.Obj (pullbackProj Z f₀)) (h : P.obj (pullbackProj Z f₀) o = y) :
    (⟨(P.obj (pullbackProj Z f₀) o, f₀), ⟨o, rfl⟩⟩ :
      Σ yf : Y × (X → Z.obj ⟨0⟩), levelsFibre P Z yf) = ⟨(y, f₀), ⟨o, h⟩⟩ := byX:TypeY:TypeP:SlicePFunctor X YZ:(Fin 2)ᵒᵖ ⥤ Typef₀:X → Z.obj (Opposite.op 0)y:Yo:P.Obj (pullbackProj Z f₀)h:P.obj (pullbackProj Z f₀) o = y⊢ ⟨(P.obj (pullbackProj Z f₀) o, f₀), ⟨o, ⋯⟩⟩ = ⟨(y, f₀), ⟨o, h⟩⟩
  subst hX:TypeY:TypeP:SlicePFunctor X YZ:(Fin 2)ᵒᵖ ⥤ Typef₀:X → Z.obj (Opposite.op 0)o:P.Obj (pullbackProj Z f₀)⊢ ⟨(P.obj (pullbackProj Z f₀) o, f₀), ⟨o, ⋯⟩⟩ = ⟨(P.obj (pullbackProj Z f₀) o, f₀), ⟨o, ⋯⟩⟩
  rflAll goals completed! 🐙

Regrouping the level-1 part over the level-0 part.

def levelsFibreEquiv :
    (Σ f₀ : X → Z.obj ⟨0⟩, P.toSliceDomPFunctor.Obj (pullbackProj Z f₀)) ≃
      Σ yf : Y × (X → Z.obj ⟨0⟩), levelsFibre P Z yf where
  toFun s := ⟨(P.obj (pullbackProj Z s.1) s.2, s.1), ⟨s.2, rfl⟩⟩
  invFun s := ⟨s.1.2, s.2.1⟩
  left_inv _ := rfl
  right_inv s := levelsFibre_ext P Z s.2.1 s.2.2

GebProto.LargeIR.Levels as a walking-arrow presheaf: the projection of the regrouped level-1 part onto the level-0 part.

def levelsPsh : (Fin 2)ᵒᵖ ⥤ Type :=
  ofSlice (Sigma.fst : (Σ yf : Y × (X → Z.obj ⟨0⟩), levelsFibre P Z yf) → Y × (X → Z.obj ⟨0⟩))

The transcription's output presheaf is levelsPsh: the two level equivalences, commuting with the restriction along 0 ⟶ 1 by GebProto.LargeIR.toLevels_objRestr.

def objPresheafEquiv : PshEquiv ((arrowPsh P).objPresheaf Z) (levelsPsh P Z) where
  base := levelZeroEquiv P Z
  total := (levelOneEquiv P Z).trans (levelsFibreEquiv P Z)
  map_total t :=
    match t with
    | ⟨⟨⟨⟨.inl _, _⟩, _⟩, _⟩, ht⟩ => absurd ht Fin.zero_ne_one
    | ⟨⟨⟨⟨.inr _, _⟩, _⟩, _⟩, _⟩ => rfl

The code's interpretation as a family

The level-0 part of GebProto.LargeIR.Levels is the index type of the code's interpretation: a σ index, a δ assignment, and the ι point.

def codeBaseEquiv :
    (Y × (X → Z.obj ⟨0⟩)) ≃ (IR.interpObj Type Type (code P) (famOfPsh Z)).1 where
  toFun yf := ⟨yf.1, yf.2, ⟨()⟩⟩
  invFun s := (s.1, s.2.1)
  left_inv _ := rfl
  right_inv s :=
    match s with
    | ⟨_, _, ⟨⟨⟩⟩⟩ => rfl

Over (y, f₀), the slice functor's value at the pullback along f₀ with output index y is the code's decoding: the fibre at y applied to the decoded family T ∘ f₀.

def codeFibreEquiv (yf : Y × (X → Z.obj ⟨0⟩)) :
    levelsFibre P Z yf ≃ fibreValue P yf.1 ((famOfPsh Z).2 ∘ yf.2) where
  toFun o := ⟨⟨o.1.1.1, o.2⟩,
    fun b ↦ ⟨(o.1.1.2 b).2.1, (o.1.1.2 b).2.2.trans (congrArg yf.2 (congrFun o.1.2 b))⟩⟩
  invFun w := ⟨⟨⟨w.1.1, fun b ↦ ⟨P.r ⟨w.1.1, b⟩, w.2 b⟩⟩, rfl⟩, w.1.2⟩
  left_inv o :=
    Subtype.ext (Subtype.ext (Sigma.ext rfl (heq_of_eq (funext fun b ↦
      pullbackAlong_ext Z (o.1.1.2 b) _ (congrFun o.1.2 b)))))
  right_inv _ := rfl

levelsPsh is the presheaf of the code's interpretation at the family of the input.

def levelsCodeEquiv :
    PshEquiv (levelsPsh P Z) (pshOfFam (IR.interpObj Type Type (code P) (famOfPsh Z))) where
  base := codeBaseEquiv P Z
  total :=
    { toFun := fun s ↦ ⟨codeBaseEquiv P Z s.1, codeFibreEquiv P Z s.1 s.2⟩
      invFun := fun s ↦
        match s with
        | ⟨⟨y, g, ⟨⟨⟩⟩⟩, w⟩ => ⟨(y, g), (codeFibreEquiv P Z (y, g)).symm w⟩
      left_inv := fun s ↦
        congrArg (Sigma.mk s.1) ((codeFibreEquiv P Z s.1).left_inv s.2)
      right_inv := fun s ↦
        match s with
        | ⟨⟨y, g, ⟨⟨⟩⟩⟩, w⟩ =>
          Sigma.ext rfl (heq_of_eq ((codeFibreEquiv P Z (y, g)).right_inv w)) }
  map_total _ := rfl

The transcription's output presheaf at Z is the presheaf of the interpretation of code P at the family of Z: the transcription of a slice polynomial functor is the large inductive-recursive code σ Y (fun y ↦ δ X (fun A ↦ ι (fibreValue P y A))).

def arrowPshCodeEquiv :
    PshEquiv ((arrowPsh P).objPresheaf Z)
      (pshOfFam (IR.interpObj Type Type (code P) (famOfPsh Z))) :=
  (objPresheafEquiv P Z).trans (levelsCodeEquiv P Z)

end GebProto.LargeIR