Special shapes for limits in Type.

The general shape (co)limits defined in CategoryTheory.Limits.Types are intended for use through the limits API, and the actual implementation should mostly be considered "sealed".

In this file, we provide definitions of the "standard" special shapes of limits in Type, giving the expected definitional implementation:

• the terminal object is PUnit
• the binary product of X and Y is X × Y
• the product of a family f : J → Type is Π j, f j
• the coproduct of a family f : J → Type is Σ j, f j
• the binary coproduct of X and Y is the sum type X ⊕ Y
• the equalizer of a pair of maps (g, h) is the subtype {x : Y // g x = h x}
• the coequalizer of a pair of maps (f, g) is the quotient of Y by ∀ x : Y, f x ~ g x
• the pullback of f : X ⟶ Z and g : Y ⟶ Z is the subtype { p : X × Y // f p.1 = g p.2 } of the product

We first construct terms of IsLimit and LimitCone, and then provide isomorphisms with the types generated by the HasLimit API.

As an example, when setting up the monoidal category structure on Type we use the Types.terminalLimitCone and Types.binaryProductLimitCone definitions.

instance CategoryTheory.Limits.Types.instHasProductsTypeTypes : CategoryTheory.Limits.HasProducts (Type v)

@[simp]

theorem CategoryTheory.Limits.Types.pi_lift_π_apply [UnivLE.{v, u} ] {β : Type v} (f : β → Type u) {P : Type u} (s : (b : β) → P ⟶ f b) (b : β) (x : P) : CategoryTheory.Limits.Pi.π β (Type u) CategoryTheory.types f (_ : CategoryTheory.Limits.HasLimit (CategoryTheory.Discrete.functor f)) b (CategoryTheory.Limits.Pi.lift s x) = s b x

A restatement of Types.Limit.lift_π_apply that uses Pi.π and Pi.lift.

theorem CategoryTheory.Limits.Types.pi_lift_π_apply' {β : Type v} (f : β → Type v) {P : Type v} (s : (b : β) → P ⟶ f b) (b : β) (x : P) : CategoryTheory.Limits.Pi.π β (Type v) CategoryTheory.types f (_ : CategoryTheory.Limits.HasLimit (CategoryTheory.Discrete.functor f)) b (CategoryTheory.Limits.Pi.lift s x) = s b x

A restatement of Types.Limit.lift_π_apply that uses Pi.π and Pi.lift, with specialized universes.

@[simp]

theorem CategoryTheory.Limits.Types.pi_map_π_apply [UnivLE.{v, u} ] {β : Type v} {f : β → Type u} {g : β → Type u} (α : (j : β) → f j ⟶ g j) (b : β) (x : ∏ fun b => f b) : CategoryTheory.Limits.Pi.π β (Type u) CategoryTheory.types g (_ : CategoryTheory.Limits.HasLimit (CategoryTheory.Discrete.functor g)) b (CategoryTheory.Limits.Pi.map α x) = α b (CategoryTheory.Limits.Pi.π β (Type u) CategoryTheory.types f (_ : CategoryTheory.Limits.HasLimit (CategoryTheory.Discrete.functor f)) b x)

A restatement of Types.Limit.map_π_apply that uses Pi.π and Pi.map.

theorem CategoryTheory.Limits.Types.pi_map_π_apply' {β : Type v} {f : β → Type v} {g : β → Type v} (α : (j : β) → f j ⟶ g j) (b : β) (x : ∏ fun b => f b) : CategoryTheory.Limits.Pi.π β (Type v) CategoryTheory.types g (_ : CategoryTheory.Limits.HasLimit (CategoryTheory.Discrete.functor g)) b (CategoryTheory.Limits.Pi.map α x) = α b (CategoryTheory.Limits.Pi.π β (Type v) CategoryTheory.types f (_ : CategoryTheory.Limits.HasLimit (CategoryTheory.Discrete.functor f)) b x)

A restatement of Types.Limit.map_π_apply that uses Pi.π and Pi.map, with specialized universes.

def CategoryTheory.Limits.Types.terminalLimitCone : CategoryTheory.Limits.LimitCone (CategoryTheory.Functor.empty (Type u))

The category of types has PUnit as a terminal object.

noncomputable def CategoryTheory.Limits.Types.terminalIso : ⊤_ Type u ≅ PUnit.{u + 1}

The terminal object in Type u is PUnit.

noncomputable def CategoryTheory.Limits.Types.isTerminalPunit : CategoryTheory.Limits.IsTerminal PUnit.{u + 1}

The terminal object in Type u is PUnit.

noncomputable instance CategoryTheory.Limits.Types.instInhabitedTerminalTypeTypesHasLimitsOfShapeOfHasLimitsDiscretePEmptyDiscreteCategoryHasLimitsOfSizeInstSmallSmall_self : Inhabited (⊤_ Type u)

instance CategoryTheory.Limits.Types.instSubsingletonTerminalTypeTypesHasLimitsOfShapeOfHasLimitsDiscretePEmptyDiscreteCategoryHasLimitsOfSizeInstSmallSmall_self : Subsingleton (⊤_ Type u)

noncomputable instance CategoryTheory.Limits.Types.instUniqueTerminalTypeTypesHasLimitsOfShapeOfHasLimitsDiscretePEmptyDiscreteCategoryHasLimitsOfSizeInstSmallSmall_self : Unique (⊤_ Type u)

noncomputable def CategoryTheory.Limits.Types.isTerminalEquivUnique (X : Type u) : CategoryTheory.Limits.IsTerminal X ≃ Unique X

A type is terminal if and only if it contains exactly one element.

noncomputable def CategoryTheory.Limits.Types.isTerminalEquivIsoPUnit (X : Type u) : CategoryTheory.Limits.IsTerminal X ≃ (X ≅ PUnit.{u + 1} )

A type is terminal if and only if it is isomorphic to PUnit.

def CategoryTheory.Limits.Types.initialColimitCocone : CategoryTheory.Limits.ColimitCocone (CategoryTheory.Functor.empty (Type u))

The category of types has PEmpty as an initial object.

noncomputable def CategoryTheory.Limits.Types.initialIso : ⊥_ Type u ≅ PEmpty.{u + 1}

The initial object in Type u is PEmpty.

noncomputable def CategoryTheory.Limits.Types.isInitialPunit : CategoryTheory.Limits.IsInitial PEmpty.{u + 1}

The initial object in Type u is PEmpty.

@[simp]

theorem CategoryTheory.Limits.Types.binaryProductCone_pt (X : Type u) (Y : Type u) : (CategoryTheory.Limits.Types.binaryProductCone X Y).pt = (X × Y)

def CategoryTheory.Limits.Types.binaryProductCone (X : Type u) (Y : Type u) : CategoryTheory.Limits.BinaryFan X Y

The product type X × Y forms a cone for the binary product of X and Y.

@[simp]

theorem CategoryTheory.Limits.Types.binaryProductCone_fst (X : Type u) (Y : Type u) : CategoryTheory.Limits.BinaryFan.fst (CategoryTheory.Limits.Types.binaryProductCone X Y) = Prod.fst

@[simp]

theorem CategoryTheory.Limits.Types.binaryProductCone_snd (X : Type u) (Y : Type u) : CategoryTheory.Limits.BinaryFan.snd (CategoryTheory.Limits.Types.binaryProductCone X Y) = Prod.snd

@[simp]

theorem CategoryTheory.Limits.Types.binaryProductLimit_lift (X : Type u) (Y : Type u) (s : CategoryTheory.Limits.BinaryFan X Y) (x : s.pt) : CategoryTheory.Limits.IsLimit.lift (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) (CategoryTheory.discreteCategory CategoryTheory.Limits.WalkingPair) (Type u) CategoryTheory.types (CategoryTheory.Limits.pair X Y) (CategoryTheory.Limits.Types.binaryProductCone X Y) (CategoryTheory.Limits.Types.binaryProductLimit X Y) s x = (CategoryTheory.Limits.BinaryFan.fst (Type u) CategoryTheory.types X Y s x, CategoryTheory.Limits.BinaryFan.snd (Type u) CategoryTheory.types X Y s x)

def CategoryTheory.Limits.Types.binaryProductLimit (X : Type u) (Y : Type u) : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Types.binaryProductCone X Y)

The product type X × Y is a binary product for X and Y.

@[simp]

theorem CategoryTheory.Limits.Types.binaryProductLimitCone_cone (X : Type u) (Y : Type u) : (CategoryTheory.Limits.Types.binaryProductLimitCone X Y).cone = CategoryTheory.Limits.Types.binaryProductCone X Y

@[simp]

theorem CategoryTheory.Limits.Types.binaryProductLimitCone_isLimit (X : Type u) (Y : Type u) : (CategoryTheory.Limits.Types.binaryProductLimitCone X Y).isLimit = CategoryTheory.Limits.Types.binaryProductLimit X Y

def CategoryTheory.Limits.Types.binaryProductLimitCone (X : Type u) (Y : Type u) : CategoryTheory.Limits.LimitCone (CategoryTheory.Limits.pair X Y)

The category of types has X × Y, the usual cartesian product, as the binary product of X and Y.

noncomputable def CategoryTheory.Limits.Types.binaryProductIso (X : Type u) (Y : Type u) : X ⨯ Y ≅ X × Y

The categorical binary product in Type u is cartesian product.

@[simp]

theorem CategoryTheory.Limits.Types.binaryProductIso_hom_comp_fst_apply (X : Type u) (Y : Type u) (x : CategoryTheory.Limits.limit (CategoryTheory.Limits.pair X Y)) : ↑Prod.fst ((CategoryTheory.Limits.limit.isoLimitCone (CategoryTheory.Limits.Types.binaryProductLimitCone X Y)).hom x) = CategoryTheory.Limits.limit.π (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) (CategoryTheory.discreteCategory CategoryTheory.Limits.WalkingPair) (Type u) CategoryTheory.types (CategoryTheory.Limits.pair X Y) (_ : CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.pair X Y)) { as := CategoryTheory.Limits.WalkingPair.left } x

@[simp]

theorem CategoryTheory.Limits.Types.binaryProductIso_hom_comp_fst (X : Type u) (Y : Type u) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Types.binaryProductIso X Y).hom Prod.fst = CategoryTheory.Limits.prod.fst

@[simp]

theorem CategoryTheory.Limits.Types.binaryProductIso_hom_comp_snd_apply (X : Type u) (Y : Type u) (x : CategoryTheory.Limits.limit (CategoryTheory.Limits.pair X Y)) : ↑Prod.snd ((CategoryTheory.Limits.limit.isoLimitCone (CategoryTheory.Limits.Types.binaryProductLimitCone X Y)).hom x) = CategoryTheory.Limits.limit.π (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) (CategoryTheory.discreteCategory CategoryTheory.Limits.WalkingPair) (Type u) CategoryTheory.types (CategoryTheory.Limits.pair X Y) (_ : CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.pair X Y)) { as := CategoryTheory.Limits.WalkingPair.right } x

@[simp]

theorem CategoryTheory.Limits.Types.binaryProductIso_hom_comp_snd (X : Type u) (Y : Type u) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Types.binaryProductIso X Y).hom Prod.snd = CategoryTheory.Limits.prod.snd

@[simp]

theorem CategoryTheory.Limits.Types.binaryProductIso_inv_comp_fst_apply (X : Type u) (Y : Type u) (x : (CategoryTheory.Limits.Types.binaryProductLimitCone X Y).cone.pt) : CategoryTheory.Limits.limit.π (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) (CategoryTheory.discreteCategory CategoryTheory.Limits.WalkingPair) (Type u) CategoryTheory.types (CategoryTheory.Limits.pair X Y) (_ : CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.pair X Y)) { as := CategoryTheory.Limits.WalkingPair.left } ((CategoryTheory.Limits.limit.isoLimitCone (CategoryTheory.Limits.Types.binaryProductLimitCone X Y)).inv x) = ↑Prod.fst x

@[simp]

theorem CategoryTheory.Limits.Types.binaryProductIso_inv_comp_fst (X : Type u) (Y : Type u) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Types.binaryProductIso X Y).inv CategoryTheory.Limits.prod.fst = Prod.fst

@[simp]

theorem CategoryTheory.Limits.Types.binaryProductIso_inv_comp_snd_apply (X : Type u) (Y : Type u) (x : (CategoryTheory.Limits.Types.binaryProductLimitCone X Y).cone.pt) : CategoryTheory.Limits.limit.π (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) (CategoryTheory.discreteCategory CategoryTheory.Limits.WalkingPair) (Type u) CategoryTheory.types (CategoryTheory.Limits.pair X Y) (_ : CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.pair X Y)) { as := CategoryTheory.Limits.WalkingPair.right } ((CategoryTheory.Limits.limit.isoLimitCone (CategoryTheory.Limits.Types.binaryProductLimitCone X Y)).inv x) = ↑Prod.snd x

@[simp]

theorem CategoryTheory.Limits.Types.binaryProductIso_inv_comp_snd (X : Type u) (Y : Type u) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Types.binaryProductIso X Y).inv CategoryTheory.Limits.prod.snd = Prod.snd

@[simp]

theorem CategoryTheory.Limits.Types.binaryProductFunctor_obj_map (X : Type u) {Y₁ : Type u} {Y₂ : Type u} (f : Y₁ ⟶ Y₂) : ∀ (a : (CategoryTheory.Limits.BinaryFan.mk Prod.fst (CategoryTheory.CategoryStruct.comp Prod.snd f)).pt), (CategoryTheory.Limits.Types.binaryProductFunctor.obj X).map f a = CategoryTheory.Limits.IsLimit.lift (CategoryTheory.Limits.Types.binaryProductLimit X Y₂) (CategoryTheory.Limits.BinaryFan.mk Prod.fst (CategoryTheory.CategoryStruct.comp Prod.snd f)) a

@[simp]

theorem CategoryTheory.Limits.Types.binaryProductFunctor_obj_obj (X : Type u) (Y : Type u) : (CategoryTheory.Limits.Types.binaryProductFunctor.obj X).obj Y = (X × Y)

@[simp]

theorem CategoryTheory.Limits.Types.binaryProductFunctor_map_app {X₁ : Type u} {X₂ : Type u} (f : X₁ ⟶ X₂) (Y : Type u) : ∀ (a : (CategoryTheory.Limits.BinaryFan.mk (CategoryTheory.CategoryStruct.comp Prod.fst f) Prod.snd).pt), (CategoryTheory.Limits.Types.binaryProductFunctor.map f).app Y a = CategoryTheory.Limits.IsLimit.lift (CategoryTheory.Limits.Types.binaryProductLimit X₂ Y) (CategoryTheory.Limits.BinaryFan.mk (CategoryTheory.CategoryStruct.comp Prod.fst f) Prod.snd) a

def CategoryTheory.Limits.Types.binaryProductFunctor : CategoryTheory.Functor (Type u) (CategoryTheory.Functor (Type u) (Type u))

The functor which sends X, Y to the product type X × Y.

noncomputable def CategoryTheory.Limits.Types.binaryProductIsoProd : CategoryTheory.Limits.Types.binaryProductFunctor ≅ CategoryTheory.Limits.prod.functor

The product functor given by the instance HasBinaryProducts (Type u) is isomorphic to the explicit binary product functor given by the product type.

@[simp]

theorem CategoryTheory.Limits.Types.binaryCoproductCocone_ι_app (X : Type u) (Y : Type u) : ∀ (x : CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) (a : (CategoryTheory.Limits.pair X Y).obj x), (CategoryTheory.Limits.Types.binaryCoproductCocone X Y).ι.app x a = CategoryTheory.Limits.WalkingPair.rec (motive := fun t => x.as = t → ((CategoryTheory.Limits.pair X Y).obj { as := x.as } ⟶ X ⊕ Y)) (fun h => (_ : CategoryTheory.Limits.WalkingPair.left = x.as) ▸ Sum.inl) (fun h => (_ : CategoryTheory.Limits.WalkingPair.right = x.as) ▸ Sum.inr) x.as (_ : x.as = x.as) a

@[simp]

theorem CategoryTheory.Limits.Types.binaryCoproductCocone_pt (X : Type u) (Y : Type u) : (CategoryTheory.Limits.Types.binaryCoproductCocone X Y).pt = (X ⊕ Y)

def CategoryTheory.Limits.Types.binaryCoproductCocone (X : Type u) (Y : Type u) : CategoryTheory.Limits.Cocone (CategoryTheory.Limits.pair X Y)

The sum type X ⊕ Y forms a cocone for the binary coproduct of X and Y.

@[simp]

theorem CategoryTheory.Limits.Types.binaryCoproductColimit_desc (X : Type u) (Y : Type u) (s : CategoryTheory.Limits.BinaryCofan X Y) : ∀ (a : X ⊕ Y), CategoryTheory.Limits.IsColimit.desc (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) (CategoryTheory.discreteCategory CategoryTheory.Limits.WalkingPair) (Type u) CategoryTheory.types (CategoryTheory.Limits.pair X Y) (CategoryTheory.Limits.Types.binaryCoproductCocone X Y) (CategoryTheory.Limits.Types.binaryCoproductColimit X Y) s a = Sum.elim (CategoryTheory.Limits.BinaryCofan.inl s) (CategoryTheory.Limits.BinaryCofan.inr s) a

def CategoryTheory.Limits.Types.binaryCoproductColimit (X : Type u) (Y : Type u) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Types.binaryCoproductCocone X Y)

The sum type X ⊕ Y is a binary coproduct for X and Y.

def CategoryTheory.Limits.Types.binaryCoproductColimitCocone (X : Type u) (Y : Type u) : CategoryTheory.Limits.ColimitCocone (CategoryTheory.Limits.pair X Y)

The category of types has X ⊕ Y, as the binary coproduct of X and Y.

noncomputable def CategoryTheory.Limits.Types.binaryCoproductIso (X : Type u) (Y : Type u) : X ⨿ Y ≅ X ⊕ Y

The categorical binary coproduct in Type u is the sum X ⊕ Y.

@[simp]

theorem CategoryTheory.Limits.Types.binaryCoproductIso_inl_comp_hom_apply (X : Type u) (Y : Type u) (x : (CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.left }) : (CategoryTheory.Limits.colimit.isoColimitCocone (CategoryTheory.Limits.Types.binaryCoproductColimitCocone X Y)).hom (CategoryTheory.Limits.colimit.ι (CategoryTheory.Limits.pair X Y) { as := CategoryTheory.Limits.WalkingPair.left } x) = ↑(CategoryTheory.Limits.BinaryCofan.inl (CategoryTheory.Limits.Types.binaryCoproductColimitCocone X Y).cocone) x

@[simp]

theorem CategoryTheory.Limits.Types.binaryCoproductIso_inl_comp_hom (X : Type u) (Y : Type u) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl (CategoryTheory.Limits.Types.binaryCoproductIso X Y).hom = Sum.inl

@[simp]

theorem CategoryTheory.Limits.Types.binaryCoproductIso_inr_comp_hom_apply (X : Type u) (Y : Type u) (x : (CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.right }) : (CategoryTheory.Limits.colimit.isoColimitCocone (CategoryTheory.Limits.Types.binaryCoproductColimitCocone X Y)).hom (CategoryTheory.Limits.colimit.ι (CategoryTheory.Limits.pair X Y) { as := CategoryTheory.Limits.WalkingPair.right } x) = ↑(CategoryTheory.Limits.BinaryCofan.inr (CategoryTheory.Limits.Types.binaryCoproductColimitCocone X Y).cocone) x

@[simp]

theorem CategoryTheory.Limits.Types.binaryCoproductIso_inr_comp_hom (X : Type u) (Y : Type u) : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr (CategoryTheory.Limits.Types.binaryCoproductIso X Y).hom = Sum.inr

@[simp]

theorem CategoryTheory.Limits.Types.binaryCoproductIso_inl_comp_inv_apply (X : Type u) (Y : Type u) (x : (CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.left }) : ↑(CategoryTheory.Limits.colimit.isoColimitCocone (CategoryTheory.Limits.Types.binaryCoproductColimitCocone X Y)).inv (CategoryTheory.Limits.BinaryCofan.inl (CategoryTheory.Limits.Types.binaryCoproductColimitCocone X Y).cocone x) = CategoryTheory.Limits.colimit.ι (CategoryTheory.Limits.pair X Y) { as := CategoryTheory.Limits.WalkingPair.left } x

@[simp]

theorem CategoryTheory.Limits.Types.binaryCoproductIso_inl_comp_inv (X : Type u) (Y : Type u) : CategoryTheory.CategoryStruct.comp (CategoryTheory.asHom Sum.inl) (CategoryTheory.Limits.Types.binaryCoproductIso X Y).inv = CategoryTheory.Limits.coprod.inl

@[simp]

theorem CategoryTheory.Limits.Types.binaryCoproductIso_inr_comp_inv_apply (X : Type u) (Y : Type u) (x : (CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.right }) : ↑(CategoryTheory.Limits.colimit.isoColimitCocone (CategoryTheory.Limits.Types.binaryCoproductColimitCocone X Y)).inv (CategoryTheory.Limits.BinaryCofan.inr (CategoryTheory.Limits.Types.binaryCoproductColimitCocone X Y).cocone x) = CategoryTheory.Limits.colimit.ι (CategoryTheory.Limits.pair X Y) { as := CategoryTheory.Limits.WalkingPair.right } x

@[simp]

theorem CategoryTheory.Limits.Types.binaryCoproductIso_inr_comp_inv (X : Type u) (Y : Type u) : CategoryTheory.CategoryStruct.comp (CategoryTheory.asHom Sum.inr) (CategoryTheory.Limits.Types.binaryCoproductIso X Y).inv = CategoryTheory.Limits.coprod.inr

theorem CategoryTheory.Limits.Types.binaryCofan_isColimit_iff {X : Type u} {Y : Type u} (c : CategoryTheory.Limits.BinaryCofan X Y) : Nonempty (CategoryTheory.Limits.IsColimit c) ↔ Function.Injective (CategoryTheory.Limits.BinaryCofan.inl c) ∧ Function.Injective (CategoryTheory.Limits.BinaryCofan.inr c) ∧ IsCompl (Set.range (CategoryTheory.Limits.BinaryCofan.inl c)) (Set.range (CategoryTheory.Limits.BinaryCofan.inr c))

noncomputable def CategoryTheory.Limits.Types.isCoprodOfMono {X : Type u} {Y : Type u} (f : X ⟶ Y) [CategoryTheory.Mono f] : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk f Subtype.val)

Any monomorphism in Type is a coproduct injection.

def CategoryTheory.Limits.Types.productLimitCone {J : Type v} (F : J → TypeMax) : CategoryTheory.Limits.LimitCone (CategoryTheory.Discrete.functor F)

The category of types has Π j, f j as the product of a type family f : J → TypeMax.{v, u}.

noncomputable def CategoryTheory.Limits.Types.productIso {J : Type v} (F : J → TypeMax) : ∏ F ≅ (j : J) → F j

The categorical product in TypeMax.{v, u} is the type theoretic product Π j, F j.

@[simp]

theorem CategoryTheory.Limits.Types.productIso_hom_comp_eval {J : Type v} (F : J → TypeMax) (j : J) : (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Types.productIso F).hom fun f => f j) = CategoryTheory.Limits.Pi.π F j

@[simp]

theorem CategoryTheory.Limits.Types.productIso_hom_comp_eval_apply {J : Type v} (F : J → TypeMax) (j : J) (x : ∏ F) : TypeMax.hom CategoryTheory.types (∏ F) ((j : J) → F j) (CategoryTheory.Limits.Types.productIso F) x j = CategoryTheory.Limits.Pi.π J TypeMax CategoryTheory.types F (_ : CategoryTheory.Limits.HasLimit (CategoryTheory.Discrete.functor F)) j x

@[simp]

theorem CategoryTheory.Limits.Types.productIso_inv_comp_π_apply {J : Type v} (F : J → TypeMax) (j : J) (x : (CategoryTheory.Limits.Types.productLimitCone F).cone.pt) : CategoryTheory.Limits.limit.π (CategoryTheory.Discrete J) (CategoryTheory.discreteCategory J) TypeMax CategoryTheory.types (CategoryTheory.Discrete.functor F) (_ : CategoryTheory.Limits.HasLimit (CategoryTheory.Discrete.functor F)) { as := j } ((CategoryTheory.Limits.limit.isoLimitCone (CategoryTheory.Limits.Types.productLimitCone F)).inv x) = ↑((CategoryTheory.Limits.Types.productLimitCone F).cone.π.app { as := j }) x

@[simp]

theorem CategoryTheory.Limits.Types.productIso_inv_comp_π {J : Type v} (F : J → TypeMax) (j : J) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Types.productIso F).inv (CategoryTheory.Limits.Pi.π F j) = fun f => f j

noncomputable def CategoryTheory.Limits.Types.UnivLE.productLimitCone {J : Type v} (F : J → Type u) [UnivLE.{v, u} ] : CategoryTheory.Limits.LimitCone (CategoryTheory.Discrete.functor F)

A variant of productLimitCone using a UnivLE hypothesis rather than a function to TypeMax.

noncomputable def CategoryTheory.Limits.Types.UnivLE.productIso {J : Type v} (F : J → Type u) [UnivLE.{v, u} ] : ∏ F ≅ Shrink ((j : J) → F j)

The categorical product in Type u indexed in Type v is the type theoretic product Π j, F j, after shrinking back to Type u.

@[simp]

theorem CategoryTheory.Limits.Types.UnivLE.productIso_hom_comp_eval {J : Type v} (F : J → Type u) [UnivLE.{v, u} ] (j : J) : (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Types.UnivLE.productIso F).hom fun f => ↑(equivShrink ((j : J) → F j)).symm f j) = CategoryTheory.Limits.Pi.π F j

@[simp]

theorem CategoryTheory.Limits.Types.UnivLE.productIso_hom_comp_eval_apply {J : Type v} (F : J → Type u) [UnivLE.{v, u} ] (j : J) (x : ∏ F) : ↑(equivShrink ((j : J) → F j)).symm ((CategoryTheory.Limits.Types.UnivLE.productIso F).hom x) j = CategoryTheory.Limits.Pi.π J (Type u) CategoryTheory.types F (_ : CategoryTheory.Limits.HasLimit (CategoryTheory.Discrete.functor F)) j x

@[simp]

theorem CategoryTheory.Limits.Types.UnivLE.productIso_inv_comp_π_apply {J : Type v} (F : J → Type u) [UnivLE.{v, u} ] (j : J) (x : (CategoryTheory.Limits.Types.UnivLE.productLimitCone F).cone.pt) : CategoryTheory.Limits.limit.π (CategoryTheory.Discrete J) (CategoryTheory.discreteCategory J) (Type u) CategoryTheory.types (CategoryTheory.Discrete.functor F) (_ : CategoryTheory.Limits.HasLimit (CategoryTheory.Discrete.functor F)) { as := j } ((CategoryTheory.Limits.limit.isoLimitCone (CategoryTheory.Limits.Types.UnivLE.productLimitCone F)).inv x) = ↑((CategoryTheory.Limits.Types.UnivLE.productLimitCone F).cone.π.app { as := j }) x

@[simp]

theorem CategoryTheory.Limits.Types.UnivLE.productIso_inv_comp_π {J : Type v} (F : J → Type u) [UnivLE.{v, u} ] (j : J) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Types.UnivLE.productIso F).inv (CategoryTheory.Limits.Pi.π F j) = fun f => ↑(equivShrink ((j : J) → F j)).symm f j

def CategoryTheory.Limits.Types.coproductColimitCocone {J : Type u} (F : J → Type u) : CategoryTheory.Limits.ColimitCocone (CategoryTheory.Discrete.functor F)

The category of types has Σ j, f j as the coproduct of a type family f : J → Type.

noncomputable def CategoryTheory.Limits.Types.coproductIso {J : Type u} (F : J → Type u) : ∐ F ≅ (j : J) × F j

The categorical coproduct in Type u is the type theoretic coproduct Σ j, F j.

@[simp]

theorem CategoryTheory.Limits.Types.coproductIso_ι_comp_hom_apply {J : Type u} (F : J → Type u) (j : J) (x : (CategoryTheory.Discrete.functor F).obj { as := j }) : (CategoryTheory.Limits.colimit.isoColimitCocone (CategoryTheory.Limits.Types.coproductColimitCocone F)).hom (CategoryTheory.Limits.colimit.ι (CategoryTheory.Discrete.functor F) { as := j } x) = ↑((CategoryTheory.Limits.Types.coproductColimitCocone F).cocone.ι.app { as := j }) x

@[simp]

theorem CategoryTheory.Limits.Types.coproductIso_ι_comp_hom {J : Type u} (F : J → Type u) (j : J) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι F j) (CategoryTheory.Limits.Types.coproductIso F).hom = fun x => { fst := j, snd := x }

theorem CategoryTheory.Limits.Types.coproductIso_mk_comp_inv {J : Type u} (F : J → Type u) (j : J) : CategoryTheory.CategoryStruct.comp (CategoryTheory.asHom fun x => { fst := j, snd := x }) (CategoryTheory.Limits.Types.coproductIso F).inv = CategoryTheory.Limits.Sigma.ι F j

noncomputable def CategoryTheory.Limits.Types.typeEqualizerOfUnique {X : Type u} {Y : Type u} {Z : Type u} (f : X ⟶ Y) {g : Y ⟶ Z} {h : Y ⟶ Z} (w : CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.comp f h) (t : ∀ (y : Y), g y = h y → ∃! x, f x = y) : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fork.ofι f w)

Show the given fork in Type u is an equalizer given that any element in the "difference kernel" comes from X. The converse of unique_of_type_equalizer.

theorem CategoryTheory.Limits.Types.unique_of_type_equalizer {X : Type u} {Y : Type u} {Z : Type u} (f : X ⟶ Y) {g : Y ⟶ Z} {h : Y ⟶ Z} (w : CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.comp f h) (t : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fork.ofι f w)) (y : Y) (hy : g y = h y) : ∃! x, f x = y

The converse of type_equalizer_of_unique.

theorem CategoryTheory.Limits.Types.type_equalizer_iff_unique {X : Type u} {Y : Type u} {Z : Type u} (f : X ⟶ Y) {g : Y ⟶ Z} {h : Y ⟶ Z} (w : CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.comp f h) : Nonempty (CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fork.ofι f w)) ↔ ∀ (y : Y), g y = h y → ∃! x, f x = y

def CategoryTheory.Limits.Types.equalizerLimit {Y : Type u} {Z : Type u} {g : Y ⟶ Z} {h : Y ⟶ Z} : CategoryTheory.Limits.LimitCone (CategoryTheory.Limits.parallelPair g h)

Show that the subtype {x : Y // g x = h x} is an equalizer for the pair (g,h).

noncomputable def CategoryTheory.Limits.Types.equalizerIso {Y : Type u} {Z : Type u} (g : Y ⟶ Z) (h : Y ⟶ Z) : CategoryTheory.Limits.equalizer g h ≅ { x // g x = h x }

The categorical equalizer in Type u is {x : Y // g x = h x}.

@[simp]

theorem CategoryTheory.Limits.Types.equalizerIso_hom_comp_subtype {Y : Type u} {Z : Type u} (g : Y ⟶ Z) (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Types.equalizerIso g h).hom Subtype.val = CategoryTheory.Limits.equalizer.ι g h

@[simp]

theorem CategoryTheory.Limits.Types.equalizerIso_inv_comp_ι_apply {Y : Type u} {Z : Type u} (g : Y ⟶ Z) (h : Y ⟶ Z) (x : CategoryTheory.Limits.Types.equalizerLimit.cone.pt) : CategoryTheory.Limits.limit.π CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory (Type u) CategoryTheory.types (CategoryTheory.Limits.parallelPair g h) (_ : CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.parallelPair g h)) CategoryTheory.Limits.WalkingParallelPair.zero ((CategoryTheory.Limits.limit.isoLimitCone CategoryTheory.Limits.Types.equalizerLimit).inv x) = ↑(CategoryTheory.Limits.Fork.ι CategoryTheory.Limits.Types.equalizerLimit.cone) x

@[simp]

theorem CategoryTheory.Limits.Types.equalizerIso_inv_comp_ι {Y : Type u} {Z : Type u} (g : Y ⟶ Z) (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Types.equalizerIso g h).inv (CategoryTheory.Limits.equalizer.ι g h) = Subtype.val

inductive CategoryTheory.Limits.Types.CoequalizerRel {X : Type u} {Y : Type u} (f : X ⟶ Y) (g : X ⟶ Y) : Y → Y → Prop

• Rel: ∀ {X Y : Type u} {f g : X ⟶ Y} (x : X), CategoryTheory.Limits.Types.CoequalizerRel f g (f x) (g x)

(Implementation) The relation to be quotiented to obtain the coequalizer.

def CategoryTheory.Limits.Types.coequalizerColimit {X : Type u} {Y : Type u} (f : X ⟶ Y) (g : X ⟶ Y) : CategoryTheory.Limits.ColimitCocone (CategoryTheory.Limits.parallelPair f g)

Show that the quotient by the relation generated by f(x) ~ g(x) is a coequalizer for the pair (f, g).

theorem CategoryTheory.Limits.Types.coequalizer_preimage_image_eq_of_preimage_eq {X : Type u} {Y : Type u} {Z : Type u} (f : X ⟶ Y) (g : X ⟶ Y) (π : Y ⟶ Z) (e : CategoryTheory.CategoryStruct.comp f π = CategoryTheory.CategoryStruct.comp g π) (h : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofork.ofπ π e)) (U : Set Y) (H : f ⁻¹' U = g ⁻¹' U) : π ⁻¹' (π '' U) = U

If π : Y ⟶ Z is an equalizer for (f, g), and U ⊆ Y such that f ⁻¹' U = g ⁻¹' U, then π ⁻¹' (π '' U) = U.

noncomputable def CategoryTheory.Limits.Types.coequalizerIso {X : Type u} {Y : Type u} (f : X ⟶ Y) (g : X ⟶ Y) : CategoryTheory.Limits.coequalizer f g ≅ Quot (CategoryTheory.Limits.Types.CoequalizerRel f g)

The categorical coequalizer in Type u is the quotient by f g ~ g x.

@[simp]

theorem CategoryTheory.Limits.Types.coequalizerIso_π_comp_hom_apply {X : Type u} {Y : Type u} (f : X ⟶ Y) (g : X ⟶ Y) (x : (CategoryTheory.Limits.parallelPair f g).obj CategoryTheory.Limits.WalkingParallelPair.one) : (CategoryTheory.Limits.colimit.isoColimitCocone (CategoryTheory.Limits.Types.coequalizerColimit f g)).hom (CategoryTheory.Limits.colimit.ι (CategoryTheory.Limits.parallelPair f g) CategoryTheory.Limits.WalkingParallelPair.one x) = ↑(CategoryTheory.Limits.Cofork.π (CategoryTheory.Limits.Types.coequalizerColimit f g).cocone) x

@[simp]

theorem CategoryTheory.Limits.Types.coequalizerIso_π_comp_hom {X : Type u} {Y : Type u} (f : X ⟶ Y) (g : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coequalizer.π f g) (CategoryTheory.Limits.Types.coequalizerIso f g).hom = Quot.mk (CategoryTheory.Limits.Types.CoequalizerRel f g)

@[simp]

theorem CategoryTheory.Limits.Types.coequalizerIso_quot_comp_inv {X : Type u} {Y : Type u} (f : X ⟶ Y) (g : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (CategoryTheory.asHom (Quot.mk (CategoryTheory.Limits.Types.CoequalizerRel f g))) (CategoryTheory.Limits.Types.coequalizerIso f g).inv = CategoryTheory.Limits.coequalizer.π f g

instance CategoryTheory.Limits.Types.instHasPullbacksTypeTypes : CategoryTheory.Limits.HasPullbacks (Type u)

@[inline, reducible]

abbrev CategoryTheory.Limits.Types.PullbackObj {X : Type u} {Y : Type u} {Z : Type u} (f : X ⟶ Z) (g : Y ⟶ Z) : Type u

The usual explicit pullback in the category of types, as a subtype of the product. The full LimitCone data is bundled as pullbackLimitCone f g.

@[inline, reducible]

abbrev CategoryTheory.Limits.Types.pullbackCone {X : Type u} {Y : Type u} {Z : Type u} (f : X ⟶ Z) (g : Y ⟶ Z) : CategoryTheory.Limits.PullbackCone f g

The explicit pullback cone on PullbackObj f g. This is bundled with the IsLimit data as pullbackLimitCone f g.

@[simp]

theorem CategoryTheory.Limits.Types.pullbackLimitCone_isLimit {X : Type u} {Y : Type u} {Z : Type u} (f : X ⟶ Z) (g : Y ⟶ Z) : (CategoryTheory.Limits.Types.pullbackLimitCone f g).isLimit = CategoryTheory.Limits.PullbackCone.isLimitAux (CategoryTheory.Limits.Types.pullbackCone f g) (fun s x => { val := (CategoryTheory.Limits.PullbackCone.fst (Type u) CategoryTheory.types X Y Z f g s x, CategoryTheory.Limits.PullbackCone.snd (Type u) CategoryTheory.types X Y Z f g s x), property := (_ : CategoryTheory.CategoryStruct.comp (Type u) CategoryTheory.Category.toCategoryStruct s.pt X Z (CategoryTheory.Limits.PullbackCone.fst s) f x = CategoryTheory.CategoryStruct.comp (Type u) CategoryTheory.Category.toCategoryStruct s.pt Y Z (CategoryTheory.Limits.PullbackCone.snd s) g x) }) (_ : ∀ (s : CategoryTheory.Limits.PullbackCone f g), CategoryTheory.CategoryStruct.comp ((fun s x => { val := (CategoryTheory.Limits.PullbackCone.fst (Type u) CategoryTheory.types X Y Z f g s x, CategoryTheory.Limits.PullbackCone.snd (Type u) CategoryTheory.types X Y Z f g s x), property := (_ : CategoryTheory.CategoryStruct.comp (Type u) CategoryTheory.Category.toCategoryStruct s.pt X Z (CategoryTheory.Limits.PullbackCone.fst s) f x = CategoryTheory.CategoryStruct.comp (Type u) CategoryTheory.Category.toCategoryStruct s.pt Y Z (CategoryTheory.Limits.PullbackCone.snd s) g x) }) s) (CategoryTheory.Limits.PullbackCone.fst (CategoryTheory.Limits.Types.pullbackCone f g)) = CategoryTheory.Limits.PullbackCone.fst s) (_ : ∀ (s : CategoryTheory.Limits.PullbackCone f g), CategoryTheory.CategoryStruct.comp ((fun s x => { val := (CategoryTheory.Limits.PullbackCone.fst (Type u) CategoryTheory.types X Y Z f g s x, CategoryTheory.Limits.PullbackCone.snd (Type u) CategoryTheory.types X Y Z f g s x), property := (_ : CategoryTheory.CategoryStruct.comp (Type u) CategoryTheory.Category.toCategoryStruct s.pt X Z (CategoryTheory.Limits.PullbackCone.fst s) f x = CategoryTheory.CategoryStruct.comp (Type u) CategoryTheory.Category.toCategoryStruct s.pt Y Z (CategoryTheory.Limits.PullbackCone.snd s) g x) }) s) (CategoryTheory.Limits.PullbackCone.snd (CategoryTheory.Limits.Types.pullbackCone f g)) = CategoryTheory.Limits.PullbackCone.snd s) (_ : ∀ (s : CategoryTheory.Limits.PullbackCone f g) (m : s.pt ⟶ (CategoryTheory.Limits.Types.pullbackCone f g).pt), (∀ (j : CategoryTheory.Limits.WalkingCospan), CategoryTheory.CategoryStruct.comp m ((CategoryTheory.Limits.Types.pullbackCone f g).π.app j) = s.π.app j) → m = (fun s x => { val := (CategoryTheory.Limits.PullbackCone.fst (Type u) CategoryTheory.types X Y Z f g s x, CategoryTheory.Limits.PullbackCone.snd (Type u) CategoryTheory.types X Y Z f g s x), property := (_ : CategoryTheory.CategoryStruct.comp (Type u) CategoryTheory.Category.toCategoryStruct s.pt X Z (CategoryTheory.Limits.PullbackCone.fst s) f x = CategoryTheory.CategoryStruct.comp (Type u) CategoryTheory.Category.toCategoryStruct s.pt Y Z (CategoryTheory.Limits.PullbackCone.snd s) g x) }) s)

@[simp]

theorem CategoryTheory.Limits.Types.pullbackLimitCone_cone {X : Type u} {Y : Type u} {Z : Type u} (f : X ⟶ Z) (g : Y ⟶ Z) : (CategoryTheory.Limits.Types.pullbackLimitCone f g).cone = CategoryTheory.Limits.Types.pullbackCone f g

def CategoryTheory.Limits.Types.pullbackLimitCone {X : Type u} {Y : Type u} {Z : Type u} (f : X ⟶ Z) (g : Y ⟶ Z) : CategoryTheory.Limits.LimitCone (CategoryTheory.Limits.cospan f g)

The explicit pullback in the category of types, bundled up as a LimitCone for given f and g.

noncomputable def CategoryTheory.Limits.Types.pullbackConeIsoPullback {X : Type u} {Y : Type u} {Z : Type u} (f : X ⟶ Z) (g : Y ⟶ Z) : CategoryTheory.Limits.limit.cone (CategoryTheory.Limits.cospan f g) ≅ CategoryTheory.Limits.Types.pullbackCone f g

The pullback cone given by the instance HasPullbacks (Type u) is isomorphic to the explicit pullback cone given by pullbackLimitCone.

noncomputable def CategoryTheory.Limits.Types.pullbackIsoPullback {X : Type u} {Y : Type u} {Z : Type u} (f : X ⟶ Z) (g : Y ⟶ Z) : CategoryTheory.Limits.pullback f g ≅ CategoryTheory.Limits.Types.PullbackObj f g

The pullback given by the instance HasPullbacks (Type u) is isomorphic to the explicit pullback object given by PullbackObj.

@[simp]

theorem CategoryTheory.Limits.Types.pullbackIsoPullback_hom_fst {X : Type u} {Y : Type u} {Z : Type u} (f : X ⟶ Z) (g : Y ⟶ Z) (p : CategoryTheory.Limits.pullback f g) : (↑((CategoryTheory.Limits.Types.pullbackIsoPullback f g).hom p)).fst = CategoryTheory.Limits.pullback.fst (Type u) CategoryTheory.types X Y Z f g (_ : CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.cospan f g)) p

@[simp]

theorem CategoryTheory.Limits.Types.pullbackIsoPullback_hom_snd {X : Type u} {Y : Type u} {Z : Type u} (f : X ⟶ Z) (g : Y ⟶ Z) (p : CategoryTheory.Limits.pullback f g) : (↑((CategoryTheory.Limits.Types.pullbackIsoPullback f g).hom p)).snd = CategoryTheory.Limits.pullback.snd (Type u) CategoryTheory.types X Y Z f g (_ : CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.cospan f g)) p

@[simp]

theorem CategoryTheory.Limits.Types.pullbackIsoPullback_inv_fst {X : Type u} {Y : Type u} {Z : Type u} (f : X ⟶ Z) (g : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Types.pullbackIsoPullback f g).inv CategoryTheory.Limits.pullback.fst = fun p => (↑p).fst

@[simp]

theorem CategoryTheory.Limits.Types.pullbackIsoPullback_inv_snd {X : Type u} {Y : Type u} {Z : Type u} (f : X ⟶ Z) (g : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Types.pullbackIsoPullback f g).inv CategoryTheory.Limits.pullback.snd = fun p => (↑p).snd

instance CategoryTheory.Limits.Types.instHasPushoutsTypeTypes : CategoryTheory.Limits.HasPushouts (Type u)