ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>A : Type u₁<VAR>B : Type u₂<VAR>C : Type u₃<VAR>D : Type u₄<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>CategoryTheory.Category.{v₄, u₄} D<VAR>F₁ : CategoryTheory.Functor A C<VAR>U₁ : CategoryTheory.Functor C A<VAR>F₂ : CategoryTheory.Functor B D<VAR>U₂ : CategoryTheory.Functor D B<VAR>L₁ : CategoryTheory.Functor A B<VAR>R₁ : CategoryTheory.Functor B A<VAR>L₂ : CategoryTheory.Functor C D<VAR>R₂ : CategoryTheory.Functor D C<VAR>adj₁ : L₁ ⊣ R₁<VAR>adj₂ : L₂ ⊣ R₂<VAR>adj₃ : F₁ ⊣ U₁<VAR>adj₄ : F₂ ⊣ U₂<VAR>α : F₁.comp L₂ ⟶ L₁.comp F₂<GOAL>(CategoryTheory.mateEquiv adj₄ adj₃) ((CategoryTheory.mateEquiv adj₁ adj₂) α) = (CategoryTheory.conjugateEquiv (adj₁.comp adj₄) (adj₃.comp adj₂)) α
<VAR>A : Type u₁<VAR>B : Type u₂<VAR>C : Type u₃<VAR>D : Type u₄<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>CategoryTheory.Category.{v₄, u₄} D<VAR>F₁ : CategoryTheory.Functor A C<VAR>U₁ : CategoryTheory.Functor C A<VAR>F₂ : CategoryTheory.Functor B D<VAR>U₂ : CategoryTheory.Functor D B<VAR>L₁ : CategoryTheory.Functor A B<VAR>R₁ : CategoryTheory.Functor B A<VAR>L₂ : CategoryTheory.Functor C D<VAR>R₂ : CategoryTheory.Functor D C<VAR>adj₁ : L₁ ⊣ R₁<VAR>adj₂ : L₂ ⊣ R₂<VAR>adj₃ : F₁ ⊣ U₁<VAR>adj₄ : F₂ ⊣ U₂<VAR>α : U₂.comp R₁ ⟶ R₂.comp U₁<GOAL>(CategoryTheory.mateEquiv adj₁ adj₂).symm ((CategoryTheory.mateEquiv adj₄ adj₃).symm α) = (CategoryTheory.conjugateEquiv (adj₁.comp adj₄) (adj₃.comp adj₂)).symm α
<VAR>A : Type u₁<VAR>B : Type u₂<VAR>C : Type u₃<VAR>D : Type u₄<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>CategoryTheory.Category.{v₄, u₄} D<VAR>G : CategoryTheory.Functor A C<VAR>H : CategoryTheory.Functor B D<VAR>L₁ : CategoryTheory.Functor A B<VAR>R₁ : CategoryTheory.Functor B A<VAR>L₂ : CategoryTheory.Functor C D<VAR>R₂ : CategoryTheory.Functor D C<VAR>L₃ : CategoryTheory.Functor C D<VAR>R₃ : CategoryTheory.Functor D C<VAR>adj₁ : L₁ ⊣ R₁<VAR>adj₂ : L₂ ⊣ R₂<VAR>adj₃ : L₃ ⊣ R₃<VAR>α : G.comp L₂ ⟶ L₁.comp H<VAR>β : L₃ ⟶ L₂<GOAL>(CategoryTheory.mateEquiv adj₁ adj₃) (CategoryTheory.leftAdjointSquareConjugate.vcomp α β) = CategoryTheory.rightAdjointSquareConjugate.vcomp ((CategoryTheory.mateEquiv adj₁ adj₂) α) ((CategoryTheory.conjugateEquiv adj₂ adj₃) β)
<VAR>A : Type u₁<VAR>B : Type u₂<VAR>C : Type u₃<VAR>D : Type u₄<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>CategoryTheory.Category.{v₄, u₄} D<VAR>G : CategoryTheory.Functor A C<VAR>H : CategoryTheory.Functor B D<VAR>L₁ : CategoryTheory.Functor A B<VAR>R₁ : CategoryTheory.Functor B A<VAR>L₂ : CategoryTheory.Functor A B<VAR>R₂ : CategoryTheory.Functor B A<VAR>L₃ : CategoryTheory.Functor C D<VAR>R₃ : CategoryTheory.Functor D C<VAR>adj₁ : L₁ ⊣ R₁<VAR>adj₂ : L₂ ⊣ R₂<VAR>adj₃ : L₃ ⊣ R₃<VAR>α : L₂ ⟶ L₁<VAR>β : G.comp L₃ ⟶ L₂.comp H<GOAL>(CategoryTheory.mateEquiv adj₁ adj₃) (CategoryTheory.leftAdjointConjugateSquare.vcomp α β) = CategoryTheory.rightAdjointConjugateSquare.vcomp ((CategoryTheory.conjugateEquiv adj₁ adj₂) α) ((CategoryTheory.mateEquiv adj₂ adj₃) β)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A F : CategoryTheory.Functor Cᵒᵖ (Type v)<VAR>η : F ⟶ A<VAR>X : C<VAR>s : CategoryTheory.yoneda.obj X ⟶ A<VAR>u : F.obj (Opposite.op X)<VAR>self : CategoryTheory.OverPresheafAux.MakesOverArrow η s u<GOAL>η.app (Opposite.op X) u = CategoryTheory.yonedaEquiv s
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A F G : CategoryTheory.Functor Cᵒᵖ (Type v)<VAR>η : F ⟶ A<VAR>μ : G ⟶ A<VAR>ε : F ⟶ G<VAR>hε : CategoryTheory.CategoryStruct.comp ε μ = η<VAR>X : C<VAR>s : CategoryTheory.yoneda.obj X ⟶ A<VAR>u : F.obj (Opposite.op X)<VAR>h : CategoryTheory.OverPresheafAux.MakesOverArrow η s u<GOAL>CategoryTheory.OverPresheafAux.MakesOverArrow μ s (ε.app (Opposite.op X) u)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A F : CategoryTheory.Functor Cᵒᵖ (Type v)<VAR>η : F ⟶ A<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>s : CategoryTheory.yoneda.obj X ⟶ A<VAR>t : CategoryTheory.yoneda.obj Y ⟶ A<VAR>hst : CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map f) t = s<VAR>u : F.obj (Opposite.op Y)<VAR>h : CategoryTheory.OverPresheafAux.MakesOverArrow η t u<GOAL>CategoryTheory.OverPresheafAux.MakesOverArrow η s (F.map f.op u)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A F : CategoryTheory.Functor Cᵒᵖ (Type v)<VAR>η : F ⟶ A<VAR>X : C<VAR>s : CategoryTheory.yoneda.obj X ⟶ A<VAR>f : CategoryTheory.yoneda.obj X ⟶ F<VAR>hf : CategoryTheory.CategoryStruct.comp f η = s<GOAL>CategoryTheory.OverPresheafAux.MakesOverArrow η s (CategoryTheory.yonedaEquiv f)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A : CategoryTheory.Functor Cᵒᵖ (Type v)<VAR>Y : C<VAR>η : CategoryTheory.yoneda.obj Y ⟶ A<VAR>X : C<VAR>s : CategoryTheory.yoneda.obj X ⟶ A<VAR>f : X ⟶ Y<VAR>hf : CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map f) η = s<GOAL>CategoryTheory.OverPresheafAux.MakesOverArrow η s f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A F : CategoryTheory.Functor Cᵒᵖ (Type v)<VAR>η : F ⟶ A<VAR>X : C<VAR>s : CategoryTheory.yoneda.obj X ⟶ A<VAR>u : F.obj (Opposite.op X)<VAR>h : CategoryTheory.OverPresheafAux.MakesOverArrow η s u<GOAL>CategoryTheory.OverPresheafAux.OverArrows.val ⟨u, h⟩ = u
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A F : CategoryTheory.Functor Cᵒᵖ (Type v)<VAR>η : F ⟶ A<VAR>X : C<VAR>s : CategoryTheory.yoneda.obj X ⟶ A<VAR>u v : CategoryTheory.OverPresheafAux.OverArrows η s<GOAL>u.val = v.val → u = v
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A F : CategoryTheory.Functor Cᵒᵖ (Type v)<VAR>η : F ⟶ A<VAR>X : C<VAR>s : CategoryTheory.yoneda.obj X ⟶ A<VAR>p : CategoryTheory.OverPresheafAux.OverArrows η s<GOAL>η.app (Opposite.op X) p.val = CategoryTheory.yonedaEquiv s
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A : CategoryTheory.Functor Cᵒᵖ (Type v)<VAR>Y : C<VAR>η : CategoryTheory.yoneda.obj Y ⟶ A<VAR>X : C<VAR>s : CategoryTheory.yoneda.obj X ⟶ A<VAR>p : CategoryTheory.OverPresheafAux.OverArrows η s<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map p.val) η = s
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A F G : CategoryTheory.Functor Cᵒᵖ (Type v)<VAR>η : F ⟶ A<VAR>μ : G ⟶ A<VAR>X : C<VAR>s : CategoryTheory.yoneda.obj X ⟶ A<VAR>u : CategoryTheory.OverPresheafAux.OverArrows η s<VAR>ε : F ⟶ G<VAR>hε : CategoryTheory.CategoryStruct.comp ε μ = η<GOAL>(u.map₁ ε hε).val = ε.app (Opposite.op X) u.val
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A F : CategoryTheory.Functor Cᵒᵖ (Type v)<VAR>η : F ⟶ A<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>s : CategoryTheory.yoneda.obj X ⟶ A<VAR>t : CategoryTheory.yoneda.obj Y ⟶ A<VAR>hst : CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map f) t = s<VAR>u : CategoryTheory.OverPresheafAux.OverArrows η t<GOAL>(u.map₂ f hst).val = F.map f.op u.val
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A F G : CategoryTheory.Functor Cᵒᵖ (Type v)<VAR>η : F ⟶ A<VAR>μ : G ⟶ A<VAR>ε : F ⟶ G<VAR>hε : CategoryTheory.CategoryStruct.comp ε μ = η<VAR>X Y : C<VAR>s : CategoryTheory.yoneda.obj X ⟶ A<VAR>t : CategoryTheory.yoneda.obj Y ⟶ A<VAR>f : X ⟶ Y<VAR>hf : CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map f) t = s<VAR>u : CategoryTheory.OverPresheafAux.OverArrows η t<GOAL>(u.map₁ ε hε).map₂ f hf = (u.map₂ f hf).map₁ ε hε
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A : CategoryTheory.Functor Cᵒᵖ (Type v)<VAR>Y : C<VAR>η : CategoryTheory.yoneda.obj Y ⟶ A<VAR>X : C<VAR>s : CategoryTheory.yoneda.obj X ⟶ A<VAR>f : X ⟶ Y<VAR>hf : CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map f) η = s<GOAL>(CategoryTheory.OverPresheafAux.OverArrows.yonedaArrow f hf).val = f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A F : CategoryTheory.Functor Cᵒᵖ (Type v)<VAR>η : F ⟶ A<VAR>s : (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ<GOAL>(CategoryTheory.OverPresheafAux.restrictedYonedaObj η).obj s = CategoryTheory.OverPresheafAux.OverArrows η (Opposite.unop s).hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A F : CategoryTheory.Functor Cᵒᵖ (Type v)<VAR>η : F ⟶ A<GOAL>∀ {X Y : (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ} (f : X ⟶ Y) (u : CategoryTheory.OverPresheafAux.OverArrows η (Opposite.unop X).hom), (CategoryTheory.OverPresheafAux.restrictedYonedaObj η).map f u = u.map₂ f.unop.left ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A F G : CategoryTheory.Functor Cᵒᵖ (Type v)<VAR>η : F ⟶ A<VAR>μ : G ⟶ A<VAR>ε : F ⟶ G<VAR>hε : CategoryTheory.CategoryStruct.comp ε μ = η<VAR>s : (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ<VAR>u : (CategoryTheory.OverPresheafAux.restrictedYonedaObj η).obj s<GOAL>(CategoryTheory.OverPresheafAux.restrictedYonedaObjMap₁ ε hε).app s u = CategoryTheory.OverPresheafAux.OverArrows.map₁ u ε hε
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A : CategoryTheory.Functor Cᵒᵖ (Type v)<VAR>η : CategoryTheory.Over A<GOAL>(CategoryTheory.OverPresheafAux.restrictedYoneda A).obj η = CategoryTheory.OverPresheafAux.restrictedYonedaObj η.hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A : CategoryTheory.Functor Cᵒᵖ (Type v)<GOAL>∀ {X Y : CategoryTheory.Over A} (ε : X ⟶ Y), (CategoryTheory.OverPresheafAux.restrictedYoneda A).map ε = CategoryTheory.OverPresheafAux.restrictedYonedaObjMap₁ ε.left ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A : CategoryTheory.Functor Cᵒᵖ (Type v)<VAR>F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>g g' : CategoryTheory.yoneda.obj Y ⟶ A<VAR>h : g = g'<VAR>x : F.obj (Opposite.op (CategoryTheory.CostructuredArrow.mk g'))<GOAL>F.map (CategoryTheory.CostructuredArrow.mkPrecomp g f).op (F.map (CategoryTheory.eqToHom ⋯) x) = F.map (CategoryTheory.eqToHom ⋯) (F.map (CategoryTheory.CostructuredArrow.mkPrecomp g' f).op x)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A : CategoryTheory.Functor Cᵒᵖ (Type v)<VAR>F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)<VAR>X : C<VAR>p : CategoryTheory.OverPresheafAux.YonedaCollection F X<GOAL>p.yonedaEquivFst = CategoryTheory.yonedaEquiv p.fst
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A : CategoryTheory.Functor Cᵒᵖ (Type v)<VAR>F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)<VAR>X : C<VAR>s : CategoryTheory.yoneda.obj X ⟶ A<VAR>x : F.obj (Opposite.op (CategoryTheory.CostructuredArrow.mk s))<GOAL>(CategoryTheory.OverPresheafAux.YonedaCollection.mk s x).fst = s
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A : CategoryTheory.Functor Cᵒᵖ (Type v)<VAR>F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)<VAR>X : C<VAR>s : CategoryTheory.yoneda.obj X ⟶ A<VAR>x : F.obj (Opposite.op (CategoryTheory.CostructuredArrow.mk s))<GOAL>(CategoryTheory.OverPresheafAux.YonedaCollection.mk s x).snd = F.map (CategoryTheory.eqToHom ⋯) x
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A : CategoryTheory.Functor Cᵒᵖ (Type v)<VAR>F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)<VAR>X : C<VAR>p q : CategoryTheory.OverPresheafAux.YonedaCollection F X<VAR>h : p.fst = q.fst<VAR>h' : F.map (CategoryTheory.eqToHom ⋯) q.snd = p.snd<GOAL>p = q
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A : CategoryTheory.Functor Cᵒᵖ (Type v)<VAR>F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)<VAR>X : C<VAR>G : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)<VAR>η : F ⟶ G<VAR>p : CategoryTheory.OverPresheafAux.YonedaCollection F X<GOAL>(CategoryTheory.OverPresheafAux.YonedaCollection.map₁ η p).fst = p.fst
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A : CategoryTheory.Functor Cᵒᵖ (Type v)<VAR>F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)<VAR>X : C<VAR>G : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)<VAR>η : F ⟶ G<VAR>p : CategoryTheory.OverPresheafAux.YonedaCollection F X<GOAL>(CategoryTheory.OverPresheafAux.YonedaCollection.map₁ η p).yonedaEquivFst = p.yonedaEquivFst
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A : CategoryTheory.Functor Cᵒᵖ (Type v)<VAR>F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)<VAR>X : C<VAR>G : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)<VAR>η : F ⟶ G<VAR>p : CategoryTheory.OverPresheafAux.YonedaCollection F X<GOAL>(CategoryTheory.OverPresheafAux.YonedaCollection.map₁ η p).snd = G.map (CategoryTheory.eqToHom ⋯) (η.app (Opposite.op (CategoryTheory.CostructuredArrow.mk p.fst)) p.snd)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A : CategoryTheory.Functor Cᵒᵖ (Type v)<VAR>F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>p : CategoryTheory.OverPresheafAux.YonedaCollection F Y<GOAL>(CategoryTheory.OverPresheafAux.YonedaCollection.map₂ F f p).fst = CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map f) p.fst
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A : CategoryTheory.Functor Cᵒᵖ (Type v)<VAR>F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>p : CategoryTheory.OverPresheafAux.YonedaCollection F Y<GOAL>(CategoryTheory.OverPresheafAux.YonedaCollection.map₂ F f p).yonedaEquivFst = A.map f.op p.yonedaEquivFst
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A : CategoryTheory.Functor Cᵒᵖ (Type v)<VAR>F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>p : CategoryTheory.OverPresheafAux.YonedaCollection F Y<GOAL>(CategoryTheory.OverPresheafAux.YonedaCollection.map₂ F f p).snd = F.map (CategoryTheory.CategoryStruct.comp (CategoryTheory.CostructuredArrow.mkPrecomp p.fst f).op (CategoryTheory.eqToHom ⋯)) p.snd
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A : CategoryTheory.Functor Cᵒᵖ (Type v)<VAR>F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)<VAR>X : C<GOAL>CategoryTheory.OverPresheafAux.YonedaCollection.map₁ (CategoryTheory.CategoryStruct.id F) = id
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A : CategoryTheory.Functor Cᵒᵖ (Type v)<VAR>F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)<VAR>X : C<VAR>G H : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)<VAR>η : F ⟶ G<VAR>μ : G ⟶ H<GOAL>CategoryTheory.OverPresheafAux.YonedaCollection.map₁ (CategoryTheory.CategoryStruct.comp η μ) = CategoryTheory.OverPresheafAux.YonedaCollection.map₁ μ ∘ CategoryTheory.OverPresheafAux.YonedaCollection.map₁ η
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A : CategoryTheory.Functor Cᵒᵖ (Type v)<VAR>F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)<VAR>X : C<GOAL>CategoryTheory.OverPresheafAux.YonedaCollection.map₂ F (CategoryTheory.CategoryStruct.id X) = id
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A : CategoryTheory.Functor Cᵒᵖ (Type v)<VAR>F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>CategoryTheory.OverPresheafAux.YonedaCollection.map₂ F (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.OverPresheafAux.YonedaCollection.map₂ F f ∘ CategoryTheory.OverPresheafAux.YonedaCollection.map₂ F g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A : CategoryTheory.Functor Cᵒᵖ (Type v)<VAR>F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)<VAR>X : C<VAR>G : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)<VAR>η : F ⟶ G<VAR>Y : C<VAR>f : X ⟶ Y<VAR>p : CategoryTheory.OverPresheafAux.YonedaCollection F Y<GOAL>CategoryTheory.OverPresheafAux.YonedaCollection.map₂ G f (CategoryTheory.OverPresheafAux.YonedaCollection.map₁ η p) = CategoryTheory.OverPresheafAux.YonedaCollection.map₁ η (CategoryTheory.OverPresheafAux.YonedaCollection.map₂ F f p)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A : CategoryTheory.Functor Cᵒᵖ (Type v)<VAR>F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)<VAR>X : Cᵒᵖ<GOAL>(CategoryTheory.OverPresheafAux.yonedaCollectionPresheaf A F).obj X = CategoryTheory.OverPresheafAux.YonedaCollection F (Opposite.unop X)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A : CategoryTheory.Functor Cᵒᵖ (Type v)<VAR>F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)<GOAL>∀ {X Y : Cᵒᵖ} (f : X ⟶ Y) (p : CategoryTheory.OverPresheafAux.YonedaCollection F (Opposite.unop X)), (CategoryTheory.OverPresheafAux.yonedaCollectionPresheaf A F).map f p = CategoryTheory.OverPresheafAux.YonedaCollection.map₂ F f.unop p
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A : CategoryTheory.Functor Cᵒᵖ (Type v)<VAR>F G : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)<VAR>η : F ⟶ G<VAR>X : Cᵒᵖ<GOAL>∀ (a : CategoryTheory.OverPresheafAux.YonedaCollection F (Opposite.unop X)), (CategoryTheory.OverPresheafAux.yonedaCollectionPresheafMap₁ η).app X a = CategoryTheory.OverPresheafAux.YonedaCollection.map₁ η a
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A : CategoryTheory.Functor Cᵒᵖ (Type v)<VAR>F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)<GOAL>(CategoryTheory.OverPresheafAux.yonedaCollectionFunctor A).obj F = CategoryTheory.OverPresheafAux.yonedaCollectionPresheaf A F
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A : CategoryTheory.Functor Cᵒᵖ (Type v)<GOAL>∀ {X Y : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)} (η : X ⟶ Y), (CategoryTheory.OverPresheafAux.yonedaCollectionFunctor A).map η = CategoryTheory.OverPresheafAux.yonedaCollectionPresheafMap₁ η
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A : CategoryTheory.Functor Cᵒᵖ (Type v)<VAR>F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)<VAR>X : Cᵒᵖ<VAR>p : CategoryTheory.OverPresheafAux.YonedaCollection F (Opposite.unop X)<GOAL>(CategoryTheory.OverPresheafAux.yonedaCollectionPresheafToA F).app X p = p.yonedaEquivFst
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A : CategoryTheory.Functor Cᵒᵖ (Type v)<GOAL>∀ {X Y : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)} (g : X ⟶ Y), (CategoryTheory.OverPresheafAux.costructuredArrowPresheafToOver A).map g = CategoryTheory.CostructuredArrow.homMk (CategoryTheory.OverPresheafAux.yonedaCollectionPresheafMap₁ g) ⋯
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A : CategoryTheory.Functor Cᵒᵖ (Type v)<VAR>Y : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)<GOAL>(CategoryTheory.OverPresheafAux.costructuredArrowPresheafToOver A).obj Y = CategoryTheory.CostructuredArrow.mk (CategoryTheory.OverPresheafAux.yonedaCollectionPresheafToA Y)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A F G : CategoryTheory.Functor Cᵒᵖ (Type v)<VAR>η : F ⟶ A<VAR>μ : G ⟶ A<VAR>ε : F ⟶ G<VAR>hε : CategoryTheory.CategoryStruct.comp ε μ = η<VAR>X : C<VAR>p : CategoryTheory.OverPresheafAux.YonedaCollection (CategoryTheory.OverPresheafAux.restrictedYonedaObj η) X<GOAL>CategoryTheory.OverPresheafAux.unitForward μ X (CategoryTheory.OverPresheafAux.YonedaCollection.map₁ (CategoryTheory.OverPresheafAux.restrictedYonedaObjMap₁ ε hε) p) = ε.app (Opposite.op X) (CategoryTheory.OverPresheafAux.unitForward η X p)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A F : CategoryTheory.Functor Cᵒᵖ (Type v)<VAR>η : F ⟶ A<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>p : CategoryTheory.OverPresheafAux.YonedaCollection (CategoryTheory.OverPresheafAux.restrictedYonedaObj η) Y<GOAL>CategoryTheory.OverPresheafAux.unitForward η X (CategoryTheory.OverPresheafAux.YonedaCollection.map₂ (CategoryTheory.OverPresheafAux.restrictedYonedaObj η) f p) = F.map f.op (CategoryTheory.OverPresheafAux.unitForward η Y p)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A F : CategoryTheory.Functor Cᵒᵖ (Type v)<VAR>η : F ⟶ A<VAR>X : Cᵒᵖ<VAR>p : CategoryTheory.OverPresheafAux.YonedaCollection (CategoryTheory.OverPresheafAux.restrictedYonedaObj η) (Opposite.unop X)<GOAL>η.app X (CategoryTheory.OverPresheafAux.unitForward η (Opposite.unop X) p) = p.yonedaEquivFst
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A F : CategoryTheory.Functor Cᵒᵖ (Type v)<VAR>η : F ⟶ A<VAR>X : C<GOAL>CategoryTheory.OverPresheafAux.unitForward η X ∘ CategoryTheory.OverPresheafAux.unitBackward η X = id
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A F : CategoryTheory.Functor Cᵒᵖ (Type v)<VAR>η : F ⟶ A<VAR>X : C<GOAL>CategoryTheory.OverPresheafAux.unitBackward η X ∘ CategoryTheory.OverPresheafAux.unitForward η X = id
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A F : CategoryTheory.Functor Cᵒᵖ (Type v)<VAR>η : F ⟶ A<VAR>X : C<GOAL>∀ (a : F.obj (Opposite.op X)), (CategoryTheory.OverPresheafAux.unitAuxAuxAux η X).inv a = CategoryTheory.OverPresheafAux.unitBackward η X a
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A F : CategoryTheory.Functor Cᵒᵖ (Type v)<VAR>η : F ⟶ A<VAR>X : C<GOAL>∀ (a : CategoryTheory.OverPresheafAux.YonedaCollection (CategoryTheory.OverPresheafAux.restrictedYonedaObj η) X), (CategoryTheory.OverPresheafAux.unitAuxAuxAux η X).hom a = CategoryTheory.OverPresheafAux.unitForward η X a
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A F : CategoryTheory.Functor Cᵒᵖ (Type v)<VAR>η : F ⟶ A<VAR>X : Cᵒᵖ<GOAL>∀ (a : F.obj X), ((CategoryTheory.OverPresheafAux.unitAuxAux η).inv.app X a).fst = η.app X a
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A F : CategoryTheory.Functor Cᵒᵖ (Type v)<VAR>η : F ⟶ A<VAR>X : Cᵒᵖ<GOAL>∀ (a : F.obj X), ↑((CategoryTheory.OverPresheafAux.unitAuxAux η).inv.app X a).snd = CategoryTheory.OverPresheafAux.OverArrows.val ⟨a, ⋯⟩
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A F : CategoryTheory.Functor Cᵒᵖ (Type v)<VAR>η : F ⟶ A<VAR>X : Cᵒᵖ<GOAL>∀ (a : (CategoryTheory.OverPresheafAux.yonedaCollectionPresheaf A (CategoryTheory.OverPresheafAux.restrictedYonedaObj η)).obj X), (CategoryTheory.OverPresheafAux.unitAuxAux η).hom.app X a = CategoryTheory.OverPresheafAux.unitForward η (Opposite.unop X) a
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A : CategoryTheory.Functor Cᵒᵖ (Type v)<VAR>η : CategoryTheory.Over A<GOAL>(CategoryTheory.OverPresheafAux.unitAux η).hom = { left := (CategoryTheory.OverPresheafAux.unitAuxAux η.hom).hom, right := CategoryTheory.CategoryStruct.id { as := PUnit.unit }, w := ⋯ }
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A : CategoryTheory.Functor Cᵒᵖ (Type v)<VAR>F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)<VAR>X : C<VAR>s : CategoryTheory.yoneda.obj X ⟶ A<VAR>p : CategoryTheory.OverPresheafAux.OverArrows (CategoryTheory.OverPresheafAux.yonedaCollectionPresheafToA F) s<GOAL>CategoryTheory.OverPresheafAux.YonedaCollection.fst p.val = s
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A : CategoryTheory.Functor Cᵒᵖ (Type v)<VAR>F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)<VAR>s : CategoryTheory.CostructuredArrow CategoryTheory.yoneda A<VAR>x : F.obj (Opposite.op s)<GOAL>CategoryTheory.OverPresheafAux.YonedaCollection.fst (CategoryTheory.OverPresheafAux.counitForward F s x).val = s.hom