Here we construct universes for the groupoid natural model.

def GroupoidModel.IsPullback.SmallUHom.toU'' : CategoryTheory.Functor (CategoryTheory.AsSmall CategoryTheory.Grpd) (CategoryTheory.AsSmall CategoryTheory.Grpd)

Equations

• GroupoidModel.IsPullback.SmallUHom.toU'' = CategoryTheory.AsSmall.down.comp (CategoryTheory.Grpd.asSmallFunctor.comp CategoryTheory.AsSmall.up)

def GroupoidModel.IsPullback.SmallUHom.toE'' : CategoryTheory.Functor (CategoryTheory.AsSmall CategoryTheory.PGrpd) (CategoryTheory.AsSmall CategoryTheory.PGrpd)

Equations

• GroupoidModel.IsPullback.SmallUHom.toE'' = CategoryTheory.AsSmall.down.comp (CategoryTheory.PGrpd.asSmallFunctor.comp CategoryTheory.AsSmall.up)

def GroupoidModel.IsPullback.SmallUHom.π'' : CategoryTheory.Functor (CategoryTheory.AsSmall CategoryTheory.PGrpd) (CategoryTheory.AsSmall CategoryTheory.Grpd)

Equations

• GroupoidModel.IsPullback.SmallUHom.π'' = CategoryTheory.AsSmall.down.comp (CategoryTheory.PGrpd.forgetToGrpd.comp CategoryTheory.AsSmall.up)

theorem GroupoidModel.IsPullback.SmallUHom.toE''_π'' : CategoryTheory.CategoryStruct.comp (CategoryTheory.Cat.homOf toE'') (CategoryTheory.Cat.homOf π'') = CategoryTheory.CategoryStruct.comp (CategoryTheory.Cat.homOf π'') (CategoryTheory.Cat.homOf toU'')

def GroupoidModel.IsPullback.SmallUHom.isPullback_forgetToGrpd_forgetToGrpd : CategoryTheory.PGrpd.asSmallFunctor.IsPullback CategoryTheory.PGrpd.forgetToGrpd CategoryTheory.PGrpd.forgetToGrpd CategoryTheory.Grpd.asSmallFunctor

The following square is a meta-theoretic pullback

PGrpd.{v} ------- asSmallFunctor ------> PGrpd.{v+1} | | | | forgetToGrpd forgetToGrpd | | | | v v Grpd.{v} ------- asSmallFunctor -----> Grpd.{v+1}

Equations

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

theorem GroupoidModel.IsPullback.SmallUHom.isPullback_π''_π'' : CategoryTheory.IsPullback (CategoryTheory.Cat.homOf toE'') (CategoryTheory.Cat.homOf π'') (CategoryTheory.Cat.homOf π'') (CategoryTheory.Cat.homOf toU'')

The following square is a pullback

AsSmall PGrpd.{v} ------- toE'' ------> AsSmall PGrpd.{v+1} | | | | π'' π'' | | | | v v AsSmall Grpd.{v} ------- toU'' -----> AsSmall Grpd.{v+1}

in the category Cat.{max u (v+2), max u (v+2)}. Note that these AsSmalls are bringing two different sized categories into the same category.

theorem GroupoidModel.IsPullback.SmallUHom.isPullback_yπ_yπ : CategoryTheory.IsPullback (CategoryTheory.yoneda.map U.toE) (CategoryTheory.yoneda.map π) (CategoryTheory.yoneda.map π) (CategoryTheory.yoneda.map U.toU)

The small universes form pullbacks y(E.{v}) ------------ toE ---------> y(E.{v+1}) | | | | y(π.{v}) y(π.{v+1}) | | v v y(U.{v}) ------------ toU ---------> y(U.{v+1})

@[reducible, inline]

abbrev GroupoidModel.IsPullback.SmallU.coreΓ (Γ : Ctx) : CategoryTheory.Grpd

Equations

• GroupoidModel.IsPullback.SmallU.coreΓ Γ = CategoryTheory.Core.map.obj (CategoryTheory.Cat.of ↑(GroupoidModel.Ctx.toGrpd.obj Γ))

@[reducible, inline]

abbrev GroupoidModel.IsPullback.SmallU.ext' {Γ : Ctx} (A : Γ ⟶ U) : CategoryTheory.Grpd

Equations

• GroupoidModel.IsPullback.SmallU.ext' A = CategoryTheory.Grpd.of (GroupoidModel.U.classifier A).Groupoidal

@[reducible, inline]

abbrev GroupoidModel.IsPullback.SmallU.disp' {Γ : Ctx} (A : Γ ⟶ U) : ext' A ⟶ Ctx.toGrpd.obj Γ

Equations

• GroupoidModel.IsPullback.SmallU.disp' A = CategoryTheory.Functor.Groupoidal.forget

@[reducible, inline]

abbrev GroupoidModel.IsPullback.SmallU.coreExt' {Γ : Ctx} (A : Γ ⟶ U) : CategoryTheory.Grpd

Equations

• GroupoidModel.IsPullback.SmallU.coreExt' A = CategoryTheory.Core.map.obj (CategoryTheory.Cat.of (GroupoidModel.U.classifier A).Groupoidal)

@[reducible, inline]

abbrev GroupoidModel.IsPullback.SmallU.coreDisp' {Γ : Ctx} (A : Γ ⟶ U) : coreExt' A ⟶ coreΓ Γ

Equations

• GroupoidModel.IsPullback.SmallU.coreDisp' A = CategoryTheory.Core.map.map (CategoryTheory.Cat.homOf CategoryTheory.Functor.Groupoidal.forget)

@[reducible, inline]

abbrev GroupoidModel.IsPullback.SmallU.coreVar' {Γ : Ctx} (A : Γ ⟶ U) : coreExt' A ⟶ CategoryTheory.Core.map.obj (CategoryTheory.Cat.asSmallFunctor.obj (CategoryTheory.Cat.of CategoryTheory.PGrpd))

Equations

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

@[reducible, inline]

abbrev GroupoidModel.IsPullback.SmallU.coreA {Γ : Ctx} (A : Γ ⟶ U) : coreΓ Γ ⟶ CategoryTheory.Core.map.obj (CategoryTheory.Cat.asSmallFunctor.obj (CategoryTheory.Cat.of CategoryTheory.Grpd))

Equations

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

def GroupoidModel.IsPullback.SmallU.isPullback_disp'_asSmallForgetToGrpd_comm_sq {Γ : Ctx} (A : Γ ⟶ U) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Cat.homOf ((CategoryTheory.Functor.Groupoidal.toPGrpd (U.classifier A)).comp CategoryTheory.AsSmall.up)) (CategoryTheory.Cat.homOf (CategoryTheory.Cat.asSmallFunctor.map (CategoryTheory.Cat.homOf CategoryTheory.PGrpd.forgetToGrpd))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Cat.homOf (CategoryTheory.Functor.Grothendieck.forget ((U.classifier A).comp CategoryTheory.Grpd.forgetToCat))) (CategoryTheory.Cat.homOf (CategoryTheory.Functor.comp (Ctx.toGrpd.map A) (CategoryTheory.Core.inclusion (CategoryTheory.AsSmall CategoryTheory.Grpd))))

Equations

• ⋯ = ⋯

theorem GroupoidModel.IsPullback.SmallU.isPullback_disp'_asSmallForgetToGrpd {Γ : Ctx} (A : Γ ⟶ U) : CategoryTheory.IsPullback (CategoryTheory.Cat.homOf ((CategoryTheory.Functor.Groupoidal.toPGrpd (U.classifier A)).comp CategoryTheory.AsSmall.up)) (CategoryTheory.Cat.homOf (CategoryTheory.Functor.Grothendieck.forget ((U.classifier A).comp CategoryTheory.Grpd.forgetToCat))) (CategoryTheory.Cat.homOf (CategoryTheory.AsSmall.down.comp (CategoryTheory.PGrpd.forgetToGrpd.comp CategoryTheory.AsSmall.up))) (CategoryTheory.Cat.homOf (CategoryTheory.Functor.comp (Ctx.toGrpd.map A) (CategoryTheory.Core.inclusion (CategoryTheory.AsSmall CategoryTheory.Grpd))))

theorem GroupoidModel.IsPullback.SmallU.isPullback_coreDisp'_π' {Γ : Ctx} (A : Γ ⟶ U) : CategoryTheory.IsPullback (coreVar' A) (coreDisp' A) (CategoryTheory.Grpd.homOf SmallUHom.π''.core) (coreA A)

The following square is a pullback in Grpd Core(U.ext' A) -- U.coreVar' A ---> U' | | | | | | | | Core(U.disp' A) π' | | | | V V Core(Ctx.toGrpd.obj Γ) - coreA A -> E'

theorem GroupoidModel.IsPullback.SmallU.isPullback_disp'_coreDisp' {Γ : Ctx} (A : Γ ⟶ U) : CategoryTheory.IsPullback (CategoryTheory.Grpd.homOf (CategoryTheory.Core.functorToCore (CategoryTheory.Functor.id (U.classifier A).Groupoidal))) (disp' A) (coreDisp' A) (CategoryTheory.Grpd.homOf (CategoryTheory.Core.functorToCore (CategoryTheory.Functor.id ↑Γ.1)))

The following square is a pullback in Grpd U.ext' A ------- functorToCore ---> Core(U.ext' A) | | | | | | π' Core(U.disp' A) | | | | V V Ctx.toGrpd.obj Γ - functorToCore -> Core(Ctx.toGrpd.obj Γ)

theorem GroupoidModel.IsPullback.SmallU.isPullback_disp'_π' {Γ : Ctx} (A : Γ ⟶ U) : CategoryTheory.IsPullback (CategoryTheory.Grpd.homOf (CategoryTheory.Core.functorToCore ((CategoryTheory.Functor.Groupoidal.toPGrpd (U.classifier A)).comp CategoryTheory.AsSmall.up))) (disp' A) (CategoryTheory.Grpd.homOf SmallUHom.π''.core) (Ctx.toGrpd.map A)

The following square is a pullback in Grpd U.ext' A -- U.var' A ---> U' | | | | | | U.disp' A π' | | | | V V Ctx.toGrpd.obj Γ ---------> E' Ctx.toGrpd.map A

theorem GroupoidModel.IsPullback.SmallU.isPullback_disp_π {Γ : Ctx} (A : Γ ⟶ U) : CategoryTheory.IsPullback (U.var A) (U.disp A) π A

The following square is a pullback in Ctx U.ext A --- U.var A ---> E | | | | | | U.disp A π | | | | V V Γ --------- A ------> U

theorem GroupoidModel.IsPullback.SmallU.isPullback_yonedaDisp_yonedaπ {Γ : Ctx} (A : Γ ⟶ U) : CategoryTheory.IsPullback (CategoryTheory.yoneda.map (U.var A)) (CategoryTheory.yoneda.map (U.disp A)) (CategoryTheory.yoneda.map π) (CategoryTheory.yoneda.map A)

The following square is a pullback in Psh Ctx y(U.ext A) --- ym(U.var A) ---> y(E) | | | | | | ym(U.disp A) ym(π) | | | | V V y(Γ) ------------- ym(A) ----> y(U)