Here we define pointed categories and pointed groupoids as well as prove some basic lemmas.

@[reducible, inline]

abbrev CategoryTheory.PCat : Type (max (max (u + 1) (v + 1)) u)

Equations

• CategoryTheory.PCat = (CategoryTheory.Functor.id CategoryTheory.Cat).Grothendieck

@[reducible, inline]

abbrev CategoryTheory.PCat.forgetToCat : Functor PCat Cat

The functor that takes PCat to Cat by forgetting the points

Equations

• CategoryTheory.PCat.forgetToCat = CategoryTheory.Functor.Grothendieck.forget (CategoryTheory.Functor.id CategoryTheory.Cat)

def CategoryTheory.PCat.«term⇓_» : Lean.ParserDescr

Equations

• CategoryTheory.PCat.«term⇓_» = Lean.ParserDescr.node `CategoryTheory.PCat.«term⇓_» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⇓") (Lean.ParserDescr.cat `term 1024))

def CategoryTheory.PCat.«term_⟱» : Lean.TrailingParserDescr

Equations

• CategoryTheory.PCat.«term_⟱» = Lean.ParserDescr.trailingNode `CategoryTheory.PCat.«term_⟱» 1024 1024 (Lean.ParserDescr.symbol "⟱")

theorem CategoryTheory.PCat.forgetToCat_map {C D : PCat} (F : C ⟶ D) : forgetToCat.map F = F.base

@[simp]

theorem CategoryTheory.PCat.id_obj {C : PCat} (X : ↑C.base) : (forgetToCat.map (CategoryStruct.id C)).obj X = X

@[simp]

theorem CategoryTheory.PCat.id_map {C : PCat} {X Y : ↑C.base} (f : X ⟶ Y) : (forgetToCat.map (CategoryStruct.id C)).map f = f

@[simp]

theorem CategoryTheory.PCat.id_fiber {C : PCat} : (CategoryStruct.id C).fiber = CategoryStruct.id (((Functor.id Cat).map (CategoryStruct.id C).base).obj C.fiber)

@[simp]

theorem CategoryTheory.PCat.comp_obj {C D E : PCat} (F : C ⟶ D) (G : D ⟶ E) (X : ↑C.base) : (forgetToCat.map (CategoryStruct.comp F G)).obj X = (forgetToCat.map G).obj ((forgetToCat.map F).obj X)

@[simp]

theorem CategoryTheory.PCat.comp_map {C D E : PCat} (F : C ⟶ D) (G : D ⟶ E) {X Y : ↑C.base} (f : X ⟶ Y) : (forgetToCat.map (CategoryStruct.comp F G)).map f = (forgetToCat.map G).map ((forgetToCat.map F).map f)

@[simp]

theorem CategoryTheory.PCat.comp_fiber {C D E : PCat} (F : C ⟶ D) (G : D ⟶ E) : (CategoryStruct.comp F G).fiber = CategoryStruct.comp ((forgetToCat.map G).map F.fiber) G.fiber

@[simp]

theorem CategoryTheory.PCat.map_id_fiber {C : Type u} [Category.{v, u} C] {F : Functor C PCat} {x : C} : (F.map (CategoryStruct.id x)).fiber = eqToHom ⋯

@[simp]

theorem CategoryTheory.PCat.map_comp_fiber {C : Type u} [Category.{v, u} C] {F : Functor C PCat} {x y z : C} (f : x ⟶ y) (g : y ⟶ z) : (F.map (CategoryStruct.comp f g)).fiber = CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp ((forgetToCat.map (F.map g)).map (F.map f).fiber) (F.map g).fiber)

theorem CategoryTheory.PCat.eqToHom_point_aux {P1 P2 : PCat} (eq : P1 = P2) : (forgetToCat.map (eqToHom eq)).obj P1.fiber = P2.fiber

This is the proof of equality used in the eqToHom in PCat.eqToHom_point

theorem CategoryTheory.PCat.eqToHom_fiber {P1 P2 : PCat} (eq : P1 = P2) : (eqToHom eq).fiber = eqToHom ⋯

This shows that the fiber map of an eqToHom in PCat is an eqToHom

def CategoryTheory.PCat.objFiber {Γ : Type u₂} [Category.{v₂, u₂} Γ] (α : Functor Γ PCat) (x : Γ) : ↑(forgetToCat.obj (α.obj x))

Equations

• CategoryTheory.PCat.objFiber α x = (α.obj x).fiber

def CategoryTheory.PCat.mapObjFiber {Γ : Type u₂} [Category.{v₂, u₂} Γ] (α : Functor Γ PCat) {x y : Γ} (f : x ⟶ y) : ↑(forgetToCat.obj (α.obj y))

Equations

• CategoryTheory.PCat.mapObjFiber α f = (CategoryTheory.PCat.forgetToCat.map (α.map f)).obj (CategoryTheory.PCat.objFiber α x)

def CategoryTheory.PCat.mapFiber {Γ : Type u₂} [Category.{v₂, u₂} Γ] (α : Functor Γ PCat) {x y : Γ} (f : x ⟶ y) : mapObjFiber α f ⟶ objFiber α y

Equations

• CategoryTheory.PCat.mapFiber α f = (α.map f).fiber

@[simp]

theorem CategoryTheory.PCat.mapFiber_id {Γ : Type u₂} [Category.{v₂, u₂} Γ] (α : Functor Γ PCat) {x : Γ} : mapFiber α (CategoryStruct.id x) = eqToHom ⋯

theorem CategoryTheory.PCat.mapFiber_comp {Γ : Type u₂} [Category.{v₂, u₂} Γ] (α : Functor Γ PCat) {x y z : Γ} (f : x ⟶ y) (g : y ⟶ z) : mapFiber α (CategoryStruct.comp f g) = CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp ((forgetToCat.map (α.map g)).map (mapFiber α f)) (mapFiber α g))

theorem CategoryTheory.PCat.eqToHom_base_map {x y : PCat} (eq : x = y) {a b : ↑x.base} (f : a ⟶ b) : (eqToHom eq).base.map f = CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp ((eqToHom ⋯).map f) (eqToHom ⋯))

def CategoryTheory.PCat.asSmallFunctor : Functor PCat PCat

Equations

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

@[reducible, inline]

abbrev CategoryTheory.PGrpd : Type (max (max (u + 1) (v + 1)) u)

Equations

• CategoryTheory.PGrpd = CategoryTheory.Grpd.forgetToCat.Grothendieck

@[reducible, inline]

abbrev CategoryTheory.PGrpd.forgetToGrpd : Functor PGrpd Grpd

The functor that takes PGrpd to Grpd by forgetting the points

Equations

• CategoryTheory.PGrpd.forgetToGrpd = CategoryTheory.Functor.Grothendieck.forget CategoryTheory.Grpd.forgetToCat

def CategoryTheory.PGrpd.forgetToPCat : Functor PGrpd PCat

The forgetful functor from PGrpd to PCat

Equations

• CategoryTheory.PGrpd.forgetToPCat = CategoryTheory.Functor.Grothendieck.pre (CategoryTheory.Functor.id CategoryTheory.Cat) CategoryTheory.Grpd.forgetToCat

def CategoryTheory.PGrpd.«term⇓_» : Lean.ParserDescr

Equations

• CategoryTheory.PGrpd.«term⇓_» = Lean.ParserDescr.node `CategoryTheory.PGrpd.«term⇓_» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⇓") (Lean.ParserDescr.cat `term 1024))

def CategoryTheory.PGrpd.«term_⟱» : Lean.TrailingParserDescr

Equations

• CategoryTheory.PGrpd.«term_⟱» = Lean.ParserDescr.trailingNode `CategoryTheory.PGrpd.«term_⟱» 1024 1024 (Lean.ParserDescr.symbol "⟱")

theorem CategoryTheory.PGrpd.forgetToGrpd_map {C D : PGrpd} (F : C ⟶ D) : forgetToGrpd.map F = F.base

@[simp]

theorem CategoryTheory.PGrpd.id_obj {C : PGrpd} (X : ↑C.base) : (forgetToGrpd.map (CategoryStruct.id C)).obj X = X

@[simp]

theorem CategoryTheory.PGrpd.id_map {C : PGrpd} {X Y : ↑C.base} (f : X ⟶ Y) : (forgetToGrpd.map (CategoryStruct.id C)).map f = f

@[simp]

theorem CategoryTheory.PGrpd.id_fiber {C : PGrpd} : (CategoryStruct.id C).fiber = CategoryStruct.id ((Grpd.forgetToCat.map (CategoryStruct.id C).base).obj C.fiber)

@[simp]

theorem CategoryTheory.PGrpd.comp_obj {C D E : PGrpd} (F : C ⟶ D) (G : D ⟶ E) (X : ↑C.base) : (forgetToGrpd.map (CategoryStruct.comp F G)).obj X = (forgetToGrpd.map G).obj ((forgetToGrpd.map F).obj X)

@[simp]

theorem CategoryTheory.PGrpd.comp_map {C D E : PGrpd} (F : C ⟶ D) (G : D ⟶ E) {X Y : ↑C.base} (f : X ⟶ Y) : (forgetToGrpd.map (CategoryStruct.comp F G)).map f = (forgetToGrpd.map G).map ((forgetToGrpd.map F).map f)

@[simp]

theorem CategoryTheory.PGrpd.comp_fiber {C D E : PGrpd} (F : C ⟶ D) (G : D ⟶ E) : (CategoryStruct.comp F G).fiber = CategoryStruct.comp ((forgetToGrpd.map G).map F.fiber) G.fiber

@[simp]

theorem CategoryTheory.PGrpd.map_id_fiber {C : Type u} [Category.{v, u} C] {F : Functor C PGrpd} {x : C} : (F.map (CategoryStruct.id x)).fiber = eqToHom ⋯

@[simp]

theorem CategoryTheory.PGrpd.map_comp_fiber {C : Type u} [Category.{v, u} C] {F : Functor C PGrpd} {x y z : C} (f : x ⟶ y) (g : y ⟶ z) : (F.map (CategoryStruct.comp f g)).fiber = CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp ((forgetToGrpd.map (F.map g)).map (F.map f).fiber) (F.map g).fiber)

theorem CategoryTheory.PGrpd.eqToHom_point_aux {P1 P2 : PGrpd} (eq : P1 = P2) : (forgetToGrpd.map (eqToHom eq)).obj P1.fiber = P2.fiber

This is the proof of equality used in the eqToHom in PGrpd.eqToHom_point

theorem CategoryTheory.PGrpd.eqToHom_fiber {P1 P2 : PGrpd} (eq : P1 = P2) : (eqToHom eq).fiber = eqToHom ⋯

This shows that the fiber map of an eqToHom in PGrpd is an eqToHom

instance CategoryTheory.PGrpd.instReflectsIsomorphismsGrpdForgetToGrpd : forgetToGrpd.ReflectsIsomorphisms

def CategoryTheory.PGrpd.objFiber {Γ : Type u₂} [Category.{v₂, u₂} Γ] (α : Functor Γ PGrpd) (x : Γ) : ↑(forgetToGrpd.obj (α.obj x))

Equations

• CategoryTheory.PGrpd.objFiber α x = (α.obj x).fiber

theorem CategoryTheory.PGrpd.objFiber_naturality {Γ : Type u₂} [Category.{v₂, u₂} Γ] {Δ : Type u_1} [Category.{u_2, u_1} Δ] (σ : Functor Δ Γ) (α : Functor Γ PGrpd) (x : Δ) : objFiber (σ.comp α) x = objFiber α (σ.obj x)

def CategoryTheory.PGrpd.mapObjFiber {Γ : Type u₂} [Category.{v₂, u₂} Γ] (α : Functor Γ PGrpd) {x y : Γ} (f : x ⟶ y) : ↑(forgetToGrpd.obj (α.obj y))

Equations

• CategoryTheory.PGrpd.mapObjFiber α f = (CategoryTheory.PGrpd.forgetToGrpd.map (α.map f)).obj (CategoryTheory.PGrpd.objFiber α x)

def CategoryTheory.PGrpd.mapFiber {Γ : Type u₂} [Category.{v₂, u₂} Γ] (α : Functor Γ PGrpd) {x y : Γ} (f : x ⟶ y) : mapObjFiber α f ⟶ objFiber α y

Equations

• CategoryTheory.PGrpd.mapFiber α f = (α.map f).fiber

@[simp]

theorem CategoryTheory.PGrpd.mapFiber_id {Γ : Type u₂} [Category.{v₂, u₂} Γ] (α : Functor Γ PGrpd) {x : Γ} : mapFiber α (CategoryStruct.id x) = eqToHom ⋯

theorem CategoryTheory.PGrpd.mapFiber_comp {Γ : Type u₂} [Category.{v₂, u₂} Γ] (α : Functor Γ PGrpd) {x y z : Γ} (f : x ⟶ y) (g : y ⟶ z) : mapFiber α (CategoryStruct.comp f g) = CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp ((forgetToGrpd.map (α.map g)).map (mapFiber α f)) (mapFiber α g))

theorem CategoryTheory.PGrpd.mapFiber_naturality {Γ : Type u₂} [Category.{v₂, u₂} Γ] (α : Functor Γ PGrpd) {Δ : Type u_1} [Category.{u_2, u_1} Δ] (σ : Functor Δ Γ) {x y : Δ} (f : x ⟶ y) : mapFiber (σ.comp α) f = mapFiber α (σ.map f)

@[reducible, inline]

abbrev CategoryTheory.PGrpd.objFiber'EqToHom {Γ : Type u₂} [Category.{v₂, u₂} Γ] {A : Functor Γ Grpd} {α : Functor Γ PGrpd} (h : α.comp forgetToGrpd = A) (x : Γ) : Functor ↑((α.comp forgetToGrpd).obj x) ↑(A.obj x)

This definition ensures that we deal with the functor (α ⋙ forgetToGrpd).obj x ⥤ A.obj x as opposed to the

Equations

• CategoryTheory.PGrpd.objFiber'EqToHom h x = CategoryTheory.eqToHom ⋯

def CategoryTheory.PGrpd.objFiber' {Γ : Type u₂} [Category.{v₂, u₂} Γ] {A : Functor Γ Grpd} {α : Functor Γ PGrpd} (h : α.comp forgetToGrpd = A) (x : Γ) : ↑(A.obj x)

Equations

• CategoryTheory.PGrpd.objFiber' h x = (CategoryTheory.PGrpd.objFiber'EqToHom h x).obj (CategoryTheory.PGrpd.objFiber α x)

@[simp]

theorem CategoryTheory.PGrpd.objFiber'_rfl {Γ : Type u₂} [Category.{v₂, u₂} Γ] {α : Functor Γ PGrpd} (x : Γ) : objFiber' ⋯ x = objFiber α x

@[simp]

theorem CategoryTheory.PGrpd.objFiber'_heq {Γ : Type u₂} [Category.{v₂, u₂} Γ] {A : Functor Γ Grpd} {α : Functor Γ PGrpd} (h : α.comp forgetToGrpd = A) {x : Γ} : objFiber' h x ≍ (α.obj x).fiber

theorem CategoryTheory.PGrpd.objFiber'_naturality {Γ : Type u₂} [Category.{v₂, u₂} Γ] {Δ : Type u_1} [Category.{u_2, u_1} Δ] (σ : Functor Δ Γ) {A : Functor Γ Grpd} {α : Functor Γ PGrpd} (h : α.comp forgetToGrpd = A) (x : Δ) : objFiber' ⋯ x = objFiber' h (σ.obj x)

def CategoryTheory.PGrpd.mapFiber'EqToHom {Γ : Type u₂} [Category.{v₂, u₂} Γ] {A : Functor Γ Grpd} {α : Functor Γ PGrpd} (h : α.comp forgetToGrpd = A) {x y : Γ} (f : x ⟶ y) : (A.map f).obj (objFiber' h x) ⟶ (objFiber'EqToHom h y).obj ((α.map f).base.obj (α.obj x).fiber)

Equations

• CategoryTheory.PGrpd.mapFiber'EqToHom h f = CategoryTheory.eqToHom ⋯

def CategoryTheory.PGrpd.mapFiber' {Γ : Type u₂} [Category.{v₂, u₂} Γ] {A : Functor Γ Grpd} {α : Functor Γ PGrpd} (h : α.comp forgetToGrpd = A) {x y : Γ} (f : x ⟶ y) : (A.map f).obj (objFiber' h x) ⟶ objFiber' h y

Equations

• CategoryTheory.PGrpd.mapFiber' h f = CategoryTheory.CategoryStruct.comp (CategoryTheory.PGrpd.mapFiber'EqToHom h f) ((CategoryTheory.PGrpd.objFiber'EqToHom h y).map (α.map f).fiber)

@[simp]

theorem CategoryTheory.PGrpd.mapFiber'_id {Γ : Type u₂} [Category.{v₂, u₂} Γ] {A : Functor Γ Grpd} {α : Functor Γ PGrpd} (h : α.comp forgetToGrpd = A) {x : Γ} : mapFiber' h (CategoryStruct.id x) = eqToHom ⋯

@[simp]

theorem CategoryTheory.PGrpd.mapFiber'_heq {Γ : Type u₂} [Category.{v₂, u₂} Γ] {A : Functor Γ Grpd} {α : Functor Γ PGrpd} (h : α.comp forgetToGrpd = A) {x y : Γ} (f : x ⟶ y) : mapFiber' h f ≍ (α.map f).fiber

theorem CategoryTheory.PGrpd.mapFiber'_comp_aux0 {Γ : Type u₂} [Category.{v₂, u₂} Γ] {A : Functor Γ Grpd} {α : Functor Γ PGrpd} (h : α.comp forgetToGrpd = A) {z : Γ} : Grpd.of ↑(forgetToGrpd.obj (α.obj z)) = A.obj z

theorem CategoryTheory.PGrpd.mapFiber'_comp_aux1 {Γ : Type u₂} [Category.{v₂, u₂} Γ] {A : Functor Γ Grpd} {α : Functor Γ PGrpd} (h : α.comp forgetToGrpd = A) {x y z : Γ} (f : x ⟶ y) (g : y ⟶ z) : (A.map (CategoryStruct.comp f g)).obj (objFiber' h x) = (eqToHom ⋯).obj ((forgetToGrpd.map (α.map (CategoryStruct.comp f g))).obj (α.obj x).fiber)

theorem CategoryTheory.PGrpd.mapFiber'_comp {Γ : Type u₂} [Category.{v₂, u₂} Γ] {A : Functor Γ Grpd} {α : Functor Γ PGrpd} (h : α.comp forgetToGrpd = A) {x y z : Γ} (f : x ⟶ y) (g : y ⟶ z) : mapFiber' h (CategoryStruct.comp f g) = CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp ((eqToHom ⋯).map ((α.map g).base.map (α.map f).fiber)) ((eqToHom ⋯).map (α.map g).fiber))

theorem CategoryTheory.PGrpd.mapFiber'_naturality {Γ : Type u₂} [Category.{v₂, u₂} Γ] {A : Functor Γ Grpd} {α : Functor Γ PGrpd} (h : α.comp forgetToGrpd = A) {Δ : Type u_1} [Category.{u_2, u_1} Δ] (σ : Functor Δ Γ) {x y : Δ} (f : x ⟶ y) : mapFiber' ⋯ f = mapFiber' h (σ.map f)

@[simp]

theorem CategoryTheory.PGrpd.mapFiber'_rfl {Γ : Type u₂} [Category.{v₂, u₂} Γ] {α : Functor Γ PGrpd} {x y : Γ} (f : x ⟶ y) : mapFiber' ⋯ f = mapFiber α f

theorem CategoryTheory.PGrpd.Functor.hext {Γ : Type u₂} [Category.{v₂, u₂} Γ] (F G : Functor Γ PGrpd) (hbase : F.comp forgetToGrpd = G.comp forgetToGrpd) (hfiber_obj : ∀ (x : Γ), (F.obj x).fiber ≍ (G.obj x).fiber) (hfiber_map : ∀ {x y : Γ} (f : x ⟶ y), (F.map f).fiber ≍ (G.map f).fiber) : F = G

theorem CategoryTheory.PGrpd.functorTo_map_id_aux {Γ : Type u₁} [Category.{v₁, u₁} Γ] (A : Functor Γ Grpd) (fibObj : (x : Γ) → ↑(A.obj x)) (x : Γ) : (A.map (CategoryStruct.id x)).obj (fibObj x) = fibObj x

theorem CategoryTheory.PGrpd.functorTo_map_comp_aux {Γ : Type u₁} [Category.{v₁, u₁} Γ] (A : Functor Γ Grpd) (fibObj : (x : Γ) → ↑(A.obj x)) {x y z : Γ} (f : x ⟶ y) (g : y ⟶ z) : (A.map (CategoryStruct.comp f g)).obj (fibObj x) = (A.map g).obj ((A.map f).obj (fibObj x))

def CategoryTheory.PGrpd.functorTo {Γ : Type u₁} [Category.{v₁, u₁} Γ] (A : Functor Γ Grpd) (fibObj : (x : Γ) → ↑(A.obj x)) (fibMap : {x y : Γ} → (f : x ⟶ y) → (A.map f).obj (fibObj x) ⟶ fibObj y) (map_id : ∀ (x : Γ), fibMap (CategoryStruct.id x) = eqToHom ⋯) (map_comp : ∀ {x y z : Γ} (f : x ⟶ y) (g : y ⟶ z), fibMap (CategoryStruct.comp f g) = CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp ((A.map g).map (fibMap f)) (fibMap g))) : Functor Γ PGrpd

To define a functor into PGrpd we can make use of an existing functor into Grpd. This is definitinoally just Grothendieck.functorTo, but giving the user a slightly less bloated context.

Equations

• CategoryTheory.PGrpd.functorTo A fibObj fibMap map_id map_comp = CategoryTheory.Functor.Grothendieck.functorTo A fibObj (fun {x y : Γ} => fibMap) map_id ⋯

@[simp]

theorem CategoryTheory.PGrpd.functorTo_obj_base {Γ : Type u₁} [Category.{v₁, u₁} Γ] (A : Functor Γ Grpd) (fibObj : (x : Γ) → ↑(A.obj x)) (fibMap : {x y : Γ} → (f : x ⟶ y) → (A.map f).obj (fibObj x) ⟶ fibObj y) (map_id : ∀ (x : Γ), fibMap (CategoryStruct.id x) = eqToHom ⋯) (map_comp : ∀ {x y z : Γ} (f : x ⟶ y) (g : y ⟶ z), fibMap (CategoryStruct.comp f g) = CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp ((A.map g).map (fibMap f)) (fibMap g))) (x : Γ) : ((functorTo A fibObj (fun {x y : Γ} => fibMap) map_id ⋯).obj x).base = A.obj x

@[simp]

theorem CategoryTheory.PGrpd.functorTo_obj_fiber {Γ : Type u₁} [Category.{v₁, u₁} Γ] (A : Functor Γ Grpd) (fibObj : (x : Γ) → ↑(A.obj x)) (fibMap : {x y : Γ} → (f : x ⟶ y) → (A.map f).obj (fibObj x) ⟶ fibObj y) (map_id : ∀ (x : Γ), fibMap (CategoryStruct.id x) = eqToHom ⋯) (map_comp : ∀ {x y z : Γ} (f : x ⟶ y) (g : y ⟶ z), fibMap (CategoryStruct.comp f g) = CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp ((A.map g).map (fibMap f)) (fibMap g))) (x : Γ) : ((functorTo A fibObj (fun {x y : Γ} => fibMap) map_id ⋯).obj x).fiber = fibObj x

@[simp]

theorem CategoryTheory.PGrpd.functorTo_map_base {Γ : Type u₁} [Category.{v₁, u₁} Γ] (A : Functor Γ Grpd) (fibObj : (x : Γ) → ↑(A.obj x)) (fibMap : {x y : Γ} → (f : x ⟶ y) → (A.map f).obj (fibObj x) ⟶ fibObj y) (map_id : ∀ (x : Γ), fibMap (CategoryStruct.id x) = eqToHom ⋯) (map_comp : ∀ {x y z : Γ} (f : x ⟶ y) (g : y ⟶ z), fibMap (CategoryStruct.comp f g) = CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp ((A.map g).map (fibMap f)) (fibMap g))) {x y : Γ} (f : x ⟶ y) : ((functorTo A fibObj (fun {x y : Γ} => fibMap) map_id ⋯).map f).base = A.map f

@[simp]

theorem CategoryTheory.PGrpd.functorTo_map_fiber {Γ : Type u₁} [Category.{v₁, u₁} Γ] (A : Functor Γ Grpd) (fibObj : (x : Γ) → ↑(A.obj x)) (fibMap : {x y : Γ} → (f : x ⟶ y) → (A.map f).obj (fibObj x) ⟶ fibObj y) (map_id : ∀ (x : Γ), fibMap (CategoryStruct.id x) = eqToHom ⋯) (map_comp : ∀ {x y z : Γ} (f : x ⟶ y) (g : y ⟶ z), fibMap (CategoryStruct.comp f g) = CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp ((A.map g).map (fibMap f)) (fibMap g))) {x y : Γ} (f : x ⟶ y) : ((functorTo A fibObj (fun {x y : Γ} => fibMap) map_id ⋯).map f).fiber = fibMap f

@[simp]

theorem CategoryTheory.PGrpd.functorTo_forget {Γ : Type u₁} [Category.{v₁, u₁} Γ] {A : Functor Γ Grpd} {fibObj : (x : Γ) → ↑(A.obj x)} {fibMap : {x y : Γ} → (f : x ⟶ y) → (A.map f).obj (fibObj x) ⟶ fibObj y} {map_id : ∀ (x : Γ), fibMap (CategoryStruct.id x) = eqToHom ⋯} {map_comp : ∀ {x y z : Γ} (f : x ⟶ y) (g : y ⟶ z), fibMap (CategoryStruct.comp f g) = CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp ((A.map g).map (fibMap f)) (fibMap g))} : (functorTo A fibObj fibMap map_id ⋯).comp (Functor.Grothendieck.forget Grpd.forgetToCat) = A