Here we construct universes for the groupoid natural model.

def GroupoidModel.smallU.ext {Γ : Ctx} (A : CategoryTheory.yoneda.obj Γ ⟶ CategoryTheory.yoneda.obj U) : Ctx

Equations

• GroupoidModel.smallU.ext A = GroupoidModel.Ctx.ofGrpd.obj (CategoryTheory.Grpd.of ∫(GroupoidModel.yonedaCategoryEquiv A))

def GroupoidModel.smallU.disp {Γ : Ctx} (A : CategoryTheory.yoneda.obj Γ ⟶ CategoryTheory.yoneda.obj U) : ext A ⟶ Γ

Equations

• GroupoidModel.smallU.disp A = GroupoidModel.Ctx.ofGrpd.map CategoryTheory.Grothendieck.Groupoidal.forget

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

Equations

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

def GroupoidModel.smallU : NaturalModelBase Ctx

The natural model that acts as the classifier of v-large terms and types. Note that Ty and Tm are representables, but since representables are Ctx-large, its representable fibers can be larger (in terms of universe levels) than itself.

Equations

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

@[simp]

theorem GroupoidModel.smallU_Tm : smallU.Tm = CategoryTheory.yoneda.obj E

@[simp]

theorem GroupoidModel.smallU_disp {Γ✝ : Ctx} (A : CategoryTheory.yoneda.obj Γ✝ ⟶ CategoryTheory.yoneda.obj U) : smallU.disp A = smallU.disp A

@[simp]

theorem GroupoidModel.smallU_ext {Γ✝ : Ctx} (A : CategoryTheory.yoneda.obj Γ✝ ⟶ CategoryTheory.yoneda.obj U) : smallU.ext A = smallU.ext A

@[simp]

theorem GroupoidModel.smallU_var {Γ✝ : Ctx} (A : CategoryTheory.yoneda.obj Γ✝ ⟶ CategoryTheory.yoneda.obj U) : smallU.var A = smallU.var A

@[simp]

theorem GroupoidModel.smallU_tp : smallU.tp = CategoryTheory.yoneda.map π

@[simp]

theorem GroupoidModel.smallU_Ty : smallU.Ty = CategoryTheory.yoneda.obj U

def GroupoidModel.U.asSmallClosedType' : CategoryTheory.MonoidalCategoryStruct.tensorUnit Ctx ⟶ U

Equations

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

def GroupoidModel.U.asSmallClosedType : CategoryTheory.yoneda.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit Ctx) ⟶ smallU.Ty

Equations

• GroupoidModel.U.asSmallClosedType = CategoryTheory.yoneda.map GroupoidModel.U.asSmallClosedType'

def GroupoidModel.U.isoGrpd : CategoryTheory.Functor (CategoryTheory.Core (CategoryTheory.AsSmall CategoryTheory.Grpd)) CategoryTheory.Grpd

Equations

• GroupoidModel.U.isoGrpd = (CategoryTheory.Core.inclusion (CategoryTheory.AsSmall CategoryTheory.Grpd)).comp CategoryTheory.AsSmall.down

def GroupoidModel.U.isoExtAsSmallClosedTypeHom : CategoryTheory.Functor (CategoryTheory.Core (CategoryTheory.AsSmall CategoryTheory.Grpd)) ∫(classifier asSmallClosedType')

Equations

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

def GroupoidModel.U.isoExtAsSmallClosedTypeInv : CategoryTheory.Functor ∫(classifier asSmallClosedType') (CategoryTheory.Core (CategoryTheory.AsSmall CategoryTheory.Grpd))

Equations

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

def GroupoidModel.U.isoExtAsSmallClosedType : U ≅ smallU.ext asSmallClosedType

Equations

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

def GroupoidModel.uHomSeqObjs (i : ℕ) (h : i < 4) : NaturalModelBase Ctx

Equations

• GroupoidModel.uHomSeqObjs 0 h_2 = GroupoidModel.smallU
• GroupoidModel.uHomSeqObjs 1 h_2 = GroupoidModel.smallU
• GroupoidModel.uHomSeqObjs 2 h_2 = GroupoidModel.smallU
• GroupoidModel.uHomSeqObjs 3 h_2 = GroupoidModel.smallU
• GroupoidModel.uHomSeqObjs n.succ.succ.succ.succ h_2 = ⋯.elim

def GroupoidModel.smallUHom : smallU.UHom smallU

Equations

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

def GroupoidModel.uHomSeqHomSucc' (i : ℕ) (h : i < 3) : (uHomSeqObjs i ⋯).UHom (uHomSeqObjs (i + 1) ⋯)

Equations

• GroupoidModel.uHomSeqHomSucc' 0 h_2 = GroupoidModel.smallUHom
• GroupoidModel.uHomSeqHomSucc' 1 h_2 = GroupoidModel.smallUHom
• GroupoidModel.uHomSeqHomSucc' 2 h_2 = GroupoidModel.smallUHom
• GroupoidModel.uHomSeqHomSucc' n.succ.succ.succ h_2 = ⋯.elim

def GroupoidModel.uHomSeq : NaturalModelBase.UHomSeq Ctx

The groupoid natural model with three nested representable universes within the ambient natural model.

Equations

• GroupoidModel.uHomSeq = { length := 3, objs := GroupoidModel.uHomSeqObjs, homSucc' := GroupoidModel.uHomSeqHomSucc' }

theorem GroupoidModel.smallU_lift {Γ Δ : Ctx} (A : CategoryTheory.yoneda.obj Γ ⟶ smallU.Ty) (fst : CategoryTheory.yoneda.obj Δ ⟶ smallU.Tm) (snd : Δ ⟶ Γ) (w : CategoryTheory.CategoryStruct.comp fst smallU.tp = CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map snd) A) : ⋯.lift fst (CategoryTheory.yoneda.map snd) w = CategoryTheory.yoneda.map (Ctx.ofGrpd.map ((CategoryTheory.Grothendieck.Groupoidal.isPullback (yonedaCategoryEquiv A)).lift (yonedaCategoryEquiv fst) (Ctx.toGrpd.map snd) ⋯))

def GroupoidModel.yonedaCategoryEquivPre {Γ Δ : Ctx} (σ : Δ ⟶ Γ) (A : CategoryTheory.yoneda.obj Γ ⟶ smallU.Ty) : CategoryTheory.Functor ∫(yonedaCategoryEquiv (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) A)) ∫(yonedaCategoryEquiv A)

Equations

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

@[simp]

theorem GroupoidModel.Ctx.toGrpd_obj_ofGrpd_obj (x : CategoryTheory.Grpd) : toGrpd.obj (ofGrpd.obj x) = x

@[simp]

theorem GroupoidModel.Ctx.ofGrpd_obj_toGrpd_obj (x : Ctx) : ofGrpd.obj (toGrpd.obj x) = x

@[simp]

theorem GroupoidModel.Ctx.toGrpd_map_ofGrpd_map {x y : CategoryTheory.Grpd} (f : x ⟶ y) : toGrpd.map (ofGrpd.map f) = f

@[simp]

theorem GroupoidModel.Ctx.ofGrpd_map_toGrpd_map {x y : Ctx} (f : x ⟶ y) : ofGrpd.map (toGrpd.map f) = f

theorem GroupoidModel.Grothendieck.Groupoidal.map_eqToHom_toPGrpd {Γ : Type u_1} [CategoryTheory.Category.{u_2, u_1} Γ] (A A' : CategoryTheory.Functor Γ CategoryTheory.Grpd) (h : A = A') : (CategoryTheory.Grothendieck.Groupoidal.map (CategoryTheory.eqToHom h)).comp (CategoryTheory.Grothendieck.Groupoidal.toPGrpd A') = CategoryTheory.Grothendieck.Groupoidal.toPGrpd A

theorem GroupoidModel.smallU_substWk {Γ Δ : Ctx} (σ : Δ ⟶ Γ) (A : CategoryTheory.yoneda.obj Γ ⟶ smallU.Ty) : smallU.substWk σ A = Ctx.ofGrpd.map (CategoryTheory.Grpd.homOf (yonedaCategoryEquivPre σ A))

@[simp]

theorem GroupoidModel.smallU_sec {Γ : Ctx} (α : CategoryTheory.yoneda.obj Γ ⟶ smallU.Tm) : smallU.sec (CategoryTheory.CategoryStruct.comp α smallU.tp) α ⋯ = Ctx.ofGrpd.map (CategoryTheory.Grothendieck.Groupoidal.sec ((yonedaCategoryEquiv α).comp CategoryTheory.PGrpd.forgetToGrpd) (yonedaCategoryEquiv α) ⋯)

def GroupoidModel.smallU.PtpEquiv.fst {Γ : Ctx} {C : Type (v + 1)} [CategoryTheory.Category.{v, v + 1} C] (AB : CategoryTheory.yoneda.obj Γ ⟶ smallU.Ptp.obj (CategoryTheory.yoneda.obj (Ctx.ofCategory C))) : CategoryTheory.Functor (↑(Ctx.toGrpd.obj Γ)) CategoryTheory.Grpd

A map (AB : y(Γ) ⟶ smallU.{v}.Ptp.obj y(Ctx.ofCategory C)) is equivalent to a pair of functors A : Γ ⥤ Grpd and B : ∫(fst AB) ⥤ C, thought of as a dependent pair A : Type and B : A ⟶ Type when C = Grpd. PtpEquiv.fst is the A in this pair.

Equations

• GroupoidModel.smallU.PtpEquiv.fst AB = GroupoidModel.yonedaCategoryEquiv (NaturalModelBase.PtpEquiv.fst GroupoidModel.smallU AB)

def GroupoidModel.smallU.PtpEquiv.snd {Γ : Ctx} {C : Type (v + 1)} [CategoryTheory.Category.{v, v + 1} C] (AB : CategoryTheory.yoneda.obj Γ ⟶ smallU.Ptp.obj (CategoryTheory.yoneda.obj (Ctx.ofCategory C))) : CategoryTheory.Functor ∫(fst AB) C

A map (AB : y(Γ) ⟶ smallU.{v}.Ptp.obj y(Ctx.ofCategory C)) is equivalent to a pair of functors A : Γ ⥤ Grpd and B : ∫(fst AB) ⥤ C, thought of as a dependent pair A : Type and B : A ⟶ Type when C = Grpd. PtpEquiv.snd is the B in this pair.

Equations

• GroupoidModel.smallU.PtpEquiv.snd AB = GroupoidModel.yonedaCategoryEquiv (NaturalModelBase.PtpEquiv.snd GroupoidModel.smallU AB)

theorem GroupoidModel.smallU.PtpEquiv.fst_naturality {Γ : Ctx} {C : Type (v + 1)} [CategoryTheory.Category.{v, v + 1} C] {Δ : Ctx} (σ : Δ ⟶ Γ) (AB : CategoryTheory.yoneda.obj Γ ⟶ smallU.Ptp.obj (CategoryTheory.yoneda.obj (Ctx.ofCategory C))) : fst (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) AB) = CategoryTheory.Functor.comp (Ctx.toGrpd.map σ) (fst AB)

theorem GroupoidModel.smallU.PtpEquiv.snd_naturality {Γ : Ctx} {C : Type (v + 1)} [CategoryTheory.Category.{v, v + 1} C] {Δ : Ctx} (σ : Δ ⟶ Γ) (AB : CategoryTheory.yoneda.obj Γ ⟶ smallU.Ptp.obj (CategoryTheory.yoneda.obj (Ctx.ofCategory C))) : snd (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) AB) = (CategoryTheory.Grothendieck.Groupoidal.map (CategoryTheory.eqToHom ⋯)).comp ((CategoryTheory.Grothendieck.Groupoidal.pre (fst AB) (Ctx.toGrpd.map σ)).comp (snd AB))

def GroupoidModel.smallU.PtpEquiv.mk {Γ : Ctx} {C : Type (v + 1)} [CategoryTheory.Category.{v, v + 1} C] (A : CategoryTheory.Functor (↑(Ctx.toGrpd.obj Γ)) CategoryTheory.Grpd) (B : CategoryTheory.Functor ∫(A) C) : CategoryTheory.yoneda.obj Γ ⟶ smallU.Ptp.obj (CategoryTheory.yoneda.obj (Ctx.ofCategory C))

A map (AB : y(Γ) ⟶ smallU.{v}.Ptp.obj y(Ctx.ofCategory C)) is equivalent to a pair of functors A : Γ ⥤ Grpd and B : ∫(fst AB) ⥤ C, thought of as a dependent pair A : Type and B : A ⟶ Type when C = Grpd. PtpEquiv.mk constructs such a map AB from such a pair A and B.

Equations

• GroupoidModel.smallU.PtpEquiv.mk A B = NaturalModelBase.PtpEquiv.mk GroupoidModel.smallU (GroupoidModel.yonedaCategoryEquiv.symm A) (GroupoidModel.yonedaCategoryEquiv.symm B)

theorem GroupoidModel.smallU.PtpEquiv.hext {Γ : Ctx} (AB1 AB2 : CategoryTheory.yoneda.obj Γ ⟶ smallU.Ptp.obj (CategoryTheory.yoneda.obj U)) (hfst : fst AB1 = fst AB2) (hsnd : snd AB1 ≍ snd AB2) : AB1 = AB2

def GroupoidModel.smallU.compDom : CategoryTheory.Psh Ctx

Equations

• GroupoidModel.smallU.compDom = GroupoidModel.smallU.uvPolyTp.compDom GroupoidModel.smallU.uvPolyTp

def GroupoidModel.smallU.comp : compDom ⟶ smallU.Ptp.obj (CategoryTheory.yoneda.obj U)

Equations

• GroupoidModel.smallU.comp = (GroupoidModel.smallU.uvPolyTp.comp GroupoidModel.smallU.uvPolyTp).p

def GroupoidModel.smallU.compDom.fst {Γ : Ctx} (ab : CategoryTheory.yoneda.obj Γ ⟶ compDom) : CategoryTheory.Functor (↑(Ctx.toGrpd.obj Γ)) CategoryTheory.PGrpd

Universal property of compDom, decomposition (part 1).

A map ab : y(Γ) ⟶ compDom is equivalently three functors fst, dependent, snd such that snd_forgetToGrpd. The functor fst : Γ ⥤ PGrpd is (a : A) in (a : A) × (b : B a).

Equations

• GroupoidModel.smallU.compDom.fst ab = GroupoidModel.yonedaCategoryEquiv (NaturalModelBase.compDomEquiv.fst GroupoidModel.smallU ab)

def GroupoidModel.smallU.compDom.dependent {Γ : Ctx} (ab : CategoryTheory.yoneda.obj Γ ⟶ compDom) : CategoryTheory.Functor ∫((fst ab).comp CategoryTheory.PGrpd.forgetToGrpd) CategoryTheory.Grpd

Universal property of compDom, decomposition (part 2).

A map ab : y(Γ) ⟶ compDom is equivalently three functors fst, dependent, snd such that snd_forgetToGrpd. The functor dependent : Γ ⥤ Grpd is B : A → Type in (a : A) × (b : B a).

Equations

• GroupoidModel.smallU.compDom.dependent ab = GroupoidModel.yonedaCategoryEquiv (NaturalModelBase.compDomEquiv.dependent GroupoidModel.smallU ab)

def GroupoidModel.smallU.compDom.snd {Γ : Ctx} (ab : CategoryTheory.yoneda.obj Γ ⟶ compDom) : CategoryTheory.Functor (↑(Ctx.toGrpd.obj Γ)) CategoryTheory.PGrpd

Universal property of compDom, decomposition (part 3).

A map ab : y(Γ) ⟶ compDom is equivalently three functors fst, dependent, snd such that snd_forgetToGrpd. The functor snd : Γ ⥤ PGrpd is (b : B a) in (a : A) × (b : B a).

Equations

• GroupoidModel.smallU.compDom.snd ab = GroupoidModel.yonedaCategoryEquiv (NaturalModelBase.compDomEquiv.snd GroupoidModel.smallU ab)

theorem GroupoidModel.smallU.compDom.snd_forgetToGrpd {Γ : Ctx} (ab : CategoryTheory.yoneda.obj Γ ⟶ compDom) : (snd ab).comp CategoryTheory.PGrpd.forgetToGrpd = (CategoryTheory.Grothendieck.Groupoidal.sec ((fst ab).comp CategoryTheory.PGrpd.forgetToGrpd) (fst ab) ⋯).comp (dependent ab)

Universal property of compDom, decomposition (part 4).

A map ab : y(Γ) ⟶ compDom is equivalently three functors fst, dependent, snd such that snd_forgetToGrpd. The equation snd_forgetToGrpd says that the type of b : B a agrees with the expression for B a obtained solely from dependent, or B : A ⟶ Type.

def GroupoidModel.smallU.compDom.mk {Γ : Ctx} (α : CategoryTheory.Functor (↑(Ctx.toGrpd.obj Γ)) CategoryTheory.PGrpd) (B : CategoryTheory.Functor ∫(α.comp CategoryTheory.PGrpd.forgetToGrpd) CategoryTheory.Grpd) (β : CategoryTheory.Functor (↑(Ctx.toGrpd.obj Γ)) CategoryTheory.PGrpd) (h : β.comp CategoryTheory.PGrpd.forgetToGrpd = (CategoryTheory.Grothendieck.Groupoidal.sec (α.comp CategoryTheory.PGrpd.forgetToGrpd) α ⋯).comp B) : CategoryTheory.yoneda.obj Γ ⟶ compDom

Universal property of compDom, constructing a map into compDom.

Equations

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

theorem GroupoidModel.smallU.compDom.fst_forgetToGrpd {Γ : Ctx} (ab : CategoryTheory.yoneda.obj Γ ⟶ compDom) : (fst ab).comp CategoryTheory.PGrpd.forgetToGrpd = PtpEquiv.fst (CategoryTheory.CategoryStruct.comp ab comp)

theorem GroupoidModel.smallU.compDom.dependent_eq {Γ : Ctx} (ab : CategoryTheory.yoneda.obj Γ ⟶ compDom) : dependent ab = (CategoryTheory.Grothendieck.Groupoidal.map (CategoryTheory.eqToHom ⋯)).comp (PtpEquiv.snd (CategoryTheory.CategoryStruct.comp ab comp))

theorem GroupoidModel.smallU.compDom.dependent_heq {Γ : Ctx} (ab : CategoryTheory.yoneda.obj Γ ⟶ compDom) : dependent ab ≍ PtpEquiv.snd (CategoryTheory.CategoryStruct.comp ab comp)

theorem GroupoidModel.smallU.compDom.fst_naturality {Γ Δ : Ctx} (σ : Δ ⟶ Γ) (ab : CategoryTheory.yoneda.obj Γ ⟶ compDom) : fst (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) ab) = CategoryTheory.Functor.comp (Ctx.toGrpd.map σ) (fst ab)

theorem GroupoidModel.smallU.compDom.dependent_naturality {Γ Δ : Ctx} (σ : Δ ⟶ Γ) (ab : CategoryTheory.yoneda.obj Γ ⟶ compDom) : dependent (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) ab) = (CategoryTheory.Grothendieck.Groupoidal.map (CategoryTheory.eqToHom ⋯)).comp ((CategoryTheory.Grothendieck.Groupoidal.pre ((fst ab).comp CategoryTheory.PGrpd.forgetToGrpd) (Ctx.toGrpd.map σ)).comp (dependent ab))

theorem GroupoidModel.smallU.compDom.snd_naturality {Γ Δ : Ctx} (σ : Δ ⟶ Γ) (ab : CategoryTheory.yoneda.obj Γ ⟶ compDom) : snd (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) ab) = CategoryTheory.Functor.comp (Ctx.toGrpd.map σ) (snd ab)

theorem GroupoidModel.smallU.compDom.fst_mk {Γ : Ctx} (α : CategoryTheory.Functor (↑(Ctx.toGrpd.obj Γ)) CategoryTheory.PGrpd) (B : CategoryTheory.Functor ∫(α.comp CategoryTheory.PGrpd.forgetToGrpd) CategoryTheory.Grpd) (β : CategoryTheory.Functor (↑(Ctx.toGrpd.obj Γ)) CategoryTheory.PGrpd) (h : β.comp CategoryTheory.PGrpd.forgetToGrpd = (CategoryTheory.Grothendieck.Groupoidal.sec (α.comp CategoryTheory.PGrpd.forgetToGrpd) α ⋯).comp B) : fst (mk α B β h) = α

First component of the computation rule for mk.

theorem GroupoidModel.smallU.compDom.dependent_mk {Γ : Ctx} (α : CategoryTheory.Functor (↑(Ctx.toGrpd.obj Γ)) CategoryTheory.PGrpd) (B : CategoryTheory.Functor ∫(α.comp CategoryTheory.PGrpd.forgetToGrpd) CategoryTheory.Grpd) (β : CategoryTheory.Functor (↑(Ctx.toGrpd.obj Γ)) CategoryTheory.PGrpd) (h : β.comp CategoryTheory.PGrpd.forgetToGrpd = (CategoryTheory.Grothendieck.Groupoidal.sec (α.comp CategoryTheory.PGrpd.forgetToGrpd) α ⋯).comp B) : dependent (mk α B β h) = (CategoryTheory.Grothendieck.Groupoidal.map (CategoryTheory.eqToHom ⋯)).comp B

Second component of the computation rule for mk.

theorem GroupoidModel.smallU.compDom.snd_mk {Γ : Ctx} (α : CategoryTheory.Functor (↑(Ctx.toGrpd.obj Γ)) CategoryTheory.PGrpd) (B : CategoryTheory.Functor ∫(α.comp CategoryTheory.PGrpd.forgetToGrpd) CategoryTheory.Grpd) (β : CategoryTheory.Functor (↑(Ctx.toGrpd.obj Γ)) CategoryTheory.PGrpd) (h : β.comp CategoryTheory.PGrpd.forgetToGrpd = (CategoryTheory.Grothendieck.Groupoidal.sec (α.comp CategoryTheory.PGrpd.forgetToGrpd) α ⋯).comp B) : snd (mk α B β h) = β

Second component of the computation rule for mk.

theorem GroupoidModel.smallU.compDom.smallU.compDom.hext {Γ : Ctx} (ab1 ab2 : CategoryTheory.yoneda.obj Γ ⟶ compDom) (hfst : fst ab1 = fst ab2) (hdependent : dependent ab1 ≍ dependent ab2) (hsnd : snd ab1 = snd ab2) : ab1 = ab2