1. Geb
  2. Prototypes
  3. LargeIR
  4. Binder
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.General meta import GebMeta -- shake: keep; supplies the cite docstring role
set_option doc.verso true

Prototype: the binder of a universe is not a walking-arrow functor

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

A universe closed under dependent products is an inductive-recursive definition whose product former takes a code a and a family of codes b : T a → U indexed by the terms of a, decoding to the dependent product Π x : T a, T (b x). As a code it is δ 1 (fun T₀ ↦ δ (T₀ ()) (fun T₁ ↦ ι (Π T₁))), whose inner δ has the arity T₀ (), a decoding rather than a fixed set. On families this is the assignment (U, T) ↦ Σ (a : U), Σ (b : T a → U), Π (x : T a), T (b x), whose component b : T a → U is contravariant in the fibre T a, so it is not a covariant functor on Fam(Type) with its morphisms proper, and the interpretation of large inductive-recursive definitions 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.
accordingly reaches it only over Fam(Cᵒᵖ) or over groupoids. The repository's PresheafIRUniv.­univPsh met the same obstruction: its formers are binary, the family of codes under the binder dropped.

This module states the obstruction against walking-arrow presheaf polynomial functors, whose values GebProto.­LargeIR.­elemEquiv computes as a shape with a base assignment on a fixed set of level-0 directions and an assignment on a fixed set of level-1 directions. At the presheaf termsPsh n with one code and n terms, the product former's level-1 value is Fin n → Fin n, piFormerEquiv, a family of types no fixed direction sets produce: not_piFormer shows that no walking-arrow presheaf polynomial functor has level-1 values in bijection with the product former's at every termsPsh n, the bijections at n = 0 and n = 1 forcing a single level-1 shape with no level-1 directions, whose value at n = 2 is then a point rather than the four functions Fin 2 → Fin 2. The bijections are not asked to be natural.

Main definitions

  • termsPsh — the walking-arrow presheaf with one code and n terms.

  • PiFormerValue — the level-1 value of the dependent-product former at a walking-arrow presheaf.

Main statements

  • piFormerEquiv — at termsPsh n the product former's value is Fin n → Fin n.

  • not_piFormer — no walking-arrow presheaf polynomial functor has the product former's values.

References

  • [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.

  • [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.

Tags

prototype, universe, dependent product, inductive-recursive, walking arrow, variance

@[expose] public sectionopen CategoryTheory PresheafIRUniv IndRecnamespace GebProto.LargeIR

The walking-arrow presheaf with one code and n terms.

def termsPsh (n : ℕ) : (Fin 2)ᵒᵖ ⥤ Type := ofSlice fun _ : Fin n ↦ ()

The code fibre of termsPsh n is a point.

theorem termsPsh_zero_eq {n : ℕ} (x y : (termsPsh n).obj ⟨0⟩) : x = y := Subsingleton.elim (α := Unit) x y

The level-1 value of the dependent-product former at a walking-arrow presheaf: a code, a family of codes indexed by its terms, and a term of each member of the family.

def PiFormerValue (Z : (Fin 2)ᵒᵖ ⥤ Type) : Type := Σ a : Z.obj ⟨0⟩, Σ b : (famOfPsh Z).2 a → Z.obj ⟨0⟩, ∀ x, (famOfPsh Z).2 (b x)

At termsPsh n the product former's value is Fin n → Fin n.

def piFormerEquiv (n : ℕ) : PiFormerValue (termsPsh n) ≃ (Fin n → Fin n) where toFun v i := (v.2.2 ⟨i, termsPsh_zero_eq _ _⟩).1 invFun f := ⟨(), fun _ ↦ (), fun x ↦ ⟨f x.1, rfl⟩⟩ left_inv v := n:ℕv:PiFormerValue (termsPsh n)⊢ (fun f ↦ ⟨(), ⟨fun x ↦ (), fun x ↦ ⟨f ↑x, ⋯⟩⟩⟩) ((fun v i ↦ ↑(v.snd.snd ⟨i, ⋯⟩)) v) = v n:ℕa:(termsPsh n).obj (Opposite.op 0)b:(famOfPsh (termsPsh n)).snd a → (termsPsh n).obj (Opposite.op 0)t:(x : (famOfPsh (termsPsh n)).snd a) → (famOfPsh (termsPsh n)).snd (b x)⊢ (fun f ↦ ⟨(), ⟨fun x ↦ (), fun x ↦ ⟨f ↑x, ⋯⟩⟩⟩) ((fun v i ↦ ↑(v.snd.snd ⟨i, ⋯⟩)) ⟨a, ⟨b, t⟩⟩) = ⟨a, ⟨b, t⟩⟩ n:ℕb:(famOfPsh (termsPsh n)).snd () → (termsPsh n).obj (Opposite.op 0)t:(x : (famOfPsh (termsPsh n)).snd ()) → (famOfPsh (termsPsh n)).snd (b x)⊢ (fun f ↦ ⟨(), ⟨fun x ↦ (), fun x ↦ ⟨f ↑x, ⋯⟩⟩⟩) ((fun v i ↦ ↑(v.snd.snd ⟨i, ⋯⟩)) ⟨(), ⟨b, t⟩⟩) = ⟨(), ⟨b, t⟩⟩ n:ℕt:(x : (famOfPsh (termsPsh n)).snd ()) → (famOfPsh (termsPsh n)).snd ((fun x ↦ ()) x)⊢ (fun f ↦ ⟨(), ⟨fun x ↦ (), fun x ↦ ⟨f ↑x, ⋯⟩⟩⟩) ((fun v i ↦ ↑(v.snd.snd ⟨i, ⋯⟩)) ⟨(), ⟨fun x ↦ (), t⟩⟩) = ⟨(), ⟨fun x ↦ (), t⟩⟩ All goals completed! 🐙 right_inv _ := rfl

The level-1 elements of a functor's value at termsPsh n in dependent-type terms.

abbrev TermsElem (F : PresheafPFunctor.{0, 0, 0, 0, 0, 0} (Fin 2) (Fin 2)) (n : ℕ) : Type := ElemAt F (termsPsh n) 1

An element at a level-1 shape with every term the term 0.

def termsElemMk (F : PresheafPFunctor.{0, 0, 0, 0, 0, 0} (Fin 2) (Fin 2)) (a : F.Shape 1) : TermsElem F 1 := ⟨a, fun _ ↦ (), fun _ ↦ ⟨(0 : Fin 1), rfl⟩⟩

No walking-arrow presheaf polynomial functor has level-1 values in bijection with the dependent-product former's at every termsPsh n.

theorem not_piFormer (F : PresheafPFunctor.{0, 0, 0, 0, 0, 0} (Fin 2) (Fin 2)) (e : ∀ n : ℕ, { x : F.obj (termsPsh n) // F.q x.shape = 1 } ≃ PiFormerValue (termsPsh n)) : False := F:PresheafPFunctor (Fin 2) (Fin 2)e:(n : ℕ) → { x // F.q x.shape = 1 } ≃ PiFormerValue (termsPsh n)⊢ False F:PresheafPFunctor (Fin 2) (Fin 2)e:(n : ℕ) → { x // F.q x.shape = 1 } ≃ PiFormerValue (termsPsh n)e':(n : ℕ) → TermsElem F n ≃ (Fin n → Fin n)⊢ False -- At `n = 1` the value is a point, so there is one level-`1` shape. F:PresheafPFunctor (Fin 2) (Fin 2)e:(n : ℕ) → { x // F.q x.shape = 1 } ≃ PiFormerValue (termsPsh n)e':(n : ℕ) → TermsElem F n ≃ (Fin n → Fin n)hshape:∀ (a a' : F.toSlicePFunctor.Shape 1), a = a'⊢ False -- At `n = 0` the value is a point, so that shape has no level-`1` directions. F:PresheafPFunctor (Fin 2) (Fin 2)e:(n : ℕ) → { x // F.q x.shape = 1 } ≃ PiFormerValue (termsPsh n)e':(n : ℕ) → TermsElem F n ≃ (Fin n → Fin n)hshape:∀ (a a' : F.toSlicePFunctor.Shape 1), a = a'hdir:∀ (a : F.toSlicePFunctor.Shape 1) (a : F.Direction (↑a) 1), False⊢ False -- Then the value at every `n` is a point. F:PresheafPFunctor (Fin 2) (Fin 2)e:(n : ℕ) → { x // F.q x.shape = 1 } ≃ PiFormerValue (termsPsh n)e':(n : ℕ) → TermsElem F n ≃ (Fin n → Fin n)hshape:∀ (a a' : F.toSlicePFunctor.Shape 1), a = a'hdir:∀ (a : F.toSlicePFunctor.Shape 1) (a : F.Direction (↑a) 1), Falsehsub:∀ (x y : TermsElem F 2), x = y⊢ False -- But `Fin 2 → Fin 2` is not. All goals completed! 🐙
end GebProto.LargeIR