Here we construct universes for the groupoid natural model.

def GroupoidModel.IsPullback.groupoidalAsSmallFunctorToPGrpd : CategoryTheory.Functor (CategoryTheory.Grothendieck.Groupoidal CategoryTheory.Grpd.asSmallFunctor) CategoryTheory.PGrpd

Equations

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

def GroupoidModel.IsPullback.pGrpdToGroupoidalAsSmallFunctor : CategoryTheory.Functor CategoryTheory.PGrpd (CategoryTheory.Grothendieck.Groupoidal CategoryTheory.Grpd.asSmallFunctor)

Equations

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

def GroupoidModel.IsPullback.PGrpd.IsMegaPullback'.lift {C : Type u₂} [CategoryTheory.Category.{v₁, u₂} C] (fst : CategoryTheory.Functor C CategoryTheory.PGrpd) (snd : CategoryTheory.Functor C CategoryTheory.Grpd) (condition : fst.comp CategoryTheory.PGrpd.forgetToGrpd = snd.comp CategoryTheory.Grpd.asSmallFunctor) : CategoryTheory.Functor C CategoryTheory.PGrpd

Equations

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

def GroupoidModel.IsPullback.PGrpd.IsMegaPullback'.fac_left {C : Type u₂} [CategoryTheory.Category.{v₁, u₂} C] (fst : CategoryTheory.Functor C CategoryTheory.PGrpd) (snd : CategoryTheory.Functor C CategoryTheory.Grpd) (condition : fst.comp CategoryTheory.PGrpd.forgetToGrpd = snd.comp CategoryTheory.Grpd.asSmallFunctor) : (lift fst snd condition).comp CategoryTheory.PGrpd.asSmallFunctor = fst

Equations

• ⋯ = ⋯

def GroupoidModel.IsPullback.PGrpd.IsMegaPullback'.fac_right {C : Type u₂} [CategoryTheory.Category.{v₁, u₂} C] (fst : CategoryTheory.Functor C CategoryTheory.PGrpd) (snd : CategoryTheory.Functor C CategoryTheory.Grpd) (condition : fst.comp CategoryTheory.PGrpd.forgetToGrpd = snd.comp CategoryTheory.Grpd.asSmallFunctor) : (lift fst snd condition).comp CategoryTheory.PGrpd.forgetToGrpd = snd

Equations

• ⋯ = ⋯

def GroupoidModel.IsPullback.PGrpd.IsMegaPullback'.lift_uniq {C : Type u₂} [CategoryTheory.Category.{v₁, u₂} C] (fst : CategoryTheory.Functor C CategoryTheory.PGrpd) (snd : CategoryTheory.Functor C CategoryTheory.Grpd) (condition : fst.comp CategoryTheory.PGrpd.forgetToGrpd = snd.comp CategoryTheory.Grpd.asSmallFunctor) (m : CategoryTheory.Functor C CategoryTheory.PGrpd) (hl : m.comp CategoryTheory.PGrpd.asSmallFunctor = fst) (hr : m.comp CategoryTheory.PGrpd.forgetToGrpd = snd) : m = lift fst snd condition

Equations

• ⋯ = ⋯

def GroupoidModel.IsPullback.LargeUHom.CAT : CategoryTheory.Cat

Equations

• GroupoidModel.IsPullback.LargeUHom.CAT = CategoryTheory.Cat.of CategoryTheory.Cat

def GroupoidModel.IsPullback.LargeUHom.PCAT : CategoryTheory.Cat

Equations

• GroupoidModel.IsPullback.LargeUHom.PCAT = CategoryTheory.Cat.of CategoryTheory.PCat

def GroupoidModel.IsPullback.LargeUHom.GRPD : CategoryTheory.Cat

Equations

• GroupoidModel.IsPullback.LargeUHom.GRPD = CategoryTheory.Cat.of CategoryTheory.Grpd

def GroupoidModel.IsPullback.LargeUHom.PGRPD : CategoryTheory.Cat

Equations

• GroupoidModel.IsPullback.LargeUHom.PGRPD = CategoryTheory.Cat.of CategoryTheory.PGrpd

def GroupoidModel.IsPullback.LargeUHom.grpd : CategoryTheory.Cat

Equations

• GroupoidModel.IsPullback.LargeUHom.grpd = CategoryTheory.Cat.ofULift (CategoryTheory.AsSmall CategoryTheory.Grpd)

def GroupoidModel.IsPullback.LargeUHom.pgrpd : CategoryTheory.Cat

Equations

• GroupoidModel.IsPullback.LargeUHom.pgrpd = CategoryTheory.Cat.ofULift (CategoryTheory.AsSmall CategoryTheory.PGrpd)

def GroupoidModel.IsPullback.LargeUHom.coregrpd : CategoryTheory.Cat

Equations

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

def GroupoidModel.IsPullback.LargeUHom.corepgrpd : CategoryTheory.Cat

Equations

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

def GroupoidModel.IsPullback.LargeUHom.PCATFORGETTOCAT : PCAT ⟶ CAT

Equations

• GroupoidModel.IsPullback.LargeUHom.PCATFORGETTOCAT = CategoryTheory.Cat.homOf CategoryTheory.PCat.forgetToCat

def GroupoidModel.IsPullback.LargeUHom.PGRPDFORGETTOGRPD : PGRPD ⟶ GRPD

Equations

• GroupoidModel.IsPullback.LargeUHom.PGRPDFORGETTOGRPD = CategoryTheory.Cat.homOf CategoryTheory.PGrpd.forgetToGrpd

def GroupoidModel.IsPullback.LargeUHom.GRPDFORGETTOCAT : GRPD ⟶ CAT

Equations

• GroupoidModel.IsPullback.LargeUHom.GRPDFORGETTOCAT = CategoryTheory.Cat.homOf CategoryTheory.Grpd.forgetToCat

def GroupoidModel.IsPullback.LargeUHom.PGRPDFORGETTOPCAT : PGRPD ⟶ PCAT

Equations

• GroupoidModel.IsPullback.LargeUHom.PGRPDFORGETTOPCAT = CategoryTheory.Cat.homOf CategoryTheory.PGrpd.forgetToPCat

def GroupoidModel.IsPullback.LargeUHom.pgrpdforgettogrpd : pgrpd ⟶ grpd

Equations

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

def GroupoidModel.IsPullback.LargeUHom.grpdassmallfunctor : grpd ⟶ GRPD

Equations

• GroupoidModel.IsPullback.LargeUHom.grpdassmallfunctor = CategoryTheory.Cat.homOf (CategoryTheory.ULift.downFunctor.comp (CategoryTheory.AsSmall.down.comp CategoryTheory.Grpd.asSmallFunctor))

def GroupoidModel.IsPullback.LargeUHom.pgrpdassmallfunctor : pgrpd ⟶ PGRPD

Equations

• GroupoidModel.IsPullback.LargeUHom.pgrpdassmallfunctor = CategoryTheory.Cat.homOf (CategoryTheory.ULift.downFunctor.comp (CategoryTheory.AsSmall.down.comp CategoryTheory.PGrpd.asSmallFunctor))

def GroupoidModel.IsPullback.LargeUHom.corepgrpdforgettogrpd : corepgrpd ⟶ coregrpd

Equations

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

def GroupoidModel.IsPullback.LargeUHom.coreFunctorPGrpdForgetToGrpd : corepgrpd ⟶ coregrpd

Equations

• GroupoidModel.IsPullback.LargeUHom.coreFunctorPGrpdForgetToGrpd = CategoryTheory.Cat.homOf (CategoryTheory.Core.map.map GroupoidModel.IsPullback.LargeUHom.pgrpdforgettogrpd)

def GroupoidModel.IsPullback.LargeUHom.inclusionGrpdCompAsSmallFunctor : coregrpd ⟶ GRPD

Equations

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

def GroupoidModel.IsPullback.LargeUHom.inclusionPGrpdCompAsSmallFunctor : corepgrpd ⟶ PGRPD

Equations

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

def GroupoidModel.IsPullback.LargeUHom.yUIsoYonedaCatGrpd : CategoryTheory.yoneda.obj U ≅ yonedaCat.obj coregrpd

Equations

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

def GroupoidModel.IsPullback.LargeUHom.yEIsoYonedaCatPGrpd : CategoryTheory.yoneda.obj E ≅ yonedaCat.obj corepgrpd

Equations

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

theorem GroupoidModel.IsPullback.LargeUHom.IsPullback.comm_sq : CategoryTheory.CategoryStruct.comp pgrpdassmallfunctor PGRPDFORGETTOGRPD = CategoryTheory.CategoryStruct.comp pgrpdforgettogrpd grpdassmallfunctor

def GroupoidModel.IsPullback.LargeUHom.IsPullback.snd (s : CategoryTheory.Limits.PullbackCone PGRPDFORGETTOGRPD grpdassmallfunctor) : CategoryTheory.Functor (↑s.pt) CategoryTheory.Grpd

Equations

• GroupoidModel.IsPullback.LargeUHom.IsPullback.snd s = CategoryTheory.Functor.comp s.snd (CategoryTheory.ULift.downFunctor.comp CategoryTheory.AsSmall.down)

def GroupoidModel.IsPullback.LargeUHom.IsPullback.condition (s : CategoryTheory.Limits.PullbackCone PGRPDFORGETTOGRPD grpdassmallfunctor) : CategoryTheory.Functor.comp s.fst CategoryTheory.PGrpd.forgetToGrpd = (snd s).comp CategoryTheory.Grpd.asSmallFunctor

Equations

• ⋯ = ⋯

def GroupoidModel.IsPullback.LargeUHom.IsPullback.lift (s : CategoryTheory.Limits.PullbackCone PGRPDFORGETTOGRPD grpdassmallfunctor) : s.pt ⟶ pgrpd

Equations

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

theorem GroupoidModel.IsPullback.LargeUHom.isPullback_pgrpdforgettogrpd_PGRPDFORGETTOGRPD : CategoryTheory.IsPullback pgrpdassmallfunctor pgrpdforgettogrpd PGRPDFORGETTOGRPD grpdassmallfunctor

The following square is a pullback

PGrpd.{v,v} -- PGrpd.asSmallFunctor --> PGrpd.{max v u, max v u} | | | | PGrpd.forgetToGrpd PGrpd.forgetToGrpd | | v v Grpd.{v,v} -- Grpd.asSmallFunctor --> Grpd.{max v u, max v u}

instance GroupoidModel.IsPullback.LargeUHom.instReflectsIsomorphismsαCategoryPgrpdGrpdPgrpdforgettogrpd : CategoryTheory.Functor.ReflectsIsomorphisms pgrpdforgettogrpd

theorem GroupoidModel.IsPullback.LargeUHom.isPullback_corepgrpdforgettogrpd_PGRPDFORGETTOGRPD : CategoryTheory.IsPullback inclusionPGrpdCompAsSmallFunctor coreFunctorPGrpdForgetToGrpd PGRPDFORGETTOGRPD inclusionGrpdCompAsSmallFunctor

The following square is a pullback

Core PGrpd.{v,v} -- PGrpd.asSmallFunctor --> PGrpd.{max v u, max v u} | | | | Core PGrpd.forgetToGrpd PGrpd.forgetToGrpd | | v v Core Grpd.{v,v} -- Grpd.asSmallFunctor --> Grpd.{max v u, max v u}

theorem GroupoidModel.IsPullback.LargeUHom.isPullback_yonedaCatCorePGrpdForgetToGrpd_tp : CategoryTheory.IsPullback (yonedaCat.map inclusionPGrpdCompAsSmallFunctor) (yonedaCat.map coreFunctorPGrpdForgetToGrpd) tp (yonedaCat.map inclusionGrpdCompAsSmallFunctor)

The image of isPullback_corepgrpdforgettogrpd_PGRPDFORGETTOGRPD under yonedaCat is a pullback

yonedaCat (Core PGrpd.{v,v}) ----> yonedaCat (PGrpd.{max v u, max v u}) = Tm | | | | | tp | | v v yonedaCat (Core Grpd.{v,v}) ----> yonedaCat (Grpd.{max v u, max v u}) = Ty

theorem GroupoidModel.IsPullback.LargeUHom.isPullback_yπ_yonedaCatCorepgrpdforgettogrpd : CategoryTheory.IsPullback yEIsoYonedaCatPGrpd.hom (CategoryTheory.yoneda.map π) (yonedaCat.map corepgrpdforgettogrpd) yUIsoYonedaCatGrpd.hom

def GroupoidModel.IsPullback.LargeUHom.toTy : CategoryTheory.yoneda.obj U ⟶ Ty

toTy is the map that classifies the universe U of v-small types as a map into the type classifier Ty. This will fit into the pullback square

E --------toTm---> Tm | | | | | | | | v v U---------toTy----->Ty

Equations

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

def GroupoidModel.IsPullback.LargeUHom.toTm : CategoryTheory.yoneda.obj E ⟶ Tm

Equations

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

theorem GroupoidModel.IsPullback.LargeUHom.isPullback_yπ_tp : CategoryTheory.IsPullback toTm (CategoryTheory.yoneda.map π) tp toTy

The small universe and the ambient natural model form a pullback y(E) ------------ toTm --------------> Tm | | | | ym(π) tp | | v v y(U) ------------ toTy --------------> Ty

@[reducible, inline]

abbrev GroupoidModel.IsPullback.Base.yonedaCatMapToPGrpd {Γ : Ctx} (A : CategoryTheory.yoneda.obj Γ ⟶ Ty) : yonedaCat.obj (CategoryTheory.Grothendieck.IsPullback.uLiftGrothendieck (CategoryTheory.Groupoid.compForgetToCat (yonedaCatEquiv A))) ⟶ Tm

The image of (roughly) Groupoidal.toPGrpd : Grothendieck A ⥤ PGrpd under yonedaCat. Used in the pullback diagram isPullback_yonedaCatULiftGrothendieckForget_tp

Equations

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

@[reducible, inline]

abbrev GroupoidModel.IsPullback.Base.yonedaCatMapGrothendieckForget {Γ : Ctx} (A : CategoryTheory.yoneda.obj Γ ⟶ Ty) : yonedaCat.obj (CategoryTheory.Grothendieck.IsPullback.uLiftGrothendieck (CategoryTheory.Groupoid.compForgetToCat (yonedaCatEquiv A))) ⟶ yonedaCat.obj (CategoryTheory.Cat.ofULift ↑(Ctx.toGrpd.obj Γ))

The image of (roughly) Grothendieck.forget : Grothendieck A ⥤ Γ under yonedaCat. Used in the pullback diagram isPullback_yonedaCatULiftGrothendieckForget_tp

Equations

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

@[reducible, inline]

abbrev GroupoidModel.IsPullback.Base.yonedaCatMapYonedaCatEquiv {Γ : Ctx} (A : CategoryTheory.yoneda.obj Γ ⟶ Ty) : yonedaCat.obj (CategoryTheory.Cat.ofULift ↑(Ctx.toGrpd.obj Γ)) ⟶ Ty

The image of yonedaCatEquiv A under yonedaCat. Used in the pullback diagram isPullback_yonedaCatULiftGrothendieckForget_tp

Equations

• GroupoidModel.IsPullback.Base.yonedaCatMapYonedaCatEquiv A = GroupoidModel.yonedaCat.map (CategoryTheory.Cat.homOf (CategoryTheory.ULift.downFunctor.comp (GroupoidModel.yonedaCatEquiv A)))

theorem GroupoidModel.IsPullback.Base.isPullback_yonedaCatGrothendieckForget_tp {Γ : Ctx} (A : CategoryTheory.yoneda.obj Γ ⟶ Ty) : CategoryTheory.IsPullback (yonedaCatMapToPGrpd A) (yonedaCatMapGrothendieckForget A) tp (yonedaCatMapYonedaCatEquiv A)

The image of the pullback Grothendieck.Groupoidal.isPullback under yonedaCat is a pullback, since yonedaCat preserves limits

theorem GroupoidModel.IsPullback.Base.isPullback_yonedaDisp_yonedaCatULiftGrothendieckForget {Γ : Ctx} (A : CategoryTheory.yoneda.obj Γ ⟶ Ty) : CategoryTheory.IsPullback (asSmallUp_comp_yoneda_iso_forgetToCat_comp_catLift_comp_yonedaCat.hom.app (CategoryTheory.Grpd.of (CategoryTheory.Grothendieck.Groupoidal (yonedaCatEquiv A)))) (CategoryTheory.yoneda.map (disp A)) (yonedaCatMapGrothendieckForget A) (asSmallUp_comp_yoneda_iso_forgetToCat_comp_catLift_comp_yonedaCat.hom.app (Ctx.toGrpd.obj Γ))

yoneda.map (disp A) is isomorphic to yonedaCat(uLiftGrothendieckForget _) in the arrow category, hence forming a pullback square

yoneda (ext A) ------≅----> yonedaCat(uLift (ext A)) | | | | | | | | | | v v yoneda Γ --------≅----> yonedaCat(uLift Γ)

theorem GroupoidModel.IsPullback.Base.isPullback_yonedaDisp_tp {Γ : Ctx} (A : CategoryTheory.yoneda.obj Γ ⟶ Ty) : CategoryTheory.IsPullback (var A) (CategoryTheory.yoneda.map (disp A)) tp A

The pullback square required for GroupoidNaturalModel.base

            var A

yoneda (ext A) ----------> Ty | | | | | tp yoneda(disp A) | | | | | v v yoneda Γ ------------> Tm A

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.toU' : U' ⟶ U'

Equations

• GroupoidModel.IsPullback.SmallUHom.toU' = CategoryTheory.Core.map.map (CategoryTheory.Cat.homOf GroupoidModel.IsPullback.SmallUHom.toU'')

def GroupoidModel.IsPullback.SmallUHom.toU : U ⟶ U

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

Equations

• GroupoidModel.IsPullback.SmallUHom.toU = GroupoidModel.Ctx.ofGrpd.map GroupoidModel.IsPullback.SmallUHom.toU'

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.toE' : E' ⟶ E'

Equations

• GroupoidModel.IsPullback.SmallUHom.toE' = CategoryTheory.Core.map.map (CategoryTheory.Cat.homOf GroupoidModel.IsPullback.SmallUHom.toE'')

def GroupoidModel.IsPullback.SmallUHom.toE : E ⟶ E

Equations

• GroupoidModel.IsPullback.SmallUHom.toE = GroupoidModel.Ctx.ofGrpd.map GroupoidModel.IsPullback.SmallUHom.toE'

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

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

Equations

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

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

Equations

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

theorem GroupoidModel.IsPullback.SmallUHom.isPullback_uLiftGrothendieckForget_forgetToGrpd : CategoryTheory.IsPullback (CategoryTheory.Cat.homOf (CategoryTheory.ULift.downFunctor.comp (CategoryTheory.Grothendieck.Groupoidal.toPGrpd toU'''))) (CategoryTheory.Grothendieck.IsPullback.uLiftGrothendieckForget (CategoryTheory.Groupoid.compForgetToCat toU''')) (CategoryTheory.Cat.homOf CategoryTheory.PGrpd.forgetToGrpd) (CategoryTheory.Cat.homOf (CategoryTheory.ULift.downFunctor.comp toU'''))

def GroupoidModel.IsPullback.SmallUHom.fst' (s : CategoryTheory.Limits.PullbackCone (CategoryTheory.Cat.homOf π'') (CategoryTheory.Cat.homOf toU'')) : CategoryTheory.Functor (↑s.pt) CategoryTheory.PGrpd

Equations

• GroupoidModel.IsPullback.SmallUHom.fst' s = CategoryTheory.Functor.comp s.fst CategoryTheory.AsSmall.down

def GroupoidModel.IsPullback.SmallUHom.snd' (s : CategoryTheory.Limits.PullbackCone (CategoryTheory.Cat.homOf π'') (CategoryTheory.Cat.homOf toU'')) : CategoryTheory.Functor (↑s.pt) CategoryTheory.Grpd

Equations

• GroupoidModel.IsPullback.SmallUHom.snd' s = CategoryTheory.Functor.comp s.snd CategoryTheory.AsSmall.down

theorem GroupoidModel.IsPullback.SmallUHom.condition' (s : CategoryTheory.Limits.PullbackCone (CategoryTheory.Cat.homOf π'') (CategoryTheory.Cat.homOf toU'')) : (fst' s).comp CategoryTheory.PGrpd.forgetToGrpd = (snd' s).comp CategoryTheory.Grpd.asSmallFunctor

def GroupoidModel.IsPullback.SmallUHom.lift' (s : CategoryTheory.Limits.PullbackCone (CategoryTheory.Cat.homOf π'') (CategoryTheory.Cat.homOf toU'')) : s.pt ⟶ CategoryTheory.Cat.of (CategoryTheory.AsSmall CategoryTheory.PGrpd)

Equations

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

theorem GroupoidModel.IsPullback.SmallUHom.fac_left' (s : CategoryTheory.Limits.PullbackCone (CategoryTheory.Cat.homOf π'') (CategoryTheory.Cat.homOf toU'')) : CategoryTheory.CategoryStruct.comp (lift' s) (CategoryTheory.Cat.homOf toE'') = s.fst

theorem GroupoidModel.IsPullback.SmallUHom.fac_right' (s : CategoryTheory.Limits.PullbackCone (CategoryTheory.Cat.homOf π'') (CategoryTheory.Cat.homOf toU'')) : CategoryTheory.CategoryStruct.comp (lift' s) (CategoryTheory.Cat.homOf π'') = s.snd

theorem GroupoidModel.IsPullback.SmallUHom.lift_uniq' (s : CategoryTheory.Limits.PullbackCone (CategoryTheory.Cat.homOf π'') (CategoryTheory.Cat.homOf toU'')) (m : s.pt ⟶ CategoryTheory.Cat.of (CategoryTheory.AsSmall CategoryTheory.PGrpd)) (hl : CategoryTheory.CategoryStruct.comp m (CategoryTheory.Cat.homOf toE'') = s.fst) (hr : CategoryTheory.CategoryStruct.comp m (CategoryTheory.Cat.homOf π'') = s.snd) : m = lift' s

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. We prove this is pullback by using the fact that this IsMegaPullback, i.e. it is universal among categories of all sizes.

theorem GroupoidModel.IsPullback.SmallUHom.isPullback_π'_π' : CategoryTheory.IsPullback toE' π' π' toU'

The following square is a pullback

E'.{v,max u (v+2)} ------- toE' ------> E'.{v+1,u} | | | | π' π' | | v v U'.{v,max u (v+2)} ------- toU' -----> U'.{v+1,u}

in the category Grpd.{max u (v+2), max u (v+2)}. This is because Core.map is a right adjoint, hence preserves limits.

theorem GroupoidModel.IsPullback.SmallUHom.isPullback_yπ_yπ : CategoryTheory.IsPullback (CategoryTheory.yoneda.map toE) (CategoryTheory.yoneda.map π) (CategoryTheory.yoneda.map π) (CategoryTheory.yoneda.map 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.SmallBase.coreΓ (Γ : Ctx) : CategoryTheory.Grpd

Equations

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

@[reducible, inline]

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

Equations

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

@[reducible, inline]

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

Equations

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

@[reducible, inline]

abbrev GroupoidModel.IsPullback.SmallBase.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.SmallBase.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.SmallBase.isPullback_disp'_asSmallForgetToGrpd_comm_sq {Γ : Ctx} (A : Γ ⟶ U) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Cat.homOf ((CategoryTheory.Grothendieck.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.Grothendieck.forget (CategoryTheory.Groupoid.compForgetToCat (U.classifier A)))) (CategoryTheory.Cat.homOf (CategoryTheory.Functor.comp (Ctx.toGrpd.map A) (CategoryTheory.Core.inclusion (CategoryTheory.AsSmall CategoryTheory.Grpd))))

Equations

• ⋯ = ⋯

def GroupoidModel.IsPullback.SmallBase.comm_sq {Γ : Ctx} {A : Γ ⟶ U} (s : CategoryTheory.Limits.PullbackCone (CategoryTheory.Cat.homOf (CategoryTheory.Cat.asSmallFunctor.map (CategoryTheory.Cat.homOf CategoryTheory.PGrpd.forgetToGrpd))) (CategoryTheory.Cat.homOf (CategoryTheory.Functor.comp (Ctx.toGrpd.map A) (CategoryTheory.Core.inclusion (CategoryTheory.AsSmall CategoryTheory.Grpd))))) : CategoryTheory.Functor.comp s.fst (CategoryTheory.AsSmall.down.comp CategoryTheory.PGrpd.forgetToGrpd) = CategoryTheory.Functor.comp s.snd (U.classifier A)

Equations

• ⋯ = ⋯

def GroupoidModel.IsPullback.SmallBase.lift {Γ : Ctx} {A : Γ ⟶ U} (s : CategoryTheory.Limits.PullbackCone (CategoryTheory.Cat.homOf (CategoryTheory.Cat.asSmallFunctor.map (CategoryTheory.Cat.homOf CategoryTheory.PGrpd.forgetToGrpd))) (CategoryTheory.Cat.homOf (CategoryTheory.Functor.comp (Ctx.toGrpd.map A) (CategoryTheory.Core.inclusion (CategoryTheory.AsSmall CategoryTheory.Grpd))))) : s.pt ⟶ CategoryTheory.Cat.of (CategoryTheory.Grothendieck.Groupoidal (U.classifier A))

Equations

• GroupoidModel.IsPullback.SmallBase.lift s = CategoryTheory.Grothendieck.Groupoidal.IsMegaPullback.lift (CategoryTheory.Functor.comp s.fst CategoryTheory.AsSmall.down) s.snd ⋯

@[simp]

theorem GroupoidModel.IsPullback.SmallBase.fac_left {Γ : Ctx} {A : Γ ⟶ U} (s : CategoryTheory.Limits.PullbackCone (CategoryTheory.Cat.homOf (CategoryTheory.Cat.asSmallFunctor.map (CategoryTheory.Cat.homOf CategoryTheory.PGrpd.forgetToGrpd))) (CategoryTheory.Cat.homOf (CategoryTheory.Functor.comp (Ctx.toGrpd.map A) (CategoryTheory.Core.inclusion (CategoryTheory.AsSmall CategoryTheory.Grpd))))) : CategoryTheory.CategoryStruct.comp (lift s) (CategoryTheory.Cat.homOf ((CategoryTheory.Grothendieck.Groupoidal.toPGrpd (U.classifier A)).comp CategoryTheory.AsSmall.up)) = s.fst

@[simp]

theorem GroupoidModel.IsPullback.SmallBase.fac_right {Γ : Ctx} {A : Γ ⟶ U} (s : CategoryTheory.Limits.PullbackCone (CategoryTheory.Cat.homOf (CategoryTheory.Cat.asSmallFunctor.map (CategoryTheory.Cat.homOf CategoryTheory.PGrpd.forgetToGrpd))) (CategoryTheory.Cat.homOf (CategoryTheory.Functor.comp (Ctx.toGrpd.map A) (CategoryTheory.Core.inclusion (CategoryTheory.AsSmall CategoryTheory.Grpd))))) : CategoryTheory.CategoryStruct.comp (lift s) (CategoryTheory.Cat.homOf (CategoryTheory.Grothendieck.forget (CategoryTheory.Groupoid.compForgetToCat (U.classifier A)))) = s.snd

theorem GroupoidModel.IsPullback.SmallBase.lift_uniq {Γ : Ctx} {A : Γ ⟶ U} (s : CategoryTheory.Limits.PullbackCone (CategoryTheory.Cat.homOf (CategoryTheory.Cat.asSmallFunctor.map (CategoryTheory.Cat.homOf CategoryTheory.PGrpd.forgetToGrpd))) (CategoryTheory.Cat.homOf (CategoryTheory.Functor.comp (Ctx.toGrpd.map A) (CategoryTheory.Core.inclusion (CategoryTheory.AsSmall CategoryTheory.Grpd))))) (m : s.pt ⟶ CategoryTheory.Cat.of (CategoryTheory.Grothendieck (CategoryTheory.Groupoid.compForgetToCat (U.classifier A)))) (hl : CategoryTheory.CategoryStruct.comp m (CategoryTheory.Cat.homOf ((CategoryTheory.Grothendieck.Groupoidal.toPGrpd (U.classifier A)).comp CategoryTheory.AsSmall.up)) = s.fst) (hr : CategoryTheory.CategoryStruct.comp m (CategoryTheory.Cat.homOf (CategoryTheory.Grothendieck.forget (CategoryTheory.Groupoid.compForgetToCat (U.classifier A)))) = s.snd) : m = lift s

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

theorem GroupoidModel.IsPullback.SmallBase.isPullback_coreDisp'_π' {Γ : Ctx} (A : Γ ⟶ U) : CategoryTheory.IsPullback (coreVar' A) (coreDisp' A) π' (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.SmallBase.isPullback_disp'_coreDisp' {Γ : Ctx} (A : Γ ⟶ U) : CategoryTheory.IsPullback (CategoryTheory.Grpd.homOf (CategoryTheory.Core.functorToCore (CategoryTheory.Functor.id (CategoryTheory.Grothendieck.Groupoidal (U.classifier A))))) (U.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.SmallBase.isPullback_disp'_π' {Γ : Ctx} (A : Γ ⟶ U) : CategoryTheory.IsPullback (U.var' A) (U.disp' A) π' (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.SmallBase.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.SmallBase.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)