Square

📁 Source: Mathlib/CategoryTheory/Square.lean

Statistics

Metric	Count
Definitions mapSquare, mapSquare, Square, comp, id, τ₁, τ₂, τ₃, τ₄, X₁, X₂, X₃, X₄, arrowArrowEquivalence, arrowArrowEquivalence', category, evaluation₁, evaluation₂, evaluation₃, evaluation₄, flip, flipEquivalence, flipFunctor, fromArrowArrowFunctor, fromArrowArrowFunctor', f₁₂, f₁₃, f₂₄, f₃₄, isoMk, map, mapFunctor, op, opEquivalence, opFunctor, toArrowArrowFunctor, toArrowArrowFunctor', unop, unopFunctor	39
Theorems mapSquare_map_τ₁, mapSquare_map_τ₂, mapSquare_map_τ₃, mapSquare_map_τ₄, mapSquare_obj, mapSquare_app_τ₁, mapSquare_app_τ₂, mapSquare_app_τ₃, mapSquare_app_τ₄, comm₁₂, comm₁₂_assoc, comm₁₃, comm₁₃_assoc, comm₂₄, comm₂₄_assoc, comm₃₄, comm₃₄_assoc, comp_τ₁, comp_τ₂, comp_τ₃, comp_τ₄, ext, ext_iff, id_τ₁, id_τ₂, id_τ₃, id_τ₄, arrowArrowEquivalence'_counitIso, arrowArrowEquivalence'_functor, arrowArrowEquivalence'_inverse, arrowArrowEquivalence'_unitIso, arrowArrowEquivalence_counitIso, arrowArrowEquivalence_functor, arrowArrowEquivalence_inverse, arrowArrowEquivalence_unitIso, category_comp_τ₁, category_comp_τ₂, category_comp_τ₃, category_comp_τ₄, category_id_τ₁, category_id_τ₂, category_id_τ₃, category_id_τ₄, commSq, evaluation₁_map, evaluation₁_obj, evaluation₂_map, evaluation₂_obj, evaluation₃_map, evaluation₃_obj, evaluation₄_map, evaluation₄_obj, fac, flipEquivalence_counitIso, flipEquivalence_functor, flipEquivalence_inverse, flipEquivalence_unitIso, flipFunctor_map_τ₁, flipFunctor_map_τ₂, flipFunctor_map_τ₃, flipFunctor_map_τ₄, flipFunctor_obj, flip_X₁, flip_X₂, flip_X₃, flip_X₄, flip_f₁₂, flip_f₁₃, flip_f₂₄, flip_f₃₄, fromArrowArrowFunctor'_map_τ₁, fromArrowArrowFunctor'_map_τ₂, fromArrowArrowFunctor'_map_τ₃, fromArrowArrowFunctor'_map_τ₄, fromArrowArrowFunctor'_obj_X₁, fromArrowArrowFunctor'_obj_X₂, fromArrowArrowFunctor'_obj_X₃, fromArrowArrowFunctor'_obj_X₄, fromArrowArrowFunctor'_obj_f₁₂, fromArrowArrowFunctor'_obj_f₁₃, fromArrowArrowFunctor'_obj_f₂₄, fromArrowArrowFunctor'_obj_f₃₄, fromArrowArrowFunctor_map_τ₁, fromArrowArrowFunctor_map_τ₂, fromArrowArrowFunctor_map_τ₃, fromArrowArrowFunctor_map_τ₄, fromArrowArrowFunctor_obj_X₁, fromArrowArrowFunctor_obj_X₂, fromArrowArrowFunctor_obj_X₃, fromArrowArrowFunctor_obj_X₄, fromArrowArrowFunctor_obj_f₁₂, fromArrowArrowFunctor_obj_f₁₃, fromArrowArrowFunctor_obj_f₂₄, fromArrowArrowFunctor_obj_f₃₄, hom_ext, hom_ext_iff, mapFunctor_map, mapFunctor_obj, map_X₁, map_X₂, map_X₃, map_X₄, map_f₁₂, map_f₁₃, map_f₂₄, map_f₃₄, opFunctor_map_τ₁, opFunctor_map_τ₂, opFunctor_map_τ₃, opFunctor_map_τ₄, opFunctor_obj, op_X₁, op_X₂, op_X₃, op_X₄, op_f₁₂, op_f₁₃, op_f₂₄, op_f₃₄, toArrowArrowFunctor'_map_left_left, toArrowArrowFunctor'_map_left_right, toArrowArrowFunctor'_map_right_left, toArrowArrowFunctor'_map_right_right, toArrowArrowFunctor'_obj_hom_left, toArrowArrowFunctor'_obj_hom_right, toArrowArrowFunctor'_obj_left_hom, toArrowArrowFunctor'_obj_left_left, toArrowArrowFunctor'_obj_left_right, toArrowArrowFunctor'_obj_right_hom, toArrowArrowFunctor'_obj_right_left, toArrowArrowFunctor'_obj_right_right, toArrowArrowFunctor_map_left_left, toArrowArrowFunctor_map_left_right, toArrowArrowFunctor_map_right_left, toArrowArrowFunctor_map_right_right, toArrowArrowFunctor_obj_hom_left, toArrowArrowFunctor_obj_hom_right, toArrowArrowFunctor_obj_left_hom, toArrowArrowFunctor_obj_left_left, toArrowArrowFunctor_obj_left_right, toArrowArrowFunctor_obj_right_hom, toArrowArrowFunctor_obj_right_left, toArrowArrowFunctor_obj_right_right, unop_X₁, unop_X₂, unop_X₃, unop_X₄, unop_f₁₂, unop_f₁₃, unop_f₂₄, unop_f₃₄	151
Total	190

CategoryTheory

Definitions

Name	Category	Theorems
Square 📖	CompData	97 math math: Square.category_id_τ₃, Square.category_comp_τ₂, Square.mapFunctor_obj, Square.arrowArrowEquivalence_functor, Square.evaluation₁_obj, NatTrans.mapSquare_app_τ₁, Square.fromArrowArrowFunctor_map_τ₃, Square.mapFunctor_map, Square.toArrowArrowFunctor_obj_hom_right, NatTrans.mapSquare_app_τ₂, Square.toArrowArrowFunctor'_obj_left_hom, Square.fromArrowArrowFunctor_obj_f₃₄, Square.flipEquivalence_unitIso, Square.fromArrowArrowFunctor'_obj_X₂, Square.fromArrowArrowFunctor'_obj_X₃, Square.evaluation₄_map, Square.toArrowArrowFunctor_obj_left_left, Square.fromArrowArrowFunctor_obj_X₃, Square.flipFunctor_map_τ₃, Square.fromArrowArrowFunctor'_map_τ₃, Square.fromArrowArrowFunctor_obj_X₂, Functor.mapSquare_map_τ₁, Square.category_id_τ₄, Square.toArrowArrowFunctor'_obj_right_right, Square.toArrowArrowFunctor_map_right_right, Square.flipEquivalence_inverse, Square.evaluation₂_map, Square.toArrowArrowFunctor'_map_right_left, Square.toArrowArrowFunctor_obj_right_right, Square.fromArrowArrowFunctor_obj_f₁₃, Square.arrowArrowEquivalence_inverse, Square.category_id_τ₁, Square.fromArrowArrowFunctor_obj_X₁, Square.evaluation₁_map, Square.category_comp_τ₃, Square.toArrowArrowFunctor_obj_hom_left, Square.opFunctor_map_τ₁, Square.flipFunctor_map_τ₁, Square.opFunctor_obj, Square.category_comp_τ₁, Square.toArrowArrowFunctor'_map_left_right, Square.fromArrowArrowFunctor'_obj_f₁₃, Functor.mapSquare_map_τ₄, Square.opFunctor_map_τ₂, Square.flipFunctor_obj, Square.arrowArrowEquivalence'_inverse, Square.fromArrowArrowFunctor_obj_X₄, Square.fromArrowArrowFunctor'_obj_X₄, Functor.mapSquare_obj, Square.evaluation₄_obj, Square.evaluation₃_map, Square.fromArrowArrowFunctor_obj_f₁₂, Square.toArrowArrowFunctor_map_left_left, Square.fromArrowArrowFunctor'_obj_X₁, Square.toArrowArrowFunctor_obj_right_hom, Square.toArrowArrowFunctor_obj_right_left, Square.fromArrowArrowFunctor'_map_τ₄, Square.toArrowArrowFunctor_obj_left_right, Square.opFunctor_map_τ₃, Square.toArrowArrowFunctor'_map_left_left, Square.fromArrowArrowFunctor_obj_f₂₄, Functor.mapSquare_map_τ₂, Square.evaluation₂_obj, Square.fromArrowArrowFunctor'_map_τ₂, Square.fromArrowArrowFunctor_map_τ₁, Square.arrowArrowEquivalence'_unitIso, Square.arrowArrowEquivalence'_functor, NatTrans.mapSquare_app_τ₄, Square.fromArrowArrowFunctor'_map_τ₁, Square.toArrowArrowFunctor'_map_right_right, Functor.mapSquare_map_τ₃, Square.fromArrowArrowFunctor_map_τ₂, Square.toArrowArrowFunctor'_obj_hom_right, Square.toArrowArrowFunctor_map_left_right, Square.toArrowArrowFunctor_map_right_left, Square.toArrowArrowFunctor'_obj_left_left, Square.arrowArrowEquivalence'_counitIso, Square.category_id_τ₂, Square.toArrowArrowFunctor'_obj_hom_left, Square.arrowArrowEquivalence_unitIso, NatTrans.mapSquare_app_τ₃, Square.category_comp_τ₄, Square.opFunctor_map_τ₄, Square.flipFunctor_map_τ₂, Square.toArrowArrowFunctor'_obj_right_left, Square.fromArrowArrowFunctor'_obj_f₂₄, Square.flipFunctor_map_τ₄, Square.toArrowArrowFunctor'_obj_right_hom, Square.toArrowArrowFunctor'_obj_left_right, Square.toArrowArrowFunctor_obj_left_hom, Square.fromArrowArrowFunctor'_obj_f₁₂, Square.flipEquivalence_functor, Square.evaluation₃_obj, Square.arrowArrowEquivalence_counitIso, Square.fromArrowArrowFunctor'_obj_f₃₄, Square.flipEquivalence_counitIso, Square.fromArrowArrowFunctor_map_τ₄

CategoryTheory.Functor

Definitions

Name	Category	Theorems
mapSquare 📖	CompOp	10 math math: CategoryTheory.Square.mapFunctor_obj, CategoryTheory.NatTrans.mapSquare_app_τ₁, CategoryTheory.NatTrans.mapSquare_app_τ₂, mapSquare_map_τ₁, mapSquare_map_τ₄, mapSquare_obj, mapSquare_map_τ₂, CategoryTheory.NatTrans.mapSquare_app_τ₄, mapSquare_map_τ₃, CategoryTheory.NatTrans.mapSquare_app_τ₃

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mapSquare_map_τ₁ 📖	mathematical	—	CategoryTheory.Square.Hom.τ₁ CategoryTheory.Square.map map CategoryTheory.Square CategoryTheory.Square.category mapSquare CategoryTheory.Square.X₁	—	—
mapSquare_map_τ₂ 📖	mathematical	—	CategoryTheory.Square.Hom.τ₂ CategoryTheory.Square.map map CategoryTheory.Square CategoryTheory.Square.category mapSquare CategoryTheory.Square.X₂	—	—
mapSquare_map_τ₃ 📖	mathematical	—	CategoryTheory.Square.Hom.τ₃ CategoryTheory.Square.map map CategoryTheory.Square CategoryTheory.Square.category mapSquare CategoryTheory.Square.X₃	—	—
mapSquare_map_τ₄ 📖	mathematical	—	CategoryTheory.Square.Hom.τ₄ CategoryTheory.Square.map map CategoryTheory.Square CategoryTheory.Square.category mapSquare CategoryTheory.Square.X₄	—	—
mapSquare_obj 📖	mathematical	—	obj CategoryTheory.Square CategoryTheory.Square.category mapSquare CategoryTheory.Square.map	—	—

CategoryTheory.NatTrans

Definitions

Name	Category	Theorems
mapSquare 📖	CompOp	5 math math: mapSquare_app_τ₁, CategoryTheory.Square.mapFunctor_map, mapSquare_app_τ₂, mapSquare_app_τ₄, mapSquare_app_τ₃

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mapSquare_app_τ₁ 📖	mathematical	—	CategoryTheory.Square.Hom.τ₁ CategoryTheory.Functor.obj CategoryTheory.Square CategoryTheory.Square.category CategoryTheory.Functor.mapSquare app mapSquare CategoryTheory.Square.X₁	—	—
mapSquare_app_τ₂ 📖	mathematical	—	CategoryTheory.Square.Hom.τ₂ CategoryTheory.Functor.obj CategoryTheory.Square CategoryTheory.Square.category CategoryTheory.Functor.mapSquare app mapSquare CategoryTheory.Square.X₂	—	—
mapSquare_app_τ₃ 📖	mathematical	—	CategoryTheory.Square.Hom.τ₃ CategoryTheory.Functor.obj CategoryTheory.Square CategoryTheory.Square.category CategoryTheory.Functor.mapSquare app mapSquare CategoryTheory.Square.X₃	—	—
mapSquare_app_τ₄ 📖	mathematical	—	CategoryTheory.Square.Hom.τ₄ CategoryTheory.Functor.obj CategoryTheory.Square CategoryTheory.Square.category CategoryTheory.Functor.mapSquare app mapSquare CategoryTheory.Square.X₄	—	—

CategoryTheory.Square

Definitions

Name	Category	Theorems
X₁ 📖	CompOp	59 math math: unop_X₁, evaluation₁_obj, CategoryTheory.NatTrans.mapSquare_app_τ₁, toArrowArrowFunctor_obj_hom_right, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.shortComplex_X₁, Hom.comm₁₃_assoc, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.mono_f₁₃, toArrowArrowFunctor_obj_left_left, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.fromBiprod_δ_assoc, Hom.comm₁₃, op_f₂₄, CategoryTheory.Functor.mapSquare_map_τ₁, toArrowArrowFunctor_map_right_right, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.mk₀_f_comp_biprodAddEquiv_symm_biprodIsoProd_hom, toArrowArrowFunctor'_map_right_left, map_f₁₃, category_id_τ₁, fromArrowArrowFunctor_obj_X₁, map_X₁, Opens.coe_mayerVietorisSquare_X₁, fac, op_X₁, toArrowArrowFunctor_obj_hom_left, IsPullback.mono_f₁₂, category_comp_τ₁, toArrowArrowFunctor'_map_left_right, Hom.comp_τ₁, flip_X₁, commSq, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.δ_toBiprod_assoc, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.δ_toBiprod, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.sheafCondition_iff_bijective_toPullbackObj, unop_f₂₄, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.fromBiprod_biprodIsoProd_inv_apply, Hom.comm₁₂_assoc, toArrowArrowFunctor_map_left_left, fromArrowArrowFunctor'_obj_X₁, isPushout_iff, map_f₁₂, toArrowArrowFunctor'_map_left_left, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.toBiprod_fromBiprod_assoc, op_X₄, Hom.comm₁₂, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.shortComplex_f, IsPullback.mono_f₁₃, toArrowArrowFunctor'_map_right_right, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.SheafCondition.bijective_toPullbackObj, toArrowArrowFunctor'_obj_hom_right, toArrowArrowFunctor_map_left_right, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.toBiprod_fromBiprod, toArrowArrowFunctor_map_right_left, toArrowArrowFunctor'_obj_left_left, unop_X₄, toArrowArrowFunctor'_obj_hom_left, Hom.id_τ₁, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.fromBiprod_δ, opFunctor_map_τ₄, op_f₃₄, unop_f₃₄
X₂ 📖	CompOp	61 math math: category_comp_τ₂, unop_X₂, Hom.comm₂₄, toArrowArrowFunctor_obj_hom_right, CategoryTheory.NatTrans.mapSquare_app_τ₂, op_f₁₂, Hom.id_τ₂, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.biprodAddEquiv_symm_biprodIsoProd_hom_toBiprod_apply, fromArrowArrowFunctor'_obj_X₂, Hom.comp_τ₂, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.fromBiprod_δ_assoc, unop_f₁₂, op_f₂₄, fromArrowArrowFunctor_obj_X₂, toArrowArrowFunctor_map_right_right, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.mk₀_f_comp_biprodAddEquiv_symm_biprodIsoProd_hom, Hom.comm₂₄_assoc, toArrowArrowFunctor'_map_right_left, Opens.mayerVietorisSquare_X₂, isPullback_iff, flip_X₃, fac, toArrowArrowFunctor_obj_hom_left, IsPullback.mono_f₁₂, toArrowArrowFunctor'_map_left_right, opFunctor_map_τ₂, commSq, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.δ_toBiprod_assoc, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.δ_toBiprod, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.sheafCondition_iff_bijective_toPullbackObj, op_X₂, unop_f₂₄, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.fromBiprod_biprodIsoProd_inv_apply, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.shortComplex_g, Hom.comm₁₂_assoc, toArrowArrowFunctor_map_left_left, IsPushout.epi_f₂₄, isPushout_iff, toArrowArrowFunctor_obj_right_left, map_f₁₂, toArrowArrowFunctor'_map_left_left, flip_X₂, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.toBiprod_fromBiprod_assoc, CategoryTheory.Functor.mapSquare_map_τ₂, evaluation₂_obj, Hom.comm₁₂, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.shortComplex_f, map_X₂, toArrowArrowFunctor'_map_right_right, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.SheafCondition.bijective_toPullbackObj, toArrowArrowFunctor'_obj_hom_right, toArrowArrowFunctor_map_left_right, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.toBiprod_fromBiprod, toArrowArrowFunctor_map_right_left, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.shortComplex_X₂, category_id_τ₂, toArrowArrowFunctor'_obj_hom_left, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.fromBiprod_δ, toArrowArrowFunctor'_obj_left_right, map_f₂₄, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.toBiprod_apply
X₃ 📖	CompOp	62 math math: category_id_τ₃, Opens.mayerVietorisSquare_X₃, toArrowArrowFunctor_obj_hom_right, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.biprodAddEquiv_symm_biprodIsoProd_hom_toBiprod_apply, Hom.comm₁₃_assoc, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.mono_f₁₃, fromArrowArrowFunctor'_obj_X₃, Hom.id_τ₃, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.fromBiprod_δ_assoc, Hom.comm₁₃, fromArrowArrowFunctor_obj_X₃, op_X₃, toArrowArrowFunctor_map_right_right, Hom.comm₃₄, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.mk₀_f_comp_biprodAddEquiv_symm_biprodIsoProd_hom, unop_X₃, toArrowArrowFunctor'_map_right_left, map_f₁₃, map_f₃₄, isPullback_iff, flip_X₃, fac, category_comp_τ₃, toArrowArrowFunctor_obj_hom_left, unop_f₁₃, toArrowArrowFunctor'_map_left_right, commSq, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.δ_toBiprod_assoc, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.δ_toBiprod, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.sheafCondition_iff_bijective_toPullbackObj, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.fromBiprod_biprodIsoProd_inv_apply, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.shortComplex_g, toArrowArrowFunctor_map_left_left, isPushout_iff, toArrowArrowFunctor_obj_left_right, opFunctor_map_τ₃, Hom.comm₃₄_assoc, toArrowArrowFunctor'_map_left_left, flip_X₂, op_f₁₃, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.toBiprod_fromBiprod_assoc, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.shortComplex_f, IsPushout.epi_f₃₄, map_X₃, IsPullback.mono_f₁₃, toArrowArrowFunctor'_map_right_right, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.SheafCondition.bijective_toPullbackObj, CategoryTheory.Functor.mapSquare_map_τ₃, toArrowArrowFunctor'_obj_hom_right, toArrowArrowFunctor_map_left_right, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.toBiprod_fromBiprod, toArrowArrowFunctor_map_right_left, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.shortComplex_X₂, toArrowArrowFunctor'_obj_hom_left, CategoryTheory.NatTrans.mapSquare_app_τ₃, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.fromBiprod_δ, toArrowArrowFunctor'_obj_right_left, op_f₃₄, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.toBiprod_apply, evaluation₃_obj, unop_f₃₄, Hom.comp_τ₃
X₄ 📖	CompOp	60 math math: CategoryTheory.GrothendieckTopology.MayerVietorisSquare.shortComplex_X₃, map_X₄, unop_X₁, flip_X₄, Hom.comm₂₄, toArrowArrowFunctor_obj_hom_right, op_f₁₂, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.SheafCondition.map_f₂₄_op_glue, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.biprodAddEquiv_symm_biprodIsoProd_hom_toBiprod_apply, Hom.id_τ₄, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.fromBiprod_δ_assoc, unop_f₁₂, category_id_τ₄, toArrowArrowFunctor'_obj_right_right, toArrowArrowFunctor_map_right_right, Hom.comm₃₄, Hom.comm₂₄_assoc, toArrowArrowFunctor'_map_right_left, toArrowArrowFunctor_obj_right_right, map_f₃₄, isPullback_iff, fac, op_X₁, toArrowArrowFunctor_obj_hom_left, opFunctor_map_τ₁, unop_f₁₃, toArrowArrowFunctor'_map_left_right, CategoryTheory.Functor.mapSquare_map_τ₄, commSq, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.δ_toBiprod_assoc, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.δ_toBiprod, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.sheafCondition_iff_bijective_toPullbackObj, fromArrowArrowFunctor_obj_X₄, Hom.comp_τ₄, fromArrowArrowFunctor'_obj_X₄, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.shortComplex_g, evaluation₄_obj, toArrowArrowFunctor_map_left_left, IsPushout.epi_f₂₄, Hom.comm₃₄_assoc, toArrowArrowFunctor'_map_left_left, op_f₁₃, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.toBiprod_fromBiprod_assoc, op_X₄, IsPushout.epi_f₃₄, CategoryTheory.NatTrans.mapSquare_app_τ₄, Opens.coe_mayerVietorisSquare_X₄, toArrowArrowFunctor'_map_right_right, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.SheafCondition.bijective_toPullbackObj, toArrowArrowFunctor'_obj_hom_right, toArrowArrowFunctor_map_left_right, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.toBiprod_fromBiprod, toArrowArrowFunctor_map_right_left, unop_X₄, toArrowArrowFunctor'_obj_hom_left, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.fromBiprod_δ, category_comp_τ₄, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.SheafCondition.map_f₃₄_op_glue, map_f₂₄, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.toBiprod_apply
arrowArrowEquivalence 📖	CompOp	4 math math: arrowArrowEquivalence_functor, arrowArrowEquivalence_inverse, arrowArrowEquivalence_unitIso, arrowArrowEquivalence_counitIso
arrowArrowEquivalence' 📖	CompOp	4 math math: arrowArrowEquivalence'_inverse, arrowArrowEquivalence'_unitIso, arrowArrowEquivalence'_functor, arrowArrowEquivalence'_counitIso
category 📖	CompOp	97 math math: category_id_τ₃, category_comp_τ₂, mapFunctor_obj, arrowArrowEquivalence_functor, evaluation₁_obj, CategoryTheory.NatTrans.mapSquare_app_τ₁, fromArrowArrowFunctor_map_τ₃, mapFunctor_map, toArrowArrowFunctor_obj_hom_right, CategoryTheory.NatTrans.mapSquare_app_τ₂, toArrowArrowFunctor'_obj_left_hom, fromArrowArrowFunctor_obj_f₃₄, flipEquivalence_unitIso, fromArrowArrowFunctor'_obj_X₂, fromArrowArrowFunctor'_obj_X₃, evaluation₄_map, toArrowArrowFunctor_obj_left_left, fromArrowArrowFunctor_obj_X₃, flipFunctor_map_τ₃, fromArrowArrowFunctor'_map_τ₃, fromArrowArrowFunctor_obj_X₂, CategoryTheory.Functor.mapSquare_map_τ₁, category_id_τ₄, toArrowArrowFunctor'_obj_right_right, toArrowArrowFunctor_map_right_right, flipEquivalence_inverse, evaluation₂_map, toArrowArrowFunctor'_map_right_left, toArrowArrowFunctor_obj_right_right, fromArrowArrowFunctor_obj_f₁₃, arrowArrowEquivalence_inverse, category_id_τ₁, fromArrowArrowFunctor_obj_X₁, evaluation₁_map, category_comp_τ₃, toArrowArrowFunctor_obj_hom_left, opFunctor_map_τ₁, flipFunctor_map_τ₁, opFunctor_obj, category_comp_τ₁, toArrowArrowFunctor'_map_left_right, fromArrowArrowFunctor'_obj_f₁₃, CategoryTheory.Functor.mapSquare_map_τ₄, opFunctor_map_τ₂, flipFunctor_obj, arrowArrowEquivalence'_inverse, fromArrowArrowFunctor_obj_X₄, fromArrowArrowFunctor'_obj_X₄, CategoryTheory.Functor.mapSquare_obj, evaluation₄_obj, evaluation₃_map, fromArrowArrowFunctor_obj_f₁₂, toArrowArrowFunctor_map_left_left, fromArrowArrowFunctor'_obj_X₁, toArrowArrowFunctor_obj_right_hom, toArrowArrowFunctor_obj_right_left, fromArrowArrowFunctor'_map_τ₄, toArrowArrowFunctor_obj_left_right, opFunctor_map_τ₃, toArrowArrowFunctor'_map_left_left, fromArrowArrowFunctor_obj_f₂₄, CategoryTheory.Functor.mapSquare_map_τ₂, evaluation₂_obj, fromArrowArrowFunctor'_map_τ₂, fromArrowArrowFunctor_map_τ₁, arrowArrowEquivalence'_unitIso, arrowArrowEquivalence'_functor, CategoryTheory.NatTrans.mapSquare_app_τ₄, fromArrowArrowFunctor'_map_τ₁, toArrowArrowFunctor'_map_right_right, CategoryTheory.Functor.mapSquare_map_τ₃, fromArrowArrowFunctor_map_τ₂, toArrowArrowFunctor'_obj_hom_right, toArrowArrowFunctor_map_left_right, toArrowArrowFunctor_map_right_left, toArrowArrowFunctor'_obj_left_left, arrowArrowEquivalence'_counitIso, category_id_τ₂, toArrowArrowFunctor'_obj_hom_left, arrowArrowEquivalence_unitIso, CategoryTheory.NatTrans.mapSquare_app_τ₃, category_comp_τ₄, opFunctor_map_τ₄, flipFunctor_map_τ₂, toArrowArrowFunctor'_obj_right_left, fromArrowArrowFunctor'_obj_f₂₄, flipFunctor_map_τ₄, toArrowArrowFunctor'_obj_right_hom, toArrowArrowFunctor'_obj_left_right, toArrowArrowFunctor_obj_left_hom, fromArrowArrowFunctor'_obj_f₁₂, flipEquivalence_functor, evaluation₃_obj, arrowArrowEquivalence_counitIso, fromArrowArrowFunctor'_obj_f₃₄, flipEquivalence_counitIso, fromArrowArrowFunctor_map_τ₄
evaluation₁ 📖	CompOp	2 math math: evaluation₁_obj, evaluation₁_map
evaluation₂ 📖	CompOp	2 math math: evaluation₂_map, evaluation₂_obj
evaluation₃ 📖	CompOp	2 math math: evaluation₃_map, evaluation₃_obj
evaluation₄ 📖	CompOp	2 math math: evaluation₄_map, evaluation₄_obj
flip 📖	CompOp	15 math math: flip_X₄, flip_f₃₄, IsPullback.flip, flipFunctor_map_τ₃, flip_X₃, flipFunctor_map_τ₁, flip_X₁, flipFunctor_obj, flip_X₂, flip_f₁₂, flip_f₂₄, IsPushout.flip, flip_f₁₃, flipFunctor_map_τ₂, flipFunctor_map_τ₄
flipEquivalence 📖	CompOp	4 math math: flipEquivalence_unitIso, flipEquivalence_inverse, flipEquivalence_functor, flipEquivalence_counitIso
flipFunctor 📖	CompOp	8 math math: flipFunctor_map_τ₃, flipEquivalence_inverse, flipFunctor_map_τ₁, flipFunctor_obj, flipFunctor_map_τ₂, flipFunctor_map_τ₄, flipEquivalence_functor, flipEquivalence_counitIso
fromArrowArrowFunctor 📖	CompOp	14 math math: fromArrowArrowFunctor_map_τ₃, fromArrowArrowFunctor_obj_f₃₄, fromArrowArrowFunctor_obj_X₃, fromArrowArrowFunctor_obj_X₂, fromArrowArrowFunctor_obj_f₁₃, arrowArrowEquivalence_inverse, fromArrowArrowFunctor_obj_X₁, fromArrowArrowFunctor_obj_X₄, fromArrowArrowFunctor_obj_f₁₂, fromArrowArrowFunctor_obj_f₂₄, fromArrowArrowFunctor_map_τ₁, fromArrowArrowFunctor_map_τ₂, arrowArrowEquivalence_counitIso, fromArrowArrowFunctor_map_τ₄
fromArrowArrowFunctor' 📖	CompOp	14 math math: fromArrowArrowFunctor'_obj_X₂, fromArrowArrowFunctor'_obj_X₃, fromArrowArrowFunctor'_map_τ₃, fromArrowArrowFunctor'_obj_f₁₃, arrowArrowEquivalence'_inverse, fromArrowArrowFunctor'_obj_X₄, fromArrowArrowFunctor'_obj_X₁, fromArrowArrowFunctor'_map_τ₄, fromArrowArrowFunctor'_map_τ₂, fromArrowArrowFunctor'_map_τ₁, arrowArrowEquivalence'_counitIso, fromArrowArrowFunctor'_obj_f₂₄, fromArrowArrowFunctor'_obj_f₁₂, fromArrowArrowFunctor'_obj_f₃₄
f₁₂ 📖	CompOp	31 math math: op_f₁₂, toArrowArrowFunctor'_obj_left_hom, unop_f₁₂, op_f₂₄, toArrowArrowFunctor_map_right_right, toArrowArrowFunctor'_map_right_left, fac, toArrowArrowFunctor_obj_hom_left, IsPullback.mono_f₁₂, toArrowArrowFunctor'_map_left_right, commSq, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.sheafCondition_iff_bijective_toPullbackObj, unop_f₂₄, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.fromBiprod_biprodIsoProd_inv_apply, Hom.comm₁₂_assoc, fromArrowArrowFunctor_obj_f₁₂, toArrowArrowFunctor_map_left_left, isPushout_iff, map_f₁₂, toArrowArrowFunctor'_map_left_left, flip_f₁₂, Hom.comm₁₂, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.shortComplex_f, toArrowArrowFunctor'_map_right_right, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.SheafCondition.bijective_toPullbackObj, toArrowArrowFunctor'_obj_hom_right, toArrowArrowFunctor_map_left_right, toArrowArrowFunctor_map_right_left, flip_f₁₃, toArrowArrowFunctor'_obj_hom_left, fromArrowArrowFunctor'_obj_f₁₂
f₁₃ 📖	CompOp	32 math math: toArrowArrowFunctor_obj_hom_right, Hom.comm₁₃_assoc, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.mono_f₁₃, Hom.comm₁₃, toArrowArrowFunctor_map_right_right, toArrowArrowFunctor'_map_right_left, map_f₁₃, fromArrowArrowFunctor_obj_f₁₃, fac, toArrowArrowFunctor_obj_hom_left, unop_f₁₃, toArrowArrowFunctor'_map_left_right, fromArrowArrowFunctor'_obj_f₁₃, commSq, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.sheafCondition_iff_bijective_toPullbackObj, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.fromBiprod_biprodIsoProd_inv_apply, toArrowArrowFunctor_map_left_left, isPushout_iff, toArrowArrowFunctor'_map_left_left, op_f₁₃, flip_f₁₂, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.shortComplex_f, IsPullback.mono_f₁₃, toArrowArrowFunctor'_map_right_right, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.SheafCondition.bijective_toPullbackObj, toArrowArrowFunctor_map_left_right, toArrowArrowFunctor_map_right_left, flip_f₁₃, toArrowArrowFunctor'_obj_hom_left, op_f₃₄, toArrowArrowFunctor_obj_left_hom, unop_f₃₄
f₂₄ 📖	CompOp	30 math math: flip_f₃₄, Hom.comm₂₄, toArrowArrowFunctor_obj_hom_right, op_f₁₂, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.SheafCondition.map_f₂₄_op_glue, unop_f₁₂, op_f₂₄, toArrowArrowFunctor_map_right_right, Hom.comm₂₄_assoc, toArrowArrowFunctor'_map_right_left, isPullback_iff, fac, toArrowArrowFunctor_obj_hom_left, toArrowArrowFunctor'_map_left_right, commSq, unop_f₂₄, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.shortComplex_g, toArrowArrowFunctor_map_left_left, IsPushout.epi_f₂₄, toArrowArrowFunctor_obj_right_hom, toArrowArrowFunctor'_map_left_left, fromArrowArrowFunctor_obj_f₂₄, flip_f₂₄, toArrowArrowFunctor'_map_right_right, toArrowArrowFunctor'_obj_hom_right, toArrowArrowFunctor_map_left_right, toArrowArrowFunctor_map_right_left, fromArrowArrowFunctor'_obj_f₂₄, map_f₂₄, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.toBiprod_apply
f₃₄ 📖	CompOp	30 math math: flip_f₃₄, toArrowArrowFunctor_obj_hom_right, fromArrowArrowFunctor_obj_f₃₄, toArrowArrowFunctor_map_right_right, Hom.comm₃₄, toArrowArrowFunctor'_map_right_left, map_f₃₄, isPullback_iff, fac, unop_f₁₃, toArrowArrowFunctor'_map_left_right, commSq, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.shortComplex_g, toArrowArrowFunctor_map_left_left, Hom.comm₃₄_assoc, toArrowArrowFunctor'_map_left_left, op_f₁₃, IsPushout.epi_f₃₄, flip_f₂₄, toArrowArrowFunctor'_map_right_right, toArrowArrowFunctor'_obj_hom_right, toArrowArrowFunctor_map_left_right, toArrowArrowFunctor_map_right_left, toArrowArrowFunctor'_obj_hom_left, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.SheafCondition.map_f₃₄_op_glue, op_f₃₄, toArrowArrowFunctor'_obj_right_hom, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.toBiprod_apply, unop_f₃₄, fromArrowArrowFunctor'_obj_f₃₄
isoMk 📖	CompOp	—
map 📖	CompOp	23 math math: map_X₄, IsPullback.map_iff, CategoryTheory.Sheaf.isPullback_square_op_map_yoneda_presheafToSheaf_yoneda_iff, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.isPushout, CategoryTheory.Functor.mapSquare_map_τ₁, map_f₁₃, map_f₃₄, map_X₁, CategoryTheory.Functor.mapSquare_map_τ₄, IsPushout.map_iff, CategoryTheory.Functor.mapSquare_obj, IsPullback.map, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.isPushoutAddCommGrpFreeSheaf, map_f₁₂, CategoryTheory.Functor.mapSquare_map_τ₂, isPullback_iff_map_coyoneda_isPullback, CategoryTheory.GrothendieckTopology.MayerVietorisSquare.shortComplex_f, map_X₂, map_X₃, CategoryTheory.Functor.mapSquare_map_τ₃, IsPushout.map, map_f₂₄, isPushout_iff_op_map_yoneda_isPullback
mapFunctor 📖	CompOp	2 math math: mapFunctor_obj, mapFunctor_map
op 📖	CompOp	17 math math: op_f₁₂, CategoryTheory.Sheaf.isPullback_square_op_map_yoneda_presheafToSheaf_yoneda_iff, op_f₂₄, op_X₃, op_X₁, opFunctor_map_τ₁, opFunctor_obj, opFunctor_map_τ₂, op_X₂, IsPullback.op, opFunctor_map_τ₃, op_f₁₃, op_X₄, IsPushout.op, opFunctor_map_τ₄, op_f₃₄, isPushout_iff_op_map_yoneda_isPullback
opEquivalence 📖	CompOp	—
opFunctor 📖	CompOp	5 math math: opFunctor_map_τ₁, opFunctor_obj, opFunctor_map_τ₂, opFunctor_map_τ₃, opFunctor_map_τ₄
toArrowArrowFunctor 📖	CompOp	14 math math: arrowArrowEquivalence_functor, toArrowArrowFunctor_obj_hom_right, toArrowArrowFunctor_obj_left_left, toArrowArrowFunctor_map_right_right, toArrowArrowFunctor_obj_right_right, toArrowArrowFunctor_obj_hom_left, toArrowArrowFunctor_map_left_left, toArrowArrowFunctor_obj_right_hom, toArrowArrowFunctor_obj_right_left, toArrowArrowFunctor_obj_left_right, toArrowArrowFunctor_map_left_right, toArrowArrowFunctor_map_right_left, toArrowArrowFunctor_obj_left_hom, arrowArrowEquivalence_counitIso
toArrowArrowFunctor' 📖	CompOp	14 math math: toArrowArrowFunctor'_obj_left_hom, toArrowArrowFunctor'_obj_right_right, toArrowArrowFunctor'_map_right_left, toArrowArrowFunctor'_map_left_right, toArrowArrowFunctor'_map_left_left, arrowArrowEquivalence'_functor, toArrowArrowFunctor'_map_right_right, toArrowArrowFunctor'_obj_hom_right, toArrowArrowFunctor'_obj_left_left, arrowArrowEquivalence'_counitIso, toArrowArrowFunctor'_obj_hom_left, toArrowArrowFunctor'_obj_right_left, toArrowArrowFunctor'_obj_right_hom, toArrowArrowFunctor'_obj_left_right
unop 📖	CompOp	10 math math: unop_X₂, unop_X₁, unop_f₁₂, unop_X₃, unop_f₁₃, unop_f₂₄, IsPullback.unop, unop_X₄, IsPushout.unop, unop_f₃₄
unopFunctor 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
arrowArrowEquivalence'_counitIso 📖	mathematical	—	CategoryTheory.Equivalence.counitIso CategoryTheory.Square CategoryTheory.Arrow CategoryTheory.instCategoryArrow category arrowArrowEquivalence' CategoryTheory.Iso.refl CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp fromArrowArrowFunctor' toArrowArrowFunctor'	—	—
arrowArrowEquivalence'_functor 📖	mathematical	—	CategoryTheory.Equivalence.functor CategoryTheory.Square CategoryTheory.Arrow CategoryTheory.instCategoryArrow category arrowArrowEquivalence' toArrowArrowFunctor'	—	—
arrowArrowEquivalence'_inverse 📖	mathematical	—	CategoryTheory.Equivalence.inverse CategoryTheory.Square CategoryTheory.Arrow CategoryTheory.instCategoryArrow category arrowArrowEquivalence' fromArrowArrowFunctor'	—	—
arrowArrowEquivalence'_unitIso 📖	mathematical	—	CategoryTheory.Equivalence.unitIso CategoryTheory.Square CategoryTheory.Arrow CategoryTheory.instCategoryArrow category arrowArrowEquivalence' CategoryTheory.Iso.refl CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.id	—	—
arrowArrowEquivalence_counitIso 📖	mathematical	—	CategoryTheory.Equivalence.counitIso CategoryTheory.Square CategoryTheory.Arrow CategoryTheory.instCategoryArrow category arrowArrowEquivalence CategoryTheory.Iso.refl CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp fromArrowArrowFunctor toArrowArrowFunctor	—	—
arrowArrowEquivalence_functor 📖	mathematical	—	CategoryTheory.Equivalence.functor CategoryTheory.Square CategoryTheory.Arrow CategoryTheory.instCategoryArrow category arrowArrowEquivalence toArrowArrowFunctor	—	—
arrowArrowEquivalence_inverse 📖	mathematical	—	CategoryTheory.Equivalence.inverse CategoryTheory.Square CategoryTheory.Arrow CategoryTheory.instCategoryArrow category arrowArrowEquivalence fromArrowArrowFunctor	—	—
arrowArrowEquivalence_unitIso 📖	mathematical	—	CategoryTheory.Equivalence.unitIso CategoryTheory.Square CategoryTheory.Arrow CategoryTheory.instCategoryArrow category arrowArrowEquivalence CategoryTheory.Iso.refl CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.id	—	—
category_comp_τ₁ 📖	mathematical	—	Hom.τ₁ CategoryTheory.CategoryStruct.comp CategoryTheory.Square CategoryTheory.Category.toCategoryStruct category X₁	—	—
category_comp_τ₂ 📖	mathematical	—	Hom.τ₂ CategoryTheory.CategoryStruct.comp CategoryTheory.Square CategoryTheory.Category.toCategoryStruct category X₂	—	—
category_comp_τ₃ 📖	mathematical	—	Hom.τ₃ CategoryTheory.CategoryStruct.comp CategoryTheory.Square CategoryTheory.Category.toCategoryStruct category X₃	—	—
category_comp_τ₄ 📖	mathematical	—	Hom.τ₄ CategoryTheory.CategoryStruct.comp CategoryTheory.Square CategoryTheory.Category.toCategoryStruct category X₄	—	—
category_id_τ₁ 📖	mathematical	—	Hom.τ₁ CategoryTheory.CategoryStruct.id CategoryTheory.Square CategoryTheory.Category.toCategoryStruct category X₁	—	—
category_id_τ₂ 📖	mathematical	—	Hom.τ₂ CategoryTheory.CategoryStruct.id CategoryTheory.Square CategoryTheory.Category.toCategoryStruct category X₂	—	—
category_id_τ₃ 📖	mathematical	—	Hom.τ₃ CategoryTheory.CategoryStruct.id CategoryTheory.Square CategoryTheory.Category.toCategoryStruct category X₃	—	—
category_id_τ₄ 📖	mathematical	—	Hom.τ₄ CategoryTheory.CategoryStruct.id CategoryTheory.Square CategoryTheory.Category.toCategoryStruct category X₄	—	—
commSq 📖	mathematical	—	CategoryTheory.CommSq X₁ X₂ X₃ X₄ f₁₂ f₁₃ f₂₄ f₃₄	—	fac
evaluation₁_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Square category evaluation₁ Hom.τ₁	—	—
evaluation₁_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Square category evaluation₁ X₁	—	—
evaluation₂_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Square category evaluation₂ Hom.τ₂	—	—
evaluation₂_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Square category evaluation₂ X₂	—	—
evaluation₃_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Square category evaluation₃ Hom.τ₃	—	—
evaluation₃_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Square category evaluation₃ X₃	—	—
evaluation₄_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Square category evaluation₄ Hom.τ₄	—	—
evaluation₄_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Square category evaluation₄ X₄	—	—
fac 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X₁ X₂ X₄ f₁₂ f₂₄ X₃ f₁₃ f₃₄	—	—
flipEquivalence_counitIso 📖	mathematical	—	CategoryTheory.Equivalence.counitIso CategoryTheory.Square category flipEquivalence CategoryTheory.Iso.refl CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp flipFunctor	—	—
flipEquivalence_functor 📖	mathematical	—	CategoryTheory.Equivalence.functor CategoryTheory.Square category flipEquivalence flipFunctor	—	—
flipEquivalence_inverse 📖	mathematical	—	CategoryTheory.Equivalence.inverse CategoryTheory.Square category flipEquivalence flipFunctor	—	—
flipEquivalence_unitIso 📖	mathematical	—	CategoryTheory.Equivalence.unitIso CategoryTheory.Square category flipEquivalence CategoryTheory.Iso.refl CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.id	—	—
flipFunctor_map_τ₁ 📖	mathematical	—	Hom.τ₁ flip CategoryTheory.Functor.map CategoryTheory.Square category flipFunctor	—	—
flipFunctor_map_τ₂ 📖	mathematical	—	Hom.τ₂ flip CategoryTheory.Functor.map CategoryTheory.Square category flipFunctor Hom.τ₃	—	—
flipFunctor_map_τ₃ 📖	mathematical	—	Hom.τ₃ flip CategoryTheory.Functor.map CategoryTheory.Square category flipFunctor Hom.τ₂	—	—
flipFunctor_map_τ₄ 📖	mathematical	—	Hom.τ₄ flip CategoryTheory.Functor.map CategoryTheory.Square category flipFunctor	—	—
flipFunctor_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Square category flipFunctor flip	—	—
flip_X₁ 📖	mathematical	—	X₁ flip	—	—
flip_X₂ 📖	mathematical	—	X₂ flip X₃	—	—
flip_X₃ 📖	mathematical	—	X₃ flip X₂	—	—
flip_X₄ 📖	mathematical	—	X₄ flip	—	—
flip_f₁₂ 📖	mathematical	—	f₁₂ flip f₁₃	—	—
flip_f₁₃ 📖	mathematical	—	f₁₃ flip f₁₂	—	—
flip_f₂₄ 📖	mathematical	—	f₂₄ flip f₃₄	—	—
flip_f₃₄ 📖	mathematical	—	f₃₄ flip f₂₄	—	—
fromArrowArrowFunctor'_map_τ₁ 📖	mathematical	—	Hom.τ₁ CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Arrow CategoryTheory.instCategoryArrow CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.Functor.map CategoryTheory.CommaMorphism.left CategoryTheory.CommaMorphism.right CategoryTheory.Square category fromArrowArrowFunctor'	—	—
fromArrowArrowFunctor'_map_τ₂ 📖	mathematical	—	Hom.τ₂ CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Arrow CategoryTheory.instCategoryArrow CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.Functor.map CategoryTheory.CommaMorphism.left CategoryTheory.CommaMorphism.right CategoryTheory.Square category fromArrowArrowFunctor'	—	—
fromArrowArrowFunctor'_map_τ₃ 📖	mathematical	—	Hom.τ₃ CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Arrow CategoryTheory.instCategoryArrow CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.Functor.map CategoryTheory.CommaMorphism.left CategoryTheory.CommaMorphism.right CategoryTheory.Square category fromArrowArrowFunctor'	—	—
fromArrowArrowFunctor'_map_τ₄ 📖	mathematical	—	Hom.τ₄ CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Arrow CategoryTheory.instCategoryArrow CategoryTheory.Comma.right CategoryTheory.Comma.hom CategoryTheory.Functor.map CategoryTheory.CommaMorphism.left CategoryTheory.CommaMorphism.right CategoryTheory.Square category fromArrowArrowFunctor'	—	—
fromArrowArrowFunctor'_obj_X₁ 📖	mathematical	—	X₁ CategoryTheory.Functor.obj CategoryTheory.Arrow CategoryTheory.instCategoryArrow CategoryTheory.Square category fromArrowArrowFunctor' CategoryTheory.Comma.left CategoryTheory.Functor.id	—	—
fromArrowArrowFunctor'_obj_X₂ 📖	mathematical	—	X₂ CategoryTheory.Functor.obj CategoryTheory.Arrow CategoryTheory.instCategoryArrow CategoryTheory.Square category fromArrowArrowFunctor' CategoryTheory.Comma.right CategoryTheory.Functor.id CategoryTheory.Comma.left	—	—
fromArrowArrowFunctor'_obj_X₃ 📖	mathematical	—	X₃ CategoryTheory.Functor.obj CategoryTheory.Arrow CategoryTheory.instCategoryArrow CategoryTheory.Square category fromArrowArrowFunctor' CategoryTheory.Comma.left CategoryTheory.Functor.id CategoryTheory.Comma.right	—	—
fromArrowArrowFunctor'_obj_X₄ 📖	mathematical	—	X₄ CategoryTheory.Functor.obj CategoryTheory.Arrow CategoryTheory.instCategoryArrow CategoryTheory.Square category fromArrowArrowFunctor' CategoryTheory.Comma.right CategoryTheory.Functor.id	—	—
fromArrowArrowFunctor'_obj_f₁₂ 📖	mathematical	—	f₁₂ CategoryTheory.Functor.obj CategoryTheory.Arrow CategoryTheory.instCategoryArrow CategoryTheory.Square category fromArrowArrowFunctor' CategoryTheory.Comma.hom CategoryTheory.Functor.id CategoryTheory.Comma.left	—	—
fromArrowArrowFunctor'_obj_f₁₃ 📖	mathematical	—	f₁₃ CategoryTheory.Functor.obj CategoryTheory.Arrow CategoryTheory.instCategoryArrow CategoryTheory.Square category fromArrowArrowFunctor' CategoryTheory.CommaMorphism.left CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.Comma.hom	—	—
fromArrowArrowFunctor'_obj_f₂₄ 📖	mathematical	—	f₂₄ CategoryTheory.Functor.obj CategoryTheory.Arrow CategoryTheory.instCategoryArrow CategoryTheory.Square category fromArrowArrowFunctor' CategoryTheory.CommaMorphism.right CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.Comma.hom	—	—
fromArrowArrowFunctor'_obj_f₃₄ 📖	mathematical	—	f₃₄ CategoryTheory.Functor.obj CategoryTheory.Arrow CategoryTheory.instCategoryArrow CategoryTheory.Square category fromArrowArrowFunctor' CategoryTheory.Comma.hom CategoryTheory.Functor.id CategoryTheory.Comma.right	—	—
fromArrowArrowFunctor_map_τ₁ 📖	mathematical	—	Hom.τ₁ CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Arrow CategoryTheory.instCategoryArrow CategoryTheory.Comma.right CategoryTheory.Functor.map CategoryTheory.CommaMorphism.left CategoryTheory.Comma.hom CategoryTheory.CommaMorphism.right CategoryTheory.Square category fromArrowArrowFunctor	—	—
fromArrowArrowFunctor_map_τ₂ 📖	mathematical	—	Hom.τ₂ CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Arrow CategoryTheory.instCategoryArrow CategoryTheory.Comma.right CategoryTheory.Functor.map CategoryTheory.CommaMorphism.left CategoryTheory.Comma.hom CategoryTheory.CommaMorphism.right CategoryTheory.Square category fromArrowArrowFunctor	—	—
fromArrowArrowFunctor_map_τ₃ 📖	mathematical	—	Hom.τ₃ CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Arrow CategoryTheory.instCategoryArrow CategoryTheory.Comma.right CategoryTheory.Functor.map CategoryTheory.CommaMorphism.left CategoryTheory.Comma.hom CategoryTheory.CommaMorphism.right CategoryTheory.Square category fromArrowArrowFunctor	—	—
fromArrowArrowFunctor_map_τ₄ 📖	mathematical	—	Hom.τ₄ CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Arrow CategoryTheory.instCategoryArrow CategoryTheory.Comma.right CategoryTheory.Functor.map CategoryTheory.CommaMorphism.left CategoryTheory.Comma.hom CategoryTheory.CommaMorphism.right CategoryTheory.Square category fromArrowArrowFunctor	—	—
fromArrowArrowFunctor_obj_X₁ 📖	mathematical	—	X₁ CategoryTheory.Functor.obj CategoryTheory.Arrow CategoryTheory.instCategoryArrow CategoryTheory.Square category fromArrowArrowFunctor CategoryTheory.Comma.left CategoryTheory.Functor.id	—	—
fromArrowArrowFunctor_obj_X₂ 📖	mathematical	—	X₂ CategoryTheory.Functor.obj CategoryTheory.Arrow CategoryTheory.instCategoryArrow CategoryTheory.Square category fromArrowArrowFunctor CategoryTheory.Comma.left CategoryTheory.Functor.id CategoryTheory.Comma.right	—	—
fromArrowArrowFunctor_obj_X₃ 📖	mathematical	—	X₃ CategoryTheory.Functor.obj CategoryTheory.Arrow CategoryTheory.instCategoryArrow CategoryTheory.Square category fromArrowArrowFunctor CategoryTheory.Comma.right CategoryTheory.Functor.id CategoryTheory.Comma.left	—	—
fromArrowArrowFunctor_obj_X₄ 📖	mathematical	—	X₄ CategoryTheory.Functor.obj CategoryTheory.Arrow CategoryTheory.instCategoryArrow CategoryTheory.Square category fromArrowArrowFunctor CategoryTheory.Comma.right CategoryTheory.Functor.id	—	—
fromArrowArrowFunctor_obj_f₁₂ 📖	mathematical	—	f₁₂ CategoryTheory.Functor.obj CategoryTheory.Arrow CategoryTheory.instCategoryArrow CategoryTheory.Square category fromArrowArrowFunctor CategoryTheory.CommaMorphism.left CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.Comma.hom	—	—
fromArrowArrowFunctor_obj_f₁₃ 📖	mathematical	—	f₁₃ CategoryTheory.Functor.obj CategoryTheory.Arrow CategoryTheory.instCategoryArrow CategoryTheory.Square category fromArrowArrowFunctor CategoryTheory.Comma.hom CategoryTheory.Functor.id CategoryTheory.Comma.left	—	—
fromArrowArrowFunctor_obj_f₂₄ 📖	mathematical	—	f₂₄ CategoryTheory.Functor.obj CategoryTheory.Arrow CategoryTheory.instCategoryArrow CategoryTheory.Square category fromArrowArrowFunctor CategoryTheory.Comma.hom CategoryTheory.Functor.id CategoryTheory.Comma.right	—	—
fromArrowArrowFunctor_obj_f₃₄ 📖	mathematical	—	f₃₄ CategoryTheory.Functor.obj CategoryTheory.Arrow CategoryTheory.instCategoryArrow CategoryTheory.Square category fromArrowArrowFunctor CategoryTheory.CommaMorphism.right CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Comma.right CategoryTheory.Comma.hom	—	—
hom_ext 📖	—	Hom.τ₁ Hom.τ₂ Hom.τ₃ Hom.τ₄	—	—	Hom.ext
hom_ext_iff 📖	mathematical	—	Hom.τ₁ Hom.τ₂ Hom.τ₃ Hom.τ₄	—	hom_ext
mapFunctor_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Square category mapFunctor CategoryTheory.NatTrans.mapSquare	—	—
mapFunctor_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Square category mapFunctor CategoryTheory.Functor.mapSquare	—	—
map_X₁ 📖	mathematical	—	X₁ map CategoryTheory.Functor.obj	—	—
map_X₂ 📖	mathematical	—	X₂ map CategoryTheory.Functor.obj	—	—
map_X₃ 📖	mathematical	—	X₃ map CategoryTheory.Functor.obj	—	—
map_X₄ 📖	mathematical	—	X₄ map CategoryTheory.Functor.obj	—	—
map_f₁₂ 📖	mathematical	—	f₁₂ map CategoryTheory.Functor.map X₁ X₂	—	—
map_f₁₃ 📖	mathematical	—	f₁₃ map CategoryTheory.Functor.map X₁ X₃	—	—
map_f₂₄ 📖	mathematical	—	f₂₄ map CategoryTheory.Functor.map X₂ X₄	—	—
map_f₃₄ 📖	mathematical	—	f₃₄ map CategoryTheory.Functor.map X₃ X₄	—	—
opFunctor_map_τ₁ 📖	mathematical	—	Hom.τ₁ Opposite CategoryTheory.Category.opposite op Opposite.unop CategoryTheory.Square CategoryTheory.Functor.map category opFunctor Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct X₄ Hom.τ₄ Quiver.Hom.unop	—	—
opFunctor_map_τ₂ 📖	mathematical	—	Hom.τ₂ Opposite CategoryTheory.Category.opposite op Opposite.unop CategoryTheory.Square CategoryTheory.Functor.map category opFunctor Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct X₂ Quiver.Hom.unop	—	—
opFunctor_map_τ₃ 📖	mathematical	—	Hom.τ₃ Opposite CategoryTheory.Category.opposite op Opposite.unop CategoryTheory.Square CategoryTheory.Functor.map category opFunctor Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct X₃ Quiver.Hom.unop	—	—
opFunctor_map_τ₄ 📖	mathematical	—	Hom.τ₄ Opposite CategoryTheory.Category.opposite op Opposite.unop CategoryTheory.Square CategoryTheory.Functor.map category opFunctor Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct X₁ Hom.τ₁ Quiver.Hom.unop	—	—
opFunctor_obj 📖	mathematical	—	CategoryTheory.Functor.obj Opposite CategoryTheory.Square CategoryTheory.Category.opposite category opFunctor op Opposite.unop	—	—
op_X₁ 📖	mathematical	—	X₁ Opposite CategoryTheory.Category.opposite op Opposite.op X₄	—	—
op_X₂ 📖	mathematical	—	X₂ Opposite CategoryTheory.Category.opposite op Opposite.op	—	—
op_X₃ 📖	mathematical	—	X₃ Opposite CategoryTheory.Category.opposite op Opposite.op	—	—
op_X₄ 📖	mathematical	—	X₄ Opposite CategoryTheory.Category.opposite op Opposite.op X₁	—	—
op_f₁₂ 📖	mathematical	—	f₁₂ Opposite CategoryTheory.Category.opposite op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct X₂ X₄ f₂₄	—	—
op_f₁₃ 📖	mathematical	—	f₁₃ Opposite CategoryTheory.Category.opposite op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct X₃ X₄ f₃₄	—	—
op_f₂₄ 📖	mathematical	—	f₂₄ Opposite CategoryTheory.Category.opposite op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct X₁ X₂ f₁₂	—	—
op_f₃₄ 📖	mathematical	—	f₃₄ Opposite CategoryTheory.Category.opposite op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct X₁ X₃ f₁₃	—	—
toArrowArrowFunctor'_map_left_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Arrow CategoryTheory.instCategoryArrow X₁ X₂ f₁₂ X₃ X₄ f₃₄ CategoryTheory.Arrow.homMk f₁₃ f₂₄ CategoryTheory.Functor.map CategoryTheory.Square category toArrowArrowFunctor' Hom.τ₁	—	—
toArrowArrowFunctor'_map_left_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Arrow CategoryTheory.instCategoryArrow X₁ X₂ f₁₂ X₃ X₄ f₃₄ CategoryTheory.Arrow.homMk f₁₃ f₂₄ CategoryTheory.CommaMorphism.left CategoryTheory.Functor.map CategoryTheory.Square category toArrowArrowFunctor' Hom.τ₂	—	—
toArrowArrowFunctor'_map_right_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Functor.id CategoryTheory.Comma.right CategoryTheory.Arrow CategoryTheory.instCategoryArrow X₁ X₂ f₁₂ X₃ X₄ f₃₄ CategoryTheory.Arrow.homMk f₁₃ f₂₄ CategoryTheory.CommaMorphism.right CategoryTheory.Functor.map CategoryTheory.Square category toArrowArrowFunctor' Hom.τ₃	—	—
toArrowArrowFunctor'_map_right_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right CategoryTheory.Functor.id CategoryTheory.Comma.right CategoryTheory.Arrow CategoryTheory.instCategoryArrow X₁ X₂ f₁₂ X₃ X₄ f₃₄ CategoryTheory.Arrow.homMk f₁₃ f₂₄ CategoryTheory.Functor.map CategoryTheory.Square category toArrowArrowFunctor' Hom.τ₄	—	—
toArrowArrowFunctor'_obj_hom_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Functor.id X₁ X₂ f₁₂ X₃ X₄ f₃₄ CategoryTheory.Comma.hom CategoryTheory.Arrow CategoryTheory.instCategoryArrow CategoryTheory.Functor.obj CategoryTheory.Square category toArrowArrowFunctor' f₁₃	—	—
toArrowArrowFunctor'_obj_hom_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right CategoryTheory.Functor.id X₁ X₂ f₁₂ X₃ X₄ f₃₄ CategoryTheory.Comma.hom CategoryTheory.Arrow CategoryTheory.instCategoryArrow CategoryTheory.Functor.obj CategoryTheory.Square category toArrowArrowFunctor' f₂₄	—	—
toArrowArrowFunctor'_obj_left_hom 📖	mathematical	—	CategoryTheory.Comma.hom CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Arrow CategoryTheory.instCategoryArrow CategoryTheory.Functor.obj CategoryTheory.Square category toArrowArrowFunctor' f₁₂	—	—
toArrowArrowFunctor'_obj_left_left 📖	mathematical	—	CategoryTheory.Comma.left CategoryTheory.Functor.id CategoryTheory.Arrow CategoryTheory.instCategoryArrow CategoryTheory.Functor.obj CategoryTheory.Square category toArrowArrowFunctor' X₁	—	—
toArrowArrowFunctor'_obj_left_right 📖	mathematical	—	CategoryTheory.Comma.right CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Arrow CategoryTheory.instCategoryArrow CategoryTheory.Functor.obj CategoryTheory.Square category toArrowArrowFunctor' X₂	—	—
toArrowArrowFunctor'_obj_right_hom 📖	mathematical	—	CategoryTheory.Comma.hom CategoryTheory.Functor.id CategoryTheory.Comma.right CategoryTheory.Arrow CategoryTheory.instCategoryArrow CategoryTheory.Functor.obj CategoryTheory.Square category toArrowArrowFunctor' f₃₄	—	—
toArrowArrowFunctor'_obj_right_left 📖	mathematical	—	CategoryTheory.Comma.left CategoryTheory.Functor.id CategoryTheory.Comma.right CategoryTheory.Arrow CategoryTheory.instCategoryArrow CategoryTheory.Functor.obj CategoryTheory.Square category toArrowArrowFunctor' X₃	—	—
toArrowArrowFunctor'_obj_right_right 📖	mathematical	—	CategoryTheory.Comma.right CategoryTheory.Functor.id CategoryTheory.Arrow CategoryTheory.instCategoryArrow CategoryTheory.Functor.obj CategoryTheory.Square category toArrowArrowFunctor' X₄	—	—
toArrowArrowFunctor_map_left_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Arrow CategoryTheory.instCategoryArrow X₁ X₃ f₁₃ X₂ X₄ f₂₄ CategoryTheory.Arrow.homMk f₁₂ f₃₄ fac CategoryTheory.Functor.map CategoryTheory.Square category toArrowArrowFunctor Hom.τ₁	—	fac
toArrowArrowFunctor_map_left_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Arrow CategoryTheory.instCategoryArrow X₁ X₃ f₁₃ X₂ X₄ f₂₄ CategoryTheory.Arrow.homMk f₁₂ f₃₄ fac CategoryTheory.CommaMorphism.left CategoryTheory.Functor.map CategoryTheory.Square category toArrowArrowFunctor Hom.τ₃	—	fac
toArrowArrowFunctor_map_right_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Functor.id CategoryTheory.Comma.right CategoryTheory.Arrow CategoryTheory.instCategoryArrow X₁ X₃ f₁₃ X₂ X₄ f₂₄ CategoryTheory.Arrow.homMk f₁₂ f₃₄ fac CategoryTheory.CommaMorphism.right CategoryTheory.Functor.map CategoryTheory.Square category toArrowArrowFunctor Hom.τ₂	—	fac
toArrowArrowFunctor_map_right_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right CategoryTheory.Functor.id CategoryTheory.Comma.right CategoryTheory.Arrow CategoryTheory.instCategoryArrow X₁ X₃ f₁₃ X₂ X₄ f₂₄ CategoryTheory.Arrow.homMk f₁₂ f₃₄ fac CategoryTheory.Functor.map CategoryTheory.Square category toArrowArrowFunctor Hom.τ₄	—	fac
toArrowArrowFunctor_obj_hom_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Functor.id X₁ X₃ f₁₃ X₂ X₄ f₂₄ CategoryTheory.Comma.hom CategoryTheory.Arrow CategoryTheory.instCategoryArrow CategoryTheory.Functor.obj CategoryTheory.Square category toArrowArrowFunctor f₁₂	—	—
toArrowArrowFunctor_obj_hom_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right CategoryTheory.Functor.id X₁ X₃ f₁₃ X₂ X₄ f₂₄ CategoryTheory.Comma.hom CategoryTheory.Arrow CategoryTheory.instCategoryArrow CategoryTheory.Functor.obj CategoryTheory.Square category toArrowArrowFunctor f₃₄	—	—
toArrowArrowFunctor_obj_left_hom 📖	mathematical	—	CategoryTheory.Comma.hom CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Arrow CategoryTheory.instCategoryArrow CategoryTheory.Functor.obj CategoryTheory.Square category toArrowArrowFunctor f₁₃	—	—
toArrowArrowFunctor_obj_left_left 📖	mathematical	—	CategoryTheory.Comma.left CategoryTheory.Functor.id CategoryTheory.Arrow CategoryTheory.instCategoryArrow CategoryTheory.Functor.obj CategoryTheory.Square category toArrowArrowFunctor X₁	—	—
toArrowArrowFunctor_obj_left_right 📖	mathematical	—	CategoryTheory.Comma.right CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Arrow CategoryTheory.instCategoryArrow CategoryTheory.Functor.obj CategoryTheory.Square category toArrowArrowFunctor X₃	—	—
toArrowArrowFunctor_obj_right_hom 📖	mathematical	—	CategoryTheory.Comma.hom CategoryTheory.Functor.id CategoryTheory.Comma.right CategoryTheory.Arrow CategoryTheory.instCategoryArrow CategoryTheory.Functor.obj CategoryTheory.Square category toArrowArrowFunctor f₂₄	—	—
toArrowArrowFunctor_obj_right_left 📖	mathematical	—	CategoryTheory.Comma.left CategoryTheory.Functor.id CategoryTheory.Comma.right CategoryTheory.Arrow CategoryTheory.instCategoryArrow CategoryTheory.Functor.obj CategoryTheory.Square category toArrowArrowFunctor X₂	—	—
toArrowArrowFunctor_obj_right_right 📖	mathematical	—	CategoryTheory.Comma.right CategoryTheory.Functor.id CategoryTheory.Arrow CategoryTheory.instCategoryArrow CategoryTheory.Functor.obj CategoryTheory.Square category toArrowArrowFunctor X₄	—	—
unop_X₁ 📖	mathematical	—	X₁ unop Opposite.unop X₄ Opposite CategoryTheory.Category.opposite	—	—
unop_X₂ 📖	mathematical	—	X₂ unop Opposite.unop Opposite CategoryTheory.Category.opposite	—	—
unop_X₃ 📖	mathematical	—	X₃ unop Opposite.unop Opposite CategoryTheory.Category.opposite	—	—
unop_X₄ 📖	mathematical	—	X₄ unop Opposite.unop X₁ Opposite CategoryTheory.Category.opposite	—	—
unop_f₁₂ 📖	mathematical	—	f₁₂ unop Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct X₂ Opposite CategoryTheory.Category.opposite X₄ f₂₄	—	—
unop_f₁₃ 📖	mathematical	—	f₁₃ unop Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct X₃ Opposite CategoryTheory.Category.opposite X₄ f₃₄	—	—
unop_f₂₄ 📖	mathematical	—	f₂₄ unop Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct X₁ Opposite CategoryTheory.Category.opposite X₂ f₁₂	—	—
unop_f₃₄ 📖	mathematical	—	f₃₄ unop Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct X₁ Opposite CategoryTheory.Category.opposite X₃ f₁₃	—	—

CategoryTheory.Square.Hom

Definitions

Name	Category	Theorems
comp 📖	CompOp	4 math math: comp_τ₂, comp_τ₁, comp_τ₄, comp_τ₃
id 📖	CompOp	4 math math: id_τ₂, id_τ₄, id_τ₃, id_τ₁
τ₁ 📖	CompOp	20 math math: CategoryTheory.NatTrans.mapSquare_app_τ₁, comm₁₃_assoc, comm₁₃, CategoryTheory.Square.hom_ext_iff, CategoryTheory.Functor.mapSquare_map_τ₁, CategoryTheory.Square.category_id_τ₁, CategoryTheory.Square.evaluation₁_map, CategoryTheory.Square.opFunctor_map_τ₁, CategoryTheory.Square.flipFunctor_map_τ₁, CategoryTheory.Square.category_comp_τ₁, comp_τ₁, comm₁₂_assoc, CategoryTheory.Square.toArrowArrowFunctor_map_left_left, ext_iff, CategoryTheory.Square.toArrowArrowFunctor'_map_left_left, CategoryTheory.Square.fromArrowArrowFunctor_map_τ₁, comm₁₂, CategoryTheory.Square.fromArrowArrowFunctor'_map_τ₁, id_τ₁, CategoryTheory.Square.opFunctor_map_τ₄
τ₂ 📖	CompOp	20 math math: CategoryTheory.Square.category_comp_τ₂, comm₂₄, CategoryTheory.NatTrans.mapSquare_app_τ₂, id_τ₂, comp_τ₂, CategoryTheory.Square.hom_ext_iff, CategoryTheory.Square.flipFunctor_map_τ₃, comm₂₄_assoc, CategoryTheory.Square.evaluation₂_map, CategoryTheory.Square.toArrowArrowFunctor'_map_left_right, CategoryTheory.Square.opFunctor_map_τ₂, comm₁₂_assoc, ext_iff, CategoryTheory.Functor.mapSquare_map_τ₂, CategoryTheory.Square.fromArrowArrowFunctor'_map_τ₂, comm₁₂, CategoryTheory.Square.fromArrowArrowFunctor_map_τ₂, CategoryTheory.Square.toArrowArrowFunctor_map_right_left, CategoryTheory.Square.category_id_τ₂, CategoryTheory.Square.flipFunctor_map_τ₂
τ₃ 📖	CompOp	20 math math: CategoryTheory.Square.category_id_τ₃, CategoryTheory.Square.fromArrowArrowFunctor_map_τ₃, comm₁₃_assoc, id_τ₃, comm₁₃, CategoryTheory.Square.hom_ext_iff, CategoryTheory.Square.flipFunctor_map_τ₃, CategoryTheory.Square.fromArrowArrowFunctor'_map_τ₃, comm₃₄, CategoryTheory.Square.toArrowArrowFunctor'_map_right_left, CategoryTheory.Square.category_comp_τ₃, CategoryTheory.Square.evaluation₃_map, ext_iff, CategoryTheory.Square.opFunctor_map_τ₃, comm₃₄_assoc, CategoryTheory.Functor.mapSquare_map_τ₃, CategoryTheory.Square.toArrowArrowFunctor_map_left_right, CategoryTheory.NatTrans.mapSquare_app_τ₃, CategoryTheory.Square.flipFunctor_map_τ₂, comp_τ₃
τ₄ 📖	CompOp	20 math math: comm₂₄, id_τ₄, CategoryTheory.Square.evaluation₄_map, CategoryTheory.Square.hom_ext_iff, CategoryTheory.Square.category_id_τ₄, CategoryTheory.Square.toArrowArrowFunctor_map_right_right, comm₃₄, comm₂₄_assoc, CategoryTheory.Square.opFunctor_map_τ₁, CategoryTheory.Functor.mapSquare_map_τ₄, comp_τ₄, ext_iff, CategoryTheory.Square.fromArrowArrowFunctor'_map_τ₄, comm₃₄_assoc, CategoryTheory.NatTrans.mapSquare_app_τ₄, CategoryTheory.Square.toArrowArrowFunctor'_map_right_right, CategoryTheory.Square.category_comp_τ₄, CategoryTheory.Square.opFunctor_map_τ₄, CategoryTheory.Square.flipFunctor_map_τ₄, CategoryTheory.Square.fromArrowArrowFunctor_map_τ₄

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comm₁₂ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Square.X₁ CategoryTheory.Square.X₂ CategoryTheory.Square.f₁₂ τ₂ τ₁	—	—
comm₁₂_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Square.X₁ CategoryTheory.Square.X₂ CategoryTheory.Square.f₁₂ τ₂ τ₁	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comm₁₂
comm₁₃ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Square.X₁ CategoryTheory.Square.X₃ CategoryTheory.Square.f₁₃ τ₃ τ₁	—	—
comm₁₃_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Square.X₁ CategoryTheory.Square.X₃ CategoryTheory.Square.f₁₃ τ₃ τ₁	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comm₁₃
comm₂₄ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Square.X₂ CategoryTheory.Square.X₄ CategoryTheory.Square.f₂₄ τ₄ τ₂	—	—
comm₂₄_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Square.X₂ CategoryTheory.Square.X₄ CategoryTheory.Square.f₂₄ τ₄ τ₂	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comm₂₄
comm₃₄ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Square.X₃ CategoryTheory.Square.X₄ CategoryTheory.Square.f₃₄ τ₄ τ₃	—	—
comm₃₄_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Square.X₃ CategoryTheory.Square.X₄ CategoryTheory.Square.f₃₄ τ₄ τ₃	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comm₃₄
comp_τ₁ 📖	mathematical	—	τ₁ comp CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Square.X₁	—	—
comp_τ₂ 📖	mathematical	—	τ₂ comp CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Square.X₂	—	—
comp_τ₃ 📖	mathematical	—	τ₃ comp CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Square.X₃	—	—
comp_τ₄ 📖	mathematical	—	τ₄ comp CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Square.X₄	—	—
ext 📖	—	τ₁ τ₂ τ₃ τ₄	—	—	—
ext_iff 📖	mathematical	—	τ₁ τ₂ τ₃ τ₄	—	ext
id_τ₁ 📖	mathematical	—	τ₁ id CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Square.X₁	—	—
id_τ₂ 📖	mathematical	—	τ₂ id CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Square.X₂	—	—
id_τ₃ 📖	mathematical	—	τ₃ id CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Square.X₃	—	—
id_τ₄ 📖	mathematical	—	τ₄ id CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Square.X₄	—	—

---

← Back to Index