Here we construct universes for the groupoid natural model.

def CategoryTheory.PGrpd.pGrpdToGroupoidalAsSmallFunctor : Functor PGrpd Grpd.asSmallFunctor.Groupoidal

Equations

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

def CategoryTheory.PGrpd.groupoidalAsSmallFunctorToPGrpd : Functor Grpd.asSmallFunctor.Groupoidal PGrpd

Equations

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

@[simp]

def CategoryTheory.PGrpd.pGrpdToGroupoidalAsSmallFunctor_groupoidalAsSmallFunctorToPGrpd : groupoidalAsSmallFunctorToPGrpd.comp pGrpdToGroupoidalAsSmallFunctor = Functor.id Grpd.asSmallFunctor.Groupoidal

Equations

• CategoryTheory.PGrpd.pGrpdToGroupoidalAsSmallFunctor_groupoidalAsSmallFunctorToPGrpd = ⋯

@[simp]

def CategoryTheory.PGrpd.groupoidalAsSmallFunctorToPGrpd_pGrpdToGroupoidalAsSmallFunctor : pGrpdToGroupoidalAsSmallFunctor.comp groupoidalAsSmallFunctorToPGrpd = Functor.id PGrpd

Equations

• CategoryTheory.PGrpd.groupoidalAsSmallFunctorToPGrpd_pGrpdToGroupoidalAsSmallFunctor = ⋯

@[simp]

def CategoryTheory.PGrpd.pGrpdToGroupoidalAsSmallFunctor_forget : pGrpdToGroupoidalAsSmallFunctor.comp Functor.Groupoidal.forget = forgetToGrpd

Equations

• CategoryTheory.PGrpd.pGrpdToGroupoidalAsSmallFunctor_forget = ⋯

def CategoryTheory.PGrpd.asSmallFunctor : Functor PGrpd PGrpd

Equations

• CategoryTheory.PGrpd.asSmallFunctor = CategoryTheory.PGrpd.pGrpdToGroupoidalAsSmallFunctor.comp (CategoryTheory.Functor.Groupoidal.toPGrpd CategoryTheory.Grpd.asSmallFunctor)

def 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

instance GroupoidModel.instSmallCategoryCtx : CategoryTheory.SmallCategory Ctx

Equations

• GroupoidModel.instSmallCategoryCtx = inferInstanceAs (CategoryTheory.SmallCategory (CategoryTheory.AsSmall CategoryTheory.Grpd))

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

Equations

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

@[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 Γ)

def GroupoidModel.Ctx.ofCategory (C : Type (v + 1)) [CategoryTheory.Category.{v, v + 1} C] : Ctx

Equations

• GroupoidModel.Ctx.ofCategory C = GroupoidModel.Ctx.ofGrpd.obj (CategoryTheory.Grpd.of (CategoryTheory.Core (CategoryTheory.AsSmall C)))

def GroupoidModel.Ctx.homOfFunctor {C : Type (v + 1)} [CategoryTheory.Category.{v, v + 1} C] {D : Type (w + 1)} [CategoryTheory.Category.{w, w + 1} D] (F : CategoryTheory.Functor C D) : ofCategory C ⟶ ofCategory D

Equations

• GroupoidModel.Ctx.homOfFunctor F = GroupoidModel.Ctx.ofGrpd.map (CategoryTheory.Grpd.homOf (CategoryTheory.AsSmall.down.comp (F.comp CategoryTheory.AsSmall.up)).core)

instance GroupoidModel.Ctx.instCartesianMonoidalCategory : CategoryTheory.CartesianMonoidalCategory Ctx

Equations

• GroupoidModel.Ctx.instCartesianMonoidalCategory = 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)

def 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.yonedaCatEquivAux {Γ : Ctx} {C : CategoryTheory.Cat} : (yonedaCat.obj C).obj (Opposite.op Γ) ≃ CategoryTheory.Functor ↑(Ctx.toGrpd.obj Γ) ↑C

Equations

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

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

Equations

• GroupoidModel.yonedaCatEquiv = CategoryTheory.yonedaEquiv.trans GroupoidModel.yonedaCatEquivAux

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)

theorem GroupoidModel.toCoreAsSmallEquiv_symm_naturality_left {Γ Δ : Ctx} (σ : Δ ⟶ Γ) {C : Type (v + 1)} [CategoryTheory.Category.{v, v + 1} C] {A : CategoryTheory.Functor (↑(Ctx.toGrpd.obj Γ)) C} : toCoreAsSmallEquiv.symm (CategoryTheory.Functor.comp (Ctx.toGrpd.map σ) A) = CategoryTheory.CategoryStruct.comp σ (toCoreAsSmallEquiv.symm A)

theorem GroupoidModel.toCoreAsSmallEquiv_naturality_left {Γ Δ : Ctx} (σ : Δ ⟶ Γ) {C : Type (v + 1)} [CategoryTheory.Category.{v, v + 1} C] (A : Γ ⟶ Ctx.ofCategory C) : toCoreAsSmallEquiv (CategoryTheory.CategoryStruct.comp σ A) = CategoryTheory.Functor.comp (Ctx.toGrpd.map σ) (toCoreAsSmallEquiv A)

def GroupoidModel.yonedaCategoryEquiv {Γ : Ctx} {C : Type (v + 1)} [CategoryTheory.Category.{v, v + 1} C] : (CategoryTheory.yoneda.obj Γ ⟶ CategoryTheory.yoneda.obj (Ctx.ofCategory C)) ≃ CategoryTheory.Functor (↑(Ctx.toGrpd.obj Γ)) C

Equations

• GroupoidModel.yonedaCategoryEquiv = CategoryTheory.Yoneda.fullyFaithful.homEquiv.symm.trans GroupoidModel.toCoreAsSmallEquiv

theorem GroupoidModel.yonedaCategoryEquiv_naturality_left {Γ Δ : Ctx} (σ : Δ ⟶ Γ) {C : Type (v + 1)} [CategoryTheory.Category.{v, v + 1} C] (A : CategoryTheory.yoneda.obj Γ ⟶ CategoryTheory.yoneda.obj (Ctx.ofCategory C)) : yonedaCategoryEquiv (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) A) = CategoryTheory.Functor.comp (Ctx.toGrpd.map σ) (yonedaCategoryEquiv A)

theorem GroupoidModel.yonedaCategoryEquiv_naturality_left' {Γ Δ : Ctx} {C : Type (v + 1)} [CategoryTheory.Category.{v, v + 1} C] (A : CategoryTheory.yoneda.obj Γ ⟶ CategoryTheory.yoneda.obj (Ctx.ofCategory C)) {σ : CategoryTheory.yoneda.obj Δ ⟶ CategoryTheory.yoneda.obj Γ} : yonedaCategoryEquiv (CategoryTheory.CategoryStruct.comp σ A) = CategoryTheory.Functor.comp (Ctx.toGrpd.map (CategoryTheory.Yoneda.fullyFaithful.preimage σ)) (yonedaCategoryEquiv A)

theorem GroupoidModel.yonedaCategoryEquiv_symm_naturality_left {Γ Δ : Ctx} (σ : Δ ⟶ Γ) {C : Type (v + 1)} [CategoryTheory.Category.{v, v + 1} C] {A : CategoryTheory.Functor (↑(Ctx.toGrpd.obj Γ)) C} : yonedaCategoryEquiv.symm (CategoryTheory.Functor.comp (Ctx.toGrpd.map σ) A) = CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) (yonedaCategoryEquiv.symm A)

theorem GroupoidModel.yonedaCategoryEquiv_naturality_right {Γ : Ctx} {C : Type (v + 1)} [CategoryTheory.Category.{v, v + 1} C] {D : Type (v + 1)} [CategoryTheory.Category.{v, v + 1} D] (A : CategoryTheory.yoneda.obj Γ ⟶ CategoryTheory.yoneda.obj (Ctx.ofCategory C)) (F : CategoryTheory.Functor C D) : yonedaCategoryEquiv (CategoryTheory.CategoryStruct.comp A (CategoryTheory.yoneda.map (Ctx.homOfFunctor F))) = (yonedaCategoryEquiv A).comp F

theorem GroupoidModel.yonedaCategoryEquiv_symm_naturality_right {Γ : Ctx} {C : Type (v + 1)} [CategoryTheory.Category.{v, v + 1} C] {D : Type (v + 1)} [CategoryTheory.Category.{v, v + 1} D] {A : CategoryTheory.Functor (↑(Ctx.toGrpd.obj Γ)) C} (F : CategoryTheory.Functor C D) : yonedaCategoryEquiv.symm (A.comp F) = CategoryTheory.CategoryStruct.comp (yonedaCategoryEquiv.symm A) (CategoryTheory.yoneda.map (Ctx.homOfFunctor F))

def GroupoidModel.asSmallUp_comp_yoneda_iso_forgetToCat_comp_catLift_comp_yonedaCat : CategoryTheory.yoneda ≅ CategoryTheory.AsSmall.down.comp (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.

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 smallU.

Equations

• GroupoidModel.U = GroupoidModel.Ctx.ofCategory CategoryTheory.Grpd

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 smallU.

Equations

• GroupoidModel.E = GroupoidModel.Ctx.ofCategory CategoryTheory.PGrpd

def GroupoidModel.π : E ⟶ U

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

Equations

• GroupoidModel.π = GroupoidModel.Ctx.homOfFunctor CategoryTheory.PGrpd.forgetToGrpd

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.

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

Equations

• GroupoidModel.U.ext A = GroupoidModel.Ctx.ofGrpd.obj (CategoryTheory.Grpd.of (GroupoidModel.U.classifier A).Groupoidal)

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

Equations

• GroupoidModel.U.disp A = GroupoidModel.Ctx.ofGrpd.map CategoryTheory.Functor.Groupoidal.forget

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

Equations

• GroupoidModel.U.var A = GroupoidModel.toCoreAsSmallEquiv.symm (CategoryTheory.Functor.Groupoidal.toPGrpd (GroupoidModel.U.classifier A))

def GroupoidModel.U.toU : U ⟶ U

toU is the base map between two v-small universes toE E.{v} --------------> E.{v+1} | | | | π | | π | | v v U.{v}-------toU-----> U.{v+1}

Equations

• GroupoidModel.U.toU = GroupoidModel.Ctx.homOfFunctor CategoryTheory.Grpd.asSmallFunctor

def GroupoidModel.U.toE : E ⟶ E

Equations

• GroupoidModel.U.toE = GroupoidModel.Ctx.homOfFunctor CategoryTheory.PGrpd.asSmallFunctor