ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>L : CategoryTheory.Functor C D<VAR>E : Type u_3<VAR>CategoryTheory.Category.{u_6, u_3} E<VAR>W : CategoryTheory.MorphismProperty C<VAR>F : CategoryTheory.Functor D E<GOAL>CategoryTheory.Localization.Lifting.iso L W (L.comp F) F = CategoryTheory.Iso.refl (L.comp F)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>L : CategoryTheory.Functor C D<VAR>W : CategoryTheory.MorphismProperty C<VAR>E : Type u_3<VAR>CategoryTheory.Category.{u_6, u_3} E<VAR>F₁ F₂ : CategoryTheory.Functor C E<VAR>F₁' F₂' : CategoryTheory.Functor D E<VAR>e : F₁ ≅ F₂<VAR>e' : F₁' ≅ F₂'<VAR>CategoryTheory.Localization.Lifting L W F₁ F₁'<GOAL>CategoryTheory.Localization.Lifting.iso' W = CategoryTheory.isoWhiskerLeft L e'.symm ≪≫ CategoryTheory.Localization.Lifting.iso L W F₁ F₁' ≪≫ e
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>W : CategoryTheory.MorphismProperty C<VAR>L₁ L₂ : CategoryTheory.Functor C D<VAR>e : L₁ ≅ L₂<VAR>L₁.IsLocalization W<GOAL>L₂.IsLocalization W
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_6, u_1} C<VAR>CategoryTheory.Category.{u_7, u_2} D<VAR>L : CategoryTheory.Functor C D<VAR>W : CategoryTheory.MorphismProperty C<VAR>E : Type u_4<VAR>CategoryTheory.Category.{u_5, u_4} E<VAR>L' : CategoryTheory.Functor C E<VAR>eq : D ≌ E<VAR>L.IsLocalization W<VAR>e : L.comp eq.functor ≅ L'<GOAL>L'.IsLocalization W
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>L : CategoryTheory.Functor C D<VAR>W : CategoryTheory.MorphismProperty C<VAR>hW : W ≤ CategoryTheory.MorphismProperty.isomorphisms C<VAR>L.IsEquivalence<GOAL>L.IsLocalization W
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_8, u_1} C<VAR>D₁ : Type u_4<VAR>D₂ : Type u_5<VAR>CategoryTheory.Category.{u_6, u_4} D₁<VAR>CategoryTheory.Category.{u_7, u_5} D₂<VAR>L₁ : CategoryTheory.Functor C D₁<VAR>L₂ : CategoryTheory.Functor C D₂<VAR>W' : CategoryTheory.MorphismProperty C<VAR>L₁.IsLocalization W'<VAR>L₂.IsLocalization W'<GOAL>(CategoryTheory.Localization.uniq L₁ L₂ W').symm = CategoryTheory.Localization.uniq L₂ L₁ W'
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>L : CategoryTheory.Functor C D<VAR>W : CategoryTheory.MorphismProperty C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>L.IsLocalization W<GOAL>CategoryTheory.AreEqualizedByLocalization W f g ↔ L.map f = L.map g
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>W : CategoryTheory.MorphismProperty C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>L : CategoryTheory.Functor C D<VAR>L.IsLocalization W<VAR>h : L.map f = L.map g<GOAL>CategoryTheory.AreEqualizedByLocalization W f g
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>W : CategoryTheory.MorphismProperty C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>h : CategoryTheory.AreEqualizedByLocalization W f g<VAR>L : CategoryTheory.Functor C D<VAR>L.IsLocalization W<GOAL>L.map f = L.map g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>self : CategoryTheory.Square C<GOAL>CategoryTheory.CategoryStruct.comp self.f₁₂ self.f₂₄ = CategoryTheory.CategoryStruct.comp self.f₁₃ self.f₃₄
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>sq : CategoryTheory.Square C<GOAL>CategoryTheory.CommSq sq.f₁₂ sq.f₁₃ sq.f₂₄ sq.f₃₄
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>sq₁ sq₂ : CategoryTheory.Square C<VAR>self : sq₁.Hom sq₂<GOAL>CategoryTheory.CategoryStruct.comp sq₁.f₁₃ self.τ₃ = CategoryTheory.CategoryStruct.comp self.τ₁ sq₂.f₁₃
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>sq₁ sq₂ : CategoryTheory.Square C<VAR>self : sq₁.Hom sq₂<GOAL>CategoryTheory.CategoryStruct.comp sq₁.f₃₄ self.τ₄ = CategoryTheory.CategoryStruct.comp self.τ₃ sq₂.f₃₄
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>sq₁ sq₂ : CategoryTheory.Square C<VAR>self : sq₁.Hom sq₂<GOAL>CategoryTheory.CategoryStruct.comp sq₁.f₁₂ self.τ₂ = CategoryTheory.CategoryStruct.comp self.τ₁ sq₂.f₁₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>sq₁ sq₂ : CategoryTheory.Square C<VAR>self : sq₁.Hom sq₂<GOAL>CategoryTheory.CategoryStruct.comp sq₁.f₂₄ self.τ₄ = CategoryTheory.CategoryStruct.comp self.τ₂ sq₂.f₂₄
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>sq : CategoryTheory.Square C<GOAL>(CategoryTheory.Square.Hom.id sq).τ₂ = CategoryTheory.CategoryStruct.id sq.X₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>sq : CategoryTheory.Square C<GOAL>(CategoryTheory.Square.Hom.id sq).τ₃ = CategoryTheory.CategoryStruct.id sq.X₃
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>sq : CategoryTheory.Square C<GOAL>(CategoryTheory.Square.Hom.id sq).τ₄ = CategoryTheory.CategoryStruct.id sq.X₄
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>sq : CategoryTheory.Square C<GOAL>(CategoryTheory.Square.Hom.id sq).τ₁ = CategoryTheory.CategoryStruct.id sq.X₁
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>sq₁ sq₂ sq₃ : CategoryTheory.Square C<VAR>f : sq₁.Hom sq₂<VAR>g : sq₂.Hom sq₃<GOAL>(f.comp g).τ₂ = CategoryTheory.CategoryStruct.comp f.τ₂ g.τ₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>sq₁ sq₂ sq₃ : CategoryTheory.Square C<VAR>f : sq₁.Hom sq₂<VAR>g : sq₂.Hom sq₃<GOAL>(f.comp g).τ₄ = CategoryTheory.CategoryStruct.comp f.τ₄ g.τ₄
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>sq₁ sq₂ sq₃ : CategoryTheory.Square C<VAR>f : sq₁.Hom sq₂<VAR>g : sq₂.Hom sq₃<GOAL>(f.comp g).τ₃ = CategoryTheory.CategoryStruct.comp f.τ₃ g.τ₃
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>sq₁ sq₂ sq₃ : CategoryTheory.Square C<VAR>f : sq₁.Hom sq₂<VAR>g : sq₂.Hom sq₃<GOAL>(f.comp g).τ₁ = CategoryTheory.CategoryStruct.comp f.τ₁ g.τ₁
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>∀ {X Y Z : CategoryTheory.Square C} (f : X.Hom Y) (g : Y.Hom Z), (CategoryTheory.CategoryStruct.comp f g).τ₁ = CategoryTheory.CategoryStruct.comp f.τ₁ g.τ₁
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>sq : CategoryTheory.Square C<GOAL>(CategoryTheory.CategoryStruct.id sq).τ₁ = CategoryTheory.CategoryStruct.id sq.X₁
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>sq : CategoryTheory.Square C<GOAL>(CategoryTheory.CategoryStruct.id sq).τ₂ = CategoryTheory.CategoryStruct.id sq.X₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>∀ {X Y Z : CategoryTheory.Square C} (f : X.Hom Y) (g : Y.Hom Z), (CategoryTheory.CategoryStruct.comp f g).τ₂ = CategoryTheory.CategoryStruct.comp f.τ₂ g.τ₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>sq : CategoryTheory.Square C<GOAL>(CategoryTheory.CategoryStruct.id sq).τ₃ = CategoryTheory.CategoryStruct.id sq.X₃
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>∀ {X Y Z : CategoryTheory.Square C} (f : X.Hom Y) (g : Y.Hom Z), (CategoryTheory.CategoryStruct.comp f g).τ₃ = CategoryTheory.CategoryStruct.comp f.τ₃ g.τ₃
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>sq : CategoryTheory.Square C<GOAL>(CategoryTheory.CategoryStruct.id sq).τ₄ = CategoryTheory.CategoryStruct.id sq.X₄
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>∀ {X Y Z : CategoryTheory.Square C} (f : X.Hom Y) (g : Y.Hom Z), (CategoryTheory.CategoryStruct.comp f g).τ₄ = CategoryTheory.CategoryStruct.comp f.τ₄ g.τ₄
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>sq₁ sq₂ : CategoryTheory.Square C<VAR>f g : sq₁ ⟶ sq₂<VAR>h₁ : f.τ₁ = g.τ₁<VAR>h₂ : f.τ₂ = g.τ₂<VAR>h₃ : f.τ₃ = g.τ₃<VAR>h₄ : f.τ₄ = g.τ₄<GOAL>f = g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>sq : CategoryTheory.Square C<GOAL>sq.flip.X₄ = sq.X₄
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>sq : CategoryTheory.Square C<GOAL>sq.flip.f₃₄ = sq.f₂₄
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>sq : CategoryTheory.Square C<GOAL>sq.flip.f₂₄ = sq.f₃₄
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>sq : CategoryTheory.Square C<GOAL>sq.flip.X₃ = sq.X₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>sq : CategoryTheory.Square C<GOAL>sq.flip.f₁₃ = sq.f₁₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>sq : CategoryTheory.Square C<GOAL>sq.flip.X₁ = sq.X₁
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>sq : CategoryTheory.Square C<GOAL>sq.flip.X₂ = sq.X₃
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>sq : CategoryTheory.Square C<GOAL>sq.flip.f₁₂ = sq.f₁₃
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>∀ {X Y : CategoryTheory.Square C} (φ : X ⟶ Y), (CategoryTheory.Square.flipFunctor.map φ).τ₃ = φ.τ₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>∀ {X Y : CategoryTheory.Square C} (φ : X ⟶ Y), (CategoryTheory.Square.flipFunctor.map φ).τ₁ = φ.τ₁
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>∀ {X Y : CategoryTheory.Square C} (φ : X ⟶ Y), (CategoryTheory.Square.flipFunctor.map φ).τ₄ = φ.τ₄
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>sq : CategoryTheory.Square C<GOAL>CategoryTheory.Square.flipFunctor.obj sq = sq.flip
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>∀ {X Y : CategoryTheory.Square C} (φ : X ⟶ Y), (CategoryTheory.Square.flipFunctor.map φ).τ₂ = φ.τ₃
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>CategoryTheory.Square.flipEquivalence.unitIso = CategoryTheory.Iso.refl (CategoryTheory.Functor.id (CategoryTheory.Square C))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>CategoryTheory.Square.flipEquivalence.functor = CategoryTheory.Square.flipFunctor
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>CategoryTheory.Square.flipEquivalence.inverse = CategoryTheory.Square.flipFunctor
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>CategoryTheory.Square.flipEquivalence.counitIso = CategoryTheory.Iso.refl (CategoryTheory.Square.flipFunctor.comp CategoryTheory.Square.flipFunctor)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>sq : CategoryTheory.Square C<GOAL>(CategoryTheory.Square.toArrowArrowFunctor.obj sq).left.hom = sq.f₁₃
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>∀ {X Y : CategoryTheory.Square C} (φ : X ⟶ Y), (CategoryTheory.Square.toArrowArrowFunctor.map φ).left.right = φ.τ₃
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>sq : CategoryTheory.Square C<GOAL>(CategoryTheory.Square.toArrowArrowFunctor.obj sq).left.right = sq.X₃
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>sq : CategoryTheory.Square C<GOAL>(CategoryTheory.Square.toArrowArrowFunctor.obj sq).hom.left = sq.f₁₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>∀ {X Y : CategoryTheory.Square C} (φ : X ⟶ Y), (CategoryTheory.Square.toArrowArrowFunctor.map φ).right.left = φ.τ₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>sq : CategoryTheory.Square C<GOAL>(CategoryTheory.Square.toArrowArrowFunctor.obj sq).right.hom = sq.f₂₄
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>sq : CategoryTheory.Square C<GOAL>(CategoryTheory.Square.toArrowArrowFunctor.obj sq).right.right = sq.X₄
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>sq : CategoryTheory.Square C<GOAL>(CategoryTheory.Square.toArrowArrowFunctor.obj sq).right.left = sq.X₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>sq : CategoryTheory.Square C<GOAL>(CategoryTheory.Square.toArrowArrowFunctor.obj sq).hom.right = sq.f₃₄
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>sq : CategoryTheory.Square C<GOAL>(CategoryTheory.Square.toArrowArrowFunctor.obj sq).left.left = sq.X₁
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>∀ {X Y : CategoryTheory.Square C} (φ : X ⟶ Y), (CategoryTheory.Square.toArrowArrowFunctor.map φ).right.right = φ.τ₄
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>∀ {X Y : CategoryTheory.Square C} (φ : X ⟶ Y), (CategoryTheory.Square.toArrowArrowFunctor.map φ).left.left = φ.τ₁
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>∀ {X Y : CategoryTheory.Arrow (CategoryTheory.Arrow C)} (φ : X ⟶ Y), (CategoryTheory.Square.fromArrowArrowFunctor.map φ).τ₁ = φ.left.left
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>f : CategoryTheory.Arrow (CategoryTheory.Arrow C)<GOAL>(CategoryTheory.Square.fromArrowArrowFunctor.obj f).f₃₄ = f.hom.right
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>∀ {X Y : CategoryTheory.Arrow (CategoryTheory.Arrow C)} (φ : X ⟶ Y), (CategoryTheory.Square.fromArrowArrowFunctor.map φ).τ₂ = φ.right.left
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>f : CategoryTheory.Arrow (CategoryTheory.Arrow C)<GOAL>(CategoryTheory.Square.fromArrowArrowFunctor.obj f).X₃ = f.left.right
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>f : CategoryTheory.Arrow (CategoryTheory.Arrow C)<GOAL>(CategoryTheory.Square.fromArrowArrowFunctor.obj f).X₄ = f.right.right
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>f : CategoryTheory.Arrow (CategoryTheory.Arrow C)<GOAL>(CategoryTheory.Square.fromArrowArrowFunctor.obj f).X₂ = f.right.left
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>f : CategoryTheory.Arrow (CategoryTheory.Arrow C)<GOAL>(CategoryTheory.Square.fromArrowArrowFunctor.obj f).f₁₂ = f.hom.left
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>f : CategoryTheory.Arrow (CategoryTheory.Arrow C)<GOAL>(CategoryTheory.Square.fromArrowArrowFunctor.obj f).f₁₃ = f.left.hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>f : CategoryTheory.Arrow (CategoryTheory.Arrow C)<GOAL>(CategoryTheory.Square.fromArrowArrowFunctor.obj f).f₂₄ = f.right.hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>∀ {X Y : CategoryTheory.Arrow (CategoryTheory.Arrow C)} (φ : X ⟶ Y), (CategoryTheory.Square.fromArrowArrowFunctor.map φ).τ₃ = φ.left.right
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>∀ {X Y : CategoryTheory.Arrow (CategoryTheory.Arrow C)} (φ : X ⟶ Y), (CategoryTheory.Square.fromArrowArrowFunctor.map φ).τ₄ = φ.right.right
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>f : CategoryTheory.Arrow (CategoryTheory.Arrow C)<GOAL>(CategoryTheory.Square.fromArrowArrowFunctor.obj f).X₁ = f.left.left
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>CategoryTheory.Square.arrowArrowEquivalence.unitIso = CategoryTheory.Iso.refl (CategoryTheory.Functor.id (CategoryTheory.Square C))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>CategoryTheory.Square.arrowArrowEquivalence.functor = CategoryTheory.Square.toArrowArrowFunctor
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>CategoryTheory.Square.arrowArrowEquivalence.inverse = CategoryTheory.Square.fromArrowArrowFunctor
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>CategoryTheory.Square.arrowArrowEquivalence.counitIso = CategoryTheory.Iso.refl (CategoryTheory.Square.fromArrowArrowFunctor.comp CategoryTheory.Square.toArrowArrowFunctor)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>sq : CategoryTheory.Square C<GOAL>(CategoryTheory.Square.toArrowArrowFunctor'.obj sq).right.right = sq.X₄
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>sq : CategoryTheory.Square C<GOAL>(CategoryTheory.Square.toArrowArrowFunctor'.obj sq).right.hom = sq.f₃₄
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>sq : CategoryTheory.Square C<GOAL>(CategoryTheory.Square.toArrowArrowFunctor'.obj sq).hom.right = sq.f₂₄
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>∀ {X Y : CategoryTheory.Square C} (φ : X ⟶ Y), (CategoryTheory.Square.toArrowArrowFunctor'.map φ).left.left = φ.τ₁
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>sq : CategoryTheory.Square C<GOAL>(CategoryTheory.Square.toArrowArrowFunctor'.obj sq).left.hom = sq.f₁₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>sq : CategoryTheory.Square C<GOAL>(CategoryTheory.Square.toArrowArrowFunctor'.obj sq).hom.left = sq.f₁₃
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>∀ {X Y : CategoryTheory.Square C} (φ : X ⟶ Y), (CategoryTheory.Square.toArrowArrowFunctor'.map φ).right.left = φ.τ₃
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>∀ {X Y : CategoryTheory.Square C} (φ : X ⟶ Y), (CategoryTheory.Square.toArrowArrowFunctor'.map φ).left.right = φ.τ₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>sq : CategoryTheory.Square C<GOAL>(CategoryTheory.Square.toArrowArrowFunctor'.obj sq).left.left = sq.X₁
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>sq : CategoryTheory.Square C<GOAL>(CategoryTheory.Square.toArrowArrowFunctor'.obj sq).right.left = sq.X₃
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>sq : CategoryTheory.Square C<GOAL>(CategoryTheory.Square.toArrowArrowFunctor'.obj sq).left.right = sq.X₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>∀ {X Y : CategoryTheory.Square C} (φ : X ⟶ Y), (CategoryTheory.Square.toArrowArrowFunctor'.map φ).right.right = φ.τ₄
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>f : CategoryTheory.Arrow (CategoryTheory.Arrow C)<GOAL>(CategoryTheory.Square.fromArrowArrowFunctor'.obj f).f₂₄ = f.hom.right
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>f : CategoryTheory.Arrow (CategoryTheory.Arrow C)<GOAL>(CategoryTheory.Square.fromArrowArrowFunctor'.obj f).X₁ = f.left.left
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>f : CategoryTheory.Arrow (CategoryTheory.Arrow C)<GOAL>(CategoryTheory.Square.fromArrowArrowFunctor'.obj f).X₂ = f.left.right
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>∀ {X Y : CategoryTheory.Arrow (CategoryTheory.Arrow C)} (φ : X ⟶ Y), (CategoryTheory.Square.fromArrowArrowFunctor'.map φ).τ₁ = φ.left.left
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>∀ {X Y : CategoryTheory.Arrow (CategoryTheory.Arrow C)} (φ : X ⟶ Y), (CategoryTheory.Square.fromArrowArrowFunctor'.map φ).τ₂ = φ.left.right
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>∀ {X Y : CategoryTheory.Arrow (CategoryTheory.Arrow C)} (φ : X ⟶ Y), (CategoryTheory.Square.fromArrowArrowFunctor'.map φ).τ₄ = φ.right.right
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>f : CategoryTheory.Arrow (CategoryTheory.Arrow C)<GOAL>(CategoryTheory.Square.fromArrowArrowFunctor'.obj f).X₃ = f.right.left
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>f : CategoryTheory.Arrow (CategoryTheory.Arrow C)<GOAL>(CategoryTheory.Square.fromArrowArrowFunctor'.obj f).f₁₃ = f.hom.left
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>∀ {X Y : CategoryTheory.Arrow (CategoryTheory.Arrow C)} (φ : X ⟶ Y), (CategoryTheory.Square.fromArrowArrowFunctor'.map φ).τ₃ = φ.right.left
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>f : CategoryTheory.Arrow (CategoryTheory.Arrow C)<GOAL>(CategoryTheory.Square.fromArrowArrowFunctor'.obj f).f₃₄ = f.right.hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>f : CategoryTheory.Arrow (CategoryTheory.Arrow C)<GOAL>(CategoryTheory.Square.fromArrowArrowFunctor'.obj f).X₄ = f.right.right
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>f : CategoryTheory.Arrow (CategoryTheory.Arrow C)<GOAL>(CategoryTheory.Square.fromArrowArrowFunctor'.obj f).f₁₂ = f.left.hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>CategoryTheory.Square.arrowArrowEquivalence'.unitIso = CategoryTheory.Iso.refl (CategoryTheory.Functor.id (CategoryTheory.Square C))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>CategoryTheory.Square.arrowArrowEquivalence'.functor = CategoryTheory.Square.toArrowArrowFunctor'
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>CategoryTheory.Square.arrowArrowEquivalence'.inverse = CategoryTheory.Square.fromArrowArrowFunctor'
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>CategoryTheory.Square.arrowArrowEquivalence'.counitIso = CategoryTheory.Iso.refl (CategoryTheory.Square.fromArrowArrowFunctor'.comp CategoryTheory.Square.toArrowArrowFunctor')
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>sq : CategoryTheory.Square C<GOAL>CategoryTheory.Square.evaluation₁.obj sq = sq.X₁
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>∀ {X Y : CategoryTheory.Square C} (φ : X ⟶ Y), CategoryTheory.Square.evaluation₁.map φ = φ.τ₁
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>∀ {X Y : CategoryTheory.Square C} (φ : X ⟶ Y), CategoryTheory.Square.evaluation₂.map φ = φ.τ₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>sq : CategoryTheory.Square C<GOAL>CategoryTheory.Square.evaluation₂.obj sq = sq.X₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>sq : CategoryTheory.Square C<GOAL>CategoryTheory.Square.evaluation₃.obj sq = sq.X₃
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>∀ {X Y : CategoryTheory.Square C} (φ : X ⟶ Y), CategoryTheory.Square.evaluation₃.map φ = φ.τ₃
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>∀ {X Y : CategoryTheory.Square C} (φ : X ⟶ Y), CategoryTheory.Square.evaluation₄.map φ = φ.τ₄
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>sq : CategoryTheory.Square C<GOAL>CategoryTheory.Square.evaluation₄.obj sq = sq.X₄
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>sq : CategoryTheory.Square C<GOAL>sq.op.f₃₄ = sq.f₁₃.op
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>sq : CategoryTheory.Square C<GOAL>sq.op.X₃ = Opposite.op sq.X₃
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>sq : CategoryTheory.Square C<GOAL>sq.op.f₁₂ = sq.f₂₄.op
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>sq : CategoryTheory.Square C<GOAL>sq.op.f₁₃ = sq.f₃₄.op
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>sq : CategoryTheory.Square C<GOAL>sq.op.X₄ = Opposite.op sq.X₁
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>sq : CategoryTheory.Square C<GOAL>sq.op.X₁ = Opposite.op sq.X₄
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>sq : CategoryTheory.Square C<GOAL>sq.op.X₂ = Opposite.op sq.X₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>sq : CategoryTheory.Square C<GOAL>sq.op.f₂₄ = sq.f₁₂.op
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>sq : CategoryTheory.Square Cᵒᵖ<GOAL>sq.unop.X₁ = Opposite.unop sq.X₄
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>sq : CategoryTheory.Square Cᵒᵖ<GOAL>sq.unop.f₁₂ = sq.f₂₄.unop
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>sq : CategoryTheory.Square Cᵒᵖ<GOAL>sq.unop.f₂₄ = sq.f₁₂.unop
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>sq : CategoryTheory.Square Cᵒᵖ<GOAL>sq.unop.X₃ = Opposite.unop sq.X₃
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>sq : CategoryTheory.Square Cᵒᵖ<GOAL>sq.unop.X₄ = Opposite.unop sq.X₁
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>sq : CategoryTheory.Square Cᵒᵖ<GOAL>sq.unop.f₃₄ = sq.f₁₃.unop
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>sq : CategoryTheory.Square Cᵒᵖ<GOAL>sq.unop.f₁₃ = sq.f₃₄.unop
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>sq : CategoryTheory.Square Cᵒᵖ<GOAL>sq.unop.X₂ = Opposite.unop sq.X₂
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>sq : (CategoryTheory.Square C)ᵒᵖ<GOAL>CategoryTheory.Square.opFunctor.obj sq = (Opposite.unop sq).op
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>∀ {X Y : (CategoryTheory.Square C)ᵒᵖ} (φ : X ⟶ Y), (CategoryTheory.Square.opFunctor.map φ).τ₃ = φ.unop.τ₃.op
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>∀ {X Y : (CategoryTheory.Square C)ᵒᵖ} (φ : X ⟶ Y), (CategoryTheory.Square.opFunctor.map φ).τ₄ = φ.unop.τ₁.op
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>∀ {X Y : (CategoryTheory.Square C)ᵒᵖ} (φ : X ⟶ Y), (CategoryTheory.Square.opFunctor.map φ).τ₂ = φ.unop.τ₂.op
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<GOAL>∀ {X Y : (CategoryTheory.Square C)ᵒᵖ} (φ : X ⟶ Y), (CategoryTheory.Square.opFunctor.map φ).τ₁ = φ.unop.τ₄.op
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u'<VAR>CategoryTheory.Category.{v', u'} D<VAR>sq : CategoryTheory.Square C<VAR>F : CategoryTheory.Functor C D<GOAL>(sq.map F).f₁₃ = F.map sq.f₁₃
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u'<VAR>CategoryTheory.Category.{v', u'} D<VAR>sq : CategoryTheory.Square C<VAR>F : CategoryTheory.Functor C D<GOAL>(sq.map F).f₃₄ = F.map sq.f₃₄