Theorems · Theorem · category theory

CategoryTheory.JointlyFaithful.jointlyReflectsIsomorphisms

∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_4, u_1} C] {I : Type u_2} {D : I → Type u_3}
  [inst_1 : (i : I) → CategoryTheory.Category.{u_5, u_3} (D i)] {F : (i : I) → CategoryTheory.Functor C (D i)}
  [CategoryTheory.Balanced C], CategoryTheory.JointlyFaithful F → CategoryTheory.JointlyReflectIsomorphisms F

Defined in

Mathlib.CategoryTheory.Functor.ReflectsIso.Jointly

Cited by

1 results in Mathlib

Foundations

Depth 13 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Balanced