def CategoryTheory.PGrpd.inc (G : Type) [Groupoid G] : Functor G PGrpd

Equations

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

@[reducible, inline]

abbrev CategoryTheory.BPGrpd : Type (max (max (u_1 + 1) (u_2 + 1)) u_1)

Equations

• CategoryTheory.BPGrpd = CategoryTheory.PGrpd.forgetToGrpd.Groupoidal

@[reducible, inline]

abbrev CategoryTheory.BPGrpd.fst : Functor BPGrpd PGrpd

Equations

• CategoryTheory.BPGrpd.fst = CategoryTheory.Functor.Groupoidal.forget

@[reducible, inline]

abbrev CategoryTheory.BPGrpd.forgetToGrpd : Functor BPGrpd Grpd

Equations

• CategoryTheory.BPGrpd.forgetToGrpd = CategoryTheory.BPGrpd.fst.comp CategoryTheory.PGrpd.forgetToGrpd

def CategoryTheory.BPGrpd.snd : Functor BPGrpd PGrpd

Equations

• CategoryTheory.BPGrpd.snd = CategoryTheory.Functor.Groupoidal.toPGrpd CategoryTheory.PGrpd.forgetToGrpd

theorem CategoryTheory.BPGrpd.fst_forgetToGrpd : fst.comp PGrpd.forgetToGrpd = snd.comp PGrpd.forgetToGrpd

The commutative square BPGrpd ----> PGrpd | | | | | | | | V V PGrpd ----> Grpd

def CategoryTheory.BPGrpd.isPullback : snd.IsPullback fst PGrpd.forgetToGrpd PGrpd.forgetToGrpd

Equations

• CategoryTheory.BPGrpd.isPullback = CategoryTheory.Functor.Groupoidal.isPullback CategoryTheory.PGrpd.forgetToGrpd

def CategoryTheory.BPGrpd.inc (G : Type) [Groupoid G] : Functor G BPGrpd

Equations

• CategoryTheory.BPGrpd.inc G = CategoryTheory.BPGrpd.isPullback.lift (CategoryTheory.PGrpd.inc G) (CategoryTheory.PGrpd.inc G) ⋯

def GroupoidModel.FunctorOperation.idObj (x : CategoryTheory.BPGrpd) : CategoryTheory.Grpd

The identity type former takes a bipointed groupoid ((A,a0),a1) to the set of isomorphisms between its two given points A(a0,a1). Here A = x.base.base, a0 = x.base.fiber and a1 = x.fiber.

Equations

• GroupoidModel.FunctorOperation.idObj x = CategoryTheory.Grpd.of (CategoryTheory.Discrete ((CategoryTheory.Functor.Groupoidal.base x).fiber ⟶ CategoryTheory.Functor.Groupoidal.fiber x))

def GroupoidModel.FunctorOperation.idMap {x y : CategoryTheory.BPGrpd} (f : x ⟶ y) : CategoryTheory.Functor ↑(idObj x) ↑(idObj y)

The identity type former takes a morphism of bipointed groupoids ((F,f0),f1) : ((A,a0),a1) ⟶ ((B,b0),b1) to the function A(a0,a1) → B(b0,b1) taking g : a0 ≅ a1 to f0⁻¹ ⋙ F g ⋙ f1 where f0⁻¹ : b0 ⟶ F a0, F g : F a0 ⟶ F a1 and f1 : F a1 ⟶ b1.

Equations

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

theorem GroupoidModel.FunctorOperation.Discrete.functor_ext' {X : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] {F G : X → C} (h : ∀ (x : X), F x = G x) : CategoryTheory.Discrete.functor F = CategoryTheory.Discrete.functor G

theorem GroupoidModel.FunctorOperation.Discrete.functor_eq {X : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] {F : CategoryTheory.Functor (CategoryTheory.Discrete X) C} : F = CategoryTheory.Discrete.functor fun (x : X) => F.obj { as := x }

theorem GroupoidModel.FunctorOperation.Discrete.functor_ext {X : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] (F G : CategoryTheory.Functor (CategoryTheory.Discrete X) C) (h : ∀ (x : X), F.obj { as := x } = G.obj { as := x }) : F = G

theorem GroupoidModel.FunctorOperation.Discrete.ext {X : Type u_1} {x y : CategoryTheory.Discrete X} (h : x.as = y.as) : x = y

def GroupoidModel.FunctorOperation.id : CategoryTheory.Functor CategoryTheory.BPGrpd CategoryTheory.Grpd

The identity type formation rule, equivalently viewed as a functor.

Equations

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

@[simp]

theorem GroupoidModel.FunctorOperation.id_obj (x : CategoryTheory.BPGrpd) : id.obj x = idObj x

@[simp]

theorem GroupoidModel.FunctorOperation.id_map {X✝ Y✝ : CategoryTheory.BPGrpd} (f : X✝ ⟶ Y✝) : id.map f = idMap f

def GroupoidModel.FunctorOperation.diag : CategoryTheory.Functor CategoryTheory.PGrpd CategoryTheory.BPGrpd

The diagonal functor into the pullback. It creates a second copy of the point from the input pointed groupoid.

This version of diag is used for better definitional reduction.

Equations

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

def GroupoidModel.FunctorOperation.diag' : CategoryTheory.Functor CategoryTheory.PGrpd CategoryTheory.BPGrpd

This version of diag is used for functor equational reasoning.

Equations

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

theorem GroupoidModel.FunctorOperation.diag_eq_diag' : diag = diag'

def GroupoidModel.FunctorOperation.reflObjFiber (x : CategoryTheory.PGrpd) : CategoryTheory.Discrete (x.fiber ⟶ x.fiber)

Equations

• GroupoidModel.FunctorOperation.reflObjFiber x = { as := CategoryTheory.CategoryStruct.id x.fiber }

def GroupoidModel.FunctorOperation.refl : CategoryTheory.Functor CategoryTheory.PGrpd CategoryTheory.PGrpd

Equations

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

theorem GroupoidModel.FunctorOperation.refl_forgetToGrpd : refl.comp CategoryTheory.PGrpd.forgetToGrpd = diag.comp id

def GroupoidModel.FunctorOperation.R : CategoryTheory.Functor CategoryTheory.PGrpd id.Groupoidal

Equations

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

theorem GroupoidModel.FunctorOperation.RKForget : R.comp (CategoryTheory.Functor.Groupoidal.forget.comp CategoryTheory.BPGrpd.forgetToGrpd) = CategoryTheory.PGrpd.forgetToGrpd

def GroupoidModel.Id' : CategoryTheory.yoneda.obj (U.ext π) ⟶ smallU.Ty

Equations

• GroupoidModel.Id' = GroupoidModel.yonedaCategoryEquiv.symm sorry

def GroupoidModel.Refl' : E ⟶ E

Equations

• GroupoidModel.Refl' = CategoryTheory.AsSmall.up.map (CategoryTheory.Functor.id (CategoryTheory.Core (CategoryTheory.AsSmall CategoryTheory.PGrpd)))

def GroupoidModel.Diag' : E ⟶ U.ext π

Equations

• GroupoidModel.Diag' = ⋯.lift (CategoryTheory.eqToHom GroupoidModel.Diag'._proof_1) (CategoryTheory.eqToHom GroupoidModel.Diag'._proof_2) GroupoidModel.Diag'._proof_3

def GroupoidModel.smallUId.id : CategoryTheory.Limits.pullback smallU.tp smallU.tp ⟶ smallU.Ty

Equations

• GroupoidModel.smallUId.id = sorry

def GroupoidModel.smallUId.refl : smallU.Tm ⟶ smallU.Tm

Equations

• GroupoidModel.smallUId.refl = sorry

def GroupoidModel.smallUId.comm : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.lift (CategoryTheory.CategoryStruct.id smallU.Tm) (CategoryTheory.CategoryStruct.id smallU.Tm) ⋯) id = CategoryTheory.CategoryStruct.comp refl smallU.tp

Equations

• GroupoidModel.smallUId.comm = ⋯

def GroupoidModel.smallUId.smallUIdBase : smallU.IdIntro

Equations

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