Geb.Mathlib.Data.PFunctor.IndRec.Universes

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

Universes closed under dependent sums and products, as IR codes

The code of the universe generated by an arbitrary family of starting types and closed under dependent sums and dependent products, combining Examples 2.5 and 2.6 of [GhaniNordvallForsbergMalatesta2015]: the coproduct of one iota code per starting type (in place of the examples' single iota code for the natural numbers), one dependent-sum former, and one dependent-product former. The universe is an endofunctor example (IR I I), so the input and output index types coincide.

Main definitions

univCode, univEndo, univEndoMor — the code of the universe generated by an arbitrary family of starting types and closed under dependent sums and dependent products, with the object and morphism maps of its interpretation.

univBinder, univSigma, univPi, univIota, UnivConstructor, univConstructorCode — the constructor subcodes: the binder-former subcode shared by the dependent-sum and dependent-product formers, the starting-type subcodes, and the constructor index assembling them.

References

[GhaniNordvallForsbergMalatesta2015]

Tags

inductive-recursive, universe

              @[expose] public sectionuniverse uK uTnamespace IndRecopen CategoryTheory

The binder-former subcode shared by univSigma and univPi: one recursive argument (the type bound by the binder), then recursive arguments indexed by its decoding (the family of types under the binder), decoding to former applied to the decodings.

def univBinder.{v} (former : (X : Type v) → (X → Type v) → Type v) :
    IR.{v, v, v + 1, v + 1} (Type v) (Type v) :=
  IR.delta (Type v) (Type v) PUnit.{v + 1} (fun f ↦
    IR.delta (Type v) (Type v) (f PUnit.unit) (fun q ↦
      IR.iota (Type v) (Type v) (former (f PUnit.unit) q)))

The dependent-sum-former subcode of a universe code.

def univSigma.{v} : IR.{v, v, v + 1, v + 1} (Type v) (Type v) :=
  univBinder (fun X q ↦ Σ x : X, q x)

The dependent-product-former subcode of a universe code.

def univPi.{v} : IR.{v, v, v + 1, v + 1} (Type v) (Type v) :=
  univBinder (fun X q ↦ Π x : X, q x)

variable (K : Type uK) (T : K → Type uT)

The starting-type subcode of a universe code: an iota code decoding to the lifted starting type selected by k.

def univIota (k : K) :
    IR.{max uK uT, max uK uT, max uK uT + 1, max uK uT + 1}
      (Type (max uK uT)) (Type (max uK uT)) :=
  IR.iota (Type (max uK uT)) (Type (max uK uT)) (ULift.{uK} (T k))

The constructors of the universe generated by a family of starting types: one nullary constructor per starting type, a dependent-sum former, and a dependent-product former.

def UnivConstructor : Type (max uK uT) :=
  K ⊕ PUnit.{max uK uT + 1} ⊕ PUnit.{max uK uT + 1}

The subcode of the universe code selected by each constructor.

def univConstructorCode :
    UnivConstructor.{uK, uT} K →
      IR.{max uK uT, max uK uT, max uK uT + 1, max uK uT + 1}
        (Type (max uK uT)) (Type (max uK uT)) :=
  Sum.elim (univIota K T)
    (Sum.elim (fun _ ↦ univSigma.{max uK uT}) (fun _ ↦ univPi.{max uK uT}))

The code of the universe generated by the starting types T: the coproduct, over UnivConstructor, of the subcodes. The universe itself — containing the (lifted) starting types and closed under dependent sums and dependent products — is the initial algebra of the code's interpretation; this file provides the code and the interpretation, not the initial algebra.

def univCode :
    IR.{max uK uT, max uK uT, max uK uT + 1, max uK uT + 1}
      (Type (max uK uT)) (Type (max uK uT)) :=
  IR.sigma (Type (max uK uT)) (Type (max uK uT)) (UnivConstructor.{uK, uT} K)
    (univConstructorCode K T)

The object map of the interpretation of univCode.

def univEndo :
    FreeCoprodCompDisc.Endo.{max uK uT, max uK uT + 1} (Type (max uK uT)) :=
  IR.interpObj (Type (max uK uT)) (Type (max uK uT)) (univCode K T)

The morphism map of the interpretation of univCode (the object map is univEndo).

def univEndoMor :
    FreeCoprodCompDisc.EndoMor (Type (max uK uT)) (univEndo K T) :=
  IR.interpMor (Type (max uK uT)) (Type (max uK uT)) (univCode K T)

end IndRec