Here we construct the natural model for groupoids.

def sGrpd : Type (u + 1)

Equations

• sGrpd = CategoryTheory.ULiftHom CategoryTheory.Grpd

instance instsGrpdSmallCategory : CategoryTheory.SmallCategory sGrpd

Equations

• instsGrpdSmallCategory = CategoryTheory.ULiftHom.category

def sGrpd.of (C : Type u) [CategoryTheory.Groupoid C] : sGrpd

Equations

• sGrpd.of C = CategoryTheory.Grpd.of C

def SmallGrpd.forget : CategoryTheory.Functor sGrpd CategoryTheory.Grpd

Equations

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

def PshsGrpd : CategoryTheory.Functor (CategoryTheory.Functor CategoryTheory.Grpdᵒᵖ (Type (u + 1))) (CategoryTheory.Functor sGrpdᵒᵖ (Type (u + 1)))

Equations

• PshsGrpd = (CategoryTheory.whiskeringLeft sGrpdᵒᵖ CategoryTheory.Grpdᵒᵖ (Type (?u.15 + 1))).obj SmallGrpd.forget.op

instance PshsGrpdPreservesLim : CategoryTheory.Limits.PreservesLimits PshsGrpd

Equations

• PshsGrpdPreservesLim = id (CategoryTheory.whiskeringLeftPreservesLimits SmallGrpd.forget.op)

instance GroupoidNM : CategoryTheory.NaturalModel.NaturalModelBase sGrpd

Equations

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

instance groupoidULift {α : Type u} [CategoryTheory.Groupoid α] : CategoryTheory.Groupoid (ULift.{u', u} α)

Equations

• groupoidULift = CategoryTheory.Groupoid.mk (fun {X Y : ULift.{?u.20, ?u.22} α} (f : X ⟶ Y) => CategoryTheory.Groupoid.inv f) ⋯ ⋯

instance groupoidULiftHom {α : Type u} [CategoryTheory.Groupoid α] : CategoryTheory.Groupoid (CategoryTheory.ULiftHom α)

Equations

• groupoidULiftHom = CategoryTheory.Groupoid.mk (fun {X Y : CategoryTheory.ULiftHom α} (f : X ⟶ Y) => { down := CategoryTheory.Groupoid.inv f.down }) ⋯ ⋯

inductive Groupoid2 : Type (u + 2)

• small: sGrpd → Groupoid2
• large: sGrpd → Groupoid2

def Groupoid2.toLarge : Groupoid2 → sGrpd

Equations

• (Groupoid2.small A).toLarge = { α := CategoryTheory.ULiftHom (ULift.{?u.152 + 1, ?u.152} ↑A), str := inferInstance }
• (Groupoid2.large A).toLarge = A

def Grpd2 : Type (u + 2)

A model of Grpd with an internal universe, with the property that the small universe injects into the large one.

Equations

• Grpd2 = CategoryTheory.InducedCategory sGrpd Groupoid2.toLarge

instance instGrpd2SmallCategory : CategoryTheory.SmallCategory Grpd2

Equations

• instGrpd2SmallCategory = CategoryTheory.InducedCategory.category Groupoid2.toLarge

def PolyDataGet (Γ : sGrpdᵒᵖ) (Q : ((CategoryTheory.NaturalModel.P CategoryTheory.NaturalModel.tp).obj CategoryTheory.NaturalModel.Ty).obj Γ) : CategoryTheory.yoneda.obj (Opposite.unop Γ) ⟶ (CategoryTheory.NaturalModel.P CategoryTheory.NaturalModel.tp).obj CategoryTheory.NaturalModel.Ty

Equations

• PolyDataGet Γ Q = CategoryTheory.yonedaEquiv.invFun Q

def GroupoidSigma {Γ : CategoryTheory.Grpd} (A : CategoryTheory.Functor (↑Γ) CategoryTheory.Grpd) (B : CategoryTheory.Functor (CategoryTheory.GroupoidalGrothendieck A) CategoryTheory.Grpd) : CategoryTheory.Functor (↑Γ) CategoryTheory.Grpd

instance GroupoidNMSigma : CategoryTheory.NaturalModel.NaturalModelSigma sGrpd

Equations

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