Here we construct universes for the groupoid natural model.

@[reducible, inline]

abbrev GroupoidModel.Ctx : Type (u + 1)

Ctx is the category of {small groupoids - size u objects and size u hom sets} which itself has size u+1 objects (small groupoids) and size u hom sets (functors).

We want our context category to be a small category so we will use AsSmall.{u} for some large enough u

Equations

• GroupoidModel.Ctx = CategoryTheory.AsSmall CategoryTheory.Grpd

def GroupoidModel.Ctx.equivalence : CategoryTheory.Grpd ≌ Ctx

Equations

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

@[simp]

theorem GroupoidModel.Ctx.equivalence_functor : equivalence.functor = CategoryTheory.AsSmall.up

@[simp]

theorem GroupoidModel.Ctx.equivalence_unitIso : equivalence.unitIso = CategoryTheory.eqToIso equivalence.proof_1

@[simp]

theorem GroupoidModel.Ctx.equivalence_counitIso : equivalence.counitIso = CategoryTheory.eqToIso equivalence.proof_2

@[simp]

theorem GroupoidModel.Ctx.equivalence_inverse : equivalence.inverse = CategoryTheory.AsSmall.down

@[reducible, inline]

abbrev GroupoidModel.Ctx.ofGrpd : CategoryTheory.Functor CategoryTheory.Grpd Ctx

Equations

• GroupoidModel.Ctx.ofGrpd = GroupoidModel.Ctx.equivalence.functor

@[reducible, inline]

abbrev GroupoidModel.Ctx.toGrpd : CategoryTheory.Functor Ctx CategoryTheory.Grpd

Equations

• GroupoidModel.Ctx.toGrpd = GroupoidModel.Ctx.equivalence.inverse

def GroupoidModel.Ctx.ofGroupoid (Γ : Type u) [CategoryTheory.Groupoid Γ] : Ctx

Equations

• GroupoidModel.Ctx.ofGroupoid Γ = GroupoidModel.Ctx.ofGrpd.obj (CategoryTheory.Grpd.of Γ)

instance GroupoidModel.Ctx.instChosenFiniteProducts : CategoryTheory.ChosenFiniteProducts Ctx

Equations

• GroupoidModel.Ctx.instChosenFiniteProducts = GroupoidModel.Ctx.equivalence.chosenFiniteProducts

def GroupoidModel.catLift : CategoryTheory.Functor CategoryTheory.Cat CategoryTheory.Cat

Equations

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

@[simp]

theorem GroupoidModel.catLift_obj (x : CategoryTheory.Cat) : catLift.obj x = CategoryTheory.Cat.of (ULift.{u + 1, u} ↑x)

@[simp]

theorem GroupoidModel.catLift_map {x y : CategoryTheory.Cat} (f : x ⟶ y) : catLift.map f = CategoryTheory.ULift.downFunctor.comp (CategoryTheory.Functor.comp f CategoryTheory.ULift.upFunctor)

@[reducible, inline]

abbrev GroupoidModel.yonedaCat : CategoryTheory.Functor CategoryTheory.Cat (CategoryTheory.Functor Ctxᵒᵖ (Type (u + 1)))

yonedaCat is the following composition

Cat --- yoneda ---> Psh Cat -- restrict along inclusion --> Psh Ctx

where Ctx --- inclusion ---> Cat takes a groupoid and forgets it to a category (with appropriate universe level adjustments)

Equations

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

instance GroupoidModel.yonedaCatPreservesLimits : CategoryTheory.Limits.PreservesLimits yonedaCat

def GroupoidModel.yonedaCatEquiv {Γ : Ctx} {C : CategoryTheory.Cat} : (CategoryTheory.yoneda.obj Γ ⟶ yonedaCat.obj C) ≃ CategoryTheory.Functor ↑(Ctx.toGrpd.obj Γ) ↑C

Equations

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

theorem GroupoidModel.yonedaCatEquiv_yonedaEquivSymm {C : CategoryTheory.Cat} {Γ : Ctx} (A : (yonedaCat.obj C).obj (Opposite.op Γ)) : yonedaCatEquiv (CategoryTheory.yonedaEquiv.symm A) = CategoryTheory.ULift.upFunctor.comp A

theorem GroupoidModel.yonedaCatEquiv_naturality_left {Γ Δ : Ctx} {C : CategoryTheory.Cat} (A : CategoryTheory.yoneda.obj Γ ⟶ yonedaCat.obj C) (σ : Δ ⟶ Γ) : yonedaCatEquiv (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) A) = CategoryTheory.Functor.comp (Ctx.toGrpd.map σ) (yonedaCatEquiv A)

theorem GroupoidModel.yonedaCatEquiv_naturality_right {Γ : Ctx} {C D : CategoryTheory.Cat} (A : CategoryTheory.yoneda.obj Γ ⟶ yonedaCat.obj D) (U : CategoryTheory.Functor ↑D ↑C) : yonedaCatEquiv (CategoryTheory.CategoryStruct.comp A (yonedaCat.map U)) = (yonedaCatEquiv A).comp U

theorem GroupoidModel.yonedaCatEquiv_symm_naturality_left {Γ Δ : Ctx} {C : CategoryTheory.Cat} (A : CategoryTheory.Functor ↑(Ctx.toGrpd.obj Γ) ↑C) (σ : Δ ⟶ Γ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) (yonedaCatEquiv.symm A) = yonedaCatEquiv.symm (CategoryTheory.Functor.comp (Ctx.toGrpd.map σ) A)

theorem GroupoidModel.yonedaCatEquiv_symm_naturality_right {Γ : Ctx} {C D : CategoryTheory.Cat} (A : CategoryTheory.Functor ↑(Ctx.toGrpd.obj Γ) ↑D) (U : CategoryTheory.Functor ↑D ↑C) : yonedaCatEquiv.symm (A.comp U) = CategoryTheory.CategoryStruct.comp (yonedaCatEquiv.symm A) (yonedaCat.map U)

def GroupoidModel.Ctx.homGrpdEquivFunctor {Γ : Ctx} {G : Type v} [CategoryTheory.Groupoid G] : (Γ ⟶ ofGrpd.obj (CategoryTheory.Grpd.of G)) ≃ CategoryTheory.Functor (↑(toGrpd.obj Γ)) G

Equations

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

def GroupoidModel.toCoreAsSmallEquiv {Γ : Ctx} {C : Type (v + 1)} [CategoryTheory.Category.{v, v + 1} C] : (Γ ⟶ Ctx.ofGrpd.obj (CategoryTheory.Grpd.of (CategoryTheory.Core (CategoryTheory.AsSmall C)))) ≃ CategoryTheory.Functor (↑(Ctx.toGrpd.obj Γ)) C

Equations

• GroupoidModel.toCoreAsSmallEquiv = GroupoidModel.Ctx.homGrpdEquivFunctor.trans (CategoryTheory.Core.functorToCoreEquiv.symm.trans CategoryTheory.functorToAsSmallEquiv)

def GroupoidModel.asSmallUp_comp_yoneda_iso_forgetToCat_comp_catLift_comp_yonedaCat : CategoryTheory.AsSmall.up.comp CategoryTheory.yoneda ≅ CategoryTheory.Grpd.forgetToCat.comp (catLift.comp yonedaCat)

This is a natural isomorphism between functors in the following diagram Ctx.{u}------ yoneda -----> Psh Ctx | Λ | | | | inclusion precomposition with inclusion | | | | | | V | Cat.{big univ}-- yoneda -----> Psh Cat

Equations

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

@[reducible, inline]

abbrev GroupoidModel.Ty : CategoryTheory.Psh Ctx

Equations

• GroupoidModel.Ty = GroupoidModel.yonedaCat.obj (CategoryTheory.Cat.of CategoryTheory.Grpd)

@[reducible, inline]

abbrev GroupoidModel.Tm : CategoryTheory.Psh Ctx

Equations

• GroupoidModel.Tm = GroupoidModel.yonedaCat.obj (CategoryTheory.Cat.of CategoryTheory.PGrpd)

@[reducible, inline]

abbrev GroupoidModel.tp : Tm ⟶ Ty

Equations

• GroupoidModel.tp = GroupoidModel.yonedaCat.map CategoryTheory.PGrpd.forgetToGrpd

@[reducible, inline]

abbrev GroupoidModel.ext {Γ : Ctx} (A : CategoryTheory.yoneda.obj Γ ⟶ Ty) : Ctx

Equations

• GroupoidModel.ext A = GroupoidModel.Ctx.ofGrpd.obj (CategoryTheory.Grpd.of (CategoryTheory.Grothendieck.Groupoidal (GroupoidModel.yonedaCatEquiv A)))

@[reducible, inline]

abbrev GroupoidModel.disp {Γ : Ctx} (A : CategoryTheory.yoneda.obj Γ ⟶ Ty) : ext A ⟶ Γ

Equations

• GroupoidModel.disp A = GroupoidModel.Ctx.ofGrpd.map (CategoryTheory.Grothendieck.forget (CategoryTheory.Groupoid.compForgetToCat (GroupoidModel.yonedaCatEquiv A)))

@[reducible, inline]

abbrev GroupoidModel.var {Γ : Ctx} (A : CategoryTheory.yoneda.obj Γ ⟶ Ty) : CategoryTheory.yoneda.obj (ext A) ⟶ Tm

Equations

• GroupoidModel.var A = GroupoidModel.yonedaCatEquiv.symm (CategoryTheory.Grothendieck.Groupoidal.toPGrpd (GroupoidModel.yonedaCatEquiv A))

def GroupoidModel.U' : CategoryTheory.Grpd

Equations

• GroupoidModel.U' = CategoryTheory.Grpd.of (CategoryTheory.Core (CategoryTheory.AsSmall CategoryTheory.Grpd))

def GroupoidModel.U : Ctx

U.{v} is the object representing the universe of v-small types i.e. y(U) = Ty for the small natural models baseU.

Equations

• GroupoidModel.U = GroupoidModel.Ctx.ofGrpd.obj GroupoidModel.U'

def GroupoidModel.E' : CategoryTheory.Grpd

Equations

• GroupoidModel.E' = CategoryTheory.Grpd.of (CategoryTheory.Core (CategoryTheory.AsSmall CategoryTheory.PGrpd))

def GroupoidModel.E : Ctx

E.{v} is the object representing v-small terms, living over U.{v} i.e. y(E) = Tm for the small natural models baseU.

Equations

• GroupoidModel.E = GroupoidModel.Ctx.ofGrpd.obj GroupoidModel.E'

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

Equations

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

@[reducible, inline]

abbrev GroupoidModel.π' : E' ⟶ U'

Equations

• GroupoidModel.π' = CategoryTheory.Grpd.homOf (CategoryTheory.Core.map' GroupoidModel.π'')

theorem GroupoidModel.π'_eq : CategoryTheory.Grpd.homOf (CategoryTheory.Core.map' π'') = CategoryTheory.Core.map.map (CategoryTheory.Cat.asSmallFunctor.map (CategoryTheory.Cat.homOf CategoryTheory.PGrpd.forgetToGrpd))

@[reducible, inline]

abbrev GroupoidModel.π : E ⟶ U

π.{v} is the morphism representing v-small tp, for the small natural models baseU.

Equations

• GroupoidModel.π = GroupoidModel.Ctx.ofGrpd.map GroupoidModel.π'

def GroupoidModel.U.classifier {Γ : Ctx} (A : Γ ⟶ U) : CategoryTheory.Functor (↑(Ctx.toGrpd.obj Γ)) CategoryTheory.Grpd

Equations

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

@[reducible, inline]

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

Equations

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

@[reducible, inline]

abbrev GroupoidModel.U.ext {Γ : Ctx} (A : Γ ⟶ U) : Ctx

Equations

• GroupoidModel.U.ext A = GroupoidModel.Ctx.ofGrpd.obj (GroupoidModel.U.ext' A)

@[reducible, inline]

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

Equations

• GroupoidModel.U.disp' A = CategoryTheory.Grothendieck.forget (CategoryTheory.Groupoid.compForgetToCat (GroupoidModel.U.classifier A))

@[reducible, inline]

abbrev GroupoidModel.U.disp {Γ : Ctx} (A : Γ ⟶ U) : ext A ⟶ Γ

Equations

• GroupoidModel.U.disp A = CategoryTheory.AsSmall.up.map (CategoryTheory.Grothendieck.forget (CategoryTheory.Groupoid.compForgetToCat (GroupoidModel.U.classifier A)))

@[reducible, inline]

abbrev GroupoidModel.U.var' {Γ : Ctx} (A : Γ ⟶ U) : ext' A ⟶ E'

Equations

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

@[reducible, inline]

abbrev GroupoidModel.U.var {Γ : Ctx} (A : Γ ⟶ U) : ext A ⟶ E

Equations

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