ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u'<VAR>CategoryTheory.Category.{v, u'} D<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.Limits.HasFiniteProducts D<VAR>F : CategoryTheory.Functor C D<VAR>L : CategoryTheory.Functor D C<VAR>CategoryTheory.CartesianClosed C<VAR>CategoryTheory.CartesianClosed D<VAR>CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F<VAR>h : L ⊣ F<VAR>F.Full<VAR>F.Faithful<VAR>CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) L<GOAL>CategoryTheory.CartesianClosedFunctor F
<VAR>D : Type u_1<VAR>C : Type u_2<VAR>CategoryTheory.Groupoid D<VAR>CategoryTheory.Category.{u_4, u_2} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.MonoidalClosed C<VAR>F Y : D ⥤ C<VAR>X : D<GOAL>(F.closedIhom.obj Y).obj X = (CategoryTheory.ihom (F.obj X)).obj (Y.obj X)
<VAR>D : Type u_1<VAR>C : Type u_2<VAR>CategoryTheory.Groupoid D<VAR>CategoryTheory.Category.{u_4, u_2} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.MonoidalClosed C<VAR>F Y : D ⥤ C<GOAL>∀ {X Y_1 : D} (f : X ⟶ Y_1), (F.closedIhom.obj Y).map f = (CategoryTheory.MonoidalClosed.pre (CategoryTheory.inv (F.map f))).app (Y.obj X) ≫ (CategoryTheory.ihom (F.obj Y_1)).map (Y.map f)
<VAR>D : Type u_1<VAR>C : Type u_2<VAR>CategoryTheory.Groupoid D<VAR>CategoryTheory.Category.{u_4, u_2} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.MonoidalClosed C<VAR>F : D ⥤ C<GOAL>∀ {X Y : D ⥤ C} (g : X ⟶ Y) (X_1 : D), (F.closedIhom.map g).app X_1 = (CategoryTheory.ihom (F.obj X_1)).map (g.app X_1)
<VAR>D : Type u_1<VAR>C : Type u_2<VAR>CategoryTheory.Groupoid D<VAR>CategoryTheory.Category.{u_4, u_2} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.MonoidalClosed C<VAR>F G : D ⥤ C<VAR>X : D<GOAL>(F.closedUnit.app G).app X = (CategoryTheory.ihom.coev (F.obj X)).app (G.obj X)
<VAR>D : Type u_1<VAR>C : Type u_2<VAR>CategoryTheory.Groupoid D<VAR>CategoryTheory.Category.{u_4, u_2} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.MonoidalClosed C<VAR>F G : D ⥤ C<VAR>X : D<GOAL>(F.closedCounit.app G).app X = (CategoryTheory.ihom.ev (F.obj X)).app (G.obj X)
<VAR>D : Type u_1<VAR>C : Type u_2<VAR>CategoryTheory.Groupoid D<VAR>CategoryTheory.Category.{u_4, u_2} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.MonoidalClosed C<VAR>X : D ⥤ C<GOAL>CategoryTheory.Closed.adj = CategoryTheory.Adjunction.mkOfUnitCounit { unit := X.closedUnit, counit := X.closedCounit, left_triangle := ⋯, right_triangle := ⋯ }
<VAR>D : Type u_1<VAR>C : Type u_2<VAR>CategoryTheory.Groupoid D<VAR>CategoryTheory.Category.{u_4, u_2} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.MonoidalClosed C<VAR>F : D ⥤ C<VAR>G H : D ⥤ C<VAR>f : G ⟶ H<GOAL>(CategoryTheory.ihom F).map f = F.closedIhom.map f
<VAR>D : Type u_1<VAR>C : Type u_2<VAR>CategoryTheory.Groupoid D<VAR>CategoryTheory.Category.{u_4, u_2} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.MonoidalClosed C<VAR>F G : D ⥤ C<GOAL>(CategoryTheory.ihom.ev F).app G = F.closedCounit.app G
<VAR>D : Type u_1<VAR>C : Type u_2<VAR>CategoryTheory.Groupoid D<VAR>CategoryTheory.Category.{u_4, u_2} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.MonoidalClosed C<VAR>F G : D ⥤ C<GOAL>(CategoryTheory.ihom.coev F).app G = F.closedUnit.app G
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} D<VAR>e : C ≌ D<VAR>CategoryTheory.Precoherent C<GOAL>CategoryTheory.Precoherent D
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>e : C ≌ D<VAR>CategoryTheory.Precoherent C<VAR>A : Type u_3<VAR>CategoryTheory.Category.{u_6, u_3} A<VAR>X : CategoryTheory.Sheaf (CategoryTheory.coherentTopology D) A<GOAL>∀ (X_1 : Dᵒᵖ), ((e.sheafCongrPrecoherent A).counitIso.inv.app X).val.app X_1 = X.val.map (e.counitIso.hom.app (Opposite.unop X_1)).op
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>e : C ≌ D<VAR>CategoryTheory.Precoherent C<VAR>A : Type u_3<VAR>CategoryTheory.Category.{u_6, u_3} A<VAR>F : CategoryTheory.Sheaf (CategoryTheory.coherentTopology D) A<GOAL>∀ {X Y : Cᵒᵖ} (f : X ⟶ Y), ((e.sheafCongrPrecoherent A).inverse.obj F).val.map f = F.val.map (e.functor.map f.unop).op
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>e : C ≌ D<VAR>CategoryTheory.Precoherent C<VAR>A : Type u_3<VAR>CategoryTheory.Category.{u_6, u_3} A<VAR>F : CategoryTheory.Sheaf (CategoryTheory.coherentTopology D) A<VAR>X : Cᵒᵖ<GOAL>((e.sheafCongrPrecoherent A).inverse.obj F).val.obj X = F.val.obj (Opposite.op (e.functor.obj (Opposite.unop X)))
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>e : C ≌ D<VAR>CategoryTheory.Precoherent C<VAR>A : Type u_3<VAR>CategoryTheory.Category.{u_6, u_3} A<VAR>X : CategoryTheory.Sheaf (CategoryTheory.coherentTopology C) A<GOAL>∀ (X_1 : Cᵒᵖ), ((e.sheafCongrPrecoherent A).unitIso.inv.app X).val.app X_1 = X.val.map (e.unitIso.hom.app (Opposite.unop X_1)).op
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>e : C ≌ D<VAR>CategoryTheory.Precoherent C<VAR>A : Type u_3<VAR>CategoryTheory.Category.{u_6, u_3} A<GOAL>∀ {X Y : CategoryTheory.Sheaf (CategoryTheory.coherentTopology C) A} (f : X ⟶ Y) (X_1 : Dᵒᵖ), ((e.sheafCongrPrecoherent A).functor.map f).val.app X_1 = f.val.app (Opposite.op (e.inverse.obj (Opposite.unop X_1)))
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>e : C ≌ D<VAR>CategoryTheory.Precoherent C<VAR>A : Type u_3<VAR>CategoryTheory.Category.{u_6, u_3} A<VAR>X : CategoryTheory.Sheaf (CategoryTheory.coherentTopology D) A<GOAL>∀ (X_1 : Dᵒᵖ), ((e.sheafCongrPrecoherent A).counitIso.hom.app X).val.app X_1 = X.val.map (e.counitIso.inv.app (Opposite.unop X_1)).op
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>e : C ≌ D<VAR>CategoryTheory.Precoherent C<VAR>A : Type u_3<VAR>CategoryTheory.Category.{u_6, u_3} A<VAR>X : CategoryTheory.Sheaf (CategoryTheory.coherentTopology C) A<GOAL>∀ (X_1 : Cᵒᵖ), ((e.sheafCongrPrecoherent A).unitIso.hom.app X).val.app X_1 = X.val.map (e.unitIso.inv.app (Opposite.unop X_1)).op
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>e : C ≌ D<VAR>CategoryTheory.Precoherent C<VAR>A : Type u_3<VAR>CategoryTheory.Category.{u_6, u_3} A<VAR>F : CategoryTheory.Sheaf (CategoryTheory.coherentTopology C) A<GOAL>∀ {X Y : Dᵒᵖ} (f : X ⟶ Y), ((e.sheafCongrPrecoherent A).functor.obj F).val.map f = F.val.map (e.inverse.map f.unop).op
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>e : C ≌ D<VAR>CategoryTheory.Precoherent C<VAR>A : Type u_3<VAR>CategoryTheory.Category.{u_6, u_3} A<VAR>F : CategoryTheory.Sheaf (CategoryTheory.coherentTopology C) A<VAR>X : Dᵒᵖ<GOAL>((e.sheafCongrPrecoherent A).functor.obj F).val.obj X = F.val.obj (Opposite.op (e.inverse.obj (Opposite.unop X)))
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>e : C ≌ D<VAR>CategoryTheory.Precoherent C<VAR>A : Type u_3<VAR>CategoryTheory.Category.{u_6, u_3} A<GOAL>∀ {X Y : CategoryTheory.Sheaf (CategoryTheory.coherentTopology D) A} (f : X ⟶ Y) (X_1 : Cᵒᵖ), ((e.sheafCongrPrecoherent A).inverse.map f).val.app X_1 = f.val.app (Opposite.op (e.functor.obj (Opposite.unop X_1)))
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_6, u_2} D<VAR>e : C ≌ D<VAR>CategoryTheory.Precoherent C<VAR>A : Type u_3<VAR>CategoryTheory.Category.{u_5, u_3} A<VAR>F : CategoryTheory.Functor Cᵒᵖ A<GOAL>CategoryTheory.Presheaf.IsSheaf (CategoryTheory.coherentTopology C) F ↔ CategoryTheory.Presheaf.IsSheaf (CategoryTheory.coherentTopology D) (e.inverse.op.comp F)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>CategoryTheory.Precoherent C<VAR>A : Type u_3<VAR>CategoryTheory.Category.{u_6, u_3} A<VAR>CategoryTheory.EssentiallySmall.{u_4, u_5, u_1} C<VAR>F : CategoryTheory.Functor Cᵒᵖ A<GOAL>CategoryTheory.Presheaf.IsSheaf (CategoryTheory.coherentTopology C) F ↔ CategoryTheory.Presheaf.IsSheaf (CategoryTheory.coherentTopology (CategoryTheory.SmallModel.{u_4, u_5, u_1} C)) ((CategoryTheory.equivSmallModel C).inverse.op.comp F)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} D<VAR>e : C ≌ D<VAR>CategoryTheory.Preregular C<GOAL>CategoryTheory.Preregular D
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>e : C ≌ D<VAR>CategoryTheory.Preregular C<VAR>A : Type u_3<VAR>CategoryTheory.Category.{u_6, u_3} A<VAR>F : CategoryTheory.Sheaf (CategoryTheory.regularTopology C) A<VAR>X : Dᵒᵖ<GOAL>((e.sheafCongrPreregular A).functor.obj F).val.obj X = F.val.obj (Opposite.op (e.inverse.obj (Opposite.unop X)))
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>e : C ≌ D<VAR>CategoryTheory.Preregular C<VAR>A : Type u_3<VAR>CategoryTheory.Category.{u_6, u_3} A<VAR>X : CategoryTheory.Sheaf (CategoryTheory.regularTopology C) A<GOAL>∀ (X_1 : Cᵒᵖ), ((e.sheafCongrPreregular A).unitIso.hom.app X).val.app X_1 = X.val.map (e.unitIso.inv.app (Opposite.unop X_1)).op
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>e : C ≌ D<VAR>CategoryTheory.Preregular C<VAR>A : Type u_3<VAR>CategoryTheory.Category.{u_6, u_3} A<VAR>F : CategoryTheory.Sheaf (CategoryTheory.regularTopology C) A<GOAL>∀ {X Y : Dᵒᵖ} (f : X ⟶ Y), ((e.sheafCongrPreregular A).functor.obj F).val.map f = F.val.map (e.inverse.map f.unop).op
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>e : C ≌ D<VAR>CategoryTheory.Preregular C<VAR>A : Type u_3<VAR>CategoryTheory.Category.{u_6, u_3} A<VAR>F : CategoryTheory.Sheaf (CategoryTheory.regularTopology D) A<GOAL>∀ {X Y : Cᵒᵖ} (f : X ⟶ Y), ((e.sheafCongrPreregular A).inverse.obj F).val.map f = F.val.map (e.functor.map f.unop).op
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>e : C ≌ D<VAR>CategoryTheory.Preregular C<VAR>A : Type u_3<VAR>CategoryTheory.Category.{u_6, u_3} A<VAR>X : CategoryTheory.Sheaf (CategoryTheory.regularTopology D) A<GOAL>∀ (X_1 : Dᵒᵖ), ((e.sheafCongrPreregular A).counitIso.inv.app X).val.app X_1 = X.val.map (e.counitIso.hom.app (Opposite.unop X_1)).op
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>e : C ≌ D<VAR>CategoryTheory.Preregular C<VAR>A : Type u_3<VAR>CategoryTheory.Category.{u_6, u_3} A<GOAL>∀ {X Y : CategoryTheory.Sheaf (CategoryTheory.regularTopology C) A} (f : X ⟶ Y) (X_1 : Dᵒᵖ), ((e.sheafCongrPreregular A).functor.map f).val.app X_1 = f.val.app (Opposite.op (e.inverse.obj (Opposite.unop X_1)))
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>e : C ≌ D<VAR>CategoryTheory.Preregular C<VAR>A : Type u_3<VAR>CategoryTheory.Category.{u_6, u_3} A<VAR>F : CategoryTheory.Sheaf (CategoryTheory.regularTopology D) A<VAR>X : Cᵒᵖ<GOAL>((e.sheafCongrPreregular A).inverse.obj F).val.obj X = F.val.obj (Opposite.op (e.functor.obj (Opposite.unop X)))
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>e : C ≌ D<VAR>CategoryTheory.Preregular C<VAR>A : Type u_3<VAR>CategoryTheory.Category.{u_6, u_3} A<GOAL>∀ {X Y : CategoryTheory.Sheaf (CategoryTheory.regularTopology D) A} (f : X ⟶ Y) (X_1 : Cᵒᵖ), ((e.sheafCongrPreregular A).inverse.map f).val.app X_1 = f.val.app (Opposite.op (e.functor.obj (Opposite.unop X_1)))
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>e : C ≌ D<VAR>CategoryTheory.Preregular C<VAR>A : Type u_3<VAR>CategoryTheory.Category.{u_6, u_3} A<VAR>X : CategoryTheory.Sheaf (CategoryTheory.regularTopology C) A<GOAL>∀ (X_1 : Cᵒᵖ), ((e.sheafCongrPreregular A).unitIso.inv.app X).val.app X_1 = X.val.map (e.unitIso.hom.app (Opposite.unop X_1)).op
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>e : C ≌ D<VAR>CategoryTheory.Preregular C<VAR>A : Type u_3<VAR>CategoryTheory.Category.{u_6, u_3} A<VAR>X : CategoryTheory.Sheaf (CategoryTheory.regularTopology D) A<GOAL>∀ (X_1 : Dᵒᵖ), ((e.sheafCongrPreregular A).counitIso.hom.app X).val.app X_1 = X.val.map (e.counitIso.inv.app (Opposite.unop X_1)).op
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_6, u_2} D<VAR>e : C ≌ D<VAR>CategoryTheory.Preregular C<VAR>A : Type u_3<VAR>CategoryTheory.Category.{u_5, u_3} A<VAR>F : CategoryTheory.Functor Cᵒᵖ A<GOAL>CategoryTheory.Presheaf.IsSheaf (CategoryTheory.regularTopology C) F ↔ CategoryTheory.Presheaf.IsSheaf (CategoryTheory.regularTopology D) (e.inverse.op.comp F)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_5, u_1} C<VAR>CategoryTheory.Preregular C<VAR>A : Type u_3<VAR>CategoryTheory.Category.{u_6, u_3} A<VAR>CategoryTheory.EssentiallySmall.{u_4, u_5, u_1} C<VAR>F : CategoryTheory.Functor Cᵒᵖ A<GOAL>CategoryTheory.Presheaf.IsSheaf (CategoryTheory.regularTopology C) F ↔ CategoryTheory.Presheaf.IsSheaf (CategoryTheory.regularTopology (CategoryTheory.SmallModel.{u_4, u_5, u_1} C)) ((CategoryTheory.equivSmallModel C).inverse.op.comp F)
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Category.{v₁, u₂} D<VAR>i : CategoryTheory.Functor D C<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.CartesianClosed C<VAR>self : CategoryTheory.ExponentialIdeal i<VAR>B : C<GOAL>B ∈ i.essImage → ∀ (A : C), (A ⟹ B) ∈ i.essImage
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Category.{v₁, u₂} D<VAR>i : CategoryTheory.Functor D C<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.CartesianClosed C<VAR>h : ∀ (B : D) (A : C), (A ⟹ i.obj B) ∈ i.essImage<GOAL>CategoryTheory.ExponentialIdeal i
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Category.{v₁, u₂} D<VAR>i : CategoryTheory.Functor D C<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.CartesianClosed C<VAR>CategoryTheory.Reflective i<VAR>h : (A : C) → i.comp ((CategoryTheory.exp A).comp ((CategoryTheory.reflector i).comp i)) ≅ i.comp (CategoryTheory.exp A)<GOAL>CategoryTheory.ExponentialIdeal i
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Category.{v₁, u₂} D<VAR>i : CategoryTheory.Functor D C<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.Reflective i<GOAL>CategoryTheory.Limits.HasFiniteProducts D
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Category.{v₁, u₂} D<VAR>i : CategoryTheory.Functor D C<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.Reflective i<VAR>CategoryTheory.CartesianClosed C<VAR>CategoryTheory.Limits.HasFiniteProducts D<VAR>CategoryTheory.ExponentialIdeal i<VAR>A B : C<GOAL>(CategoryTheory.bijection i A B ((CategoryTheory.reflector i).obj A ⨯ (CategoryTheory.reflector i).obj B)).symm (CategoryTheory.CategoryStruct.id ((CategoryTheory.reflector i).obj A ⨯ (CategoryTheory.reflector i).obj B)) = CategoryTheory.Limits.prodComparison (CategoryTheory.reflector i) A B
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Category.{v₁, u₂} D<VAR>i : CategoryTheory.Functor D C<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.Reflective i<VAR>CategoryTheory.CartesianClosed C<VAR>CategoryTheory.Limits.HasFiniteProducts D<VAR>CategoryTheory.ExponentialIdeal i<VAR>A B : C<VAR>X X' : D<VAR>f : (CategoryTheory.reflector i).obj (A ⨯ B) ⟶ X<VAR>g : X ⟶ X'<GOAL>(CategoryTheory.bijection i A B X') (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.bijection i A B X) f) g
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.Category.{v₁, u₂} D<VAR>i : CategoryTheory.Functor D C<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.Reflective i<VAR>CategoryTheory.CartesianClosed C<VAR>CategoryTheory.Limits.HasFiniteProducts D<VAR>CategoryTheory.ExponentialIdeal i<VAR>A B : C<GOAL>CategoryTheory.IsIso (CategoryTheory.Limits.prodComparison (CategoryTheory.reflector i) A B)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>self : CategoryTheory.Precoherent C<VAR>B₁ B₂ : C<VAR>f : B₂ ⟶ B₁<VAR>α : Type<VAR>Finite α<VAR>X₁ : α → C<VAR>π₁ : (a : α) → X₁ a ⟶ B₁<GOAL>CategoryTheory.EffectiveEpiFamily X₁ π₁ → ∃ β, ∃ (_ : Finite β), ∃ X₂ π₂, CategoryTheory.EffectiveEpiFamily X₂ π₂ ∧ ∃ i ι, ∀ (b : β), CategoryTheory.CategoryStruct.comp (ι b) (π₁ (i b)) = CategoryTheory.CategoryStruct.comp (π₂ b) f
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>self : CategoryTheory.Preregular C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : Z ⟶ Y<VAR>CategoryTheory.EffectiveEpi g<GOAL>∃ W h, ∃ (_ : CategoryTheory.EffectiveEpi h), ∃ i, CategoryTheory.CategoryStruct.comp i g = CategoryTheory.CategoryStruct.comp h f
<VAR>C : Type u₁<VAR>Quiver C<VAR>X Y : C<GOAL>Function.Injective Quiver.Hom.op
<VAR>C : Type u₁<VAR>Quiver C<VAR>X Y : Cᵒᵖ<GOAL>Function.Injective Quiver.Hom.unop
<VAR>C : Type u₁<VAR>Quiver C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>f.op.unop = f
<VAR>C : Type u₁<VAR>Quiver C<VAR>X Y : Cᵒᵖ<VAR>x : Opposite.unop Y ⟶ Opposite.unop X<GOAL>Quiver.Hom.unop (Opposite.op x) = x
<VAR>C : Type u₁<VAR>Quiver C<VAR>X Y : Cᵒᵖ<VAR>f : X ⟶ Y<GOAL>f.unop.op = f
<VAR>C : Type u₁<VAR>Quiver C<VAR>X Y : Cᵒᵖ<VAR>f : X ⟶ Y<GOAL>Quiver.Hom.unop (Opposite.op f) = f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>(CategoryTheory.CategoryStruct.comp f g).op = CategoryTheory.CategoryStruct.comp g.op f.op
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<GOAL>(CategoryTheory.CategoryStruct.id X).op = CategoryTheory.CategoryStruct.id (Opposite.op X)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y Z : Cᵒᵖ<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>(CategoryTheory.CategoryStruct.comp f g).unop = CategoryTheory.CategoryStruct.comp g.unop f.unop
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : Cᵒᵖ<GOAL>(CategoryTheory.CategoryStruct.id X).unop = CategoryTheory.CategoryStruct.id (Opposite.unop X)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<GOAL>(CategoryTheory.CategoryStruct.id (Opposite.op X)).unop = CategoryTheory.CategoryStruct.id X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : Cᵒᵖ<GOAL>(CategoryTheory.CategoryStruct.id (Opposite.unop X)).op = CategoryTheory.CategoryStruct.id X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : Cᵒᵖᵒᵖ<GOAL>(CategoryTheory.unopUnop C).obj X = Opposite.unop (Opposite.unop X)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<GOAL>∀ {X Y : Cᵒᵖᵒᵖ} (f : X ⟶ Y), (CategoryTheory.unopUnop C).map f = f.unop.unop
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<GOAL>∀ {X Y : C} (f : X ⟶ Y), (CategoryTheory.opOp C).map f = f.op.op
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<GOAL>(CategoryTheory.opOp C).obj X = Opposite.op (Opposite.op X)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<GOAL>(CategoryTheory.opOpEquivalence C).inverse = CategoryTheory.opOp C
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<GOAL>(CategoryTheory.opOpEquivalence C).counitIso = CategoryTheory.Iso.refl ((CategoryTheory.opOp C).comp (CategoryTheory.unopUnop C))
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<GOAL>(CategoryTheory.opOpEquivalence C).unitIso = CategoryTheory.Iso.refl (CategoryTheory.Functor.id Cᵒᵖᵒᵖ)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<GOAL>(CategoryTheory.opOpEquivalence C).functor = CategoryTheory.unopUnop C
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.IsIso f.op<GOAL>CategoryTheory.IsIso f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>CategoryTheory.IsIso f.op ↔ CategoryTheory.IsIso f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : Cᵒᵖ<VAR>f : X ⟶ Y<GOAL>CategoryTheory.IsIso f.unop ↔ CategoryTheory.IsIso f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.IsIso f<GOAL>(CategoryTheory.inv f).op = CategoryTheory.inv f.op
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : Cᵒᵖ<VAR>f : X ⟶ Y<VAR>CategoryTheory.IsIso f<GOAL>(CategoryTheory.inv f).unop = CategoryTheory.inv f.unop
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor C D<VAR>X : Cᵒᵖ<GOAL>F.op.obj X = Opposite.op (F.obj (Opposite.unop X))
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor C D<GOAL>∀ {X Y : Cᵒᵖ} (f : X ⟶ Y), F.op.map f = (F.map f.unop).op
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ<GOAL>∀ {X Y : C} (f : X ⟶ Y), F.unop.map f = (F.map f.op).unop
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ<VAR>X : C<GOAL>F.unop.obj X = Opposite.unop (F.obj (Opposite.op X))
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor C D<VAR>X : C<GOAL>F.opUnopIso.inv.app X = CategoryTheory.CategoryStruct.id (F.obj X)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor C D<VAR>X : C<GOAL>F.opUnopIso.hom.app X = CategoryTheory.CategoryStruct.id (F.obj X)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ<VAR>X : Cᵒᵖ<GOAL>F.unopOpIso.hom.app X = CategoryTheory.CategoryStruct.id (F.obj X)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ<VAR>X : Cᵒᵖ<GOAL>F.unopOpIso.inv.app X = CategoryTheory.CategoryStruct.id (F.obj X)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : (CategoryTheory.Functor C D)ᵒᵖ<GOAL>(CategoryTheory.Functor.opHom C D).obj F = (Opposite.unop F).op
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<GOAL>∀ {X Y : (CategoryTheory.Functor C D)ᵒᵖ} (α : X ⟶ Y) (X_1 : Cᵒᵖ), ((CategoryTheory.Functor.opHom C D).map α).app X_1 = (α.unop.app (Opposite.unop X_1)).op
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<GOAL>∀ {X Y : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ} (α : X ⟶ Y), (CategoryTheory.Functor.opInv C D).map α = Quiver.Hom.op { app := fun X_1 => (α.app (Opposite.op X_1)).unop, naturality := ⋯ }
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ<GOAL>(CategoryTheory.Functor.opInv C D).obj F = Opposite.op F.unop
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F : CategoryTheory.Functor C Dᵒᵖ<VAR>X : Cᵒᵖ<GOAL>F.leftOp.obj X = Opposite.unop (F.obj (Opposite.unop X))