@[reducible, inline]

abbrev CategoryTheory.TotalCat {C : Type u_3} {E : Type u_4} [CategoryTheory.Category.{u_5, u_3} C] [CategoryTheory.Category.{u_6, u_4} E] (P : CategoryTheory.Functor E C) : Type (max u_3 u_4)

Equations

• ∫ P = Fiber.Total P.obj

def CategoryTheory.«term∫_» : Lean.ParserDescr

Equations

• CategoryTheory.«term∫_» = Lean.ParserDescr.node `CategoryTheory.term∫_ 75 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∫ ") (Lean.ParserDescr.cat `term 75))

theorem CategoryTheory.TotalCatHom.ext_iff {C : Type u_1} {E : Type u_2} : ∀ {inst : CategoryTheory.Category.{u_3, u_1} C} {inst_1 : CategoryTheory.Category.{u_4, u_2} E} {P : CategoryTheory.Functor E C} {X Y : ∫ P} (x y : CategoryTheory.TotalCatHom X Y), x = y ↔ x.base = y.base ∧ x.fiber = y.fiber

theorem CategoryTheory.TotalCatHom.ext {C : Type u_1} {E : Type u_2} : ∀ {inst : CategoryTheory.Category.{u_3, u_1} C} {inst_1 : CategoryTheory.Category.{u_4, u_2} E} {P : CategoryTheory.Functor E C} {X Y : ∫ P} (x y : CategoryTheory.TotalCatHom X Y), x.base = y.base → x.fiber = y.fiber → x = y

structure CategoryTheory.TotalCatHom {C : Type u_1} {E : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} E] {P : CategoryTheory.Functor E C} (X : ∫ P) (Y : ∫ P) : Type (max u_3 u_4)

• base : X.base ⟶ Y.base
• fiber : ↑X.fiber ⟶ ↑Y.fiber
• eq : CategoryTheory.CategoryStruct.comp (P.map self.fiber) (CategoryTheory.eqToHom ⋯) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) self.base

theorem CategoryTheory.TotalCatHom.eq {C : Type u_1} {E : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} E] {P : CategoryTheory.Functor E C} {X : ∫ P} {Y : ∫ P} (self : CategoryTheory.TotalCatHom X Y) : CategoryTheory.CategoryStruct.comp (P.map self.fiber) (CategoryTheory.eqToHom ⋯) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) self.base

def CategoryTheory.TotalCat.BasedLiftOf {C : Type u_1} {E : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} E] {P : CategoryTheory.Functor E C} {X : ∫ P} {Y : ∫ P} (g : CategoryTheory.TotalCatHom X Y) : CategoryTheory.BasedLift P g.base X.fiber Y.fiber

Equations

• CategoryTheory.TotalCat.BasedLiftOf g = { hom := g.fiber, over := ⋯ }

@[simp]

theorem CategoryTheory.TotalCat.over_base {C : Type u_1} {E : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_3, u_2} E] {P : CategoryTheory.Functor E C} {X : ∫ P} {Y : ∫ P} (g : CategoryTheory.TotalCatHom X Y) : P.map g.fiber = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp g.base (CategoryTheory.eqToHom ⋯))

instance CategoryTheory.TotalCat.instCatOfTotal {C : Type u_1} {E : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} E] (P : CategoryTheory.Functor E C) : CategoryTheory.Category.{max u_4 u_3, max u_2 u_1} ( ∫ P)

Equations

• CategoryTheory.TotalCat.instCatOfTotal P = CategoryTheory.Category.mk ⋯ ⋯ ⋯