Here we construct universes for the groupoid natural model.

def GroupoidModel.base : NaturalModelBase Ctx

The natural model that acts as the ambient model in which the other universes live. Note that unlike the other universes this is not representable, but enjoys having representable fibers that land in itself.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem GroupoidModel.base_Tm : base.Tm = Tm

@[simp]

theorem GroupoidModel.base_Ty : base.Ty = Ty

@[simp]

theorem GroupoidModel.base_tp : base.tp = tp

@[simp]

theorem GroupoidModel.base_disp {Γ✝ : Ctx} (A : CategoryTheory.yoneda.obj Γ✝ ⟶ Ty) : base.disp A = disp A

@[simp]

theorem GroupoidModel.base_ext {Γ✝ : Ctx} (A : CategoryTheory.yoneda.obj Γ✝ ⟶ Ty) : base.ext A = ext A

@[simp]

theorem GroupoidModel.base_var {Γ✝ : Ctx} (A : CategoryTheory.yoneda.obj Γ✝ ⟶ Ty) : base.var A = var A

def GroupoidModel.smallU : NaturalModelBase Ctx

The natural model that acts as the classifier of v-large terms and types. Note that unlike GroupoidNaturalModel.base this is representable, but since representables are max u (v+1)-large, its representable fibers can be larger than itself.

Equations

• One or more equations did not get rendered due to their size.

def GroupoidModel.U.asSmallClosedType' : 𝟙_ Ctx ⟶ U

Equations

• One or more equations did not get rendered due to their size.

def GroupoidModel.U.asSmallClosedType : CategoryTheory.yoneda.obj (𝟙_ Ctx) ⟶ smallU.Ty

Equations

• GroupoidModel.U.asSmallClosedType = CategoryTheory.yoneda.map GroupoidModel.U.asSmallClosedType'

def GroupoidModel.U.isoGrpd : CategoryTheory.Functor (CategoryTheory.Core (CategoryTheory.AsSmall CategoryTheory.Grpd)) CategoryTheory.Grpd

Equations

• GroupoidModel.U.isoGrpd = (CategoryTheory.Core.inclusion (CategoryTheory.AsSmall CategoryTheory.Grpd)).comp CategoryTheory.AsSmall.down

def GroupoidModel.U.isoExtAsSmallClosedTypeHom : CategoryTheory.Functor (CategoryTheory.Core (CategoryTheory.AsSmall CategoryTheory.Grpd)) (CategoryTheory.Grothendieck.Groupoidal (classifier asSmallClosedType'))

Equations

• One or more equations did not get rendered due to their size.

def GroupoidModel.U.isoExtAsSmallClosedTypeInv : CategoryTheory.Functor (CategoryTheory.Grothendieck.Groupoidal (classifier asSmallClosedType')) (CategoryTheory.Core (CategoryTheory.AsSmall CategoryTheory.Grpd))

Equations

• One or more equations did not get rendered due to their size.

def GroupoidModel.U.isoExtAsSmallClosedType : U ≅ smallU.ext asSmallClosedType

Equations

• One or more equations did not get rendered due to their size.

def GroupoidModel.U.asClosedType : CategoryTheory.yoneda.obj (𝟙_ Ctx) ⟶ base.Ty

Equations

• One or more equations did not get rendered due to their size.

def GroupoidModel.U.isoExtAsClosedTypeFun : CategoryTheory.Functor (CategoryTheory.Core (CategoryTheory.AsSmall CategoryTheory.Grpd)) (CategoryTheory.Grothendieck.Groupoidal (yonedaCatEquiv asClosedType))

Equations

• One or more equations did not get rendered due to their size.

def GroupoidModel.U.isoExtAsClosedTypeInv : CategoryTheory.Functor (CategoryTheory.Grothendieck.Groupoidal (yonedaCatEquiv asClosedType)) (CategoryTheory.Core (CategoryTheory.AsSmall CategoryTheory.Grpd))

Equations

• One or more equations did not get rendered due to their size.

def GroupoidModel.U.isoExtAsClosedType : U ≅ base.ext asClosedType

Equations

• One or more equations did not get rendered due to their size.

def GroupoidModel.largeUHom : smallU.UHom base

Equations

• One or more equations did not get rendered due to their size.

def GroupoidModel.uHomSeqObjs (i : ℕ) (h : i < 4) : NaturalModelBase Ctx

Equations

• GroupoidModel.uHomSeqObjs 0 h_2 = GroupoidModel.smallU
• GroupoidModel.uHomSeqObjs 1 h_2 = GroupoidModel.smallU
• GroupoidModel.uHomSeqObjs 2 h_2 = GroupoidModel.smallU
• GroupoidModel.uHomSeqObjs 3 h_2 = GroupoidModel.base
• GroupoidModel.uHomSeqObjs n.succ.succ.succ.succ h_2 = ⋯.elim

def GroupoidModel.smallUHom : smallU.UHom smallU

Equations

• One or more equations did not get rendered due to their size.

def GroupoidModel.uHomSeqHomSucc' (i : ℕ) (h : i < 3) : (uHomSeqObjs i ⋯).UHom (uHomSeqObjs (i + 1) ⋯)

Equations

• GroupoidModel.uHomSeqHomSucc' 0 h_2 = GroupoidModel.smallUHom
• GroupoidModel.uHomSeqHomSucc' 1 h_2 = GroupoidModel.smallUHom
• GroupoidModel.uHomSeqHomSucc' 2 h_2 = GroupoidModel.largeUHom
• GroupoidModel.uHomSeqHomSucc' n.succ.succ.succ h_2 = ⋯.elim

def GroupoidModel.uHomSeq : NaturalModelBase.UHomSeq Ctx

The groupoid natural model with three nested representable universes within the ambient natural model.

Equations

• GroupoidModel.uHomSeq = { length := 3, objs := GroupoidModel.uHomSeqObjs, homSucc' := GroupoidModel.uHomSeqHomSucc' }

def GroupoidModel.baseUvPolyTpEquiv {Γ : Ctx} {C : CategoryTheory.Cat} : (base.Ptp.obj (yonedaCat.obj C)).obj (Opposite.op Γ) ≃ (A : CategoryTheory.Functor (↑(Ctx.toGrpd.obj Γ)) CategoryTheory.Grpd) × CategoryTheory.Functor (CategoryTheory.Grothendieck.Groupoidal A) ↑C

A specialization of the polynomial universal property to the natural model base The polynomial functor on tp taken at yonedaCat.obj C P_tp(yonedaCat C) takes a groupoid Γ to a pair of functors A and B

  B

C ⇇ Groupoidal A ⥤ PGrpd ⇊ ⇊ Γ ⥤ Grpd A As a special case, if C is taken to be Grpd, then this is how P_tp(Ty) classifies dependent pairs.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem GroupoidModel.base_sec {Γ : Ctx} (α : CategoryTheory.yoneda.obj Γ ⟶ base.Tm) : base.sec α = CategoryTheory.yoneda.map (Ctx.ofGrpd.map (CategoryTheory.Grothendieck.Groupoidal.sec (yonedaCatEquiv α)))

def GroupoidModel.baseUvPolyTpCompDomEquiv {Γ : Ctx} : (base.uvPolyTp.compDom base.uvPolyTp).obj (Opposite.op Γ) ≃ (α : CategoryTheory.Functor (↑(Ctx.toGrpd.obj Γ)) CategoryTheory.PGrpd) × (B : CategoryTheory.Functor (CategoryTheory.Grothendieck.Groupoidal (α.comp CategoryTheory.PGrpd.forgetToGrpd)) CategoryTheory.Grpd) × (β : CategoryTheory.Functor (↑(Ctx.toGrpd.obj Γ)) CategoryTheory.PGrpd) ×' β.comp CategoryTheory.PGrpd.forgetToGrpd = (CategoryTheory.Grothendieck.Groupoidal.sec α).comp B

A specialization of the universal property of UvPoly.compDom to the natural model base. This consists of a pair of dependent types A = α ⋙ forgetToGrpd and B, a : A captured by α, and b : B[a / x] = β ⋙ forgetToGrpd caputred by β.

Equations

• One or more equations did not get rendered due to their size.