@[reducible]

def GroupoidModel.FunctorOperation.sigmaObj {Γ : Type u₂} [CategoryTheory.Category.{v₂, u₂} Γ] {A : CategoryTheory.Functor Γ CategoryTheory.Grpd} (B : CategoryTheory.Functor ∫(A) CategoryTheory.Grpd) (x : Γ) : Type u₁

For a point x : Γ, (sigma A B).obj x is the groupoidal Grothendieck construction on the composition ι _ x ⋙ B : A.obj x ⥤ Groupoidal A ⥤ Grpd

Equations

• GroupoidModel.FunctorOperation.sigmaObj B x = ∫((CategoryTheory.Grothendieck.Groupoidal.ι A x).comp B)

def GroupoidModel.FunctorOperation.sigmaMap {Γ : Type u₂} [CategoryTheory.Category.{v₂, u₂} Γ] {A : CategoryTheory.Functor Γ CategoryTheory.Grpd} (B : CategoryTheory.Functor ∫(A) CategoryTheory.Grpd) {x y : Γ} (f : x ⟶ y) : CategoryTheory.Functor (sigmaObj B x) (sigmaObj B y)

For a morphism f : x ⟶ y in Γ, (sigma A B).map y is a composition of functors. The first functor map (whiskerRight (ιNatTrans f) B) is an equivalence which replaces ι A x with the naturally isomorphic A.map f ⋙ ι A y. The second functor is the action of precomposing A.map f with ι A y ⋙ B on the Grothendieck constructions.

        map ⋯                  pre ⋯

∫ ι A x ⋙ B ⥤ ∫ A.map f ⋙ ι A y ⋙ B ⥤ ∫ ι A y ⋙ B

Equations

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

@[simp]

theorem GroupoidModel.FunctorOperation.sigmaMap_obj_base {Γ : Type u₂} [CategoryTheory.Category.{v₂, u₂} Γ] {A : CategoryTheory.Functor Γ CategoryTheory.Grpd} (B : CategoryTheory.Functor ∫(A) CategoryTheory.Grpd) {x y : Γ} (f : x ⟶ y) (a : sigmaObj B x) : CategoryTheory.Grothendieck.Groupoidal.base ((sigmaMap B f).obj a) = (A.map f).obj (CategoryTheory.Grothendieck.Groupoidal.base a)

@[simp]

theorem GroupoidModel.FunctorOperation.sigmaMap_obj_fiber {Γ : Type u₂} [CategoryTheory.Category.{v₂, u₂} Γ] {A : CategoryTheory.Functor Γ CategoryTheory.Grpd} (B : CategoryTheory.Functor ∫(A) CategoryTheory.Grpd) {x y : Γ} (f : x ⟶ y) (a : sigmaObj B x) : CategoryTheory.Grothendieck.Groupoidal.fiber ((sigmaMap B f).obj a) = (B.map ((CategoryTheory.Grothendieck.Groupoidal.ιNatTrans f).app (CategoryTheory.Grothendieck.Groupoidal.base a))).obj (CategoryTheory.Grothendieck.Groupoidal.fiber a)

@[simp]

theorem GroupoidModel.FunctorOperation.sigmaMap_map_base {Γ : Type u₂} [CategoryTheory.Category.{v₂, u₂} Γ] {A : CategoryTheory.Functor Γ CategoryTheory.Grpd} (B : CategoryTheory.Functor ∫(A) CategoryTheory.Grpd) {x y : Γ} (f : x ⟶ y) {a b : sigmaObj B x} {p : a ⟶ b} : CategoryTheory.Grothendieck.Groupoidal.Hom.base ((sigmaMap B f).map p) = (A.map f).map (CategoryTheory.Grothendieck.Groupoidal.Hom.base p)

theorem GroupoidModel.FunctorOperation.sigmaMap_map_fiber_aux {Γ : Type u₂} [CategoryTheory.Category.{v₂, u₂} Γ] {A : CategoryTheory.Functor Γ CategoryTheory.Grpd} (B : CategoryTheory.Functor ∫(A) CategoryTheory.Grpd) {x y : Γ} (f : x ⟶ y) {a b : sigmaObj B x} {p : a ⟶ b} : (((CategoryTheory.Grothendieck.Groupoidal.ι A y).comp B).map (CategoryTheory.Grothendieck.Groupoidal.Hom.base ((sigmaMap B f).map p))).obj (CategoryTheory.Grothendieck.Groupoidal.fiber ((sigmaMap B f).obj a)) = (B.map ((CategoryTheory.Grothendieck.Groupoidal.ιNatTrans f).app (CategoryTheory.Grothendieck.Groupoidal.base b))).obj ((((CategoryTheory.Grothendieck.Groupoidal.ι A x).comp B).map (CategoryTheory.Grothendieck.Groupoidal.Hom.base p)).obj (CategoryTheory.Grothendieck.Groupoidal.fiber a))

@[simp]

theorem GroupoidModel.FunctorOperation.sigmaMap_map_fiber {Γ : Type u₂} [CategoryTheory.Category.{v₂, u₂} Γ] {A : CategoryTheory.Functor Γ CategoryTheory.Grpd} (B : CategoryTheory.Functor ∫(A) CategoryTheory.Grpd) {x y : Γ} (f : x ⟶ y) {a b : sigmaObj B x} {p : a ⟶ b} : CategoryTheory.Grothendieck.Groupoidal.Hom.fiber ((sigmaMap B f).map p) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) ((B.map ((CategoryTheory.Grothendieck.Groupoidal.ιNatTrans f).app (CategoryTheory.Grothendieck.Groupoidal.base b))).map (CategoryTheory.Grothendieck.Groupoidal.Hom.fiber p))

@[simp]

theorem GroupoidModel.FunctorOperation.sigmaMap_id_obj {Γ : Type u₂} [CategoryTheory.Category.{v₂, u₂} Γ] {A : CategoryTheory.Functor Γ CategoryTheory.Grpd} {B : CategoryTheory.Functor ∫(A) CategoryTheory.Grpd} {x : Γ} {p : sigmaObj B x} : (sigmaMap B (CategoryTheory.CategoryStruct.id x)).obj p = p

@[simp]

theorem GroupoidModel.FunctorOperation.sigmaMap_id_map {Γ : Type u₂} [CategoryTheory.Category.{v₂, u₂} Γ] {A : CategoryTheory.Functor Γ CategoryTheory.Grpd} {B : CategoryTheory.Functor ∫(A) CategoryTheory.Grpd} {x : Γ} {p1 p2 : sigmaObj B x} {hp2 : p2 = (sigmaMap B (CategoryTheory.CategoryStruct.id x)).obj p2} (f : p1 ⟶ p2) : (sigmaMap B (CategoryTheory.CategoryStruct.id x)).map f = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp f (CategoryTheory.eqToHom ⋯))

theorem GroupoidModel.FunctorOperation.sigmaMap_id {Γ : Type u₂} [CategoryTheory.Category.{v₂, u₂} Γ] {A : CategoryTheory.Functor Γ CategoryTheory.Grpd} {B : CategoryTheory.Functor ∫(A) CategoryTheory.Grpd} {x : Γ} : sigmaMap B (CategoryTheory.CategoryStruct.id x) = CategoryTheory.Functor.id (sigmaObj B x)

@[simp]

theorem GroupoidModel.FunctorOperation.sigmaMap_comp_obj {Γ : Type u₂} [CategoryTheory.Category.{v₂, u₂} Γ] {A : CategoryTheory.Functor Γ CategoryTheory.Grpd} {B : CategoryTheory.Functor ∫(A) CategoryTheory.Grpd} {x y : Γ} {f : x ⟶ y} {z : Γ} {g : y ⟶ z} {p : sigmaObj B x} : (sigmaMap B (CategoryTheory.CategoryStruct.comp f g)).obj p = (sigmaMap B g).obj ((sigmaMap B f).obj p)

@[simp]

theorem GroupoidModel.FunctorOperation.sigmaMap_comp_map {Γ : Type u₂} [CategoryTheory.Category.{v₂, u₂} Γ] {A : CategoryTheory.Functor Γ CategoryTheory.Grpd} {B : CategoryTheory.Functor ∫(A) CategoryTheory.Grpd} {x y z : Γ} {f : x ⟶ y} {g : y ⟶ z} {p q : sigmaObj B x} (hpq : p ⟶ q) {h1 : (sigmaMap B (CategoryTheory.CategoryStruct.comp f g)).obj p = (sigmaMap B g).obj ((sigmaMap B f).obj p)} {h2 : (sigmaMap B g).obj ((sigmaMap B f).obj q) = (sigmaMap B (CategoryTheory.CategoryStruct.comp f g)).obj q} : (sigmaMap B (CategoryTheory.CategoryStruct.comp f g)).map hpq = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h1) (CategoryTheory.CategoryStruct.comp ((sigmaMap B g).map ((sigmaMap B f).map hpq)) (CategoryTheory.eqToHom h2))

theorem GroupoidModel.FunctorOperation.sigmaMap_comp {Γ : Type u₂} [CategoryTheory.Category.{v₂, u₂} Γ] {A : CategoryTheory.Functor Γ CategoryTheory.Grpd} {B : CategoryTheory.Functor ∫(A) CategoryTheory.Grpd} {x y : Γ} {f : x ⟶ y} {z : Γ} {g : y ⟶ z} : sigmaMap B (CategoryTheory.CategoryStruct.comp f g) = (sigmaMap B f).comp (sigmaMap B g)

theorem GroupoidModel.FunctorOperation.sigmaMap_forget {Γ : Type u₂} [CategoryTheory.Category.{v₂, u₂} Γ] {A : CategoryTheory.Functor Γ CategoryTheory.Grpd} {B : CategoryTheory.Functor ∫(A) CategoryTheory.Grpd} {x y : Γ} {f : x ⟶ y} : (sigmaMap B f).comp CategoryTheory.Grothendieck.Groupoidal.forget = CategoryTheory.Grothendieck.Groupoidal.forget.comp (A.map f)

def GroupoidModel.FunctorOperation.sigma {Γ : Type u₂} [CategoryTheory.Category.{v₂, u₂} Γ] (A : CategoryTheory.Functor Γ CategoryTheory.Grpd) (B : CategoryTheory.Functor ∫(A) CategoryTheory.Grpd) : CategoryTheory.Functor Γ CategoryTheory.Grpd

The formation rule for Σ-types for the ambient natural model base unfolded into operations between functors. See sigmaObj and sigmaMap for the actions of this functor.

Equations

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

@[simp]

theorem GroupoidModel.FunctorOperation.sigma_obj {Γ : Type u₂} [CategoryTheory.Category.{v₂, u₂} Γ] (A : CategoryTheory.Functor Γ CategoryTheory.Grpd) (B : CategoryTheory.Functor ∫(A) CategoryTheory.Grpd) (x : Γ) : (sigma A B).obj x = CategoryTheory.Grpd.of (sigmaObj B x)

@[simp]

theorem GroupoidModel.FunctorOperation.sigma_map {Γ : Type u₂} [CategoryTheory.Category.{v₂, u₂} Γ] (A : CategoryTheory.Functor Γ CategoryTheory.Grpd) (B : CategoryTheory.Functor ∫(A) CategoryTheory.Grpd) {X✝ Y✝ : Γ} (f : X✝ ⟶ Y✝) : (sigma A B).map f = sigmaMap B f

theorem GroupoidModel.FunctorOperation.sigma_naturality_aux {Γ : Type u₂} [CategoryTheory.Category.{v₂, u₂} Γ] {A : CategoryTheory.Functor Γ CategoryTheory.Grpd} (B : CategoryTheory.Functor ∫(A) CategoryTheory.Grpd) {Δ : Type u₃} [CategoryTheory.Category.{v₃, u₃} Δ] (σ : CategoryTheory.Functor Δ Γ) (x : Δ) : (CategoryTheory.Grothendieck.Groupoidal.ι (σ.comp A) x).comp ((CategoryTheory.Grothendieck.Groupoidal.pre A σ).comp B) = (CategoryTheory.Grothendieck.Groupoidal.ι A (σ.obj x)).comp B

theorem GroupoidModel.FunctorOperation.whiskerRight_ιNatTrans_naturality {Γ : Type u₂} [CategoryTheory.Category.{v₂, u₂} Γ] {A : CategoryTheory.Functor Γ CategoryTheory.Grpd} (B : CategoryTheory.Functor ∫(A) CategoryTheory.Grpd) {Δ : Type u₃} [CategoryTheory.Category.{v₃, u₃} Δ] (σ : CategoryTheory.Functor Δ Γ) {x y : Δ} (f : x ⟶ y) : CategoryTheory.Functor.whiskerRight (CategoryTheory.Grothendieck.Groupoidal.ιNatTrans f) ((CategoryTheory.Grothendieck.Groupoidal.pre A σ).comp B) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (CategoryTheory.Grothendieck.Groupoidal.ιNatTrans (σ.map f)) B) (CategoryTheory.eqToHom ⋯))

theorem GroupoidModel.FunctorOperation.sigma_naturality_obj {Γ : Type u₂} [CategoryTheory.Category.{v₂, u₂} Γ] {A : CategoryTheory.Functor Γ CategoryTheory.Grpd} (B : CategoryTheory.Functor ∫(A) CategoryTheory.Grpd) {Δ : Type u₃} [CategoryTheory.Category.{v₃, u₃} Δ] (σ : CategoryTheory.Functor Δ Γ) (x : Δ) : (σ.comp (sigma A B)).obj x = (sigma (σ.comp A) ((CategoryTheory.Grothendieck.Groupoidal.pre A σ).comp B)).obj x

theorem GroupoidModel.FunctorOperation.sigma_naturality {Γ : Type u₂} [CategoryTheory.Category.{v₂, u₂} Γ] {A : CategoryTheory.Functor Γ CategoryTheory.Grpd} (B : CategoryTheory.Functor ∫(A) CategoryTheory.Grpd) {Δ : Type u₃} [CategoryTheory.Category.{v₃, u₃} Δ] (σ : CategoryTheory.Functor Δ Γ) : σ.comp (sigma A B) = sigma (σ.comp A) ((CategoryTheory.Grothendieck.Groupoidal.pre A σ).comp B)

def GroupoidModel.FunctorOperation.pairObjFiber {Γ : Type u₂} [CategoryTheory.Category.{v₂, u₂} Γ] {α β : CategoryTheory.Functor Γ CategoryTheory.PGrpd} {B : CategoryTheory.Functor ∫(α.comp CategoryTheory.PGrpd.forgetToGrpd) CategoryTheory.Grpd} (h : β.comp CategoryTheory.PGrpd.forgetToGrpd = (CategoryTheory.Grothendieck.Groupoidal.sec (α.comp CategoryTheory.PGrpd.forgetToGrpd) α ⋯).comp B) (x : Γ) : sigmaObj B x

Equations

• GroupoidModel.FunctorOperation.pairObjFiber h x = CategoryTheory.Grothendieck.Groupoidal.objMk (CategoryTheory.PGrpd.objFiber α x) (CategoryTheory.PGrpd.objFiber' h x)

@[simp]

theorem GroupoidModel.FunctorOperation.pairObjFiber_base {Γ : Type u₂} [CategoryTheory.Category.{v₂, u₂} Γ] {α β : CategoryTheory.Functor Γ CategoryTheory.PGrpd} {B : CategoryTheory.Functor ∫(α.comp CategoryTheory.PGrpd.forgetToGrpd) CategoryTheory.Grpd} (h : β.comp CategoryTheory.PGrpd.forgetToGrpd = (CategoryTheory.Grothendieck.Groupoidal.sec (α.comp CategoryTheory.PGrpd.forgetToGrpd) α ⋯).comp B) (x : Γ) : CategoryTheory.Grothendieck.Groupoidal.base (pairObjFiber h x) = CategoryTheory.PGrpd.objFiber α x

@[simp]

theorem GroupoidModel.FunctorOperation.pairObjFiber_fiber {Γ : Type u₂} [CategoryTheory.Category.{v₂, u₂} Γ] {α β : CategoryTheory.Functor Γ CategoryTheory.PGrpd} {B : CategoryTheory.Functor ∫(α.comp CategoryTheory.PGrpd.forgetToGrpd) CategoryTheory.Grpd} (h : β.comp CategoryTheory.PGrpd.forgetToGrpd = (CategoryTheory.Grothendieck.Groupoidal.sec (α.comp CategoryTheory.PGrpd.forgetToGrpd) α ⋯).comp B) (x : Γ) : CategoryTheory.Grothendieck.Groupoidal.fiber (pairObjFiber h x) = CategoryTheory.PGrpd.objFiber' h x

theorem GroupoidModel.FunctorOperation.pairSectionMap_aux_aux {Γ : Type u₂} [CategoryTheory.Category.{v₂, u₂} Γ] {α β : CategoryTheory.Functor Γ CategoryTheory.PGrpd} {B : CategoryTheory.Functor ∫(α.comp CategoryTheory.PGrpd.forgetToGrpd) CategoryTheory.Grpd} (h : β.comp CategoryTheory.PGrpd.forgetToGrpd = (CategoryTheory.Grothendieck.Groupoidal.sec (α.comp CategoryTheory.PGrpd.forgetToGrpd) α ⋯).comp B) {x y : Γ} (f : x ⟶ y) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.Grothendieck.Groupoidal.ιNatTrans f).app (CategoryTheory.Grothendieck.Groupoidal.base (pairObjFiber h x))) ((CategoryTheory.Grothendieck.Groupoidal.ι (α.comp CategoryTheory.PGrpd.forgetToGrpd) y).map (CategoryTheory.PGrpd.mapFiber α f)) = (CategoryTheory.Grothendieck.Groupoidal.sec (α.comp CategoryTheory.PGrpd.forgetToGrpd) α ⋯).map f

theorem GroupoidModel.FunctorOperation.pairMapFiber_aux {Γ : Type u₂} [CategoryTheory.Category.{v₂, u₂} Γ] {α β : CategoryTheory.Functor Γ CategoryTheory.PGrpd} {B : CategoryTheory.Functor ∫(α.comp CategoryTheory.PGrpd.forgetToGrpd) CategoryTheory.Grpd} (h : β.comp CategoryTheory.PGrpd.forgetToGrpd = (CategoryTheory.Grothendieck.Groupoidal.sec (α.comp CategoryTheory.PGrpd.forgetToGrpd) α ⋯).comp B) {x y : Γ} (f : x ⟶ y) : (((CategoryTheory.Grothendieck.Groupoidal.ι (α.comp CategoryTheory.PGrpd.forgetToGrpd) y).comp B).map (CategoryTheory.PGrpd.mapFiber α f)).obj (CategoryTheory.Grothendieck.Groupoidal.fiber ((sigmaMap B f).obj (pairObjFiber h x))) = (((CategoryTheory.Grothendieck.Groupoidal.sec (α.comp CategoryTheory.PGrpd.forgetToGrpd) α ⋯).comp B).map f).obj (CategoryTheory.PGrpd.objFiber' h x)

The left hand side mapPairSectionObjFiber h f is an object in the fiber sigma A B y over y The fiber itself consists of bundles, so (mapPairSectionObjFiber h f).fiber is an object in the fiber B a for an a in the fiber A y. But this a is isomorphic to (pairSectionObjFiber y).base and the functor (ι _ y ⋙ B).map (mapPoint α f) converts the data along this isomorphism.

The right hand side is (*) in the diagram. sec α B Γ -------> ∫(A) ------------> Grpd

x (B ⋙ sec α).obj x objPt' h x | f (B ⋙ sec α).map f | - V V | y (B ⋙ sec α).obj y V (*)

def GroupoidModel.FunctorOperation.pairMapFiber {Γ : Type u₂} [CategoryTheory.Category.{v₂, u₂} Γ] {α β : CategoryTheory.Functor Γ CategoryTheory.PGrpd} {B : CategoryTheory.Functor ∫(α.comp CategoryTheory.PGrpd.forgetToGrpd) CategoryTheory.Grpd} (h : β.comp CategoryTheory.PGrpd.forgetToGrpd = (CategoryTheory.Grothendieck.Groupoidal.sec (α.comp CategoryTheory.PGrpd.forgetToGrpd) α ⋯).comp B) {x y : Γ} (f : x ⟶ y) : (sigmaMap B f).obj (pairObjFiber h x) ⟶ pairObjFiber h y

This can be thought of as the action of parallel transport on f or perhaps the path over f, but defined within the fiber over y

sigma A B x ∋ pairObjFiber h x
sigma A B f
V V
sigma A B y ∋ PairMapFiber

                       _ ⟶ pairObjFiber h y

Equations

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

@[simp]

theorem GroupoidModel.FunctorOperation.pairMapFiber_base {Γ : Type u₂} [CategoryTheory.Category.{v₂, u₂} Γ] {α β : CategoryTheory.Functor Γ CategoryTheory.PGrpd} {B : CategoryTheory.Functor ∫(α.comp CategoryTheory.PGrpd.forgetToGrpd) CategoryTheory.Grpd} (h : β.comp CategoryTheory.PGrpd.forgetToGrpd = (CategoryTheory.Grothendieck.Groupoidal.sec (α.comp CategoryTheory.PGrpd.forgetToGrpd) α ⋯).comp B) {x y : Γ} (f : x ⟶ y) : CategoryTheory.Grothendieck.Groupoidal.Hom.base (pairMapFiber h f) = CategoryTheory.PGrpd.mapFiber α f

@[simp]

theorem GroupoidModel.FunctorOperation.pairMapFiber_fiber {Γ : Type u₂} [CategoryTheory.Category.{v₂, u₂} Γ] {α β : CategoryTheory.Functor Γ CategoryTheory.PGrpd} {B : CategoryTheory.Functor ∫(α.comp CategoryTheory.PGrpd.forgetToGrpd) CategoryTheory.Grpd} (h : β.comp CategoryTheory.PGrpd.forgetToGrpd = (CategoryTheory.Grothendieck.Groupoidal.sec (α.comp CategoryTheory.PGrpd.forgetToGrpd) α ⋯).comp B) {x y : Γ} (f : x ⟶ y) : CategoryTheory.Grothendieck.Groupoidal.Hom.fiber (pairMapFiber h f) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.PGrpd.mapFiber' h f)

theorem GroupoidModel.FunctorOperation.pairMapFiber_id {Γ : Type u₂} [CategoryTheory.Category.{v₂, u₂} Γ] {α β : CategoryTheory.Functor Γ CategoryTheory.PGrpd} {B : CategoryTheory.Functor ∫(α.comp CategoryTheory.PGrpd.forgetToGrpd) CategoryTheory.Grpd} (h : β.comp CategoryTheory.PGrpd.forgetToGrpd = (CategoryTheory.Grothendieck.Groupoidal.sec (α.comp CategoryTheory.PGrpd.forgetToGrpd) α ⋯).comp B) (x : Γ) : pairMapFiber h (CategoryTheory.CategoryStruct.id x) = CategoryTheory.eqToHom ⋯

theorem GroupoidModel.FunctorOperation.pairMapFiber_comp_aux_aux {Γ : Type u₂} [CategoryTheory.Category.{v₂, u₂} Γ] {α β : CategoryTheory.Functor Γ CategoryTheory.PGrpd} {B : CategoryTheory.Functor ∫(α.comp CategoryTheory.PGrpd.forgetToGrpd) CategoryTheory.Grpd} (h : β.comp CategoryTheory.PGrpd.forgetToGrpd = (CategoryTheory.Grothendieck.Groupoidal.sec (α.comp CategoryTheory.PGrpd.forgetToGrpd) α ⋯).comp B) {x y z : Γ} (f : x ⟶ y) (g : y ⟶ z) : (((CategoryTheory.Grothendieck.Groupoidal.ι (α.comp CategoryTheory.PGrpd.forgetToGrpd) z).comp B).map (CategoryTheory.PGrpd.mapFiber α g)).obj ((((CategoryTheory.Grothendieck.Groupoidal.ι (α.comp CategoryTheory.PGrpd.forgetToGrpd) z).comp (B.comp CategoryTheory.Grpd.forgetToCat)).map (CategoryTheory.Grothendieck.Groupoidal.Hom.base ((sigmaMap B g).map (pairMapFiber h f)))).obj (CategoryTheory.Grothendieck.Groupoidal.fiber ((sigmaMap B g).obj ((sigmaMap B f).obj (pairObjFiber h x))))) = (CategoryTheory.CategoryStruct.comp (((CategoryTheory.Grothendieck.Groupoidal.sec (α.comp CategoryTheory.PGrpd.forgetToGrpd) α ⋯).comp B).map f) (((CategoryTheory.Grothendieck.Groupoidal.sec (α.comp CategoryTheory.PGrpd.forgetToGrpd) α ⋯).comp B).map g)).obj (CategoryTheory.PGrpd.objFiber' h x)

theorem GroupoidModel.FunctorOperation.pairMapFiber_comp_aux {Γ : Type u₂} [CategoryTheory.Category.{v₂, u₂} Γ] {α β : CategoryTheory.Functor Γ CategoryTheory.PGrpd} {B : CategoryTheory.Functor ∫(α.comp CategoryTheory.PGrpd.forgetToGrpd) CategoryTheory.Grpd} (h : β.comp CategoryTheory.PGrpd.forgetToGrpd = (CategoryTheory.Grothendieck.Groupoidal.sec (α.comp CategoryTheory.PGrpd.forgetToGrpd) α ⋯).comp B) {x y z : Γ} (f : x ⟶ y) (g : y ⟶ z) : (((CategoryTheory.Grothendieck.Groupoidal.ι (α.comp CategoryTheory.PGrpd.forgetToGrpd) z).comp B).map (CategoryTheory.PGrpd.mapFiber α g)).map (CategoryTheory.Grothendieck.Groupoidal.Hom.fiber ((sigmaMap B g).map (pairMapFiber h f))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((((CategoryTheory.Grothendieck.Groupoidal.sec (α.comp CategoryTheory.PGrpd.forgetToGrpd) α ⋯).comp B).map g).map (CategoryTheory.PGrpd.mapFiber' h f)) (CategoryTheory.eqToHom ⋯))

theorem GroupoidModel.FunctorOperation.pairMapFiber_comp {Γ : Type u₂} [CategoryTheory.Category.{v₂, u₂} Γ] {α β : CategoryTheory.Functor Γ CategoryTheory.PGrpd} {B : CategoryTheory.Functor ∫(α.comp CategoryTheory.PGrpd.forgetToGrpd) CategoryTheory.Grpd} (h : β.comp CategoryTheory.PGrpd.forgetToGrpd = (CategoryTheory.Grothendieck.Groupoidal.sec (α.comp CategoryTheory.PGrpd.forgetToGrpd) α ⋯).comp B) {x y z : Γ} (f : x ⟶ y) (g : y ⟶ z) : pairMapFiber h (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (((sigma (α.comp CategoryTheory.PGrpd.forgetToGrpd) B).map g).map (pairMapFiber h f)) (pairMapFiber h g))

def GroupoidModel.FunctorOperation.pair {Γ : Type u₂} [CategoryTheory.Category.{v₂, u₂} Γ] (α β : CategoryTheory.Functor Γ CategoryTheory.PGrpd) (B : CategoryTheory.Functor ∫(α.comp CategoryTheory.PGrpd.forgetToGrpd) CategoryTheory.Grpd) (h : β.comp CategoryTheory.PGrpd.forgetToGrpd = (CategoryTheory.Grothendieck.Groupoidal.sec (α.comp CategoryTheory.PGrpd.forgetToGrpd) α ⋯).comp B) : CategoryTheory.Functor Γ CategoryTheory.PGrpd

Equations

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

@[simp]

theorem GroupoidModel.FunctorOperation.pair_obj_base {Γ : Type u₂} [CategoryTheory.Category.{v₂, u₂} Γ] {α β : CategoryTheory.Functor Γ CategoryTheory.PGrpd} {B : CategoryTheory.Functor ∫(α.comp CategoryTheory.PGrpd.forgetToGrpd) CategoryTheory.Grpd} (h : β.comp CategoryTheory.PGrpd.forgetToGrpd = (CategoryTheory.Grothendieck.Groupoidal.sec (α.comp CategoryTheory.PGrpd.forgetToGrpd) α ⋯).comp B) (x : Γ) : ↑((pair α β B h).obj x).base = ∫((CategoryTheory.Grothendieck.Groupoidal.ι (α.comp CategoryTheory.PGrpd.forgetToGrpd) x).comp B)

@[simp]

theorem GroupoidModel.FunctorOperation.pair_obj_fiber {Γ : Type u₂} [CategoryTheory.Category.{v₂, u₂} Γ] {α β : CategoryTheory.Functor Γ CategoryTheory.PGrpd} {B : CategoryTheory.Functor ∫(α.comp CategoryTheory.PGrpd.forgetToGrpd) CategoryTheory.Grpd} (h : β.comp CategoryTheory.PGrpd.forgetToGrpd = (CategoryTheory.Grothendieck.Groupoidal.sec (α.comp CategoryTheory.PGrpd.forgetToGrpd) α ⋯).comp B) (x : Γ) : ((pair α β B h).obj x).fiber = pairObjFiber h x

@[simp]

theorem GroupoidModel.FunctorOperation.pair_map_base {Γ : Type u₂} [CategoryTheory.Category.{v₂, u₂} Γ] {α β : CategoryTheory.Functor Γ CategoryTheory.PGrpd} {B : CategoryTheory.Functor ∫(α.comp CategoryTheory.PGrpd.forgetToGrpd) CategoryTheory.Grpd} (h : β.comp CategoryTheory.PGrpd.forgetToGrpd = (CategoryTheory.Grothendieck.Groupoidal.sec (α.comp CategoryTheory.PGrpd.forgetToGrpd) α ⋯).comp B) {x y : Γ} (f : x ⟶ y) : ((pair α β B h).map f).base = sigmaMap B f

@[simp]

theorem GroupoidModel.FunctorOperation.pair_map_fiber {Γ : Type u₂} [CategoryTheory.Category.{v₂, u₂} Γ] {α β : CategoryTheory.Functor Γ CategoryTheory.PGrpd} {B : CategoryTheory.Functor ∫(α.comp CategoryTheory.PGrpd.forgetToGrpd) CategoryTheory.Grpd} (h : β.comp CategoryTheory.PGrpd.forgetToGrpd = (CategoryTheory.Grothendieck.Groupoidal.sec (α.comp CategoryTheory.PGrpd.forgetToGrpd) α ⋯).comp B) {x y : Γ} (f : x ⟶ y) : ((pair α β B h).map f).fiber = pairMapFiber h f

@[simp]

theorem GroupoidModel.FunctorOperation.pair_comp_forgetToGrpd {Γ : Type u₂} [CategoryTheory.Category.{v₂, u₂} Γ] {α β : CategoryTheory.Functor Γ CategoryTheory.PGrpd} {B : CategoryTheory.Functor ∫(α.comp CategoryTheory.PGrpd.forgetToGrpd) CategoryTheory.Grpd} (h : β.comp CategoryTheory.PGrpd.forgetToGrpd = (CategoryTheory.Grothendieck.Groupoidal.sec (α.comp CategoryTheory.PGrpd.forgetToGrpd) α ⋯).comp B) : (pair α β B h).comp CategoryTheory.PGrpd.forgetToGrpd = sigma (α.comp CategoryTheory.PGrpd.forgetToGrpd) B

theorem GroupoidModel.FunctorOperation.pair_naturality_aux {Γ : Type u₂} [CategoryTheory.Category.{v₂, u₂} Γ] {α β : CategoryTheory.Functor Γ CategoryTheory.PGrpd} {B : CategoryTheory.Functor ∫(α.comp CategoryTheory.PGrpd.forgetToGrpd) CategoryTheory.Grpd} (h : β.comp CategoryTheory.PGrpd.forgetToGrpd = (CategoryTheory.Grothendieck.Groupoidal.sec (α.comp CategoryTheory.PGrpd.forgetToGrpd) α ⋯).comp B) {Δ : Type u₃} [CategoryTheory.Category.{v₃, u₃} Δ] (σ : CategoryTheory.Functor Δ Γ) : (σ.comp β).comp CategoryTheory.PGrpd.forgetToGrpd = (CategoryTheory.Grothendieck.Groupoidal.sec ((σ.comp α).comp CategoryTheory.PGrpd.forgetToGrpd) (σ.comp α) ⋯).comp ((CategoryTheory.Grothendieck.Groupoidal.pre (α.comp CategoryTheory.PGrpd.forgetToGrpd) σ).comp B)

theorem GroupoidModel.FunctorOperation.pair_naturality_ι_pre {Γ : Type u₂} [CategoryTheory.Category.{v₂, u₂} Γ] {α : CategoryTheory.Functor Γ CategoryTheory.PGrpd} {Δ : Type u₃} [CategoryTheory.Category.{v₃, u₃} Δ] (σ : CategoryTheory.Functor Δ Γ) (x : Δ) : (CategoryTheory.Grothendieck.Groupoidal.ι ((σ.comp α).comp CategoryTheory.PGrpd.forgetToGrpd) x).comp (CategoryTheory.Grothendieck.Groupoidal.pre (α.comp CategoryTheory.PGrpd.forgetToGrpd) σ) = CategoryTheory.Grothendieck.Groupoidal.ι (α.comp CategoryTheory.PGrpd.forgetToGrpd) (σ.obj x)

theorem GroupoidModel.FunctorOperation.pair_naturality_obj {Γ : Type u₂} [CategoryTheory.Category.{v₂, u₂} Γ] {α β : CategoryTheory.Functor Γ CategoryTheory.PGrpd} {B : CategoryTheory.Functor ∫(α.comp CategoryTheory.PGrpd.forgetToGrpd) CategoryTheory.Grpd} (h : β.comp CategoryTheory.PGrpd.forgetToGrpd = (CategoryTheory.Grothendieck.Groupoidal.sec (α.comp CategoryTheory.PGrpd.forgetToGrpd) α ⋯).comp B) {Δ : Type u₃} [CategoryTheory.Category.{v₃, u₃} Δ] (σ : CategoryTheory.Functor Δ Γ) (x : Δ) : pairObjFiber h (σ.obj x) ≍ pairObjFiber ⋯ x

theorem GroupoidModel.FunctorOperation.pair_naturality_aux_1 {Γ : Type u₂} [CategoryTheory.Category.{v₂, u₂} Γ] {α β : CategoryTheory.Functor Γ CategoryTheory.PGrpd} {B : CategoryTheory.Functor ∫(α.comp CategoryTheory.PGrpd.forgetToGrpd) CategoryTheory.Grpd} (h : β.comp CategoryTheory.PGrpd.forgetToGrpd = (CategoryTheory.Grothendieck.Groupoidal.sec (α.comp CategoryTheory.PGrpd.forgetToGrpd) α ⋯).comp B) {Δ : Type u₃} [CategoryTheory.Category.{v₃, u₃} Δ] (σ : CategoryTheory.Functor Δ Γ) {x y : Δ} (f : x ⟶ y) : (sigmaMap B (σ.map f)).obj (pairObjFiber h (σ.obj x)) ≍ (sigmaMap ((CategoryTheory.Grothendieck.Groupoidal.pre (α.comp CategoryTheory.PGrpd.forgetToGrpd) σ).comp B) f).obj (pairObjFiber ⋯ x)

theorem GroupoidModel.FunctorOperation.pair_naturality {Γ : Type u₂} [CategoryTheory.Category.{v₂, u₂} Γ] {α β : CategoryTheory.Functor Γ CategoryTheory.PGrpd} {B : CategoryTheory.Functor ∫(α.comp CategoryTheory.PGrpd.forgetToGrpd) CategoryTheory.Grpd} (h : β.comp CategoryTheory.PGrpd.forgetToGrpd = (CategoryTheory.Grothendieck.Groupoidal.sec (α.comp CategoryTheory.PGrpd.forgetToGrpd) α ⋯).comp B) {Δ : Type u₃} [CategoryTheory.Category.{v₃, u₃} Δ] (σ : CategoryTheory.Functor Δ Γ) : σ.comp (pair α β B h) = pair (σ.comp α) (σ.comp β) ((CategoryTheory.Grothendieck.Groupoidal.pre (α.comp CategoryTheory.PGrpd.forgetToGrpd) σ).comp B) ⋯

def GroupoidModel.FunctorOperation.sigma.fstAux {Γ : Type u₂} [CategoryTheory.Category.{v₂, u₂} Γ] {A : CategoryTheory.Functor Γ CategoryTheory.Grpd} (B : CategoryTheory.Functor ∫(A) CategoryTheory.Grpd) : sigma A B ⟶ A

Equations

• GroupoidModel.FunctorOperation.sigma.fstAux B = { app := fun (x : Γ) => CategoryTheory.Grpd.homOf CategoryTheory.Grothendieck.Groupoidal.forget, naturality := ⋯ }

@[simp]

theorem GroupoidModel.FunctorOperation.sigma.fstAux_app {Γ : Type u₂} [CategoryTheory.Category.{v₂, u₂} Γ] {A : CategoryTheory.Functor Γ CategoryTheory.Grpd} (B : CategoryTheory.Functor ∫(A) CategoryTheory.Grpd) (x : Γ) : (fstAux B).app x = CategoryTheory.Grpd.homOf CategoryTheory.Grothendieck.Groupoidal.forget

def GroupoidModel.FunctorOperation.sigma.fstAux' {Γ : Type u₂} [CategoryTheory.Category.{v₂, u₂} Γ] {A : CategoryTheory.Functor Γ CategoryTheory.Grpd} (B : CategoryTheory.Functor ∫(A) CategoryTheory.Grpd) : CategoryTheory.Functor ∫(sigma A B) ∫(A)

Equations

• GroupoidModel.FunctorOperation.sigma.fstAux' B = CategoryTheory.Grothendieck.Groupoidal.map (GroupoidModel.FunctorOperation.sigma.fstAux B)

def GroupoidModel.FunctorOperation.sigma.fst {Γ : Type u₂} [CategoryTheory.Category.{v₂, u₂} Γ] {A : CategoryTheory.Functor Γ CategoryTheory.Grpd} (B : CategoryTheory.Functor ∫(A) CategoryTheory.Grpd) : CategoryTheory.Functor ∫(sigma A B) CategoryTheory.PGrpd

fst projects out the pointed groupoid (A,a) appearing in (A,B,a : A,b : B a)

Equations

• GroupoidModel.FunctorOperation.sigma.fst B = (GroupoidModel.FunctorOperation.sigma.fstAux' B).comp (CategoryTheory.Grothendieck.Groupoidal.toPGrpd A)

theorem GroupoidModel.FunctorOperation.sigma.fst_forgetToGrpd {Γ : Type u₂} [CategoryTheory.Category.{v₂, u₂} Γ] {A : CategoryTheory.Functor Γ CategoryTheory.Grpd} (B : CategoryTheory.Functor ∫(A) CategoryTheory.Grpd) : (fst B).comp CategoryTheory.PGrpd.forgetToGrpd = CategoryTheory.Grothendieck.Groupoidal.forget.comp A

def GroupoidModel.FunctorOperation.sigma.assocFib {Γ : Type u₂} [CategoryTheory.Groupoid Γ] {A : CategoryTheory.Functor Γ CategoryTheory.Grpd} (B : CategoryTheory.Functor ∫(A) CategoryTheory.Grpd) (x : Γ) : CategoryTheory.Functor (sigmaObj B x) ∫(B)

Equations

• GroupoidModel.FunctorOperation.sigma.assocFib B x = CategoryTheory.Grothendieck.Groupoidal.pre B (CategoryTheory.Grothendieck.Groupoidal.ι A x)

def GroupoidModel.FunctorOperation.sigma.assocIso {Γ : Type u₂} [CategoryTheory.Groupoid Γ] {A : CategoryTheory.Functor Γ CategoryTheory.Grpd} (B : CategoryTheory.Functor ∫(A) CategoryTheory.Grpd) {x y : Γ} (f : x ⟶ y) : assocFib B x ≅ (sigmaMap B f).comp (assocFib B y)

Equations

• GroupoidModel.FunctorOperation.sigma.assocIso B f = CategoryTheory.Grothendieck.Groupoidal.preNatIso B (CategoryTheory.Grothendieck.Groupoidal.ιNatIso A f)

@[simp]

theorem GroupoidModel.FunctorOperation.sigma.assocIso_id {Γ : Type u₂} [CategoryTheory.Groupoid Γ] {A : CategoryTheory.Functor Γ CategoryTheory.Grpd} (B : CategoryTheory.Functor ∫(A) CategoryTheory.Grpd) {x : Γ} : assocIso B (CategoryTheory.CategoryStruct.id x) = CategoryTheory.eqToIso ⋯

theorem GroupoidModel.FunctorOperation.sigma.assocIso_comp {Γ : Type u₂} [CategoryTheory.Groupoid Γ] {A : CategoryTheory.Functor Γ CategoryTheory.Grpd} (B : CategoryTheory.Functor ∫(A) CategoryTheory.Grpd) {x y z : Γ} (f : x ⟶ y) (g : y ⟶ z) : assocIso B (CategoryTheory.CategoryStruct.comp f g) = assocIso B f ≪≫ (sigmaMap B f).isoWhiskerLeft (assocIso B g) ≪≫ CategoryTheory.eqToIso ⋯

def GroupoidModel.FunctorOperation.sigma.assocHom {Γ : Type u₂} [CategoryTheory.Groupoid Γ] {A : CategoryTheory.Functor Γ CategoryTheory.Grpd} (B : CategoryTheory.Functor ∫(A) CategoryTheory.Grpd) {x y : Γ} (f : x ⟶ y) : assocFib B x ⟶ (sigmaMap B f).comp (assocFib B y)

Equations

• GroupoidModel.FunctorOperation.sigma.assocHom B f = (GroupoidModel.FunctorOperation.sigma.assocIso B f).hom

@[simp]

theorem GroupoidModel.FunctorOperation.sigma.assocHom_id {Γ : Type u₂} [CategoryTheory.Groupoid Γ] {A : CategoryTheory.Functor Γ CategoryTheory.Grpd} (B : CategoryTheory.Functor ∫(A) CategoryTheory.Grpd) {x : Γ} : assocHom B (CategoryTheory.CategoryStruct.id x) = CategoryTheory.eqToHom ⋯

theorem GroupoidModel.FunctorOperation.sigma.assocHom_comp {Γ : Type u₂} [CategoryTheory.Groupoid Γ] {A : CategoryTheory.Functor Γ CategoryTheory.Grpd} (B : CategoryTheory.Functor ∫(A) CategoryTheory.Grpd) {x y z : Γ} (f : x ⟶ y) (g : y ⟶ z) : assocHom B (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (assocHom B f) (CategoryTheory.CategoryStruct.comp ((sigmaMap B f).whiskerLeft (assocHom B g)) (CategoryTheory.eqToHom ⋯))

def GroupoidModel.FunctorOperation.sigma.assoc {Γ : Type u₂} [CategoryTheory.Groupoid Γ] {A : CategoryTheory.Functor Γ CategoryTheory.Grpd} (B : CategoryTheory.Functor ∫(A) CategoryTheory.Grpd) : CategoryTheory.Functor ∫(sigma A B) ∫(B)

Equations

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

def GroupoidModel.FunctorOperation.sigma.snd {Γ : Type u₂} [CategoryTheory.Groupoid Γ] {A : CategoryTheory.Functor Γ CategoryTheory.Grpd} (B : CategoryTheory.Functor ∫(A) CategoryTheory.Grpd) : CategoryTheory.Functor ∫(sigma A B) CategoryTheory.PGrpd

Equations

• GroupoidModel.FunctorOperation.sigma.snd B = (GroupoidModel.FunctorOperation.sigma.assoc B).comp (CategoryTheory.Grothendieck.Groupoidal.toPGrpd B)

theorem GroupoidModel.FunctorOperation.sigma.ι_sigma_comp_map_fstAux {Γ : Type u₂} [CategoryTheory.Groupoid Γ] {A : CategoryTheory.Functor Γ CategoryTheory.Grpd} (B : CategoryTheory.Functor ∫(A) CategoryTheory.Grpd) (x : Γ) : (CategoryTheory.Grothendieck.Groupoidal.ι (sigma A B) x).comp (CategoryTheory.Grothendieck.Groupoidal.map (fstAux B)) = CategoryTheory.Grothendieck.Groupoidal.forget.comp (CategoryTheory.Grothendieck.Groupoidal.ι A x)

theorem GroupoidModel.FunctorOperation.sigma.asFunctorFrom_fib_map_fstAux {Γ : Type u₂} [CategoryTheory.Groupoid Γ] {A : CategoryTheory.Functor Γ CategoryTheory.Grpd} (B : CategoryTheory.Functor ∫(A) CategoryTheory.Grpd) {x : Γ} : CategoryTheory.Grothendieck.Groupoidal.asFunctorFrom_fib (CategoryTheory.Grothendieck.Groupoidal.map (fstAux B)) x = (CategoryTheory.Grothendieck.Groupoidal.ι (sigma A B) x).comp (CategoryTheory.Grothendieck.Groupoidal.map (fstAux B))

theorem GroupoidModel.FunctorOperation.sigma.asFunctorFrom_hom_map_fstAux {Γ : Type u₂} [CategoryTheory.Groupoid Γ] {A : CategoryTheory.Functor Γ CategoryTheory.Grpd} (B : CategoryTheory.Functor ∫(A) CategoryTheory.Grpd) {c c' : Γ} (f : c ⟶ c') : CategoryTheory.Grothendieck.Groupoidal.asFunctorFrom_hom (CategoryTheory.Grothendieck.Groupoidal.map (fstAux B)) f = CategoryTheory.Functor.whiskerRight (CategoryTheory.Grothendieck.Groupoidal.ιNatTrans f) (CategoryTheory.Grothendieck.Groupoidal.map (fstAux B))

theorem GroupoidModel.FunctorOperation.sigma.functorFrom_comp_fib_assocFib_forget {Γ : Type u₂} [CategoryTheory.Groupoid Γ] {A : CategoryTheory.Functor Γ CategoryTheory.Grpd} (B : CategoryTheory.Functor ∫(A) CategoryTheory.Grpd) : CategoryTheory.Grothendieck.Groupoidal.functorFrom_comp_fib (assocFib B) CategoryTheory.Grothendieck.Groupoidal.forget = CategoryTheory.Grothendieck.Groupoidal.asFunctorFrom_fib (CategoryTheory.Grothendieck.Groupoidal.map (fstAux B))

theorem GroupoidModel.FunctorOperation.sigma.ιNatTrans_app_base_eq {Γ : Type u₂} [CategoryTheory.Groupoid Γ] {A : CategoryTheory.Functor Γ CategoryTheory.Grpd} (B : CategoryTheory.Functor ∫(A) CategoryTheory.Grpd) {c₁ c₂ : Γ} (f : c₁ ⟶ c₂) (x : ↑((sigma A B).obj c₁)) : (CategoryTheory.Grothendieck.Groupoidal.ιNatTrans f).app (CategoryTheory.Grothendieck.Groupoidal.base x) = (CategoryTheory.Grothendieck.Groupoidal.map (fstAux B)).map ((CategoryTheory.Grothendieck.Groupoidal.ιNatTrans f).app x)

theorem GroupoidModel.FunctorOperation.sigma.assoc_forget {Γ : Type u₂} [CategoryTheory.Groupoid Γ] {A : CategoryTheory.Functor Γ CategoryTheory.Grpd} (B : CategoryTheory.Functor ∫(A) CategoryTheory.Grpd) : (assoc B).comp CategoryTheory.Grothendieck.Groupoidal.forget = fstAux' B

theorem GroupoidModel.FunctorOperation.sigma.snd_forgetToGrpd {Γ : Type u₂} [CategoryTheory.Groupoid Γ] {A : CategoryTheory.Functor Γ CategoryTheory.Grpd} (B : CategoryTheory.Functor ∫(A) CategoryTheory.Grpd) : (snd B).comp CategoryTheory.PGrpd.forgetToGrpd = (fstAux' B).comp B

@[simp]

theorem GroupoidModel.FunctorOperation.sigma.fst_obj_fiber {Γ : Type u₂} [CategoryTheory.Groupoid Γ] {A : CategoryTheory.Functor Γ CategoryTheory.Grpd} (B : CategoryTheory.Functor ∫(A) CategoryTheory.Grpd) {x : ∫(sigma A B)} : ((fst B).obj x).fiber = CategoryTheory.Grothendieck.Groupoidal.base x.fiber

@[simp]

theorem GroupoidModel.FunctorOperation.sigma.fst_map_fiber {Γ : Type u₂} [CategoryTheory.Groupoid Γ] {A : CategoryTheory.Functor Γ CategoryTheory.Grpd} (B : CategoryTheory.Functor ∫(A) CategoryTheory.Grpd) {x y : ∫(sigma A B)} (f : x ⟶ y) : ((fst B).map f).fiber = CategoryTheory.Grothendieck.Groupoidal.Hom.base (CategoryTheory.Grothendieck.Groupoidal.Hom.fiber f)

@[simp]

theorem GroupoidModel.FunctorOperation.sigma.snd_obj_fiber {Γ : Type u₂} [CategoryTheory.Groupoid Γ] {A : CategoryTheory.Functor Γ CategoryTheory.Grpd} (B : CategoryTheory.Functor ∫(A) CategoryTheory.Grpd) {x : ∫(sigma A B)} : ((snd B).obj x).fiber = CategoryTheory.Grothendieck.Groupoidal.fiber x.fiber

@[simp]

theorem GroupoidModel.FunctorOperation.sigma.assoc_hom_app_fiber {Γ : Type u₂} [CategoryTheory.Groupoid Γ] {A : CategoryTheory.Functor Γ CategoryTheory.Grpd} (B : CategoryTheory.Functor ∫(A) CategoryTheory.Grpd) {x y : ∫(sigma A B)} (f : x ⟶ y) : (assocHom B (CategoryTheory.Grothendieck.Groupoidal.Hom.base f)).app x.fiber = CategoryTheory.Grothendieck.Groupoidal.homMk (CategoryTheory.Grothendieck.Groupoidal.homMk (CategoryTheory.Grothendieck.Groupoidal.Hom.base f) (CategoryTheory.CategoryStruct.id ((A.map (CategoryTheory.Grothendieck.Groupoidal.Hom.base f)).obj ((assocFib B x.base).obj x.fiber).base.fiber))) (CategoryTheory.CategoryStruct.id ((B.map (CategoryTheory.Grothendieck.Groupoidal.homMk (CategoryTheory.Grothendieck.Groupoidal.Hom.base f) (CategoryTheory.CategoryStruct.id ((A.map (CategoryTheory.Grothendieck.Groupoidal.Hom.base f)).obj ((assocFib B x.base).obj x.fiber).base.fiber)))).obj ((assocFib B x.base).obj x.fiber).fiber))

@[simp]

theorem GroupoidModel.FunctorOperation.sigma.snd_map_fiber {Γ : Type u₂} [CategoryTheory.Groupoid Γ] {A : CategoryTheory.Functor Γ CategoryTheory.Grpd} (B : CategoryTheory.Functor ∫(A) CategoryTheory.Grpd) {x y : ∫(sigma A B)} (f : x ⟶ y) : ((snd B).map f).fiber = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.Grothendieck.Groupoidal.Hom.fiber (CategoryTheory.Grothendieck.Groupoidal.Hom.fiber f))

def GroupoidModel.FunctorOperation.sigma.fst' {Γ : Type u_1} [CategoryTheory.Category.{u_2, u_1} Γ] {A : CategoryTheory.Functor Γ CategoryTheory.Grpd} (B : CategoryTheory.Functor ∫(A) CategoryTheory.Grpd) (αβ : CategoryTheory.Functor Γ CategoryTheory.PGrpd) (hαβ : αβ.comp CategoryTheory.PGrpd.forgetToGrpd = sigma A B) : CategoryTheory.Functor Γ CategoryTheory.PGrpd

Let Γ be a category. For any pair of functors A : Γ ⥤ Grpd and B : ∫(A) ⥤ Grpd, and any "groupoid-term", meaning a functor αβ : Γ ⥤ PGrpd satisfying αβ ⋙ forgetToGrpd = sigma A B : Γ ⥤ Grpd, there is a groupoid-term fst' : Γ ⥤ PGrpd such that fst ⋙ forgetToGrpd = A, thought of as fst' : A. There is a "groupoid-type" dependent' : ∫(fst ⋙ forgetToGrpd) ⥤ Grpd, which is hequal to B modulo fst ⋙ forgetToGrpd being equal to A. And there is a groupoid-term snd' : Γ ⥤ PGrpd satisfying snd' ⋙ forgetToGrpd = sec _ fst rfl ⋙ dependent'.

Equations

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

theorem GroupoidModel.FunctorOperation.sigma.fst'_forgetToGrpd {Γ : Type u_1} [CategoryTheory.Category.{u_2, u_1} Γ] {A : CategoryTheory.Functor Γ CategoryTheory.Grpd} (B : CategoryTheory.Functor ∫(A) CategoryTheory.Grpd) (αβ : CategoryTheory.Functor Γ CategoryTheory.PGrpd) (hαβ : αβ.comp CategoryTheory.PGrpd.forgetToGrpd = sigma A B) : (fst' B αβ hαβ).comp CategoryTheory.PGrpd.forgetToGrpd = A

Let Γ be a category. For any pair of functors A : Γ ⥤ Grpd and B : ∫(A) ⥤ Grpd, and any "groupoid-term", meaning a functor αβ : Γ ⥤ PGrpd satisfying αβ ⋙ forgetToGrpd = sigma A B : Γ ⥤ Grpd, there is a groupoid-term fst' : Γ ⥤ PGrpd such that fst ⋙ forgetToGrpd = A, thought of as fst' : A. There is a "groupoid-type" dependent' : ∫(fst ⋙ forgetToGrpd) ⥤ Grpd, which is hequal to B modulo fst ⋙ forgetToGrpd being equal to A. And there is a groupoid-term snd' : Γ ⥤ PGrpd satisfying snd' ⋙ forgetToGrpd = sec _ fst rfl ⋙ dependent'.

def GroupoidModel.FunctorOperation.sigma.dependent' {Γ : Type u_1} [CategoryTheory.Category.{u_2, u_1} Γ] {A : CategoryTheory.Functor Γ CategoryTheory.Grpd} (B : CategoryTheory.Functor ∫(A) CategoryTheory.Grpd) (αβ : CategoryTheory.Functor Γ CategoryTheory.PGrpd) (hαβ : αβ.comp CategoryTheory.PGrpd.forgetToGrpd = sigma A B) : CategoryTheory.Functor ∫((fst' B αβ hαβ).comp CategoryTheory.PGrpd.forgetToGrpd) CategoryTheory.Grpd

Let Γ be a category. For any pair of functors A : Γ ⥤ Grpd and B : ∫(A) ⥤ Grpd, and any "groupoid-term", meaning a functor αβ : Γ ⥤ PGrpd satisfying αβ ⋙ forgetToGrpd = sigma A B : Γ ⥤ Grpd, there is a groupoid-term fst' : Γ ⥤ PGrpd such that fst ⋙ forgetToGrpd = A, thought of as fst' : A. There is a "groupoid-type" dependent' : ∫(fst ⋙ forgetToGrpd) ⥤ Grpd, which is hequal to B modulo fst ⋙ forgetToGrpd being equal to A. And there is a groupoid-term snd' : Γ ⥤ PGrpd satisfying snd' ⋙ forgetToGrpd = sec _ fst rfl ⋙ dependent'.

Equations

• GroupoidModel.FunctorOperation.sigma.dependent' B αβ hαβ = (CategoryTheory.Grothendieck.Groupoidal.map (CategoryTheory.eqToHom ⋯)).comp B

def GroupoidModel.FunctorOperation.sigma.snd' {Γ : Type u_1} [CategoryTheory.Groupoid Γ] {A : CategoryTheory.Functor Γ CategoryTheory.Grpd} (B : CategoryTheory.Functor ∫(A) CategoryTheory.Grpd) (αβ : CategoryTheory.Functor Γ CategoryTheory.PGrpd) (hαβ : αβ.comp CategoryTheory.PGrpd.forgetToGrpd = sigma A B) : CategoryTheory.Functor Γ CategoryTheory.PGrpd

Let Γ be a category. For any pair of functors A : Γ ⥤ Grpd and B : ∫(A) ⥤ Grpd, and any "groupoid-term", meaning a functor αβ : Γ ⥤ PGrpd satisfying αβ ⋙ forgetToGrpd = sigma A B : Γ ⥤ Grpd, there is a groupoid-term fst' : Γ ⥤ PGrpd such that fst ⋙ forgetToGrpd = A, thought of as fst' : A. There is a "groupoid-type" dependent' : ∫(fst ⋙ forgetToGrpd) ⥤ Grpd, which is hequal to B modulo fst ⋙ forgetToGrpd being equal to A. And there is a groupoid-term snd' : Γ ⥤ PGrpd satisfying snd' ⋙ forgetToGrpd = sec _ fst rfl ⋙ dependent'.

Equations

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

@[simp]

theorem GroupoidModel.FunctorOperation.sigma.fst'_obj_base {Γ : Type u_1} [CategoryTheory.Groupoid Γ] {A : CategoryTheory.Functor Γ CategoryTheory.Grpd} (B : CategoryTheory.Functor ∫(A) CategoryTheory.Grpd) (αβ : CategoryTheory.Functor Γ CategoryTheory.PGrpd) (hαβ : αβ.comp CategoryTheory.PGrpd.forgetToGrpd = sigma A B) {x : Γ} : ((fst' B αβ hαβ).obj x).base = A.obj x

theorem GroupoidModel.FunctorOperation.sigma.fst'_obj_fiber {Γ : Type u_1} [CategoryTheory.Groupoid Γ] {A : CategoryTheory.Functor Γ CategoryTheory.Grpd} (B : CategoryTheory.Functor ∫(A) CategoryTheory.Grpd) (αβ : CategoryTheory.Functor Γ CategoryTheory.PGrpd) (hαβ : αβ.comp CategoryTheory.PGrpd.forgetToGrpd = sigma A B) {x : Γ} : ((fst' B αβ hαβ).obj x).fiber = CategoryTheory.Grothendieck.Groupoidal.base (CategoryTheory.PGrpd.objFiber' hαβ x)

@[simp]

theorem GroupoidModel.FunctorOperation.sigma.fst'_map_base {Γ : Type u_1} [CategoryTheory.Groupoid Γ] {A : CategoryTheory.Functor Γ CategoryTheory.Grpd} (B : CategoryTheory.Functor ∫(A) CategoryTheory.Grpd) (αβ : CategoryTheory.Functor Γ CategoryTheory.PGrpd) (hαβ : αβ.comp CategoryTheory.PGrpd.forgetToGrpd = sigma A B) {x y : Γ} (f : x ⟶ y) : ((fst' B αβ hαβ).map f).base = A.map f

theorem GroupoidModel.FunctorOperation.sigma.fst'_map_fiber {Γ : Type u_1} [CategoryTheory.Groupoid Γ] {A : CategoryTheory.Functor Γ CategoryTheory.Grpd} (B : CategoryTheory.Functor ∫(A) CategoryTheory.Grpd) (αβ : CategoryTheory.Functor Γ CategoryTheory.PGrpd) (hαβ : αβ.comp CategoryTheory.PGrpd.forgetToGrpd = sigma A B) {x y : Γ} (f : x ⟶ y) : ((fst' B αβ hαβ).map f).fiber = CategoryTheory.Grothendieck.Groupoidal.Hom.base (CategoryTheory.PGrpd.mapFiber' hαβ f)

theorem GroupoidModel.FunctorOperation.sigma.sec_fstAux' {Γ : Type u_1} [CategoryTheory.Groupoid Γ] {A : CategoryTheory.Functor Γ CategoryTheory.Grpd} (B : CategoryTheory.Functor ∫(A) CategoryTheory.Grpd) (αβ : CategoryTheory.Functor Γ CategoryTheory.PGrpd) (hαβ : αβ.comp CategoryTheory.PGrpd.forgetToGrpd = sigma A B) : (CategoryTheory.Grothendieck.Groupoidal.sec (sigma A B) αβ hαβ).comp (fstAux' B) = CategoryTheory.Grothendieck.Groupoidal.sec ((fst' B αβ hαβ).comp CategoryTheory.PGrpd.forgetToGrpd) (fst' B αβ hαβ) ⋯

theorem GroupoidModel.FunctorOperation.sigma.snd'_forgetToGrpd {Γ : Type u_1} [CategoryTheory.Groupoid Γ] {A : CategoryTheory.Functor Γ CategoryTheory.Grpd} (B : CategoryTheory.Functor ∫(A) CategoryTheory.Grpd) (αβ : CategoryTheory.Functor Γ CategoryTheory.PGrpd) (hαβ : αβ.comp CategoryTheory.PGrpd.forgetToGrpd = sigma A B) : (snd' B αβ hαβ).comp CategoryTheory.PGrpd.forgetToGrpd = (CategoryTheory.Grothendieck.Groupoidal.sec ((fst' B αβ hαβ).comp CategoryTheory.PGrpd.forgetToGrpd) (fst' B αβ hαβ) ⋯).comp (dependent' B αβ hαβ)

fst projects out the pointed groupoid (A,a) appearing in (A,B,a : A,b : B a)

theorem GroupoidModel.FunctorOperation.sigma.snd'_obj_fiber {Γ : Type u_1} [CategoryTheory.Groupoid Γ] {A : CategoryTheory.Functor Γ CategoryTheory.Grpd} (B : CategoryTheory.Functor ∫(A) CategoryTheory.Grpd) (αβ : CategoryTheory.Functor Γ CategoryTheory.PGrpd) (hαβ : αβ.comp CategoryTheory.PGrpd.forgetToGrpd = sigma A B) {x : Γ} : ((snd' B αβ hαβ).obj x).fiber = CategoryTheory.Grothendieck.Groupoidal.fiber (CategoryTheory.PGrpd.objFiber' hαβ x)

theorem GroupoidModel.FunctorOperation.sigma.snd'_map_fiber {Γ : Type u_1} [CategoryTheory.Groupoid Γ] {A : CategoryTheory.Functor Γ CategoryTheory.Grpd} (B : CategoryTheory.Functor ∫(A) CategoryTheory.Grpd) (αβ : CategoryTheory.Functor Γ CategoryTheory.PGrpd) (hαβ : αβ.comp CategoryTheory.PGrpd.forgetToGrpd = sigma A B) {x y : Γ} (f : x ⟶ y) : ((snd' B αβ hαβ).map f).fiber = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.Grothendieck.Groupoidal.Hom.fiber (CategoryTheory.PGrpd.mapFiber' hαβ f))

theorem GroupoidModel.FunctorOperation.sigma.ι_fst'_forgetToGrpd_comp_dependent' {Γ : Type u_1} [CategoryTheory.Groupoid Γ] {A : CategoryTheory.Functor Γ CategoryTheory.Grpd} (B : CategoryTheory.Functor ∫(A) CategoryTheory.Grpd) (αβ : CategoryTheory.Functor Γ CategoryTheory.PGrpd) (hαβ : αβ.comp CategoryTheory.PGrpd.forgetToGrpd = sigma A B) (x : Γ) : (CategoryTheory.Grothendieck.Groupoidal.ι ((fst' B αβ hαβ).comp CategoryTheory.PGrpd.forgetToGrpd) x).comp (dependent' B αβ hαβ) = (CategoryTheory.Grothendieck.Groupoidal.ι A x).comp B

theorem GroupoidModel.FunctorOperation.sigma.pairObjFiber_snd'_eq {Γ : Type u_1} [CategoryTheory.Groupoid Γ] {A : CategoryTheory.Functor Γ CategoryTheory.Grpd} (B : CategoryTheory.Functor ∫(A) CategoryTheory.Grpd) (αβ : CategoryTheory.Functor Γ CategoryTheory.PGrpd) (hαβ : αβ.comp CategoryTheory.PGrpd.forgetToGrpd = sigma A B) (x : Γ) : pairObjFiber ⋯ x = CategoryTheory.Grothendieck.Groupoidal.objMk (CategoryTheory.Grothendieck.Groupoidal.base (CategoryTheory.PGrpd.objFiber' hαβ x)) (CategoryTheory.PGrpd.objFiber' ⋯ x)

theorem GroupoidModel.FunctorOperation.sigma.pairObjFiber_snd'_heq {Γ : Type u_1} [CategoryTheory.Groupoid Γ] {A : CategoryTheory.Functor Γ CategoryTheory.Grpd} (B : CategoryTheory.Functor ∫(A) CategoryTheory.Grpd) (αβ : CategoryTheory.Functor Γ CategoryTheory.PGrpd) (hαβ : αβ.comp CategoryTheory.PGrpd.forgetToGrpd = sigma A B) (x : Γ) : pairObjFiber ⋯ x ≍ (αβ.obj x).fiber

theorem GroupoidModel.FunctorOperation.sigma.pairMapFiber_snd'_eq {Γ : Type u_1} [CategoryTheory.Groupoid Γ] {A : CategoryTheory.Functor Γ CategoryTheory.Grpd} (B : CategoryTheory.Functor ∫(A) CategoryTheory.Grpd) (αβ : CategoryTheory.Functor Γ CategoryTheory.PGrpd) (hαβ : αβ.comp CategoryTheory.PGrpd.forgetToGrpd = sigma A B) {x y : Γ} (f : x ⟶ y) : pairMapFiber ⋯ f = CategoryTheory.Grothendieck.Groupoidal.homMk (CategoryTheory.PGrpd.mapFiber (fst' B αβ hαβ) f) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.PGrpd.mapFiber' ⋯ f))

theorem GroupoidModel.FunctorOperation.sigma.pairMapFiber_snd'_heq_src_heq {Γ : Type u_1} [CategoryTheory.Groupoid Γ] {A : CategoryTheory.Functor Γ CategoryTheory.Grpd} (B : CategoryTheory.Functor ∫(A) CategoryTheory.Grpd) (αβ : CategoryTheory.Functor Γ CategoryTheory.PGrpd) (hαβ : αβ.comp CategoryTheory.PGrpd.forgetToGrpd = sigma A B) {x y : Γ} (f : x ⟶ y) : (sigmaMap (dependent' B αβ hαβ) f).obj (pairObjFiber ⋯ x) ≍ (CategoryTheory.PGrpd.objFiber'EqToHom hαβ y).obj ((αβ.map f).base.obj (αβ.obj x).fiber)

theorem GroupoidModel.FunctorOperation.sigma.pairMapFiber_snd'_heq_trg_heq {Γ : Type u_1} [CategoryTheory.Groupoid Γ] {A : CategoryTheory.Functor Γ CategoryTheory.Grpd} (B : CategoryTheory.Functor ∫(A) CategoryTheory.Grpd) (αβ : CategoryTheory.Functor Γ CategoryTheory.PGrpd) (hαβ : αβ.comp CategoryTheory.PGrpd.forgetToGrpd = sigma A B) {y : Γ} : pairObjFiber ⋯ y ≍ (CategoryTheory.PGrpd.objFiber'EqToHom hαβ y).obj (αβ.obj y).fiber

theorem GroupoidModel.FunctorOperation.sigma.sigmaMap_obj_objFiber' {Γ : Type u_1} [CategoryTheory.Groupoid Γ] {A : CategoryTheory.Functor Γ CategoryTheory.Grpd} (B : CategoryTheory.Functor ∫(A) CategoryTheory.Grpd) (αβ : CategoryTheory.Functor Γ CategoryTheory.PGrpd) (hαβ : αβ.comp CategoryTheory.PGrpd.forgetToGrpd = sigma A B) {x y : Γ} (f : x ⟶ y) : (sigmaMap B f).obj (CategoryTheory.PGrpd.objFiber' hαβ x) = (CategoryTheory.PGrpd.objFiber'EqToHom hαβ y).obj ((αβ.map f).base.obj (αβ.obj x).fiber)

theorem GroupoidModel.FunctorOperation.sigma.pairMapFiber_snd'_heq {Γ : Type u_1} [CategoryTheory.Groupoid Γ] {A : CategoryTheory.Functor Γ CategoryTheory.Grpd} (B : CategoryTheory.Functor ∫(A) CategoryTheory.Grpd) (αβ : CategoryTheory.Functor Γ CategoryTheory.PGrpd) (hαβ : αβ.comp CategoryTheory.PGrpd.forgetToGrpd = sigma A B) {x y : Γ} (f : x ⟶ y) : pairMapFiber ⋯ f ≍ (αβ.map f).fiber

theorem GroupoidModel.FunctorOperation.sigma.eta {Γ : Type u_1} [CategoryTheory.Groupoid Γ] {A : CategoryTheory.Functor Γ CategoryTheory.Grpd} (B : CategoryTheory.Functor ∫(A) CategoryTheory.Grpd) (αβ : CategoryTheory.Functor Γ CategoryTheory.PGrpd) (hαβ : αβ.comp CategoryTheory.PGrpd.forgetToGrpd = sigma A B) : pair (fst' B αβ hαβ) (snd' B αβ hαβ) (dependent' B αβ hαβ) ⋯ = αβ

@[simp]

theorem GroupoidModel.FunctorOperation.sigma.fst'_pair {Γ : Type u_1} [CategoryTheory.Groupoid Γ] {α β : CategoryTheory.Functor Γ CategoryTheory.PGrpd} {B : CategoryTheory.Functor ∫(α.comp CategoryTheory.PGrpd.forgetToGrpd) CategoryTheory.Grpd} (h : β.comp CategoryTheory.PGrpd.forgetToGrpd = (CategoryTheory.Grothendieck.Groupoidal.sec (α.comp CategoryTheory.PGrpd.forgetToGrpd) α ⋯).comp B) : fst' B (pair α β B h) ⋯ = α

@[simp]

theorem GroupoidModel.FunctorOperation.sigma.snd'_pair {Γ : Type u_1} [CategoryTheory.Groupoid Γ] {α β : CategoryTheory.Functor Γ CategoryTheory.PGrpd} {B : CategoryTheory.Functor ∫(α.comp CategoryTheory.PGrpd.forgetToGrpd) CategoryTheory.Grpd} (h : β.comp CategoryTheory.PGrpd.forgetToGrpd = (CategoryTheory.Grothendieck.Groupoidal.sec (α.comp CategoryTheory.PGrpd.forgetToGrpd) α ⋯).comp B) : snd' B (pair α β B h) ⋯ = β

def GroupoidModel.smallUSig_app {Γ : Ctx} (AB : CategoryTheory.yoneda.obj Γ ⟶ smallU.Ptp.obj smallU.Ty) : CategoryTheory.yoneda.obj Γ ⟶ smallU.Ty

Behavior of the Σ-type former (a natural transformation) on an input. By Yoneda, "an input" is the same as a map from a representable into the domain.

Equations

• GroupoidModel.smallUSig_app AB = GroupoidModel.yonedaCategoryEquiv.symm (GroupoidModel.FunctorOperation.sigma (GroupoidModel.smallU.PtpEquiv.fst AB) (GroupoidModel.smallU.PtpEquiv.snd AB))

theorem GroupoidModel.smallUSig_naturality {Γ Δ : Ctx} (σ : Δ ⟶ Γ) (AB : CategoryTheory.yoneda.obj Γ ⟶ smallU.Ptp.obj smallU.Ty) : smallUSig_app (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) AB) = CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map σ) (smallUSig_app AB)

Naturality for the formation rule for Σ-types. Also known as Beck-Chevalley

def GroupoidModel.smallUSig : smallU.Ptp.obj smallU.Ty ⟶ smallU.Ty

The formation rule for Σ-types for the ambient natural model base If possible, don't use NatTrans.app on this, instead precompose it with maps from representables.

Equations

• GroupoidModel.smallUSig = CategoryTheory.NatTrans.yonedaMk (fun {X : GroupoidModel.Ctx} => GroupoidModel.smallUSig_app) ⋯

theorem GroupoidModel.smallUSig_app_eq {Γ : Ctx} (AB : CategoryTheory.yoneda.obj Γ ⟶ smallU.Ptp.obj smallU.Ty) : CategoryTheory.CategoryStruct.comp AB smallUSig = smallUSig_app AB

def GroupoidModel.smallUPair_app {Γ : Ctx} (ab : CategoryTheory.yoneda.obj Γ ⟶ smallU.uvPolyTp.compDom smallU.uvPolyTp) : CategoryTheory.yoneda.obj Γ ⟶ smallU.Tm

Equations

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

theorem GroupoidModel.smallUPair_naturality {Γ Δ : Ctx} (f : Δ ⟶ Γ) (ab : CategoryTheory.yoneda.obj Γ ⟶ smallU.compDom) : smallUPair_app (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map f) ab) = CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map f) (smallUPair_app ab)

def GroupoidModel.smallUPair : smallU.compDom ⟶ smallU.Tm

Equations

• GroupoidModel.smallUPair = CategoryTheory.NatTrans.yonedaMk (fun {X : GroupoidModel.Ctx} => GroupoidModel.smallUPair_app) ⋯

theorem GroupoidModel.smallUPair_app_eq {Γ : Ctx} (ab : CategoryTheory.yoneda.obj Γ ⟶ smallU.compDom) : CategoryTheory.CategoryStruct.comp ab smallUPair = yonedaCategoryEquiv.symm (FunctorOperation.pair (smallU.compDom.fst ab) (smallU.compDom.snd ab) (smallU.compDom.dependent ab) ⋯)

theorem GroupoidModel.SigmaPullback.smallUPair_tp : CategoryTheory.CategoryStruct.comp smallUPair smallU.tp = CategoryTheory.CategoryStruct.comp smallU.comp smallUSig

theorem GroupoidModel.SigmaPullback.yonedaCategoryEquiv_forgetToGrpd {Γ : Ctx} (AB : CategoryTheory.yoneda.obj Γ ⟶ smallU.Ptp.obj (CategoryTheory.yoneda.obj U)) (αβ : CategoryTheory.yoneda.obj Γ ⟶ CategoryTheory.yoneda.obj E) (hαβ : CategoryTheory.CategoryStruct.comp αβ (CategoryTheory.yoneda.map π) = CategoryTheory.CategoryStruct.comp AB smallUSig) : (yonedaCategoryEquiv αβ).comp CategoryTheory.PGrpd.forgetToGrpd = FunctorOperation.sigma (smallU.PtpEquiv.fst AB) (smallU.PtpEquiv.snd AB)

def GroupoidModel.SigmaPullback.lift {Γ : Ctx} (AB : CategoryTheory.yoneda.obj Γ ⟶ smallU.Ptp.obj (CategoryTheory.yoneda.obj U)) (αβ : CategoryTheory.yoneda.obj Γ ⟶ CategoryTheory.yoneda.obj E) (hαβ : CategoryTheory.CategoryStruct.comp αβ (CategoryTheory.yoneda.map π) = CategoryTheory.CategoryStruct.comp AB smallUSig) : CategoryTheory.yoneda.obj Γ ⟶ smallU.compDom

Equations

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

theorem GroupoidModel.SigmaPullback.fac_left {Γ : Ctx} (AB : CategoryTheory.yoneda.obj Γ ⟶ smallU.Ptp.obj (CategoryTheory.yoneda.obj U)) (αβ : CategoryTheory.yoneda.obj Γ ⟶ CategoryTheory.yoneda.obj E) (hαβ : CategoryTheory.CategoryStruct.comp αβ (CategoryTheory.yoneda.map π) = CategoryTheory.CategoryStruct.comp AB smallUSig) : CategoryTheory.CategoryStruct.comp (lift AB αβ hαβ) smallUPair = αβ

theorem GroupoidModel.SigmaPullback.fac_right {Γ : Ctx} (AB : CategoryTheory.yoneda.obj Γ ⟶ smallU.Ptp.obj (CategoryTheory.yoneda.obj U)) (αβ : CategoryTheory.yoneda.obj Γ ⟶ CategoryTheory.yoneda.obj E) (hαβ : CategoryTheory.CategoryStruct.comp αβ (CategoryTheory.yoneda.map π) = CategoryTheory.CategoryStruct.comp AB smallUSig) : CategoryTheory.CategoryStruct.comp (lift AB αβ hαβ) smallU.comp = AB

theorem GroupoidModel.SigmaPullback.hom_ext {Γ : Ctx} (m n : CategoryTheory.yoneda.obj Γ ⟶ smallU.compDom) (hComp : CategoryTheory.CategoryStruct.comp m smallU.comp = CategoryTheory.CategoryStruct.comp n smallU.comp) (hPair : CategoryTheory.CategoryStruct.comp m smallUPair = CategoryTheory.CategoryStruct.comp n smallUPair) : m = n

theorem GroupoidModel.SigmaPullback.uniq {Γ : Ctx} (AB : CategoryTheory.yoneda.obj Γ ⟶ smallU.Ptp.obj (CategoryTheory.yoneda.obj U)) (αβ : CategoryTheory.yoneda.obj Γ ⟶ CategoryTheory.yoneda.obj E) (hαβ : CategoryTheory.CategoryStruct.comp αβ (CategoryTheory.yoneda.map π) = CategoryTheory.CategoryStruct.comp AB smallUSig) (m : CategoryTheory.yoneda.obj Γ ⟶ smallU.compDom) (hmAB : CategoryTheory.CategoryStruct.comp m smallU.comp = AB) (hmαβ : CategoryTheory.CategoryStruct.comp m smallUPair = αβ) : m = lift AB αβ hαβ

@[reducible, inline]

abbrev GroupoidModel.SigmaPullback.A (s : CategoryTheory.Limits.RepPullbackCone smallU.tp smallUSig) : CategoryTheory.Functor (↑(Ctx.toGrpd.obj s.pt)) CategoryTheory.Grpd

Equations

• GroupoidModel.SigmaPullback.A s = GroupoidModel.smallU.PtpEquiv.fst s.snd

@[reducible, inline]

abbrev GroupoidModel.SigmaPullback.B (s : CategoryTheory.Limits.RepPullbackCone smallU.tp smallUSig) : CategoryTheory.Functor ∫(smallU.PtpEquiv.fst s.snd) CategoryTheory.Grpd

Equations

• GroupoidModel.SigmaPullback.B s = GroupoidModel.smallU.PtpEquiv.snd s.snd

theorem GroupoidModel.smallU_pb : CategoryTheory.IsPullback smallUPair smallU.comp smallU.tp smallUSig

def GroupoidModel.smallUSigma : smallU.NaturalModelSigma

Equations

• GroupoidModel.smallUSigma = { Sig := GroupoidModel.smallUSig, pair := GroupoidModel.smallUPair, Sig_pullback := GroupoidModel.smallU_pb }

def GroupoidModel.uHomSeqSigmas' (i : ℕ) (ilen : i < 4) : (uHomSeqObjs i ilen).NaturalModelSigma

Equations

• GroupoidModel.uHomSeqSigmas' 0 ilen_2 = GroupoidModel.smallUSigma
• GroupoidModel.uHomSeqSigmas' 1 ilen_2 = GroupoidModel.smallUSigma
• GroupoidModel.uHomSeqSigmas' 2 ilen_2 = GroupoidModel.smallUSigma
• GroupoidModel.uHomSeqSigmas' 3 ilen_2 = GroupoidModel.smallUSigma
• GroupoidModel.uHomSeqSigmas' n.succ.succ.succ.succ ilen_2 = ⋯.elim