ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>F : CategoryTheory.Functor Cᵒᵖ (Type v)<VAR>X : CategoryTheory.CostructuredArrow CategoryTheory.yoneda F<GOAL>(CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalenceInverseπ F).hom.app X = CategoryTheory.CategoryStruct.id X.left
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>F : CategoryTheory.Functor C D<VAR>G H : CategoryTheory.Functor D E<VAR>α : G ⟶ H<VAR>X : C<GOAL>(CategoryTheory.whiskerLeft F α).app X = α.app (F.obj X)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>G H : CategoryTheory.Functor C D<VAR>α : G ⟶ H<VAR>F : CategoryTheory.Functor D E<VAR>X : C<GOAL>(CategoryTheory.whiskerRight α F).app X = F.map (α.app X)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<GOAL>∀ {X Y : CategoryTheory.Functor C D} (τ : X ⟶ Y) (H : CategoryTheory.Functor D E) (c : C), (((CategoryTheory.whiskeringLeft C D E).map τ).app H).app c = H.map (τ.app c)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>F : CategoryTheory.Functor C D<VAR>G : CategoryTheory.Functor D E<GOAL>((CategoryTheory.whiskeringLeft C D E).obj F).obj G = F.comp G
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>F : CategoryTheory.Functor C D<GOAL>∀ {X Y : CategoryTheory.Functor D E} (α : X ⟶ Y), ((CategoryTheory.whiskeringLeft C D E).obj F).map α = CategoryTheory.whiskerLeft F α
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>H : CategoryTheory.Functor D E<VAR>F : CategoryTheory.Functor C D<GOAL>((CategoryTheory.whiskeringRight C D E).obj H).obj F = F.comp H
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>H : CategoryTheory.Functor D E<GOAL>∀ {X Y : CategoryTheory.Functor C D} (α : X ⟶ Y), ((CategoryTheory.whiskeringRight C D E).obj H).map α = CategoryTheory.whiskerRight α H
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<GOAL>∀ {X Y : CategoryTheory.Functor D E} (τ : X ⟶ Y) (F : CategoryTheory.Functor C D) (c : C), (((CategoryTheory.whiskeringRight C D E).map τ).app F).app c = τ.app (F.obj c)
<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>F : CategoryTheory.Functor D E<VAR>hF : F.FullyFaithful<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<GOAL>∀ {X Y : CategoryTheory.Functor C D} (f : ((CategoryTheory.whiskeringRight C D E).obj F).obj X ⟶ ((CategoryTheory.whiskeringRight C D E).obj F).obj Y) (X_1 : C), ((hF.whiskeringRight C).preimage f).app X_1 = hF.preimage (f.app X_1)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>F : CategoryTheory.Functor C D<VAR>G : CategoryTheory.Functor D E<GOAL>CategoryTheory.whiskerLeft F (CategoryTheory.NatTrans.id G) = CategoryTheory.NatTrans.id (F.comp G)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>F : CategoryTheory.Functor C D<VAR>G : CategoryTheory.Functor D E<GOAL>CategoryTheory.whiskerLeft F (CategoryTheory.CategoryStruct.id G) = CategoryTheory.CategoryStruct.id (F.comp G)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>G : CategoryTheory.Functor C D<VAR>F : CategoryTheory.Functor D E<GOAL>CategoryTheory.whiskerRight (CategoryTheory.NatTrans.id G) F = CategoryTheory.NatTrans.id (G.comp F)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>G : CategoryTheory.Functor C D<VAR>F : CategoryTheory.Functor D E<GOAL>CategoryTheory.whiskerRight (CategoryTheory.CategoryStruct.id G) F = CategoryTheory.CategoryStruct.id (G.comp F)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>F : CategoryTheory.Functor C D<VAR>G H K : CategoryTheory.Functor D E<VAR>α : G ⟶ H<VAR>β : H ⟶ K<GOAL>CategoryTheory.whiskerLeft F (CategoryTheory.CategoryStruct.comp α β) = CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft F α) (CategoryTheory.whiskerLeft F β)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>G H K : CategoryTheory.Functor C D<VAR>α : G ⟶ H<VAR>β : H ⟶ K<VAR>F : CategoryTheory.Functor D E<GOAL>CategoryTheory.whiskerRight (CategoryTheory.CategoryStruct.comp α β) F = CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerRight α F) (CategoryTheory.whiskerRight β F)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>F : CategoryTheory.Functor C D<VAR>G H : CategoryTheory.Functor D E<VAR>α : G ≅ H<GOAL>(CategoryTheory.isoWhiskerLeft F α).hom = CategoryTheory.whiskerLeft F α.hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>F : CategoryTheory.Functor C D<VAR>G H : CategoryTheory.Functor D E<VAR>α : G ≅ H<GOAL>(CategoryTheory.isoWhiskerLeft F α).inv = CategoryTheory.whiskerLeft F α.inv
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>G H : CategoryTheory.Functor C D<VAR>α : G ≅ H<VAR>F : CategoryTheory.Functor D E<GOAL>(CategoryTheory.isoWhiskerRight α F).hom = CategoryTheory.whiskerRight α.hom F
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>G H : CategoryTheory.Functor C D<VAR>α : G ≅ H<VAR>F : CategoryTheory.Functor D E<GOAL>(CategoryTheory.isoWhiskerRight α F).inv = CategoryTheory.whiskerRight α.inv F
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>B : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} B<VAR>F : CategoryTheory.Functor B C<VAR>G : CategoryTheory.Functor C D<VAR>H K : CategoryTheory.Functor D E<VAR>α : H ⟶ K<GOAL>CategoryTheory.whiskerLeft F (CategoryTheory.whiskerLeft G α) = CategoryTheory.whiskerLeft (F.comp G) α
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>B : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} B<VAR>H K : CategoryTheory.Functor B C<VAR>F : CategoryTheory.Functor C D<VAR>G : CategoryTheory.Functor D E<VAR>α : H ⟶ K<GOAL>CategoryTheory.whiskerRight (CategoryTheory.whiskerRight α F) G = CategoryTheory.whiskerRight α (F.comp G)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>B : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} B<VAR>F : CategoryTheory.Functor B C<VAR>G H : CategoryTheory.Functor C D<VAR>α : G ⟶ H<VAR>K : CategoryTheory.Functor D E<GOAL>CategoryTheory.whiskerRight (CategoryTheory.whiskerLeft F α) K = CategoryTheory.whiskerLeft F (CategoryTheory.whiskerRight α K)
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>F : CategoryTheory.Functor A B<VAR>X : A<GOAL>F.leftUnitor.inv.app X = CategoryTheory.CategoryStruct.id (F.obj X)
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>F : CategoryTheory.Functor A B<VAR>X : A<GOAL>F.leftUnitor.hom.app X = CategoryTheory.CategoryStruct.id (F.obj X)
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>F : CategoryTheory.Functor A B<VAR>X : A<GOAL>F.rightUnitor.hom.app X = CategoryTheory.CategoryStruct.id (F.obj X)
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>F : CategoryTheory.Functor A B<VAR>X : A<GOAL>F.rightUnitor.inv.app X = CategoryTheory.CategoryStruct.id (F.obj X)
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>D : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} D<VAR>F : CategoryTheory.Functor A B<VAR>G : CategoryTheory.Functor B C<VAR>H : CategoryTheory.Functor C D<GOAL>∀ (x : A), (F.associator G H).hom.app x = CategoryTheory.CategoryStruct.id (((F.comp G).comp H).obj x)
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>D : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} D<VAR>F : CategoryTheory.Functor A B<VAR>G : CategoryTheory.Functor B C<VAR>H : CategoryTheory.Functor C D<GOAL>∀ (x : A), (F.associator G H).inv.app x = CategoryTheory.CategoryStruct.id ((F.comp (G.comp H)).obj x)
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>D : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} D<VAR>F : CategoryTheory.Functor A B<VAR>G : CategoryTheory.Functor B C<VAR>H : CategoryTheory.Functor C D<GOAL>(F.comp G).comp H = F.comp (G.comp H)
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>F : CategoryTheory.Functor A B<VAR>G : CategoryTheory.Functor B C<GOAL>CategoryTheory.CategoryStruct.comp (F.associator (CategoryTheory.Functor.id B) G).hom (CategoryTheory.whiskerLeft F G.leftUnitor.hom) = CategoryTheory.whiskerRight F.rightUnitor.hom G
<VAR>A : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} B<VAR>C : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} C<VAR>D : Type u₄<VAR>CategoryTheory.Category.{v₄, u₄} D<VAR>E : Type u₅<VAR>CategoryTheory.Category.{v₅, u₅} E<VAR>F : CategoryTheory.Functor A B<VAR>G : CategoryTheory.Functor B C<VAR>H : CategoryTheory.Functor C D<VAR>K : CategoryTheory.Functor D E<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerRight (F.associator G H).hom K) (CategoryTheory.CategoryStruct.comp (F.associator (G.comp H) K).hom (CategoryTheory.whiskerLeft F (G.associator H K).hom)) = CategoryTheory.CategoryStruct.comp ((F.comp G).associator H K).hom (F.associator G (H.comp K)).hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<VAR>p : X = X<GOAL>CategoryTheory.eqToHom p = CategoryTheory.CategoryStruct.id X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y Z : C<VAR>p : X = Y<VAR>q : Y = Z<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom p) (CategoryTheory.eqToHom q) = CategoryTheory.eqToHom ⋯
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y Y' : C<VAR>p : Y = Y'<VAR>f : X ⟶ Y<VAR>g : X ⟶ Y'<GOAL>CategoryTheory.CategoryStruct.comp f (CategoryTheory.eqToHom p) = g ↔ f = CategoryTheory.CategoryStruct.comp g (CategoryTheory.eqToHom ⋯)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X X' Y : C<VAR>p : X = X'<VAR>f : X ⟶ Y<VAR>g : X' ⟶ Y<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom p) g = f ↔ g = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) f
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>β : Sort u_1<VAR>f g : β → C<VAR>z : (b : β) → f b ⟶ g b<VAR>j j' : β<VAR>w : j = j'<GOAL>CategoryTheory.CategoryStruct.comp (z j) (CategoryTheory.eqToHom ⋯) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (z j')
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>β : Sort u_1<VAR>f g : β → C<VAR>z : (b : β) → f b ≅ g b<VAR>j j' : β<VAR>w : j = j'<GOAL>CategoryTheory.CategoryStruct.comp (z j).hom (CategoryTheory.eqToHom ⋯) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (z j').hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>β : Sort u_1<VAR>f g : β → C<VAR>z : (b : β) → f b ≅ g b<VAR>j j' : β<VAR>w : j = j'<GOAL>CategoryTheory.CategoryStruct.comp (z j).inv (CategoryTheory.eqToHom ⋯) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (z j').inv
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y Z : C<VAR>p : X = Y<VAR>q : Y ⟶ Z<GOAL>cast ⋯ q = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom p) q
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y Z : C<VAR>p : X = Y<VAR>q : Y ⟶ Z<GOAL>⋯.mpr q = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom p) q
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y Z : C<VAR>p : X ⟶ Y<VAR>q : Z = Y<GOAL>cast ⋯ p = CategoryTheory.CategoryStruct.comp p (CategoryTheory.eqToHom ⋯)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y Z : C<VAR>p : X ⟶ Y<VAR>q : Z = Y<GOAL>⋯.mpr p = CategoryTheory.CategoryStruct.comp p (CategoryTheory.eqToHom ⋯)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>p : X = Y<GOAL>(CategoryTheory.eqToIso p).hom = CategoryTheory.eqToHom p
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>p : X = Y<GOAL>(CategoryTheory.eqToIso p).inv = CategoryTheory.eqToHom ⋯
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X : C<VAR>p : X = X<GOAL>CategoryTheory.eqToIso p = CategoryTheory.Iso.refl X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y Z : C<VAR>p : X = Y<VAR>q : Y = Z<GOAL>CategoryTheory.eqToIso p ≪≫ CategoryTheory.eqToIso q = CategoryTheory.eqToIso ⋯
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>h : X = Y<GOAL>(CategoryTheory.eqToHom h).op = CategoryTheory.eqToHom ⋯
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : Cᵒᵖ<VAR>h : X = Y<GOAL>(CategoryTheory.eqToHom h).unop = CategoryTheory.eqToHom ⋯
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>h : X = Y<GOAL>CategoryTheory.inv (CategoryTheory.eqToHom h) = CategoryTheory.eqToHom ⋯
<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>h_obj : ∀ (X : C), F.obj X = G.obj X<VAR>h_map : ∀ (X Y : C) (f : X ⟶ Y), F.map f = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (G.map f) (CategoryTheory.eqToHom ⋯)) := by aesop_cat<GOAL>F = G
<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>e : F ≅ G<VAR>hobj : ∀ (X : C), F.obj X = G.obj X<VAR>happ : ∀ (X : C), e.hom.app X = CategoryTheory.eqToHom ⋯<GOAL>F = G
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>W X Y Z : C<VAR>f : W ⟶ X<VAR>g : Y ⟶ Z<VAR>h : W = Y<VAR>h' : X = Z<GOAL>f = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h) (CategoryTheory.CategoryStruct.comp g (CategoryTheory.eqToHom ⋯)) ↔ HEq f g
<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>h_obj : ∀ (X : C), F.obj X = G.obj X<VAR>h_map : ∀ (X Y : C) (f : X ⟶ Y), HEq (F.map f) (G.map f)<GOAL>F = G
<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>h : F = G<VAR>X : C<GOAL>F.obj X = G.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>h : F = G<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>F.map f = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (G.map f) (CategoryTheory.eqToHom ⋯))
<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>X Y : C<VAR>e : X ≅ Y<VAR>hX : F.obj X = G.obj X<VAR>hY : F.obj Y = G.obj Y<VAR>h₂ : F.map e.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (G.map e.hom) (CategoryTheory.eqToHom ⋯))<GOAL>F.map e.inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (G.map e.inv) (CategoryTheory.eqToHom ⋯))
<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>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>hx : F.obj X = G.obj X<VAR>hy : F.obj Y = G.obj Y<VAR>hz : F.obj Z = G.obj Z<VAR>hf : HEq (F.map f) (G.map f)<VAR>hg : HEq (F.map g) (G.map g)<GOAL>HEq (F.map (CategoryTheory.CategoryStruct.comp f g)) (G.map (CategoryTheory.CategoryStruct.comp f g))
<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>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>hobj : ∀ (X : C), F.obj X = G.obj X<VAR>hmap : ∀ {X Y : C} (f : X ⟶ Y), HEq (F.map f) (G.map f)<GOAL>HEq (F.map (CategoryTheory.CategoryStruct.comp f g)) (G.map (CategoryTheory.CategoryStruct.comp f g))
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>F G : CategoryTheory.Functor C D<VAR>H : CategoryTheory.Functor E C<VAR>hmap : ∀ {X Y : C} (f : X ⟶ Y), HEq (F.map f) (G.map f)<VAR>X Y : E<VAR>f : X ⟶ Y<GOAL>HEq ((H.comp F).map f) ((H.comp G).map f)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>F G : CategoryTheory.Functor C D<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>H : CategoryTheory.Functor D E<VAR>hx : F.obj X = G.obj X<VAR>hy : F.obj Y = G.obj Y<VAR>hmap : HEq (F.map f) (G.map f)<GOAL>HEq ((F.comp H).map f) ((G.comp H).map f)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>CategoryTheory.Category.{v₃, u₃} E<VAR>F G : CategoryTheory.Functor C D<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>H : CategoryTheory.Functor D E<VAR>hobj : ∀ (X : C), F.obj X = G.obj X<VAR>hmap : ∀ {X Y : C} (f : X ⟶ Y), HEq (F.map f) (G.map f)<GOAL>HEq ((F.comp H).map f) ((G.comp H).map 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>h : F = G<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>HEq (F.map f) (G.map f)
<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>p : X = Y<GOAL>F.map (CategoryTheory.eqToHom p) = CategoryTheory.eqToHom ⋯
<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 Z : C<VAR>p : X = Y<VAR>q : Y = Z<GOAL>CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.eqToHom p)) (F.map (CategoryTheory.eqToHom q)) = F.map (CategoryTheory.eqToHom ⋯)
<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>p : X = Y<GOAL>F.mapIso (CategoryTheory.eqToIso p) = CategoryTheory.eqToIso ⋯
<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 Z : C<VAR>p : X = Y<VAR>q : Y = Z<GOAL>F.mapIso (CategoryTheory.eqToIso p) ≪≫ F.mapIso (CategoryTheory.eqToIso q) = F.mapIso (CategoryTheory.eqToIso ⋯)
<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>h : F = G<VAR>X : C<GOAL>(CategoryTheory.eqToHom h).app X = CategoryTheory.eqToHom ⋯
<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 Y : C<VAR>h : X = Y<GOAL>α.app X = CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.eqToHom h)) (CategoryTheory.CategoryStruct.comp (α.app Y) (G.map (CategoryTheory.eqToHom ⋯)))
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>f = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp f (CategoryTheory.eqToHom ⋯))
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>ι : Type u_2<VAR>F G : ι → C<VAR>α : (i : ι) → F i ⟶ G i<VAR>i j : ι<VAR>h : i = j<GOAL>α i = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (α j) (CategoryTheory.eqToHom ⋯))
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>L : CategoryTheory.Functor C D<VAR>R : CategoryTheory.Functor D C<VAR>h : L ⊣ R<GOAL>h.toMonad.η = h.unit
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>L : CategoryTheory.Functor C D<VAR>R : CategoryTheory.Functor D C<VAR>h : L ⊣ R<GOAL>h.toMonad.toFunctor = L.comp R
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>L : CategoryTheory.Functor C D<VAR>R : CategoryTheory.Functor D C<VAR>h : L ⊣ R<GOAL>h.toMonad.μ = CategoryTheory.whiskerRight (CategoryTheory.whiskerLeft L h.counit) R
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>L : CategoryTheory.Functor C D<VAR>R : CategoryTheory.Functor D C<VAR>h : L ⊣ R<GOAL>h.toComonad.toFunctor = R.comp L
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>L : CategoryTheory.Functor C D<VAR>R : CategoryTheory.Functor D C<VAR>h : L ⊣ R<GOAL>h.toComonad.ε = h.counit
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} D<VAR>L : CategoryTheory.Functor C D<VAR>R : CategoryTheory.Functor D C<VAR>h : L ⊣ R<GOAL>h.toComonad.δ = CategoryTheory.whiskerRight (CategoryTheory.whiskerLeft R h.unit) L
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>T : CategoryTheory.Monad C<VAR>X : C<GOAL>(CategoryTheory.Adjunction.adjToMonadIso T).hom.app X = CategoryTheory.CategoryStruct.id (T.obj X)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>T : CategoryTheory.Monad C<VAR>X : C<GOAL>(CategoryTheory.Adjunction.adjToMonadIso T).inv.app X = CategoryTheory.CategoryStruct.id (T.obj X)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>G : CategoryTheory.Comonad C<VAR>X : C<GOAL>(CategoryTheory.Adjunction.adjToComonadIso G).hom.app X = CategoryTheory.CategoryStruct.id (G.obj X)
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>G : CategoryTheory.Comonad C<VAR>X : C<GOAL>(CategoryTheory.Adjunction.adjToComonadIso G).inv.app X = CategoryTheory.CategoryStruct.id (G.obj X)