OrthogonalReflection

📁 Source: Mathlib/CategoryTheory/Presentable/OrthogonalReflection.lean

Statistics

Metric	Count
Definitions D₁, l, obj₁, obj₂, t, ιLeft, ιRight, D₂, multispanIndex, multispanShape, corepresentableBy, fromStep, iteration, iterationObjSuccIso, reflection, reflectionObj, step, succ, succStruct, toStep, toSucc, transfiniteCompositionOfShapeReflection	22
Theorems isCardinalAccessible_ι_isLocal, isClosedUnderColimitsOfShape_isLocal, isLocallyPresentable_isLocal, isRightAdjoint_ι_isLocal, hasCoproductsOfShape, ιLeft_comp_l, ιLeft_comp_l_assoc, ιLeft_comp_t, ιLeft_comp_t_assoc, ι_comp_t, ι_comp_t_assoc, condition, condition_assoc, hasColimitsOfShape, multispanIndex_fst, multispanIndex_left, multispanIndex_right, multispanIndex_snd, multispanShape_L, multispanShape_R, multispanShape_fst, multispanShape_snd, instSmallD₁OfIsSmallOfLocallySmall, instSmallD₂, instSmallLMultispanShape, isIso_toSucc_iff, isLocal_isLocal_reflection, isLocal_isLocal_toSucc, isLocal_reflectionObj, isRightAdjoint_ι, iteration_map_succ, iteration_map_succ_assoc, iteration_map_succ_injectivity, iteration_map_succ_surjectivity, leftBousfieldW_isLocal_toSucc, toSucc_injectivity, toSucc_surjectivity	37
Total	59

CategoryTheory.MorphismProperty

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isCardinalAccessible_ι_isLocal 📖	mathematical	CategoryTheory.IsCardinalPresentable	CategoryTheory.Functor.IsCardinalAccessible CategoryTheory.ObjectProperty.FullSubcategory isLocal CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.ObjectProperty.ι	—	isClosedUnderColimitsOfShape_isLocal CategoryTheory.essentiallySmall_of_small_of_locallySmall UnivLE.small univLE_of_max UnivLE.self CategoryTheory.locallySmall_of_univLE CategoryTheory.preservesColimitOfShape_of_createsColimitsOfShape_and_hasColimitsOfShape CategoryTheory.HasCardinalFilteredColimits.hasColimitsOfShape
isClosedUnderColimitsOfShape_isLocal 📖	mathematical	CategoryTheory.IsCardinalPresentable	CategoryTheory.ObjectProperty.IsClosedUnderColimitsOfShape isLocal	—	CategoryTheory.IsCardinalPresentable.exists_hom_of_isColimit CategoryTheory.IsCardinalPresentable.exists_eq_of_isColimit CategoryTheory.Category.assoc CategoryTheory.Limits.ColimitPresentation.w Mathlib.Tactic.Reassoc.eq_whisker' CategoryTheory.ObjectProperty.ColimitOfShape.prop_diag_obj
isLocallyPresentable_isLocal 📖	mathematical	CategoryTheory.IsCardinalPresentable	CategoryTheory.IsCardinalLocallyPresentable CategoryTheory.ObjectProperty.FullSubcategory isLocal CategoryTheory.ObjectProperty.FullSubcategory.category	—	isRightAdjoint_ι_isLocal CategoryTheory.HasCardinalFilteredGenerator.toLocallySmall CategoryTheory.IsCardinalAccessibleCategory.toHasCardinalFilteredGenerator CategoryTheory.instIsCardinalAccessibleCategoryOfIsCardinalLocallyPresentable CategoryTheory.IsCardinalLocallyPresentable.toHasColimitsOfSize isCardinalAccessible_ι_isLocal CategoryTheory.IsCardinalAccessibleCategory.toHasCardinalFilteredColimits CategoryTheory.Adjunction.isCardinalLocallyPresentable CategoryTheory.ObjectProperty.full_ι CategoryTheory.ObjectProperty.faithful_ι
isRightAdjoint_ι_isLocal 📖	mathematical	CategoryTheory.IsCardinalPresentable	CategoryTheory.Functor.IsRightAdjoint CategoryTheory.ObjectProperty.FullSubcategory isLocal CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.ObjectProperty.ι	—	Cardinal.IsRegular.ne_zero Fact.out CategoryTheory.OrthogonalReflection.D₁.hasCoproductsOfShape CategoryTheory.OrthogonalReflection.D₂.hasColimitsOfShape CategoryTheory.OrthogonalReflection.isRightAdjoint_ι CategoryTheory.Limits.hasPushouts_of_hasWidePushouts CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.instHasIterationOfShapeOfHasColimitsOfSize

CategoryTheory.OrthogonalReflection

Definitions

Name	Category	Theorems
D₁ 📖	CompOp	8 math math: D₁.ιLeft_comp_l, D₁.ι_comp_t_assoc, D₁.ιLeft_comp_t, D₁.ιLeft_comp_l_assoc, D₁.ιLeft_comp_t_assoc, D₁.ι_comp_t, D₁.hasCoproductsOfShape, instSmallD₁OfIsSmallOfLocallySmall
D₂ 📖	CompOp	2 math math: instSmallD₂, D₂.multispanShape_L
corepresentableBy 📖	CompOp	—
fromStep 📖	CompOp	3 math math: D₂.condition, D₂.condition_assoc, iteration_map_succ_assoc
iteration 📖	CompOp	3 math math: iteration_map_succ, iteration_map_succ_assoc, iteration_map_succ_surjectivity
iterationObjSuccIso 📖	CompOp	2 math math: iteration_map_succ, iteration_map_succ_assoc
reflection 📖	CompOp	1 math math: isLocal_isLocal_reflection
reflectionObj 📖	CompOp	2 math math: isLocal_isLocal_reflection, isLocal_reflectionObj
step 📖	CompOp	5 math math: D₂.multispanIndex_right, iteration_map_succ_assoc, D₂.multispanIndex_left, D₂.multispanIndex_fst, D₂.multispanIndex_snd
succ 📖	CompOp	9 math math: toSucc_injectivity, iteration_map_succ, toSucc_surjectivity, leftBousfieldW_isLocal_toSucc, D₂.condition, isLocal_isLocal_toSucc, D₂.condition_assoc, iteration_map_succ_assoc, isIso_toSucc_iff
succStruct 📖	CompOp	—
toStep 📖	CompOp	1 math math: iteration_map_succ_assoc
toSucc 📖	CompOp	6 math math: toSucc_injectivity, iteration_map_succ, toSucc_surjectivity, leftBousfieldW_isLocal_toSucc, isLocal_isLocal_toSucc, isIso_toSucc_iff
transfiniteCompositionOfShapeReflection 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instSmallD₁OfIsSmallOfLocallySmall 📖	mathematical	—	Small D₁	—	small_sigma CategoryTheory.MorphismProperty.IsSmall.small_toSet CategoryTheory.instSmallHomOfLocallySmall
instSmallD₂ 📖	mathematical	—	Small D₂	—	small_sigma CategoryTheory.MorphismProperty.IsSmall.small_toSet small_subtype small_prod CategoryTheory.instSmallHomOfLocallySmall
instSmallLMultispanShape 📖	mathematical	—	Small CategoryTheory.Limits.MultispanShape.L D₂.multispanShape	—	instSmallD₂
isIso_toSucc_iff 📖	mathematical	—	CategoryTheory.IsIso succ toSucc CategoryTheory.MorphismProperty.isLocal	—	CategoryTheory.cancel_mono CategoryTheory.mono_of_strongMono CategoryTheory.instStrongMonoOfIsRegularMono CategoryTheory.instIsRegularMonoOfIsSplitMono CategoryTheory.IsSplitMono.of_iso CategoryTheory.Category.assoc D₂.condition Mathlib.Tactic.Reassoc.eq_whisker' CategoryTheory.IsIso.hom_inv_id CategoryTheory.Limits.pushout.condition_assoc CategoryTheory.Category.comp_id CategoryTheory.Limits.colimit.ι_desc isLocal_isLocal_toSucc CategoryTheory.Limits.Multicoequalizer.hom_ext CategoryTheory.Limits.pushout.hom_ext CategoryTheory.Limits.Sigma.hom_ext D₁.ι_comp_t_assoc CategoryTheory.Category.id_comp CategoryTheory.Limits.pushout.condition
isLocal_isLocal_reflection 📖	mathematical	CategoryTheory.Limits.HasCoproduct D₁ D₁.obj₁ D₁.obj₂ CategoryTheory.Limits.HasMulticoequalizer D₂.multispanShape D₂.multispanIndex	CategoryTheory.ObjectProperty.isLocal CategoryTheory.MorphismProperty.isLocal reflectionObj reflection	—	CategoryTheory.MorphismProperty.transfiniteCompositionsOfShape_le wellFoundedLT_toType CategoryTheory.ObjectProperty.instIsStableUnderTransfiniteCompositionOfShapeIsLocal
isLocal_isLocal_toSucc 📖	mathematical	—	CategoryTheory.ObjectProperty.isLocal CategoryTheory.MorphismProperty.isLocal succ toSucc	—	CategoryTheory.Limits.Multicoequalizer.hom_ext CategoryTheory.Limits.pushout.hom_ext CategoryTheory.Limits.Sigma.hom_ext CategoryTheory.Limits.pushout.condition_assoc CategoryTheory.Category.assoc CategoryTheory.Limits.Sigma.ι_map_assoc CategoryTheory.Limits.colimit.ι_desc CategoryTheory.Limits.colimit.ι_desc_assoc Mathlib.Tactic.Reassoc.eq_whisker'
isLocal_reflectionObj 📖	mathematical	CategoryTheory.Limits.HasCoproduct D₁ D₁.obj₁ D₁.obj₂ CategoryTheory.Limits.HasMulticoequalizer D₂.multispanShape D₂.multispanIndex CategoryTheory.IsCardinalPresentable	CategoryTheory.MorphismProperty.isLocal reflectionObj	—	wellFoundedLT_toType CategoryTheory.IsCardinalPresentable.exists_hom_of_isColimit CategoryTheory.essentiallySmall_of_small_of_locallySmall UnivLE.small UnivLE.self CategoryTheory.locallySmall_of_thin Preorder.subsingleton_hom CategoryTheory.instIsCardinalFilteredToTypeOrd le_max_left le_max_right CategoryTheory.Category.assoc CategoryTheory.NatTrans.naturality CategoryTheory.Category.comp_id CategoryTheory.IsCardinalPresentable.exists_eq_of_isColimit' Order.le_succ iteration_map_succ_injectivity CategoryTheory.Functor.map_comp Mathlib.Tactic.Reassoc.eq_whisker' iteration_map_succ_surjectivity
isRightAdjoint_ι 📖	mathematical	CategoryTheory.Limits.HasCoproduct D₁ D₁.obj₁ D₁.obj₂ CategoryTheory.Limits.HasMulticoequalizer D₂.multispanShape D₂.multispanIndex CategoryTheory.IsCardinalPresentable	CategoryTheory.Functor.IsRightAdjoint CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.MorphismProperty.isLocal CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.ObjectProperty.ι	—	CategoryTheory.Functor.isRightAdjoint_iff_leftAdjointObjIsDefined_eq_top CategoryTheory.Functor.CorepresentableBy.isCorepresentable isLocal_reflectionObj
iteration_map_succ 📖	mathematical	CategoryTheory.Limits.HasCoproduct D₁ D₁.obj₁ D₁.obj₂ CategoryTheory.Limits.HasMulticoequalizer D₂.multispanShape D₂.multispanIndex	CategoryTheory.Functor.map Ordinal.ToType Cardinal.ord Preorder.smallCategory PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder linearOrder_toType iteration Order.succ Ordinal.instSuccOrderToType CategoryTheory.homOfLE Order.le_succ CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj succ toSucc CategoryTheory.Iso.inv iterationObjSuccIso	—	CategoryTheory.SmallObject.SuccStruct.iterationFunctor_map_succ
iteration_map_succ_assoc 📖	mathematical	CategoryTheory.Limits.HasCoproduct D₁ D₁.obj₁ D₁.obj₂ CategoryTheory.Limits.HasMulticoequalizer D₂.multispanShape D₂.multispanIndex	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Ordinal.ToType Cardinal.ord Preorder.smallCategory PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder linearOrder_toType iteration Order.succ Ordinal.instSuccOrderToType CategoryTheory.Functor.map CategoryTheory.homOfLE Order.le_succ step toStep succ fromStep CategoryTheory.Iso.inv iterationObjSuccIso	—	Order.le_succ CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' iteration_map_succ
iteration_map_succ_injectivity 📖	mathematical	CategoryTheory.Limits.HasCoproduct D₁ D₁.obj₁ D₁.obj₂ CategoryTheory.Limits.HasMulticoequalizer D₂.multispanShape D₂.multispanIndex CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Ordinal.ToType Cardinal.ord Preorder.smallCategory PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder linearOrder_toType iteration	Order.succ Ordinal.instSuccOrderToType CategoryTheory.Functor.map CategoryTheory.homOfLE Order.le_succ	—	Order.le_succ iteration_map_succ CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' toSucc_injectivity
iteration_map_succ_surjectivity 📖	mathematical	CategoryTheory.Limits.HasCoproduct D₁ D₁.obj₁ D₁.obj₂ CategoryTheory.Limits.HasMulticoequalizer D₂.multispanShape D₂.multispanIndex	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Ordinal.ToType Cardinal.ord Preorder.smallCategory PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder linearOrder_toType iteration Order.succ Ordinal.instSuccOrderToType CategoryTheory.Functor.map CategoryTheory.homOfLE Order.le_succ	—	Order.le_succ iteration_map_succ toSucc_surjectivity CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker'
leftBousfieldW_isLocal_toSucc 📖	mathematical	—	CategoryTheory.ObjectProperty.isLocal CategoryTheory.MorphismProperty.isLocal succ toSucc	—	isLocal_isLocal_toSucc
toSucc_injectivity 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	succ toSucc	—	CategoryTheory.Category.assoc D₂.condition Mathlib.Tactic.Reassoc.eq_whisker'
toSucc_surjectivity 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct succ toSucc	—	CategoryTheory.Limits.pushout.condition_assoc CategoryTheory.Limits.colimit.ι_desc_assoc

CategoryTheory.OrthogonalReflection.D₁

Definitions

Name	Category	Theorems
l 📖	CompOp	2 math math: ιLeft_comp_l, ιLeft_comp_l_assoc
obj₁ 📖	CompOp	6 math math: ιLeft_comp_l, ι_comp_t_assoc, ιLeft_comp_t, ιLeft_comp_l_assoc, ιLeft_comp_t_assoc, ι_comp_t
obj₂ 📖	CompOp	4 math math: ι_comp_t_assoc, ιLeft_comp_t, ιLeft_comp_t_assoc, ι_comp_t
t 📖	CompOp	4 math math: ι_comp_t_assoc, ιLeft_comp_t, ιLeft_comp_t_assoc, ι_comp_t
ιLeft 📖	CompOp	4 math math: ιLeft_comp_l, ιLeft_comp_t, ιLeft_comp_l_assoc, ιLeft_comp_t_assoc
ιRight 📖	CompOp	2 math math: ιLeft_comp_t, ιLeft_comp_t_assoc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasCoproductsOfShape 📖	mathematical	CategoryTheory.Limits.HasCoproducts	CategoryTheory.Limits.HasCoproductsOfShape CategoryTheory.OrthogonalReflection.D₁	—	CategoryTheory.Limits.hasColimitsOfShape_of_equivalence CategoryTheory.OrthogonalReflection.instSmallD₁OfIsSmallOfLocallySmall
ιLeft_comp_l 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.sigmaObj CategoryTheory.OrthogonalReflection.D₁ obj₁ ιLeft l	—	CategoryTheory.Limits.Sigma.ι_desc
ιLeft_comp_l_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.sigmaObj CategoryTheory.OrthogonalReflection.D₁ obj₁ ιLeft l	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ιLeft_comp_l
ιLeft_comp_t 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.sigmaObj CategoryTheory.OrthogonalReflection.D₁ obj₁ obj₂ ιLeft t ιRight	—	CategoryTheory.Limits.ι_colimMap
ιLeft_comp_t_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.sigmaObj CategoryTheory.OrthogonalReflection.D₁ obj₁ ιLeft obj₂ t ιRight	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ιLeft_comp_t
ι_comp_t 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj₁ CategoryTheory.Limits.sigmaObj CategoryTheory.OrthogonalReflection.D₁ obj₂ CategoryTheory.Limits.Sigma.ι t CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Arrow Set Set.instMembership CategoryTheory.MorphismProperty.toSet Set.Elem Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Comma.right CategoryTheory.Comma.hom	—	CategoryTheory.Limits.ι_colimMap
ι_comp_t_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct obj₁ CategoryTheory.Limits.sigmaObj CategoryTheory.OrthogonalReflection.D₁ CategoryTheory.Limits.Sigma.ι obj₂ t CategoryTheory.Comma.right CategoryTheory.Functor.id CategoryTheory.Arrow Set Set.instMembership CategoryTheory.MorphismProperty.toSet Set.Elem Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Comma.left CategoryTheory.Comma.hom	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι_comp_t

CategoryTheory.OrthogonalReflection.D₂

Definitions

Name	Category	Theorems
multispanIndex 📖	CompOp	4 math math: multispanIndex_right, multispanIndex_left, multispanIndex_fst, multispanIndex_snd
multispanShape 📖	CompOp	10 math math: multispanShape_R, multispanIndex_right, multispanShape_fst, multispanShape_snd, multispanIndex_left, hasColimitsOfShape, multispanShape_L, CategoryTheory.OrthogonalReflection.instSmallLMultispanShape, multispanIndex_fst, multispanIndex_snd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
condition 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.OrthogonalReflection.step	CategoryTheory.OrthogonalReflection.succ CategoryTheory.OrthogonalReflection.fromStep	—	CategoryTheory.Limits.Multicoequalizer.condition
condition_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.OrthogonalReflection.step	CategoryTheory.OrthogonalReflection.succ CategoryTheory.OrthogonalReflection.fromStep	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' condition
hasColimitsOfShape 📖	mathematical	—	CategoryTheory.Limits.HasColimitsOfShape CategoryTheory.Limits.WalkingMultispan multispanShape CategoryTheory.Limits.WalkingMultispan.instSmallCategory	—	CategoryTheory.Limits.hasColimitsOfShape_of_equivalence CategoryTheory.essentiallySmall_of_small_of_locallySmall CategoryTheory.Limits.WalkingMultispan.instSmallOfLOfR CategoryTheory.OrthogonalReflection.instSmallLMultispanShape UnivLE.small univLE_of_max UnivLE.self CategoryTheory.Limits.WalkingMultispan.instLocallySmall CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize
multispanIndex_fst 📖	mathematical	—	CategoryTheory.Limits.MultispanIndex.fst multispanShape multispanIndex Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.right CategoryTheory.Functor.id CategoryTheory.Arrow Set Set.instMembership CategoryTheory.MorphismProperty.toSet Set.Elem CategoryTheory.OrthogonalReflection.step CategoryTheory.Functor.obj CategoryTheory.Comma.left CategoryTheory.CategoryStruct.comp CategoryTheory.Comma.hom	—	—
multispanIndex_left 📖	mathematical	—	CategoryTheory.Limits.MultispanIndex.left multispanShape multispanIndex CategoryTheory.Comma.right CategoryTheory.Functor.id CategoryTheory.Arrow Set Set.instMembership CategoryTheory.MorphismProperty.toSet Set.Elem Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.OrthogonalReflection.step CategoryTheory.Functor.obj CategoryTheory.Comma.left CategoryTheory.CategoryStruct.comp CategoryTheory.Comma.hom	—	—
multispanIndex_right 📖	mathematical	—	CategoryTheory.Limits.MultispanIndex.right multispanShape multispanIndex CategoryTheory.OrthogonalReflection.step	—	—
multispanIndex_snd 📖	mathematical	—	CategoryTheory.Limits.MultispanIndex.snd multispanShape multispanIndex Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Comma.right CategoryTheory.Functor.id CategoryTheory.Arrow Set Set.instMembership CategoryTheory.MorphismProperty.toSet Set.Elem CategoryTheory.OrthogonalReflection.step CategoryTheory.Functor.obj CategoryTheory.Comma.left CategoryTheory.CategoryStruct.comp CategoryTheory.Comma.hom	—	—
multispanShape_L 📖	mathematical	—	CategoryTheory.Limits.MultispanShape.L multispanShape CategoryTheory.OrthogonalReflection.D₂	—	—
multispanShape_R 📖	mathematical	—	CategoryTheory.Limits.MultispanShape.R multispanShape	—	—
multispanShape_fst 📖	mathematical	—	CategoryTheory.Limits.MultispanShape.fst multispanShape	—	—
multispanShape_snd 📖	mathematical	—	CategoryTheory.Limits.MultispanShape.snd multispanShape	—	—

---

← Back to Index