1. Geb
  2. Prototypes
  3. LargeIR
  4. Grothendieck
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.Morphism public import Geb.Mathlib.CategoryTheory.Grothendieck.Basic public import Mathlib.CategoryTheory.Pi.Basic meta import GebMeta -- shake: keep; supplies the cite docstring role
set_option doc.verso true

Prototype: the free coproduct completion as a Grothendieck construction

Throwaway exploration, not upstream-eligible content. This module names mathlib's CategoryTheory.­Cat and functor categories, so it depends on Classical.­choice and is listed in GebMeta.­classicalAllowedModules; its content is packaging, the choice-free content being in GebProto.­LargeIR.­FamHom and GebProto.­LargeIR.­codeMap.

The free coproduct completion Fam(Type), with its morphisms proper, is the contravariant Grothendieck construction CategoryTheory.­CoGrothendieck of the functor famFib : Typeᵒᵖ ⥤ Cat sending an index type U to the category U → Type of families over it, with pointwise morphisms, and a map of index types to precomposition, CategoryTheory.­Pi.­comap, which is strictly functorial. Its objects are the objects of CategoryTheory.­FreeCoprodCompDisc at Type, objGrEquiv, and its morphisms are GebProto.­LargeIR.­FamHom, homGrEquiv: a base map with a fibre morphism into the precomposed family. The action GebProto.­LargeIR.­codeMap of the code GebProto.­LargeIR.­code on morphisms of families then packages, with its laws GebProto.­LargeIR.­codeMap_id and GebProto.­LargeIR.­codeMap_comp, as an endofunctor codeFunctor of the construction: the interpretation of the code as a functor on Fam(Type) proper, which is the positive inductive-recursive interpretation 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.
for this code.

Main definitions

  • famFib — the functor Typeᵒᵖ ⥤ Cat, U ↦ (U → Type).

  • FamGr — Fam(Type) as its contravariant Grothendieck construction.

  • objGrEquiv, homGrEquiv — its objects are the families and its morphisms are GebProto.­LargeIR.­FamHom.

  • codeFunctor — the code's interpretation as an endofunctor of FamGr.

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.

Tags

prototype, free coproduct completion, Grothendieck construction, inductive-recursive, code

@[expose] public sectionopen CategoryTheory IndRecnamespace GebProto.LargeIR

The Grothendieck construction

The functor Typeᵒᵖ ⥤ Cat sending an index type to the category of families over it and a map of index types to precomposition.

def famFib : Typeᵒᵖ ⥤ Cat.{0, 1} where obj U := Cat.of (U.unop → Type) map h := (Pi.comap (fun _ ↦ Type) (⇑h.unop)).toCatHom map_id _ := rfl map_comp _ _ := rfl

Fam(Type) as the contravariant Grothendieck construction of famFib.

abbrev FamGr : Type 1 := CoGrothendieck famFib

A family as an object of the construction.

def toGr (F : FreeCoprodCompDisc.{0, 1} Type) : FamGr := CoGrothendieck.mk F.1 F.2

An object of the construction as a family.

def ofGr (A : FamGr) : FreeCoprodCompDisc.{0, 1} Type := ⟨A.base, A.fiber⟩

The objects of the construction are the families.

def objGrEquiv : FreeCoprodCompDisc.{0, 1} Type ≃ FamGr where toFun := toGr invFun := ofGr left_inv _ := rfl right_inv _ := rfl

The morphisms of the construction are the morphisms of families: a base map with a fibre morphism into the precomposed family.

def homGrEquiv (F G : FreeCoprodCompDisc.{0, 1} Type) : FamHom F G ≃ (toGr F ⟶ toGr G) where toFun φ := CoGrothendieck.homMk (↾ φ.1) fun u ↦ ↾ φ.2 u invFun f := ⟨⇑(CoGrothendieck.homBase f), fun u ↦ ⇑(CoGrothendieck.homFiber f u)⟩ left_inv _ := rfl right_inv _ := rfl

The code as an endofunctor

variable {X Y : Type} (P : SlicePFunctor.{0, 0, 0, 0} X Y)

The interpretation of the code as an endofunctor of Fam(Type): IndRec.­IR.­interpObj on objects and GebProto.­LargeIR.­codeMap on morphisms.

def codeFunctor : FamGr ⥤ FamGr where obj A := toGr (IR.interpObj Type Type (code P) (ofGr A)) map f := homGrEquiv _ _ (codeMap P ((homGrEquiv _ _).symm f)) map_id _ := rfl map_comp _ _ := rfl
end GebProto.LargeIR