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>F : CategoryTheory.Functor C Dᵒᵖ<GOAL>∀ {X Y : Cᵒᵖ} (f : X ⟶ Y), F.leftOp.map f = (F.map f.unop).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.rightOp.obj X = Opposite.op (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<GOAL>∀ {X Y : C} (f : X ⟶ Y), F.rightOp.map f = (F.map f.op).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<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>(F.rightOp.map f).unop = F.map f.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ᵒᵖ<VAR>X : C<GOAL>F.leftOpRightOpIso.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.leftOpRightOpIso.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.rightOpLeftOpIso.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.rightOpLeftOpIso.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<GOAL>F.rightOp.leftOp = F
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F G : CategoryTheory.Functor C D<VAR>α : F ⟶ G<VAR>X : Cᵒᵖ<GOAL>(CategoryTheory.NatTrans.op α).app X = (α.app (Opposite.unop X)).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>CategoryTheory.NatTrans.op (CategoryTheory.CategoryStruct.id F) = CategoryTheory.CategoryStruct.id F.op
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F G : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ<VAR>α : F ⟶ G<VAR>X : C<GOAL>(CategoryTheory.NatTrans.unop α).app X = (α.app (Opposite.op X)).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ᵒᵖ<GOAL>CategoryTheory.NatTrans.unop (CategoryTheory.CategoryStruct.id F) = CategoryTheory.CategoryStruct.id F.unop
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F G : CategoryTheory.Functor C D<VAR>α : F.op ⟶ G.op<VAR>X : C<GOAL>(CategoryTheory.NatTrans.removeOp α).app X = (α.app (Opposite.op X)).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<GOAL>CategoryTheory.NatTrans.removeOp (CategoryTheory.CategoryStruct.id F.op) = CategoryTheory.CategoryStruct.id F
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F G : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ<VAR>α : F.unop ⟶ G.unop<VAR>X : Cᵒᵖ<GOAL>(CategoryTheory.NatTrans.removeUnop α).app X = (α.app (Opposite.unop X)).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>CategoryTheory.NatTrans.removeUnop (CategoryTheory.CategoryStruct.id F.unop) = CategoryTheory.CategoryStruct.id F
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F G : CategoryTheory.Functor C Dᵒᵖ<VAR>α : F ⟶ G<VAR>X : Cᵒᵖ<GOAL>(CategoryTheory.NatTrans.leftOp α).app X = (α.app (Opposite.unop X)).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ᵒᵖ<GOAL>CategoryTheory.NatTrans.leftOp (CategoryTheory.CategoryStruct.id F) = CategoryTheory.CategoryStruct.id F.leftOp
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F G H : CategoryTheory.Functor C Dᵒᵖ<VAR>α : F ⟶ G<VAR>β : G ⟶ H<GOAL>CategoryTheory.NatTrans.leftOp (CategoryTheory.CategoryStruct.comp α β) = CategoryTheory.CategoryStruct.comp (CategoryTheory.NatTrans.leftOp β) (CategoryTheory.NatTrans.leftOp α)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F G : CategoryTheory.Functor C Dᵒᵖ<VAR>α : F.leftOp ⟶ G.leftOp<VAR>X : C<GOAL>(CategoryTheory.NatTrans.removeLeftOp α).app X = (α.app (Opposite.op X)).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>CategoryTheory.NatTrans.removeLeftOp (CategoryTheory.CategoryStruct.id F.leftOp) = CategoryTheory.CategoryStruct.id F
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F G : CategoryTheory.Functor Cᵒᵖ D<VAR>α : F ⟶ G<VAR>X : C<GOAL>(CategoryTheory.NatTrans.rightOp α).app X = (α.app (Opposite.op X)).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>CategoryTheory.NatTrans.rightOp (CategoryTheory.CategoryStruct.id F) = CategoryTheory.CategoryStruct.id F.rightOp
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F G H : CategoryTheory.Functor Cᵒᵖ D<VAR>α : F ⟶ G<VAR>β : G ⟶ H<GOAL>CategoryTheory.NatTrans.rightOp (CategoryTheory.CategoryStruct.comp α β) = CategoryTheory.CategoryStruct.comp (CategoryTheory.NatTrans.rightOp β) (CategoryTheory.NatTrans.rightOp α)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F G : CategoryTheory.Functor Cᵒᵖ D<VAR>α : F.rightOp ⟶ G.rightOp<VAR>X : Cᵒᵖ<GOAL>(CategoryTheory.NatTrans.removeRightOp α).app X = (α.app (Opposite.unop X)).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<GOAL>CategoryTheory.NatTrans.removeRightOp (CategoryTheory.CategoryStruct.id F.rightOp) = CategoryTheory.CategoryStruct.id F
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>α : X ≅ Y<GOAL>α.op.inv = α.inv.op
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>α : X ≅ Y<GOAL>α.op.hom = α.hom.op
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : Cᵒᵖ<VAR>f : X ≅ Y<GOAL>f.unop.hom = f.hom.unop
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : Cᵒᵖ<VAR>f : X ≅ Y<GOAL>f.unop.inv = f.inv.unop
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : Cᵒᵖ<VAR>f : X ≅ Y<GOAL>f.unop.op = f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>f : X ≅ Y<GOAL>f.op.unop = f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<VAR>F G : CategoryTheory.Functor C Dᵒᵖ<VAR>e : F ≅ G<VAR>X : C<GOAL>CategoryTheory.CategoryStruct.comp (e.hom.app X).unop (e.inv.app X).unop = CategoryTheory.CategoryStruct.id (Opposite.unop (G.obj X))
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} D<VAR>F G : CategoryTheory.Functor C Dᵒᵖ<VAR>e : F ≅ G<VAR>X : C<GOAL>CategoryTheory.CategoryStruct.comp (e.inv.app X).unop (e.hom.app X).unop = CategoryTheory.CategoryStruct.id (Opposite.unop (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 G : CategoryTheory.Functor C D<VAR>α : F ≅ G<GOAL>(CategoryTheory.NatIso.op α).inv = CategoryTheory.NatTrans.op α.inv
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F G : CategoryTheory.Functor C D<VAR>α : F ≅ G<GOAL>(CategoryTheory.NatIso.op α).hom = CategoryTheory.NatTrans.op α.hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F G : CategoryTheory.Functor C D<VAR>α : F.op ≅ G.op<GOAL>(CategoryTheory.NatIso.removeOp α).inv = CategoryTheory.NatTrans.removeOp α.inv
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F G : CategoryTheory.Functor C D<VAR>α : F.op ≅ G.op<GOAL>(CategoryTheory.NatIso.removeOp α).hom = CategoryTheory.NatTrans.removeOp α.hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F G : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ<VAR>α : F ≅ G<GOAL>(CategoryTheory.NatIso.unop α).inv = CategoryTheory.NatTrans.unop α.inv
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>F G : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ<VAR>α : F ≅ G<GOAL>(CategoryTheory.NatIso.unop α).hom = CategoryTheory.NatTrans.unop α.hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>e : C ≌ D<GOAL>e.op.unitIso = (CategoryTheory.NatIso.op e.unitIso).symm
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>e : C ≌ D<GOAL>e.op.functor = e.functor.op
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>e : C ≌ D<GOAL>e.op.inverse = e.inverse.op
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>e : C ≌ D<GOAL>e.op.counitIso = (CategoryTheory.NatIso.op e.counitIso).symm
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>e : Cᵒᵖ ≌ Dᵒᵖ<GOAL>e.unop.functor = e.functor.unop
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>e : Cᵒᵖ ≌ Dᵒᵖ<GOAL>e.unop.unitIso = (CategoryTheory.NatIso.unop e.unitIso).symm
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>e : Cᵒᵖ ≌ Dᵒᵖ<GOAL>e.unop.counitIso = (CategoryTheory.NatIso.unop e.counitIso).symm
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>e : Cᵒᵖ ≌ Dᵒᵖ<GOAL>e.unop.inverse = e.inverse.unop
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>A B : Cᵒᵖ<VAR>f : A ⟶ B<GOAL>(CategoryTheory.opEquiv A B) f = f.unop
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>A B : Cᵒᵖ<VAR>g : Opposite.unop B ⟶ Opposite.unop A<GOAL>(CategoryTheory.opEquiv A B).symm g = g.op
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>A B : Cᵒᵖ<VAR>g : Opposite.unop B ≅ Opposite.unop A<GOAL>(CategoryTheory.isoOpEquiv A B).symm g = g.op
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>A B : Cᵒᵖ<VAR>f : A ≅ B<GOAL>(CategoryTheory.isoOpEquiv A B) f = f.unop
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<GOAL>(CategoryTheory.Functor.opUnopEquiv C D).unitIso = CategoryTheory.NatIso.ofComponents (fun F => (Opposite.unop F).opUnopIso.op) ⋯
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<GOAL>(CategoryTheory.Functor.opUnopEquiv C D).inverse = CategoryTheory.Functor.opInv C D
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<GOAL>(CategoryTheory.Functor.opUnopEquiv C D).counitIso = CategoryTheory.NatIso.ofComponents (fun F => F.unopOpIso) ⋯
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<GOAL>(CategoryTheory.Functor.opUnopEquiv C D).functor = CategoryTheory.Functor.opHom C D
<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.leftOpRightOpEquiv C D).inverse.map η = (CategoryTheory.NatTrans.leftOp η).op
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>X : (CategoryTheory.Functor Cᵒᵖ D)ᵒᵖ<GOAL>(CategoryTheory.Functor.leftOpRightOpEquiv C D).unitIso.inv.app X = (Opposite.unop X).rightOpLeftOpIso.inv.op
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>X : CategoryTheory.Functor C Dᵒᵖ<GOAL>∀ (X_1 : C), ((CategoryTheory.Functor.leftOpRightOpEquiv C D).counitIso.hom.app X).app X_1 = CategoryTheory.CategoryStruct.id (X.obj X_1)
<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.leftOpRightOpEquiv C D).inverse.obj F = Opposite.op F.leftOp
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>X : CategoryTheory.Functor C Dᵒᵖ<GOAL>∀ (X_1 : C), ((CategoryTheory.Functor.leftOpRightOpEquiv C D).counitIso.inv.app X).app X_1 = CategoryTheory.CategoryStruct.id (X.obj X_1)
<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>((CategoryTheory.Functor.leftOpRightOpEquiv C D).functor.obj F).obj X = Opposite.op ((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)ᵒᵖ<GOAL>∀ {X Y : C} (f : X ⟶ Y), ((CategoryTheory.Functor.leftOpRightOpEquiv C D).functor.obj F).map f = ((Opposite.unop F).map f.op).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.leftOpRightOpEquiv C D).functor.map η).app X_1 = (η.unop.app (Opposite.op X_1)).op
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>X : (CategoryTheory.Functor Cᵒᵖ D)ᵒᵖ<GOAL>(CategoryTheory.Functor.leftOpRightOpEquiv C D).unitIso.hom.app X = (Opposite.unop X).rightOpLeftOpIso.hom.op
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Precoherent C<VAR>P : CategoryTheory.Functor Cᵒᵖ (Type w)<GOAL>CategoryTheory.Presieve.IsSheaf (CategoryTheory.coherentTopology C) P ↔ ∀ (B : C) (α : Type) [inst : Finite α] (X : α → C) (π : (a : α) → X a ⟶ B), CategoryTheory.EffectiveEpiFamily X π → CategoryTheory.Presieve.IsSheafFor P (CategoryTheory.Presieve.ofArrows X π)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Precoherent C<VAR>W : C<GOAL>CategoryTheory.Presieve.IsSheaf (CategoryTheory.coherentTopology C) (CategoryTheory.yoneda.obj W)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Precoherent C<GOAL>CategoryTheory.Sheaf.Subcanonical (CategoryTheory.coherentTopology C)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>W X Y Z : C<VAR>f : W ⟶ X<VAR>g : W ⟶ Y<VAR>h : X ⟶ Z<VAR>i : Y ⟶ Z<VAR>H : CategoryTheory.IsPushout f g h i<VAR>H' : H.IsVanKampen<GOAL>⋯.IsVanKampen
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>W X Y Z : C<VAR>f : W ⟶ X<VAR>g : W ⟶ Y<VAR>h : X ⟶ Z<VAR>i : Y ⟶ Z<VAR>H : CategoryTheory.IsPushout f g h i<GOAL>H.IsVanKampen ↔ CategoryTheory.IsVanKampenColimit (CategoryTheory.Limits.PushoutCocone.mk h i ⋯)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X E Y YE : C<VAR>c : CategoryTheory.Limits.BinaryCofan X E<VAR>hc : CategoryTheory.Limits.IsColimit c<VAR>f : X ⟶ Y<VAR>iY : Y ⟶ YE<VAR>fE : c.pt ⟶ YE<VAR>H : CategoryTheory.CommSq f c.inl iY fE<GOAL>Nonempty (CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk (CategoryTheory.CategoryStruct.comp c.inr fE) iY)) ↔ CategoryTheory.IsPushout f c.inl iY fE
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>W E X Z : C<VAR>c : CategoryTheory.Limits.BinaryCofan W E<VAR>CategoryTheory.FinitaryExtensive C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>hc : CategoryTheory.Limits.IsColimit c<VAR>f : W ⟶ X<VAR>h : X ⟶ Z<VAR>i : c.pt ⟶ Z<VAR>H : CategoryTheory.IsPushout f c.inl h i<GOAL>H.IsVanKampen
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>W X Y Z : C<VAR>f : W ⟶ X<VAR>g : W ⟶ Y<VAR>h : X ⟶ Z<VAR>i : Y ⟶ Z<VAR>CategoryTheory.Mono f<VAR>H : CategoryTheory.IsPushout f g h i<VAR>H' : H.IsVanKampen<GOAL>CategoryTheory.IsPullback f g h i
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>W X Y Z : C<VAR>f : W ⟶ X<VAR>g : W ⟶ Y<VAR>h : X ⟶ Z<VAR>i : Y ⟶ Z<VAR>CategoryTheory.Mono g<VAR>H : CategoryTheory.IsPushout f g h i<VAR>H' : H.IsVanKampen<GOAL>CategoryTheory.IsPullback f g h i
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>W X Y Z : C<VAR>f : W ⟶ X<VAR>g : W ⟶ Y<VAR>h : X ⟶ Z<VAR>i : Y ⟶ Z<VAR>CategoryTheory.Mono f<VAR>H : CategoryTheory.IsPushout f g h i<VAR>H' : H.IsVanKampen<GOAL>CategoryTheory.Mono i
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>W X Y Z : C<VAR>f : W ⟶ X<VAR>g : W ⟶ Y<VAR>h : X ⟶ Z<VAR>i : Y ⟶ Z<VAR>CategoryTheory.Mono g<VAR>H : CategoryTheory.IsPushout f g h i<VAR>H' : H.IsVanKampen<GOAL>CategoryTheory.Mono h
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>self : CategoryTheory.Adhesive C<VAR>X Y S : C<VAR>f : S ⟶ X<VAR>g : S ⟶ Y<VAR>CategoryTheory.Mono f<GOAL>CategoryTheory.Limits.HasPushout f g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>self : CategoryTheory.Adhesive C<VAR>X Y S : C<VAR>f : X ⟶ S<VAR>g : Y ⟶ S<VAR>CategoryTheory.Mono f<GOAL>CategoryTheory.Limits.HasPullback f g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>self : CategoryTheory.Adhesive C<VAR>W X Y Z : C<VAR>f : W ⟶ X<VAR>g : W ⟶ Y<VAR>h : X ⟶ Z<VAR>i : Y ⟶ Z<VAR>CategoryTheory.Mono f<VAR>H : CategoryTheory.IsPushout f g h i<GOAL>H.IsVanKampen
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>W X Y Z : C<VAR>f : W ⟶ X<VAR>g : W ⟶ Y<VAR>h : X ⟶ Z<VAR>i : Y ⟶ Z<VAR>CategoryTheory.Adhesive C<VAR>CategoryTheory.Mono g<VAR>H : CategoryTheory.IsPushout f g h i<GOAL>H.IsVanKampen
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>W X Y Z : C<VAR>f : W ⟶ X<VAR>g : W ⟶ Y<VAR>h : X ⟶ Z<VAR>i : Y ⟶ Z<VAR>CategoryTheory.Adhesive C<VAR>H : CategoryTheory.IsPushout f g h i<VAR>CategoryTheory.Mono f<GOAL>CategoryTheory.IsPullback f g h i
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>W X Y Z : C<VAR>f : W ⟶ X<VAR>g : W ⟶ Y<VAR>h : X ⟶ Z<VAR>i : Y ⟶ Z<VAR>CategoryTheory.Adhesive C<VAR>H : CategoryTheory.IsPushout f g h i<VAR>CategoryTheory.Mono g<GOAL>CategoryTheory.IsPullback f g h i
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>W X Y Z : C<VAR>f : W ⟶ X<VAR>g : W ⟶ Y<VAR>h : X ⟶ Z<VAR>i : Y ⟶ Z<VAR>CategoryTheory.Adhesive C<VAR>H : CategoryTheory.IsPushout f g h i<VAR>CategoryTheory.Mono f<GOAL>CategoryTheory.Mono i
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>W X Y Z : C<VAR>f : W ⟶ X<VAR>g : W ⟶ Y<VAR>h : X ⟶ Z<VAR>i : Y ⟶ Z<VAR>CategoryTheory.Adhesive C<VAR>H : CategoryTheory.IsPushout f g h i<VAR>CategoryTheory.Mono g<GOAL>CategoryTheory.Mono h
<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>CategoryTheory.Adhesive D<VAR>H₁ : ∀ {X Y S : C} (f : X ⟶ S) (g : Y ⟶ S) [inst : CategoryTheory.Mono f], CategoryTheory.Limits.HasPullback f g<VAR>H₂ : ∀ {X Y S : C} (f : S ⟶ X) (g : S ⟶ Y) [inst : CategoryTheory.Mono f], CategoryTheory.Limits.HasPushout f g<VAR>CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingCospan F<VAR>CategoryTheory.Limits.ReflectsLimitsOfShape CategoryTheory.Limits.WalkingCospan F<VAR>CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingSpan F<VAR>CategoryTheory.Limits.ReflectsColimitsOfShape CategoryTheory.Limits.WalkingSpan F<GOAL>CategoryTheory.Adhesive C
<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>CategoryTheory.Adhesive D<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>CategoryTheory.Limits.HasPushouts C<VAR>CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingCospan F<VAR>CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingSpan F<VAR>F.ReflectsIsomorphisms<GOAL>CategoryTheory.Adhesive C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u''<VAR>CategoryTheory.Category.{v'', u''} D<VAR>CategoryTheory.Limits.HasPullbacks D<VAR>CategoryTheory.Adhesive C<VAR>CategoryTheory.Limits.HasPullbacks C<VAR>CategoryTheory.Limits.HasPushouts C<VAR>H₂ : ∀ {X Y S : D} (f : S ⟶ X) (g : S ⟶ Y) [inst : CategoryTheory.Mono f], CategoryTheory.Limits.HasPushout f g<VAR>Gl : CategoryTheory.Functor C D<VAR>Gr : CategoryTheory.Functor D C<VAR>adj : Gl ⊣ Gr<VAR>Gr.Full<VAR>Gr.Faithful<VAR>CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingCospan Gl<GOAL>CategoryTheory.Adhesive D
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>F : CategoryTheory.Functor C D<VAR>F.PreservesFiniteEffectiveEpiFamilies<VAR>F.ReflectsFiniteEffectiveEpiFamilies<VAR>F.EffectivelyEnough<VAR>CategoryTheory.Precoherent D<VAR>F.Full<VAR>F.Faithful<GOAL>CategoryTheory.Precoherent C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J₁ : CategoryTheory.GrothendieckTopology C<VAR>X : C<VAR>S : CategoryTheory.Sieve X<GOAL>∀ (x : C) (f : x ⟶ X), (J₁.close S).arrows f = J₁.Covers S f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J₁ : CategoryTheory.GrothendieckTopology C<VAR>X : C<VAR>S : CategoryTheory.Sieve X<GOAL>S ≤ J₁.close S
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J₁ : CategoryTheory.GrothendieckTopology C<VAR>X : C<VAR>S : CategoryTheory.Sieve X<VAR>h : J₁.IsClosed S<VAR>Y : C<VAR>f : Y ⟶ X<GOAL>J₁.Covers S f ↔ S.arrows f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J₁ : CategoryTheory.GrothendieckTopology C<VAR>X Y : C<VAR>f : Y ⟶ X<VAR>S : CategoryTheory.Sieve X<GOAL>J₁.IsClosed S → J₁.IsClosed (CategoryTheory.Sieve.pullback f S)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J₁ : CategoryTheory.GrothendieckTopology C<VAR>X : C<VAR>S T : CategoryTheory.Sieve X<VAR>h : S ≤ T<VAR>hT : J₁.IsClosed T<GOAL>J₁.close S ≤ T
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J₁ : CategoryTheory.GrothendieckTopology C<VAR>X : C<VAR>S : CategoryTheory.Sieve X<GOAL>J₁.IsClosed (J₁.close S)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J₁ : CategoryTheory.GrothendieckTopology C<VAR>X : C<VAR>S : CategoryTheory.Sieve X<GOAL>(J₁.closureOperator X).IsClosed S = J₁.IsClosed S
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J₁ : CategoryTheory.GrothendieckTopology C<VAR>X : C<VAR>S : CategoryTheory.Sieve X<GOAL>J₁.IsClosed S ↔ J₁.close S = S
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J₁ : CategoryTheory.GrothendieckTopology C<VAR>X : C<VAR>S : CategoryTheory.Sieve X<VAR>hS : J₁.IsClosed S<GOAL>J₁.close S = S
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J₁ : CategoryTheory.GrothendieckTopology C<VAR>X Y : C<VAR>f : Y ⟶ X<VAR>S : CategoryTheory.Sieve X<GOAL>J₁.close (CategoryTheory.Sieve.pullback f S) = CategoryTheory.Sieve.pullback f (J₁.close S)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J₁ : CategoryTheory.GrothendieckTopology C<VAR>X : C<GOAL>Monotone J₁.close