Loogle!

Result

Found 242 declarations mentioning CategoryTheory.Square. Of these, only the first 200 are shown.

CategoryTheory.Square 📋 Mathlib.CategoryTheory.Square
(C : Type u) [CategoryTheory.Category.{v, u} C] : Type (max u v)
CategoryTheory.Square.X₁ 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] (self : CategoryTheory.Square C) : C
CategoryTheory.Square.X₂ 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] (self : CategoryTheory.Square C) : C
CategoryTheory.Square.X₃ 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] (self : CategoryTheory.Square C) : C
CategoryTheory.Square.X₄ 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] (self : CategoryTheory.Square C) : C
CategoryTheory.Square.category 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] : CategoryTheory.Category.{v, max u v} (CategoryTheory.Square C)
CategoryTheory.Square.flip 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C) : CategoryTheory.Square C
CategoryTheory.Square.Hom 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] (sq₁ sq₂ : CategoryTheory.Square C) : Type v
CategoryTheory.Square.Hom.id 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C) : sq.Hom sq
CategoryTheory.Square.evaluation₁ 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] : CategoryTheory.Functor (CategoryTheory.Square C) C
CategoryTheory.Square.evaluation₂ 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] : CategoryTheory.Functor (CategoryTheory.Square C) C
CategoryTheory.Square.evaluation₃ 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] : CategoryTheory.Functor (CategoryTheory.Square C) C
CategoryTheory.Square.evaluation₄ 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] : CategoryTheory.Functor (CategoryTheory.Square C) C
CategoryTheory.Square.op 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C) : CategoryTheory.Square Cᵒᵖ
CategoryTheory.Square.unop 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square Cᵒᵖ) : CategoryTheory.Square C
CategoryTheory.Square.flipEquivalence 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] : CategoryTheory.Square C ≌ CategoryTheory.Square C
CategoryTheory.Square.flipFunctor 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] : CategoryTheory.Functor (CategoryTheory.Square C) (CategoryTheory.Square C)
CategoryTheory.Square.map 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (sq : CategoryTheory.Square C) (F : CategoryTheory.Functor C D) : CategoryTheory.Square D
CategoryTheory.Square.flip_X₁ 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C) : sq.flip.X₁ = sq.X₁
CategoryTheory.Square.flip_X₂ 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C) : sq.flip.X₂ = sq.X₃
CategoryTheory.Square.flip_X₃ 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C) : sq.flip.X₃ = sq.X₂
CategoryTheory.Square.flip_X₄ 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C) : sq.flip.X₄ = sq.X₄
CategoryTheory.Square.f₁₂ 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] (self : CategoryTheory.Square C) : self.X₁ ⟶ self.X₂
CategoryTheory.Square.f₁₃ 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] (self : CategoryTheory.Square C) : self.X₁ ⟶ self.X₃
CategoryTheory.Square.f₂₄ 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] (self : CategoryTheory.Square C) : self.X₂ ⟶ self.X₄
CategoryTheory.Square.f₃₄ 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] (self : CategoryTheory.Square C) : self.X₃ ⟶ self.X₄
CategoryTheory.Functor.mapSquare 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (F : CategoryTheory.Functor C D) : CategoryTheory.Functor (CategoryTheory.Square C) (CategoryTheory.Square D)
CategoryTheory.Square.arrowArrowEquivalence 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] : CategoryTheory.Square C ≌ CategoryTheory.Arrow (CategoryTheory.Arrow C)
CategoryTheory.Square.arrowArrowEquivalence' 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] : CategoryTheory.Square C ≌ CategoryTheory.Arrow (CategoryTheory.Arrow C)
CategoryTheory.Square.fromArrowArrowFunctor 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] : CategoryTheory.Functor (CategoryTheory.Arrow (CategoryTheory.Arrow C)) (CategoryTheory.Square C)
CategoryTheory.Square.fromArrowArrowFunctor' 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] : CategoryTheory.Functor (CategoryTheory.Arrow (CategoryTheory.Arrow C)) (CategoryTheory.Square C)
CategoryTheory.Square.toArrowArrowFunctor 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] : CategoryTheory.Functor (CategoryTheory.Square C) (CategoryTheory.Arrow (CategoryTheory.Arrow C))
CategoryTheory.Square.toArrowArrowFunctor' 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] : CategoryTheory.Functor (CategoryTheory.Square C) (CategoryTheory.Arrow (CategoryTheory.Arrow C))
CategoryTheory.Square.evaluation₁_obj 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C) : CategoryTheory.Square.evaluation₁.obj sq = sq.X₁
CategoryTheory.Square.evaluation₂_obj 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C) : CategoryTheory.Square.evaluation₂.obj sq = sq.X₂
CategoryTheory.Square.evaluation₃_obj 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C) : CategoryTheory.Square.evaluation₃.obj sq = sq.X₃
CategoryTheory.Square.evaluation₄_obj 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C) : CategoryTheory.Square.evaluation₄.obj sq = sq.X₄
CategoryTheory.Square.op_X₁ 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C) : sq.op.X₁ = Opposite.op sq.X₄
CategoryTheory.Square.op_X₂ 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C) : sq.op.X₂ = Opposite.op sq.X₂
CategoryTheory.Square.op_X₃ 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C) : sq.op.X₃ = Opposite.op sq.X₃
CategoryTheory.Square.op_X₄ 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C) : sq.op.X₄ = Opposite.op sq.X₁
CategoryTheory.Square.opEquivalence 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] : (CategoryTheory.Square C)ᵒᵖ ≌ CategoryTheory.Square Cᵒᵖ
CategoryTheory.Square.opFunctor 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] : CategoryTheory.Functor (CategoryTheory.Square C)ᵒᵖ (CategoryTheory.Square Cᵒᵖ)
CategoryTheory.Square.unop_X₁ 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square Cᵒᵖ) : sq.unop.X₁ = Opposite.unop sq.X₄
CategoryTheory.Square.unop_X₂ 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square Cᵒᵖ) : sq.unop.X₂ = Opposite.unop sq.X₂
CategoryTheory.Square.unop_X₃ 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square Cᵒᵖ) : sq.unop.X₃ = Opposite.unop sq.X₃
CategoryTheory.Square.unop_X₄ 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square Cᵒᵖ) : sq.unop.X₄ = Opposite.unop sq.X₁
CategoryTheory.Square.Hom.comp 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] {sq₁ sq₂ sq₃ : CategoryTheory.Square C} (f : sq₁.Hom sq₂) (g : sq₂.Hom sq₃) : sq₁.Hom sq₃
CategoryTheory.Square.Hom.τ₁ 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] {sq₁ sq₂ : CategoryTheory.Square C} (self : sq₁.Hom sq₂) : sq₁.X₁ ⟶ sq₂.X₁
CategoryTheory.Square.Hom.τ₂ 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] {sq₁ sq₂ : CategoryTheory.Square C} (self : sq₁.Hom sq₂) : sq₁.X₂ ⟶ sq₂.X₂
CategoryTheory.Square.Hom.τ₃ 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] {sq₁ sq₂ : CategoryTheory.Square C} (self : sq₁.Hom sq₂) : sq₁.X₃ ⟶ sq₂.X₃
CategoryTheory.Square.Hom.τ₄ 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] {sq₁ sq₂ : CategoryTheory.Square C} (self : sq₁.Hom sq₂) : sq₁.X₄ ⟶ sq₂.X₄
CategoryTheory.Square.unopFunctor 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] : CategoryTheory.Functor (CategoryTheory.Square Cᵒᵖ)ᵒᵖ (CategoryTheory.Square C)
CategoryTheory.Square.flipFunctor_obj 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C) : CategoryTheory.Square.flipFunctor.obj sq = sq.flip
CategoryTheory.Square.flip_f₁₂ 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C) : sq.flip.f₁₂ = sq.f₁₃
CategoryTheory.Square.flip_f₁₃ 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C) : sq.flip.f₁₃ = sq.f₁₂
CategoryTheory.Square.flip_f₂₄ 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C) : sq.flip.f₂₄ = sq.f₃₄
CategoryTheory.Square.flip_f₃₄ 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C) : sq.flip.f₃₄ = sq.f₂₄
CategoryTheory.Square.flipEquivalence_functor 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] : CategoryTheory.Square.flipEquivalence.functor = CategoryTheory.Square.flipFunctor
CategoryTheory.Square.flipEquivalence_inverse 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] : CategoryTheory.Square.flipEquivalence.inverse = CategoryTheory.Square.flipFunctor
CategoryTheory.Square.map_X₁ 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (sq : CategoryTheory.Square C) (F : CategoryTheory.Functor C D) : (sq.map F).X₁ = F.obj sq.X₁
CategoryTheory.Square.map_X₂ 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (sq : CategoryTheory.Square C) (F : CategoryTheory.Functor C D) : (sq.map F).X₂ = F.obj sq.X₂
CategoryTheory.Square.map_X₃ 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (sq : CategoryTheory.Square C) (F : CategoryTheory.Functor C D) : (sq.map F).X₃ = F.obj sq.X₃
CategoryTheory.Square.map_X₄ 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (sq : CategoryTheory.Square C) (F : CategoryTheory.Functor C D) : (sq.map F).X₄ = F.obj sq.X₄
CategoryTheory.Square.Hom.id_τ₁ 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C) : (CategoryTheory.Square.Hom.id sq).τ₁ = CategoryTheory.CategoryStruct.id sq.X₁
CategoryTheory.Square.Hom.id_τ₂ 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C) : (CategoryTheory.Square.Hom.id sq).τ₂ = CategoryTheory.CategoryStruct.id sq.X₂
CategoryTheory.Square.Hom.id_τ₃ 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C) : (CategoryTheory.Square.Hom.id sq).τ₃ = CategoryTheory.CategoryStruct.id sq.X₃
CategoryTheory.Square.Hom.id_τ₄ 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C) : (CategoryTheory.Square.Hom.id sq).τ₄ = CategoryTheory.CategoryStruct.id sq.X₄
CategoryTheory.Square.commSq 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C) : CategoryTheory.CommSq sq.f₁₂ sq.f₁₃ sq.f₂₄ sq.f₃₄
CategoryTheory.Square.mapFunctor 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] : CategoryTheory.Functor (CategoryTheory.Functor C D) (CategoryTheory.Functor (CategoryTheory.Square C) (CategoryTheory.Square D))
CategoryTheory.Functor.mapSquare_obj 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (F : CategoryTheory.Functor C D) (sq : CategoryTheory.Square C) : F.mapSquare.obj sq = sq.map F
CategoryTheory.Square.category_id_τ₁ 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C) : (CategoryTheory.CategoryStruct.id sq).τ₁ = CategoryTheory.CategoryStruct.id sq.X₁
CategoryTheory.Square.category_id_τ₂ 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C) : (CategoryTheory.CategoryStruct.id sq).τ₂ = CategoryTheory.CategoryStruct.id sq.X₂
CategoryTheory.Square.category_id_τ₃ 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C) : (CategoryTheory.CategoryStruct.id sq).τ₃ = CategoryTheory.CategoryStruct.id sq.X₃
CategoryTheory.Square.category_id_τ₄ 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C) : (CategoryTheory.CategoryStruct.id sq).τ₄ = CategoryTheory.CategoryStruct.id sq.X₄
CategoryTheory.Square.opFunctor_obj 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] (sq : (CategoryTheory.Square C)ᵒᵖ) : CategoryTheory.Square.opFunctor.obj sq = (Opposite.unop sq).op
CategoryTheory.Square.fromArrowArrowFunctor'_obj_X₁ 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] (f : CategoryTheory.Arrow (CategoryTheory.Arrow C)) : (CategoryTheory.Square.fromArrowArrowFunctor'.obj f).X₁ = f.left.left
CategoryTheory.Square.fromArrowArrowFunctor'_obj_X₂ 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] (f : CategoryTheory.Arrow (CategoryTheory.Arrow C)) : (CategoryTheory.Square.fromArrowArrowFunctor'.obj f).X₂ = f.left.right
CategoryTheory.Square.fromArrowArrowFunctor'_obj_X₃ 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] (f : CategoryTheory.Arrow (CategoryTheory.Arrow C)) : (CategoryTheory.Square.fromArrowArrowFunctor'.obj f).X₃ = f.right.left
CategoryTheory.Square.fromArrowArrowFunctor'_obj_X₄ 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] (f : CategoryTheory.Arrow (CategoryTheory.Arrow C)) : (CategoryTheory.Square.fromArrowArrowFunctor'.obj f).X₄ = f.right.right
CategoryTheory.Square.fromArrowArrowFunctor_obj_X₁ 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] (f : CategoryTheory.Arrow (CategoryTheory.Arrow C)) : (CategoryTheory.Square.fromArrowArrowFunctor.obj f).X₁ = f.left.left
CategoryTheory.Square.fromArrowArrowFunctor_obj_X₂ 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] (f : CategoryTheory.Arrow (CategoryTheory.Arrow C)) : (CategoryTheory.Square.fromArrowArrowFunctor.obj f).X₂ = f.right.left
CategoryTheory.Square.fromArrowArrowFunctor_obj_X₃ 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] (f : CategoryTheory.Arrow (CategoryTheory.Arrow C)) : (CategoryTheory.Square.fromArrowArrowFunctor.obj f).X₃ = f.left.right
CategoryTheory.Square.fromArrowArrowFunctor_obj_X₄ 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] (f : CategoryTheory.Arrow (CategoryTheory.Arrow C)) : (CategoryTheory.Square.fromArrowArrowFunctor.obj f).X₄ = f.right.right
CategoryTheory.Square.arrowArrowEquivalence'_functor 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] : CategoryTheory.Square.arrowArrowEquivalence'.functor = CategoryTheory.Square.toArrowArrowFunctor'
CategoryTheory.Square.arrowArrowEquivalence'_inverse 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] : CategoryTheory.Square.arrowArrowEquivalence'.inverse = CategoryTheory.Square.fromArrowArrowFunctor'
CategoryTheory.Square.arrowArrowEquivalence_functor 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] : CategoryTheory.Square.arrowArrowEquivalence.functor = CategoryTheory.Square.toArrowArrowFunctor
CategoryTheory.Square.arrowArrowEquivalence_inverse 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] : CategoryTheory.Square.arrowArrowEquivalence.inverse = CategoryTheory.Square.fromArrowArrowFunctor
CategoryTheory.Square.op_f₁₂ 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C) : sq.op.f₁₂ = sq.f₂₄.op
CategoryTheory.Square.op_f₁₃ 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C) : sq.op.f₁₃ = sq.f₃₄.op
CategoryTheory.Square.op_f₂₄ 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C) : sq.op.f₂₄ = sq.f₁₂.op
CategoryTheory.Square.op_f₃₄ 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C) : sq.op.f₃₄ = sq.f₁₃.op
CategoryTheory.Square.evaluation₁_map 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] {X✝ Y✝ : CategoryTheory.Square C} (φ : X✝ ⟶ Y✝) : CategoryTheory.Square.evaluation₁.map φ = φ.τ₁
CategoryTheory.Square.evaluation₂_map 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] {X✝ Y✝ : CategoryTheory.Square C} (φ : X✝ ⟶ Y✝) : CategoryTheory.Square.evaluation₂.map φ = φ.τ₂
CategoryTheory.Square.evaluation₃_map 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] {X✝ Y✝ : CategoryTheory.Square C} (φ : X✝ ⟶ Y✝) : CategoryTheory.Square.evaluation₃.map φ = φ.τ₃
CategoryTheory.Square.evaluation₄_map 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] {X✝ Y✝ : CategoryTheory.Square C} (φ : X✝ ⟶ Y✝) : CategoryTheory.Square.evaluation₄.map φ = φ.τ₄
CategoryTheory.Square.map_f₁₂ 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (sq : CategoryTheory.Square C) (F : CategoryTheory.Functor C D) : (sq.map F).f₁₂ = F.map sq.f₁₂
CategoryTheory.Square.map_f₁₃ 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (sq : CategoryTheory.Square C) (F : CategoryTheory.Functor C D) : (sq.map F).f₁₃ = F.map sq.f₁₃
CategoryTheory.Square.map_f₂₄ 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (sq : CategoryTheory.Square C) (F : CategoryTheory.Functor C D) : (sq.map F).f₂₄ = F.map sq.f₂₄
CategoryTheory.Square.map_f₃₄ 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (sq : CategoryTheory.Square C) (F : CategoryTheory.Functor C D) : (sq.map F).f₃₄ = F.map sq.f₃₄
CategoryTheory.Square.unop_f₁₂ 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square Cᵒᵖ) : sq.unop.f₁₂ = sq.f₂₄.unop
CategoryTheory.Square.unop_f₁₃ 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square Cᵒᵖ) : sq.unop.f₁₃ = sq.f₃₄.unop
CategoryTheory.Square.unop_f₂₄ 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square Cᵒᵖ) : sq.unop.f₂₄ = sq.f₁₂.unop
CategoryTheory.Square.unop_f₃₄ 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square Cᵒᵖ) : sq.unop.f₃₄ = sq.f₁₃.unop
CategoryTheory.Square.fac 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] (self : CategoryTheory.Square C) : CategoryTheory.CategoryStruct.comp self.f₁₂ self.f₂₄ = CategoryTheory.CategoryStruct.comp self.f₁₃ self.f₃₄
CategoryTheory.Square.mapFunctor_obj 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (F : CategoryTheory.Functor C D) : CategoryTheory.Square.mapFunctor.obj F = F.mapSquare
CategoryTheory.Square.mk 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ X₄ : C} (f₁₂ : X₁ ⟶ X₂) (f₁₃ : X₁ ⟶ X₃) (f₂₄ : X₂ ⟶ X₄) (f₃₄ : X₃ ⟶ X₄) (fac : CategoryTheory.CategoryStruct.comp f₁₂ f₂₄ = CategoryTheory.CategoryStruct.comp f₁₃ f₃₄) : CategoryTheory.Square C
CategoryTheory.Square.flipFunctor_map_τ₁ 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] {X✝ Y✝ : CategoryTheory.Square C} (φ : X✝ ⟶ Y✝) : (CategoryTheory.Square.flipFunctor.map φ).τ₁ = φ.τ₁
CategoryTheory.Square.flipFunctor_map_τ₂ 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] {X✝ Y✝ : CategoryTheory.Square C} (φ : X✝ ⟶ Y✝) : (CategoryTheory.Square.flipFunctor.map φ).τ₂ = φ.τ₃
CategoryTheory.Square.flipFunctor_map_τ₃ 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] {X✝ Y✝ : CategoryTheory.Square C} (φ : X✝ ⟶ Y✝) : (CategoryTheory.Square.flipFunctor.map φ).τ₃ = φ.τ₂
CategoryTheory.Square.flipFunctor_map_τ₄ 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] {X✝ Y✝ : CategoryTheory.Square C} (φ : X✝ ⟶ Y✝) : (CategoryTheory.Square.flipFunctor.map φ).τ₄ = φ.τ₄
CategoryTheory.Square.fromArrowArrowFunctor'_obj_f₁₂ 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] (f : CategoryTheory.Arrow (CategoryTheory.Arrow C)) : (CategoryTheory.Square.fromArrowArrowFunctor'.obj f).f₁₂ = f.left.hom
CategoryTheory.Square.fromArrowArrowFunctor'_obj_f₃₄ 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] (f : CategoryTheory.Arrow (CategoryTheory.Arrow C)) : (CategoryTheory.Square.fromArrowArrowFunctor'.obj f).f₃₄ = f.right.hom
CategoryTheory.Square.fromArrowArrowFunctor_obj_f₁₃ 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] (f : CategoryTheory.Arrow (CategoryTheory.Arrow C)) : (CategoryTheory.Square.fromArrowArrowFunctor.obj f).f₁₃ = f.left.hom
CategoryTheory.Square.fromArrowArrowFunctor_obj_f₂₄ 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] (f : CategoryTheory.Arrow (CategoryTheory.Arrow C)) : (CategoryTheory.Square.fromArrowArrowFunctor.obj f).f₂₄ = f.right.hom
CategoryTheory.Square.Hom.comp_τ₁ 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] {sq₁ sq₂ sq₃ : CategoryTheory.Square C} (f : sq₁.Hom sq₂) (g : sq₂.Hom sq₃) : (f.comp g).τ₁ = CategoryTheory.CategoryStruct.comp f.τ₁ g.τ₁
CategoryTheory.Square.Hom.comp_τ₂ 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] {sq₁ sq₂ sq₃ : CategoryTheory.Square C} (f : sq₁.Hom sq₂) (g : sq₂.Hom sq₃) : (f.comp g).τ₂ = CategoryTheory.CategoryStruct.comp f.τ₂ g.τ₂
CategoryTheory.Square.Hom.comp_τ₃ 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] {sq₁ sq₂ sq₃ : CategoryTheory.Square C} (f : sq₁.Hom sq₂) (g : sq₂.Hom sq₃) : (f.comp g).τ₃ = CategoryTheory.CategoryStruct.comp f.τ₃ g.τ₃
CategoryTheory.Square.Hom.comp_τ₄ 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] {sq₁ sq₂ sq₃ : CategoryTheory.Square C} (f : sq₁.Hom sq₂) (g : sq₂.Hom sq₃) : (f.comp g).τ₄ = CategoryTheory.CategoryStruct.comp f.τ₄ g.τ₄
CategoryTheory.Square.toArrowArrowFunctor'_obj_left_left 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C) : (CategoryTheory.Square.toArrowArrowFunctor'.obj sq).left.left = sq.X₁
CategoryTheory.Square.toArrowArrowFunctor'_obj_left_right 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C) : (CategoryTheory.Square.toArrowArrowFunctor'.obj sq).left.right = sq.X₂
CategoryTheory.Square.toArrowArrowFunctor'_obj_right_left 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C) : (CategoryTheory.Square.toArrowArrowFunctor'.obj sq).right.left = sq.X₃
CategoryTheory.Square.toArrowArrowFunctor'_obj_right_right 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C) : (CategoryTheory.Square.toArrowArrowFunctor'.obj sq).right.right = sq.X₄
CategoryTheory.Square.toArrowArrowFunctor_obj_left_left 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C) : (CategoryTheory.Square.toArrowArrowFunctor.obj sq).left.left = sq.X₁
CategoryTheory.Square.toArrowArrowFunctor_obj_left_right 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C) : (CategoryTheory.Square.toArrowArrowFunctor.obj sq).left.right = sq.X₃
CategoryTheory.Square.toArrowArrowFunctor_obj_right_left 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C) : (CategoryTheory.Square.toArrowArrowFunctor.obj sq).right.left = sq.X₂
CategoryTheory.Square.toArrowArrowFunctor_obj_right_right 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C) : (CategoryTheory.Square.toArrowArrowFunctor.obj sq).right.right = sq.X₄
CategoryTheory.Square.Hom.comm₁₂ 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] {sq₁ sq₂ : CategoryTheory.Square C} (self : sq₁.Hom sq₂) : CategoryTheory.CategoryStruct.comp sq₁.f₁₂ self.τ₂ = CategoryTheory.CategoryStruct.comp self.τ₁ sq₂.f₁₂
CategoryTheory.Square.Hom.comm₁₃ 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] {sq₁ sq₂ : CategoryTheory.Square C} (self : sq₁.Hom sq₂) : CategoryTheory.CategoryStruct.comp sq₁.f₁₃ self.τ₃ = CategoryTheory.CategoryStruct.comp self.τ₁ sq₂.f₁₃
CategoryTheory.Square.Hom.comm₂₄ 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] {sq₁ sq₂ : CategoryTheory.Square C} (self : sq₁.Hom sq₂) : CategoryTheory.CategoryStruct.comp sq₁.f₂₄ self.τ₄ = CategoryTheory.CategoryStruct.comp self.τ₂ sq₂.f₂₄
CategoryTheory.Square.Hom.comm₃₄ 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] {sq₁ sq₂ : CategoryTheory.Square C} (self : sq₁.Hom sq₂) : CategoryTheory.CategoryStruct.comp sq₁.f₃₄ self.τ₄ = CategoryTheory.CategoryStruct.comp self.τ₃ sq₂.f₃₄
CategoryTheory.Square.category_comp_τ₁ 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] {X✝ Y✝ Z✝ : CategoryTheory.Square C} (f : X✝.Hom Y✝) (g : Y✝.Hom Z✝) : (CategoryTheory.CategoryStruct.comp f g).τ₁ = CategoryTheory.CategoryStruct.comp f.τ₁ g.τ₁
CategoryTheory.Square.category_comp_τ₂ 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] {X✝ Y✝ Z✝ : CategoryTheory.Square C} (f : X✝.Hom Y✝) (g : Y✝.Hom Z✝) : (CategoryTheory.CategoryStruct.comp f g).τ₂ = CategoryTheory.CategoryStruct.comp f.τ₂ g.τ₂
CategoryTheory.Square.category_comp_τ₃ 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] {X✝ Y✝ Z✝ : CategoryTheory.Square C} (f : X✝.Hom Y✝) (g : Y✝.Hom Z✝) : (CategoryTheory.CategoryStruct.comp f g).τ₃ = CategoryTheory.CategoryStruct.comp f.τ₃ g.τ₃
CategoryTheory.Square.category_comp_τ₄ 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] {X✝ Y✝ Z✝ : CategoryTheory.Square C} (f : X✝.Hom Y✝) (g : Y✝.Hom Z✝) : (CategoryTheory.CategoryStruct.comp f g).τ₄ = CategoryTheory.CategoryStruct.comp f.τ₄ g.τ₄
CategoryTheory.Square.flipEquivalence_unitIso 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] : CategoryTheory.Square.flipEquivalence.unitIso = CategoryTheory.Iso.refl (CategoryTheory.Functor.id (CategoryTheory.Square C))
CategoryTheory.Square.fromArrowArrowFunctor'_obj_f₁₃ 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] (f : CategoryTheory.Arrow (CategoryTheory.Arrow C)) : (CategoryTheory.Square.fromArrowArrowFunctor'.obj f).f₁₃ = CategoryTheory.Arrow.Hom.left f.hom
CategoryTheory.Square.fromArrowArrowFunctor'_obj_f₂₄ 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] (f : CategoryTheory.Arrow (CategoryTheory.Arrow C)) : (CategoryTheory.Square.fromArrowArrowFunctor'.obj f).f₂₄ = CategoryTheory.Arrow.Hom.right f.hom
CategoryTheory.Square.fromArrowArrowFunctor_obj_f₁₂ 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] (f : CategoryTheory.Arrow (CategoryTheory.Arrow C)) : (CategoryTheory.Square.fromArrowArrowFunctor.obj f).f₁₂ = CategoryTheory.Arrow.Hom.left f.hom
CategoryTheory.Square.fromArrowArrowFunctor_obj_f₃₄ 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] (f : CategoryTheory.Arrow (CategoryTheory.Arrow C)) : (CategoryTheory.Square.fromArrowArrowFunctor.obj f).f₃₄ = CategoryTheory.Arrow.Hom.right f.hom
CategoryTheory.Square.toArrowArrowFunctor'_obj_left_hom 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C) : (CategoryTheory.Square.toArrowArrowFunctor'.obj sq).left.hom = sq.f₁₂
CategoryTheory.Square.toArrowArrowFunctor'_obj_right_hom 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C) : (CategoryTheory.Square.toArrowArrowFunctor'.obj sq).right.hom = sq.f₃₄
CategoryTheory.Square.toArrowArrowFunctor_obj_left_hom 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C) : (CategoryTheory.Square.toArrowArrowFunctor.obj sq).left.hom = sq.f₁₃
CategoryTheory.Square.toArrowArrowFunctor_obj_right_hom 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C) : (CategoryTheory.Square.toArrowArrowFunctor.obj sq).right.hom = sq.f₂₄
CategoryTheory.Square.arrowArrowEquivalence'_unitIso 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] : CategoryTheory.Square.arrowArrowEquivalence'.unitIso = CategoryTheory.Iso.refl (CategoryTheory.Functor.id (CategoryTheory.Square C))
CategoryTheory.Square.arrowArrowEquivalence_unitIso 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] : CategoryTheory.Square.arrowArrowEquivalence.unitIso = CategoryTheory.Iso.refl (CategoryTheory.Functor.id (CategoryTheory.Square C))
CategoryTheory.NatTrans.mapSquare 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {F G : CategoryTheory.Functor C D} (τ : F ⟶ G) : F.mapSquare ⟶ G.mapSquare
CategoryTheory.Square.Hom.comm₁₂_assoc 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] {sq₁ sq₂ : CategoryTheory.Square C} (self : sq₁.Hom sq₂) {Z : C} (h : sq₂.X₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp sq₁.f₁₂ (CategoryTheory.CategoryStruct.comp self.τ₂ h) = CategoryTheory.CategoryStruct.comp self.τ₁ (CategoryTheory.CategoryStruct.comp sq₂.f₁₂ h)
CategoryTheory.Square.Hom.comm₁₃_assoc 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] {sq₁ sq₂ : CategoryTheory.Square C} (self : sq₁.Hom sq₂) {Z : C} (h : sq₂.X₃ ⟶ Z) : CategoryTheory.CategoryStruct.comp sq₁.f₁₃ (CategoryTheory.CategoryStruct.comp self.τ₃ h) = CategoryTheory.CategoryStruct.comp self.τ₁ (CategoryTheory.CategoryStruct.comp sq₂.f₁₃ h)
CategoryTheory.Square.Hom.comm₂₄_assoc 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] {sq₁ sq₂ : CategoryTheory.Square C} (self : sq₁.Hom sq₂) {Z : C} (h : sq₂.X₄ ⟶ Z) : CategoryTheory.CategoryStruct.comp sq₁.f₂₄ (CategoryTheory.CategoryStruct.comp self.τ₄ h) = CategoryTheory.CategoryStruct.comp self.τ₂ (CategoryTheory.CategoryStruct.comp sq₂.f₂₄ h)
CategoryTheory.Square.Hom.comm₃₄_assoc 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] {sq₁ sq₂ : CategoryTheory.Square C} (self : sq₁.Hom sq₂) {Z : C} (h : sq₂.X₄ ⟶ Z) : CategoryTheory.CategoryStruct.comp sq₁.f₃₄ (CategoryTheory.CategoryStruct.comp self.τ₄ h) = CategoryTheory.CategoryStruct.comp self.τ₃ (CategoryTheory.CategoryStruct.comp sq₂.f₃₄ h)
CategoryTheory.Functor.mapSquare_map_τ₁ 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (F : CategoryTheory.Functor C D) {X✝ Y✝ : CategoryTheory.Square C} (φ : X✝ ⟶ Y✝) : (F.mapSquare.map φ).τ₁ = F.map φ.τ₁
CategoryTheory.Functor.mapSquare_map_τ₂ 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (F : CategoryTheory.Functor C D) {X✝ Y✝ : CategoryTheory.Square C} (φ : X✝ ⟶ Y✝) : (F.mapSquare.map φ).τ₂ = F.map φ.τ₂
CategoryTheory.Functor.mapSquare_map_τ₃ 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (F : CategoryTheory.Functor C D) {X✝ Y✝ : CategoryTheory.Square C} (φ : X✝ ⟶ Y✝) : (F.mapSquare.map φ).τ₃ = F.map φ.τ₃
CategoryTheory.Functor.mapSquare_map_τ₄ 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (F : CategoryTheory.Functor C D) {X✝ Y✝ : CategoryTheory.Square C} (φ : X✝ ⟶ Y✝) : (F.mapSquare.map φ).τ₄ = F.map φ.τ₄
CategoryTheory.Square.toArrowArrowFunctor'_obj_hom_left 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C) : (CategoryTheory.Square.toArrowArrowFunctor'.obj sq).hom.left = sq.f₁₃
CategoryTheory.Square.toArrowArrowFunctor'_obj_hom_right 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C) : (CategoryTheory.Square.toArrowArrowFunctor'.obj sq).hom.right = sq.f₂₄
CategoryTheory.Square.toArrowArrowFunctor_obj_hom_left 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C) : (CategoryTheory.Square.toArrowArrowFunctor.obj sq).hom.left = sq.f₁₂
CategoryTheory.Square.toArrowArrowFunctor_obj_hom_right 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C) : (CategoryTheory.Square.toArrowArrowFunctor.obj sq).hom.right = sq.f₃₄
CategoryTheory.Square.Hom.ext 📋 Mathlib.CategoryTheory.Square
{C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {sq₁ sq₂ : CategoryTheory.Square C} {x y : sq₁.Hom sq₂} (τ₁ : x.τ₁ = y.τ₁) (τ₂ : x.τ₂ = y.τ₂) (τ₃ : x.τ₃ = y.τ₃) (τ₄ : x.τ₄ = y.τ₄) : x = y
CategoryTheory.Square.Hom.ext_iff 📋 Mathlib.CategoryTheory.Square
{C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} {sq₁ sq₂ : CategoryTheory.Square C} {x y : sq₁.Hom sq₂} : x = y ↔ x.τ₁ = y.τ₁ ∧ x.τ₂ = y.τ₂ ∧ x.τ₃ = y.τ₃ ∧ x.τ₄ = y.τ₄
CategoryTheory.Square.flipEquivalence_counitIso 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] : CategoryTheory.Square.flipEquivalence.counitIso = CategoryTheory.Iso.refl (CategoryTheory.Square.flipFunctor.comp CategoryTheory.Square.flipFunctor)
CategoryTheory.NatTrans.mapSquare_app_τ₁ 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {F G : CategoryTheory.Functor C D} (τ : F ⟶ G) (sq : CategoryTheory.Square C) : ((CategoryTheory.NatTrans.mapSquare τ).app sq).τ₁ = τ.app sq.X₁
CategoryTheory.NatTrans.mapSquare_app_τ₂ 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {F G : CategoryTheory.Functor C D} (τ : F ⟶ G) (sq : CategoryTheory.Square C) : ((CategoryTheory.NatTrans.mapSquare τ).app sq).τ₂ = τ.app sq.X₂
CategoryTheory.NatTrans.mapSquare_app_τ₃ 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {F G : CategoryTheory.Functor C D} (τ : F ⟶ G) (sq : CategoryTheory.Square C) : ((CategoryTheory.NatTrans.mapSquare τ).app sq).τ₃ = τ.app sq.X₃
CategoryTheory.NatTrans.mapSquare_app_τ₄ 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {F G : CategoryTheory.Functor C D} (τ : F ⟶ G) (sq : CategoryTheory.Square C) : ((CategoryTheory.NatTrans.mapSquare τ).app sq).τ₄ = τ.app sq.X₄
CategoryTheory.Square.mapFunctor_map 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {X✝ Y✝ : CategoryTheory.Functor C D} (τ : X✝ ⟶ Y✝) : CategoryTheory.Square.mapFunctor.map τ = CategoryTheory.NatTrans.mapSquare τ
CategoryTheory.Square.opFunctor_map_τ₁ 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] {X✝ Y✝ : (CategoryTheory.Square C)ᵒᵖ} (φ : X✝ ⟶ Y✝) : (CategoryTheory.Square.opFunctor.map φ).τ₁ = φ.unop.τ₄.op
CategoryTheory.Square.opFunctor_map_τ₂ 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] {X✝ Y✝ : (CategoryTheory.Square C)ᵒᵖ} (φ : X✝ ⟶ Y✝) : (CategoryTheory.Square.opFunctor.map φ).τ₂ = φ.unop.τ₂.op
CategoryTheory.Square.opFunctor_map_τ₃ 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] {X✝ Y✝ : (CategoryTheory.Square C)ᵒᵖ} (φ : X✝ ⟶ Y✝) : (CategoryTheory.Square.opFunctor.map φ).τ₃ = φ.unop.τ₃.op
CategoryTheory.Square.opFunctor_map_τ₄ 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] {X✝ Y✝ : (CategoryTheory.Square C)ᵒᵖ} (φ : X✝ ⟶ Y✝) : (CategoryTheory.Square.opFunctor.map φ).τ₄ = φ.unop.τ₁.op
CategoryTheory.Square.hom_ext 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] {sq₁ sq₂ : CategoryTheory.Square C} {f g : sq₁ ⟶ sq₂} (h₁ : f.τ₁ = g.τ₁) (h₂ : f.τ₂ = g.τ₂) (h₃ : f.τ₃ = g.τ₃) (h₄ : f.τ₄ = g.τ₄) : f = g
CategoryTheory.Square.hom_ext_iff 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] {sq₁ sq₂ : CategoryTheory.Square C} {f g : sq₁ ⟶ sq₂} : f = g ↔ f.τ₁ = g.τ₁ ∧ f.τ₂ = g.τ₂ ∧ f.τ₃ = g.τ₃ ∧ f.τ₄ = g.τ₄
CategoryTheory.Square.arrowArrowEquivalence'_counitIso 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] : CategoryTheory.Square.arrowArrowEquivalence'.counitIso = CategoryTheory.Iso.refl (CategoryTheory.Square.fromArrowArrowFunctor'.comp CategoryTheory.Square.toArrowArrowFunctor')
CategoryTheory.Square.arrowArrowEquivalence_counitIso 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] : CategoryTheory.Square.arrowArrowEquivalence.counitIso = CategoryTheory.Iso.refl (CategoryTheory.Square.fromArrowArrowFunctor.comp CategoryTheory.Square.toArrowArrowFunctor)
CategoryTheory.Square.Hom.mk 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] {sq₁ sq₂ : CategoryTheory.Square C} (τ₁ : sq₁.X₁ ⟶ sq₂.X₁) (τ₂ : sq₁.X₂ ⟶ sq₂.X₂) (τ₃ : sq₁.X₃ ⟶ sq₂.X₃) (τ₄ : sq₁.X₄ ⟶ sq₂.X₄) (comm₁₂ : CategoryTheory.CategoryStruct.comp sq₁.f₁₂ τ₂ = CategoryTheory.CategoryStruct.comp τ₁ sq₂.f₁₂ := by cat_disch) (comm₁₃ : CategoryTheory.CategoryStruct.comp sq₁.f₁₃ τ₃ = CategoryTheory.CategoryStruct.comp τ₁ sq₂.f₁₃ := by cat_disch) (comm₂₄ : CategoryTheory.CategoryStruct.comp sq₁.f₂₄ τ₄ = CategoryTheory.CategoryStruct.comp τ₂ sq₂.f₂₄ := by cat_disch) (comm₃₄ : CategoryTheory.CategoryStruct.comp sq₁.f₃₄ τ₄ = CategoryTheory.CategoryStruct.comp τ₃ sq₂.f₃₄ := by cat_disch) : sq₁.Hom sq₂
CategoryTheory.Square.isoMk 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] {sq₁ sq₂ : CategoryTheory.Square C} (e₁ : sq₁.X₁ ≅ sq₂.X₁) (e₂ : sq₁.X₂ ≅ sq₂.X₂) (e₃ : sq₁.X₃ ≅ sq₂.X₃) (e₄ : sq₁.X₄ ≅ sq₂.X₄) (comm₁₂ : CategoryTheory.CategoryStruct.comp sq₁.f₁₂ e₂.hom = CategoryTheory.CategoryStruct.comp e₁.hom sq₂.f₁₂) (comm₁₃ : CategoryTheory.CategoryStruct.comp sq₁.f₁₃ e₃.hom = CategoryTheory.CategoryStruct.comp e₁.hom sq₂.f₁₃) (comm₂₄ : CategoryTheory.CategoryStruct.comp sq₁.f₂₄ e₄.hom = CategoryTheory.CategoryStruct.comp e₂.hom sq₂.f₂₄) (comm₃₄ : CategoryTheory.CategoryStruct.comp sq₁.f₃₄ e₄.hom = CategoryTheory.CategoryStruct.comp e₃.hom sq₂.f₃₄) : sq₁ ≅ sq₂
CategoryTheory.Square.fromArrowArrowFunctor'_map_τ₁ 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] {X✝ Y✝ : CategoryTheory.Arrow (CategoryTheory.Arrow C)} (φ : X✝ ⟶ Y✝) : (CategoryTheory.Square.fromArrowArrowFunctor'.map φ).τ₁ = CategoryTheory.Arrow.Hom.left (CategoryTheory.Arrow.Hom.left φ)
CategoryTheory.Square.fromArrowArrowFunctor'_map_τ₂ 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] {X✝ Y✝ : CategoryTheory.Arrow (CategoryTheory.Arrow C)} (φ : X✝ ⟶ Y✝) : (CategoryTheory.Square.fromArrowArrowFunctor'.map φ).τ₂ = CategoryTheory.Arrow.Hom.right (CategoryTheory.Arrow.Hom.left φ)
CategoryTheory.Square.fromArrowArrowFunctor'_map_τ₃ 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] {X✝ Y✝ : CategoryTheory.Arrow (CategoryTheory.Arrow C)} (φ : X✝ ⟶ Y✝) : (CategoryTheory.Square.fromArrowArrowFunctor'.map φ).τ₃ = CategoryTheory.Arrow.Hom.left (CategoryTheory.Arrow.Hom.right φ)
CategoryTheory.Square.fromArrowArrowFunctor'_map_τ₄ 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] {X✝ Y✝ : CategoryTheory.Arrow (CategoryTheory.Arrow C)} (φ : X✝ ⟶ Y✝) : (CategoryTheory.Square.fromArrowArrowFunctor'.map φ).τ₄ = CategoryTheory.Arrow.Hom.right (CategoryTheory.Arrow.Hom.right φ)
CategoryTheory.Square.fromArrowArrowFunctor_map_τ₁ 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] {X✝ Y✝ : CategoryTheory.Arrow (CategoryTheory.Arrow C)} (φ : X✝ ⟶ Y✝) : (CategoryTheory.Square.fromArrowArrowFunctor.map φ).τ₁ = CategoryTheory.Arrow.Hom.left (CategoryTheory.Arrow.Hom.left φ)
CategoryTheory.Square.fromArrowArrowFunctor_map_τ₂ 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] {X✝ Y✝ : CategoryTheory.Arrow (CategoryTheory.Arrow C)} (φ : X✝ ⟶ Y✝) : (CategoryTheory.Square.fromArrowArrowFunctor.map φ).τ₂ = CategoryTheory.Arrow.Hom.left (CategoryTheory.Arrow.Hom.right φ)
CategoryTheory.Square.fromArrowArrowFunctor_map_τ₃ 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] {X✝ Y✝ : CategoryTheory.Arrow (CategoryTheory.Arrow C)} (φ : X✝ ⟶ Y✝) : (CategoryTheory.Square.fromArrowArrowFunctor.map φ).τ₃ = CategoryTheory.Arrow.Hom.right (CategoryTheory.Arrow.Hom.left φ)
CategoryTheory.Square.fromArrowArrowFunctor_map_τ₄ 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] {X✝ Y✝ : CategoryTheory.Arrow (CategoryTheory.Arrow C)} (φ : X✝ ⟶ Y✝) : (CategoryTheory.Square.fromArrowArrowFunctor.map φ).τ₄ = CategoryTheory.Arrow.Hom.right (CategoryTheory.Arrow.Hom.right φ)
CategoryTheory.Square.toArrowArrowFunctor'_map_left_left 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] {X✝ Y✝ : CategoryTheory.Square C} (φ : X✝ ⟶ Y✝) : (CategoryTheory.Square.toArrowArrowFunctor'.map φ).left.left = φ.τ₁
CategoryTheory.Square.toArrowArrowFunctor'_map_left_right 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] {X✝ Y✝ : CategoryTheory.Square C} (φ : X✝ ⟶ Y✝) : (CategoryTheory.Square.toArrowArrowFunctor'.map φ).left.right = φ.τ₂
CategoryTheory.Square.toArrowArrowFunctor'_map_right_left 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] {X✝ Y✝ : CategoryTheory.Square C} (φ : X✝ ⟶ Y✝) : (CategoryTheory.Square.toArrowArrowFunctor'.map φ).right.left = φ.τ₃
CategoryTheory.Square.toArrowArrowFunctor'_map_right_right 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] {X✝ Y✝ : CategoryTheory.Square C} (φ : X✝ ⟶ Y✝) : (CategoryTheory.Square.toArrowArrowFunctor'.map φ).right.right = φ.τ₄
CategoryTheory.Square.toArrowArrowFunctor_map_left_left 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] {X✝ Y✝ : CategoryTheory.Square C} (φ : X✝ ⟶ Y✝) : (CategoryTheory.Square.toArrowArrowFunctor.map φ).left.left = φ.τ₁
CategoryTheory.Square.toArrowArrowFunctor_map_left_right 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] {X✝ Y✝ : CategoryTheory.Square C} (φ : X✝ ⟶ Y✝) : (CategoryTheory.Square.toArrowArrowFunctor.map φ).left.right = φ.τ₃
CategoryTheory.Square.toArrowArrowFunctor_map_right_left 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] {X✝ Y✝ : CategoryTheory.Square C} (φ : X✝ ⟶ Y✝) : (CategoryTheory.Square.toArrowArrowFunctor.map φ).right.left = φ.τ₂
CategoryTheory.Square.toArrowArrowFunctor_map_right_right 📋 Mathlib.CategoryTheory.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] {X✝ Y✝ : CategoryTheory.Square C} (φ : X✝ ⟶ Y✝) : (CategoryTheory.Square.toArrowArrowFunctor.map φ).right.right = φ.τ₄
CategoryTheory.Square.IsPullback 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C) : Prop
CategoryTheory.Square.IsPushout 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C) : Prop
CategoryTheory.Square.IsPullback.flip 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] {sq : CategoryTheory.Square C} (h : sq.IsPullback) : sq.flip.IsPullback
CategoryTheory.Square.IsPushout.flip 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] {sq : CategoryTheory.Square C} (h : sq.IsPushout) : sq.flip.IsPushout
CategoryTheory.Square.IsPullback.op 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] {sq : CategoryTheory.Square C} (h : sq.IsPullback) : sq.op.IsPushout
CategoryTheory.Square.IsPushout.op 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] {sq : CategoryTheory.Square C} (h : sq.IsPushout) : sq.op.IsPullback
CategoryTheory.Square.IsPullback.unop 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square
{C : Type u} [CategoryTheory.Category.{v, u} C] {sq : CategoryTheory.Square Cᵒᵖ} (h : sq.IsPullback) : sq.unop.IsPushout

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using the Loogle command from the command palette. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

By constant:
🔍 Real.sin
finds all lemmas whose statement somehow mentions the sine function.
By lemma name substring:
🔍 "differ"
finds all lemmas that have "differ" somewhere in their lemma name.
By subexpression:
🔍 _ * (_ ^ _)
finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

The pattern can also be non-linear, as in
🔍 Real.sqrt ?a * Real.sqrt ?a

If the pattern has parameters, they are matched in any order. Both of these will find List.map:
🔍 (?a -> ?b) -> List ?a -> List ?b
🔍 List ?a -> (?a -> ?b) -> List ?b
By main conclusion:
🔍 |- tsum _ = _ * tsum _
finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
🔍 |- _ < _ → tsum _ < tsum _
will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.
You can filter for definitions vs theorems: Using ⊢ (_ : Type _) finds all definitions which provide data while ⊢ (_ : Prop) finds all theorems (and definitions of proofs).

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO. Please review the Lean FRO Terms of Use and Privacy Policy.

This is Loogle revision 9f11169 serving mathlib revision ce5dd8c