Documentation

Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Multi-(co)equalizers #

A multiequalizer is an equalizer of two morphisms between two products. Since both products and equalizers are limits, such an object is again a limit. This file provides the diagram whose limit is indeed such an object. In fact, it is well-known that any limit can be obtained as a multiequalizer. The dual construction (multicoequalizers) is also provided.

Projects #

Prove that a multiequalizer can be identified with an equalizer between products (and analogously for multicoequalizers).

Prove that the limit of any diagram is a multiequalizer (and similarly for colimits).

structure CategoryTheory.Limits.MulticospanShape :
Type (max (w + 1) (w' + 1))

The shape of a multiequalizer diagram. It involves two types L and R, and two maps RL.

  • L : Type w

    the left type

  • R : Type w'

    the right type

  • fst : self.Rself.L

    the first map RL

  • snd : self.Rself.L

    the second map RL

Instances For

    Given a type ι, this is the shape of multiequalizer diagrams corresponding to situations where we want to equalize two families of maps U i ⟶ V ⟨i, j⟩ and U j ⟶ V ⟨i, j⟩ with i : ι and j : ι.

    Equations
    Instances For
      @[simp]
      @[simp]
      theorem CategoryTheory.Limits.MulticospanShape.prod_fst (ι : Type w) (self : ι × ι) :
      (prod ι).fst self = self.1
      @[simp]
      theorem CategoryTheory.Limits.MulticospanShape.prod_snd (ι : Type w) (self : ι × ι) :
      (prod ι).snd self = self.2
      structure CategoryTheory.Limits.MultispanShape :
      Type (max (w + 1) (w' + 1))

      The shape of a multicoequalizer diagram. It involves two types L and R, and two maps LR.

      • L : Type w

        the left type

      • R : Type w'

        the right type

      • fst : self.Lself.R

        the first map LR

      • snd : self.Lself.R

        the second map LR

      Instances For

        Given a type ι, this is the shape of multicoequalizer diagrams corresponding to situations where we want to coequalize two families of maps V ⟨i, j⟩ ⟶ U i and V ⟨i, j⟩ ⟶ U j with i : ι and j : ι.

        Equations
        Instances For
          @[simp]
          theorem CategoryTheory.Limits.MultispanShape.prod_snd (ι : Type w) (self : ι × ι) :
          (prod ι).snd self = self.2
          @[simp]
          @[simp]
          theorem CategoryTheory.Limits.MultispanShape.prod_fst (ι : Type w) (self : ι × ι) :
          (prod ι).fst self = self.1

          Given a linearly ordered type ι, this is the shape of multicoequalizer diagrams corresponding to situations where we want to coequalize two families of maps V ⟨i, j⟩ ⟶ U i and V ⟨i, j⟩ ⟶ U j with i < j.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            @[simp]
            @[simp]
            theorem CategoryTheory.Limits.MultispanShape.ofLinearOrder_fst (ι : Type w) [LinearOrder ι] (x : {x : ι × ι | x.1 < x.2}) :
            (ofLinearOrder ι).fst x = (↑x).1
            @[simp]
            theorem CategoryTheory.Limits.MultispanShape.ofLinearOrder_snd (ι : Type w) [LinearOrder ι] (x : {x : ι × ι | x.1 < x.2}) :
            (ofLinearOrder ι).snd x = (↑x).2

            The type underlying the multiequalizer diagram.

            Instances For

              The type underlying the multiecoqualizer diagram.

              Instances For

                Morphisms for WalkingMulticospan.

                Instances For

                  Composition of morphisms for WalkingMulticospan.

                  Equations
                  Instances For
                    Equations
                    • One or more equations did not get rendered due to their size.

                    Morphisms for WalkingMultispan.

                    Instances For

                      Composition of morphisms for WalkingMultispan.

                      Equations
                      Instances For
                        Equations
                        • One or more equations did not get rendered due to their size.
                        structure CategoryTheory.Limits.MulticospanIndex (J : MulticospanShape) (C : Type u) [Category.{v, u} C] :
                        Type (max (max (max u v) w) w')

                        This is a structure encapsulating the data necessary to define a Multicospan.

                        Instances For
                          structure CategoryTheory.Limits.MultispanIndex (J : MultispanShape) (C : Type u) [Category.{v, u} C] :
                          Type (max (max (max u v) w) w')

                          This is a structure encapsulating the data necessary to define a Multispan.

                          Instances For

                            The multicospan associated to I : MulticospanIndex.

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For

                              Taking the multiequalizer over the multicospan index is equivalent to taking the equalizer over the two morphisms ∏ᶜ I.left ⇉ ∏ᶜ I.right. This is the diagram of the latter.

                              Equations
                              Instances For

                                The multispan associated to I : MultispanIndex.

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  @[reducible, inline]

                                  Taking the multicoequalizer over the multispan index is equivalent to taking the coequalizer over the two morphsims ∐ I.left ⇉ ∐ I.right. This is the diagram of the latter.

                                  Equations
                                  Instances For
                                    @[reducible, inline]
                                    abbrev CategoryTheory.Limits.Multifork {C : Type u} [Category.{v, u} C] {J : MulticospanShape} (I : MulticospanIndex J C) :
                                    Type (max (max (max w w') u) v)

                                    A multifork is a cone over a multicospan.

                                    Equations
                                    Instances For
                                      @[reducible, inline]
                                      abbrev CategoryTheory.Limits.Multicofork {C : Type u} [Category.{v, u} C] {J : MultispanShape} (I : MultispanIndex J C) :
                                      Type (max (max (max w w') u) v)

                                      A multicofork is a cocone over a multispan.

                                      Equations
                                      Instances For

                                        The maps from the cone point of a multifork to the objects on the left.

                                        Equations
                                        Instances For
                                          @[simp]
                                          theorem CategoryTheory.Limits.Multifork.hom_comp_ι {C : Type u} [Category.{v, u} C] {J : MulticospanShape} {I : MulticospanIndex J C} (K₁ K₂ : Multifork I) (f : K₁ K₂) (j : J.L) :
                                          CategoryStruct.comp f.hom (K₂.ι j) = K₁.ι j
                                          @[simp]
                                          theorem CategoryTheory.Limits.Multifork.hom_comp_ι_assoc {C : Type u} [Category.{v, u} C] {J : MulticospanShape} {I : MulticospanIndex J C} (K₁ K₂ : Multifork I) (f : K₁ K₂) (j : J.L) {Z : C} (h : I.left j Z) :
                                          def CategoryTheory.Limits.Multifork.ofι {C : Type u} [Category.{v, u} C] {J : MulticospanShape} (I : MulticospanIndex J C) (P : C) (ι : (a : J.L) → P I.left a) (w : ∀ (b : J.R), CategoryStruct.comp (ι (J.fst b)) (I.fst b) = CategoryStruct.comp (ι (J.snd b)) (I.snd b)) :

                                          Construct a multifork using a collection ι of morphisms.

                                          Equations
                                          • One or more equations did not get rendered due to their size.
                                          Instances For
                                            @[simp]
                                            theorem CategoryTheory.Limits.Multifork.ofι_pt {C : Type u} [Category.{v, u} C] {J : MulticospanShape} (I : MulticospanIndex J C) (P : C) (ι : (a : J.L) → P I.left a) (w : ∀ (b : J.R), CategoryStruct.comp (ι (J.fst b)) (I.fst b) = CategoryStruct.comp (ι (J.snd b)) (I.snd b)) :
                                            (ofι I P ι w).pt = P
                                            @[simp]
                                            theorem CategoryTheory.Limits.Multifork.ofι_π_app {C : Type u} [Category.{v, u} C] {J : MulticospanShape} (I : MulticospanIndex J C) (P : C) (ι : (a : J.L) → P I.left a) (w : ∀ (b : J.R), CategoryStruct.comp (ι (J.fst b)) (I.fst b) = CategoryStruct.comp (ι (J.snd b)) (I.snd b)) (x : WalkingMulticospan J) :
                                            (ofι I P ι w).π.app x = match x with | WalkingMulticospan.left a => ι a | WalkingMulticospan.right b => CategoryStruct.comp (ι (J.fst b)) (I.fst b)
                                            def CategoryTheory.Limits.Multifork.IsLimit.mk {C : Type u} [Category.{v, u} C] {J : MulticospanShape} {I : MulticospanIndex J C} (K : Multifork I) (lift : (E : Multifork I) → E.pt K.pt) (fac : ∀ (E : Multifork I) (i : J.L), CategoryStruct.comp (lift E) (K.ι i) = E.ι i) (uniq : ∀ (E : Multifork I) (m : E.pt K.pt), (∀ (i : J.L), CategoryStruct.comp m (K.ι i) = E.ι i)m = lift E) :

                                            This definition provides a convenient way to show that a multifork is a limit.

                                            Equations
                                            Instances For
                                              @[simp]
                                              theorem CategoryTheory.Limits.Multifork.IsLimit.mk_lift {C : Type u} [Category.{v, u} C] {J : MulticospanShape} {I : MulticospanIndex J C} (K : Multifork I) (lift : (E : Multifork I) → E.pt K.pt) (fac : ∀ (E : Multifork I) (i : J.L), CategoryStruct.comp (lift E) (K.ι i) = E.ι i) (uniq : ∀ (E : Multifork I) (m : E.pt K.pt), (∀ (i : J.L), CategoryStruct.comp m (K.ι i) = E.ι i)m = lift E) (E : Multifork I) :
                                              (mk K lift fac uniq).lift E = lift E
                                              theorem CategoryTheory.Limits.Multifork.IsLimit.hom_ext {C : Type u} [Category.{v, u} C] {J : MulticospanShape} {I : MulticospanIndex J C} {K : Multifork I} (hK : IsLimit K) {T : C} {f g : T K.pt} (h : ∀ (a : J.L), CategoryStruct.comp f (K.ι a) = CategoryStruct.comp g (K.ι a)) :
                                              f = g
                                              def CategoryTheory.Limits.Multifork.IsLimit.lift {C : Type u} [Category.{v, u} C] {J : MulticospanShape} {I : MulticospanIndex J C} {K : Multifork I} (hK : IsLimit K) {T : C} (k : (a : J.L) → T I.left a) (hk : ∀ (b : J.R), CategoryStruct.comp (k (J.fst b)) (I.fst b) = CategoryStruct.comp (k (J.snd b)) (I.snd b)) :
                                              T K.pt

                                              Constructor for morphisms to the point of a limit multifork.

                                              Equations
                                              Instances For
                                                @[simp]
                                                theorem CategoryTheory.Limits.Multifork.IsLimit.fac {C : Type u} [Category.{v, u} C] {J : MulticospanShape} {I : MulticospanIndex J C} {K : Multifork I} (hK : IsLimit K) {T : C} (k : (a : J.L) → T I.left a) (hk : ∀ (b : J.R), CategoryStruct.comp (k (J.fst b)) (I.fst b) = CategoryStruct.comp (k (J.snd b)) (I.snd b)) (a : J.L) :
                                                CategoryStruct.comp (lift hK k hk) (K.ι a) = k a
                                                @[simp]
                                                theorem CategoryTheory.Limits.Multifork.IsLimit.fac_assoc {C : Type u} [Category.{v, u} C] {J : MulticospanShape} {I : MulticospanIndex J C} {K : Multifork I} (hK : IsLimit K) {T : C} (k : (a : J.L) → T I.left a) (hk : ∀ (b : J.R), CategoryStruct.comp (k (J.fst b)) (I.fst b) = CategoryStruct.comp (k (J.snd b)) (I.snd b)) (a : J.L) {Z : C} (h : I.left a Z) :

                                                Given a multifork, we may obtain a fork over ∏ᶜ I.left ⇉ ∏ᶜ I.right.

                                                Equations
                                                • One or more equations did not get rendered due to their size.
                                                Instances For

                                                  Given a fork over ∏ᶜ I.left ⇉ ∏ᶜ I.right, we may obtain a multifork.

                                                  Equations
                                                  • One or more equations did not get rendered due to their size.
                                                  Instances For

                                                    Multifork.toPiFork as a functor.

                                                    Equations
                                                    • One or more equations did not get rendered due to their size.
                                                    Instances For

                                                      Multifork.ofPiFork as a functor.

                                                      Equations
                                                      • One or more equations did not get rendered due to their size.
                                                      Instances For

                                                        The category of multiforks is equivalent to the category of forks over ∏ᶜ I.left ⇉ ∏ᶜ I.right. It then follows from CategoryTheory.IsLimit.ofPreservesConeTerminal (or reflects) that it preserves and reflects limit cones.

                                                        Equations
                                                        • One or more equations did not get rendered due to their size.
                                                        Instances For

                                                          The maps to the cocone point of a multicofork from the objects on the right.

                                                          Equations
                                                          Instances For
                                                            @[simp]
                                                            theorem CategoryTheory.Limits.Multicofork.π_comp_hom {C : Type u} [Category.{v, u} C] {J : MultispanShape} {I : MultispanIndex J C} (K₁ K₂ : Multicofork I) (f : K₁ K₂) (b : J.R) :
                                                            CategoryStruct.comp (K₁.π b) f.hom = K₂.π b
                                                            @[simp]
                                                            theorem CategoryTheory.Limits.Multicofork.π_comp_hom_assoc {C : Type u} [Category.{v, u} C] {J : MultispanShape} {I : MultispanIndex J C} (K₁ K₂ : Multicofork I) (f : K₁ K₂) (b : J.R) {Z : C} (h : K₂.pt Z) :
                                                            def CategoryTheory.Limits.Multicofork.ofπ {C : Type u} [Category.{v, u} C] {J : MultispanShape} (I : MultispanIndex J C) (P : C) (π : (b : J.R) → I.right b P) (w : ∀ (a : J.L), CategoryStruct.comp (I.fst a) (π (J.fst a)) = CategoryStruct.comp (I.snd a) (π (J.snd a))) :

                                                            Construct a multicofork using a collection π of morphisms.

                                                            Equations
                                                            • One or more equations did not get rendered due to their size.
                                                            Instances For
                                                              @[simp]
                                                              theorem CategoryTheory.Limits.Multicofork.ofπ_pt {C : Type u} [Category.{v, u} C] {J : MultispanShape} (I : MultispanIndex J C) (P : C) (π : (b : J.R) → I.right b P) (w : ∀ (a : J.L), CategoryStruct.comp (I.fst a) (π (J.fst a)) = CategoryStruct.comp (I.snd a) (π (J.snd a))) :
                                                              (ofπ I P π w).pt = P
                                                              @[simp]
                                                              theorem CategoryTheory.Limits.Multicofork.ofπ_ι_app {C : Type u} [Category.{v, u} C] {J : MultispanShape} (I : MultispanIndex J C) (P : C) (π : (b : J.R) → I.right b P) (w : ∀ (a : J.L), CategoryStruct.comp (I.fst a) (π (J.fst a)) = CategoryStruct.comp (I.snd a) (π (J.snd a))) (x : WalkingMultispan J) :
                                                              (ofπ I P π w).ι.app x = match x with | WalkingMultispan.left a => CategoryStruct.comp (I.fst a) (π (J.fst a)) | WalkingMultispan.right a => π a
                                                              def CategoryTheory.Limits.Multicofork.IsColimit.mk {C : Type u} [Category.{v, u} C] {J : MultispanShape} {I : MultispanIndex J C} (K : Multicofork I) (desc : (E : Multicofork I) → K.pt E.pt) (fac : ∀ (E : Multicofork I) (i : J.R), CategoryStruct.comp (K.π i) (desc E) = E.π i) (uniq : ∀ (E : Multicofork I) (m : K.pt E.pt), (∀ (i : J.R), CategoryStruct.comp (K.π i) m = E.π i)m = desc E) :

                                                              This definition provides a convenient way to show that a multicofork is a colimit.

                                                              Equations
                                                              Instances For
                                                                @[simp]
                                                                theorem CategoryTheory.Limits.Multicofork.IsColimit.mk_desc {C : Type u} [Category.{v, u} C] {J : MultispanShape} {I : MultispanIndex J C} (K : Multicofork I) (desc : (E : Multicofork I) → K.pt E.pt) (fac : ∀ (E : Multicofork I) (i : J.R), CategoryStruct.comp (K.π i) (desc E) = E.π i) (uniq : ∀ (E : Multicofork I) (m : K.pt E.pt), (∀ (i : J.R), CategoryStruct.comp (K.π i) m = E.π i)m = desc E) (E : Multicofork I) :
                                                                (mk K desc fac uniq).desc E = desc E
                                                                theorem CategoryTheory.Limits.Multicofork.IsColimit.hom_ext {C : Type u} [Category.{v, u} C] {J : MultispanShape} {I : MultispanIndex J C} {K : Multicofork I} (hK : IsColimit K) {T : C} {f g : K.pt T} (h : ∀ (a : J.R), CategoryStruct.comp (K.π a) f = CategoryStruct.comp (K.π a) g) :
                                                                f = g

                                                                Given a multicofork, we may obtain a cofork over ∐ I.left ⇉ ∐ I.right.

                                                                Equations
                                                                • One or more equations did not get rendered due to their size.
                                                                Instances For

                                                                  Given a cofork over ∐ I.left ⇉ ∐ I.right, we may obtain a multicofork.

                                                                  Equations
                                                                  • One or more equations did not get rendered due to their size.
                                                                  Instances For
                                                                    def CategoryTheory.Limits.Multicofork.ext {C : Type u} [Category.{v, u} C] {J : MultispanShape} {I : MultispanIndex J C} {K K' : Multicofork I} (e : K.pt K'.pt) (h : ∀ (i : J.R), CategoryStruct.comp (K.π i) e.hom = K'.π i := by aesop_cat) :
                                                                    K K'

                                                                    Constructor for isomorphisms between multicoforks.

                                                                    Equations
                                                                    Instances For
                                                                      @[simp]
                                                                      theorem CategoryTheory.Limits.Multicofork.ext_hom_hom {C : Type u} [Category.{v, u} C] {J : MultispanShape} {I : MultispanIndex J C} {K K' : Multicofork I} (e : K.pt K'.pt) (h : ∀ (i : J.R), CategoryStruct.comp (K.π i) e.hom = K'.π i := by aesop_cat) :
                                                                      (ext e h).hom.hom = e.hom
                                                                      @[simp]
                                                                      theorem CategoryTheory.Limits.Multicofork.ext_inv_hom {C : Type u} [Category.{v, u} C] {J : MultispanShape} {I : MultispanIndex J C} {K K' : Multicofork I} (e : K.pt K'.pt) (h : ∀ (i : J.R), CategoryStruct.comp (K.π i) e.hom = K'.π i := by aesop_cat) :
                                                                      (ext e h).inv.hom = e.inv

                                                                      Multicofork.toSigmaCofork as a functor.

                                                                      Equations
                                                                      • One or more equations did not get rendered due to their size.
                                                                      Instances For

                                                                        Multicofork.ofSigmaCofork as a functor.

                                                                        Equations
                                                                        • One or more equations did not get rendered due to their size.
                                                                        Instances For

                                                                          The category of multicoforks is equivalent to the category of coforks over ∐ I.left ⇉ ∐ I.right. It then follows from CategoryTheory.IsColimit.ofPreservesCoconeInitial (or reflects) that it preserves and reflects colimit cocones.

                                                                          Equations
                                                                          • One or more equations did not get rendered due to their size.
                                                                          Instances For
                                                                            @[reducible, inline]

                                                                            For I : MulticospanIndex J C, we say that it has a multiequalizer if the associated multicospan has a limit.

                                                                            Equations
                                                                            Instances For
                                                                              @[reducible, inline]

                                                                              For I : MultispanIndex J C, we say that it has a multicoequalizer if the associated multicospan has a limit.

                                                                              Equations
                                                                              Instances For
                                                                                @[reducible, inline]

                                                                                The canonical map from the multiequalizer to the objects on the left.

                                                                                Equations
                                                                                Instances For
                                                                                  @[reducible, inline]
                                                                                  abbrev CategoryTheory.Limits.Multiequalizer.lift {C : Type u} [Category.{v, u} C] {J : MulticospanShape} (I : MulticospanIndex J C) [HasMultiequalizer I] (W : C) (k : (a : J.L) → W I.left a) (h : ∀ (b : J.R), CategoryStruct.comp (k (J.fst b)) (I.fst b) = CategoryStruct.comp (k (J.snd b)) (I.snd b)) :

                                                                                  Construct a morphism to the multiequalizer from its universal property.

                                                                                  Equations
                                                                                  Instances For
                                                                                    theorem CategoryTheory.Limits.Multiequalizer.lift_ι {C : Type u} [Category.{v, u} C] {J : MulticospanShape} (I : MulticospanIndex J C) [HasMultiequalizer I] (W : C) (k : (a : J.L) → W I.left a) (h : ∀ (b : J.R), CategoryStruct.comp (k (J.fst b)) (I.fst b) = CategoryStruct.comp (k (J.snd b)) (I.snd b)) (a : J.L) :
                                                                                    CategoryStruct.comp (lift I W k h) (ι I a) = k a
                                                                                    theorem CategoryTheory.Limits.Multiequalizer.lift_ι_assoc {C : Type u} [Category.{v, u} C] {J : MulticospanShape} (I : MulticospanIndex J C) [HasMultiequalizer I] (W : C) (k : (a : J.L) → W I.left a) (h : ∀ (b : J.R), CategoryStruct.comp (k (J.fst b)) (I.fst b) = CategoryStruct.comp (k (J.snd b)) (I.snd b)) (a : J.L) {Z : C} (h✝ : I.left a Z) :

                                                                                    The multiequalizer is isomorphic to the equalizer of ∏ᶜ I.left ⇉ ∏ᶜ I.right.

                                                                                    Equations
                                                                                    • One or more equations did not get rendered due to their size.
                                                                                    Instances For

                                                                                      The canonical injection multiequalizer I ⟶ ∏ᶜ I.left.

                                                                                      Equations
                                                                                      • One or more equations did not get rendered due to their size.
                                                                                      Instances For
                                                                                        @[reducible, inline]

                                                                                        The canonical map from the multiequalizer to the objects on the left.

                                                                                        Equations
                                                                                        Instances For
                                                                                          @[reducible, inline]
                                                                                          abbrev CategoryTheory.Limits.Multicoequalizer.desc {C : Type u} [Category.{v, u} C] {J : MultispanShape} (I : MultispanIndex J C) [HasMulticoequalizer I] (W : C) (k : (b : J.R) → I.right b W) (h : ∀ (a : J.L), CategoryStruct.comp (I.fst a) (k (J.fst a)) = CategoryStruct.comp (I.snd a) (k (J.snd a))) :

                                                                                          Construct a morphism from the multicoequalizer from its universal property.

                                                                                          Equations
                                                                                          Instances For
                                                                                            theorem CategoryTheory.Limits.Multicoequalizer.π_desc {C : Type u} [Category.{v, u} C] {J : MultispanShape} (I : MultispanIndex J C) [HasMulticoequalizer I] (W : C) (k : (b : J.R) → I.right b W) (h : ∀ (a : J.L), CategoryStruct.comp (I.fst a) (k (J.fst a)) = CategoryStruct.comp (I.snd a) (k (J.snd a))) (b : J.R) :
                                                                                            CategoryStruct.comp (π I b) (desc I W k h) = k b
                                                                                            theorem CategoryTheory.Limits.Multicoequalizer.π_desc_assoc {C : Type u} [Category.{v, u} C] {J : MultispanShape} (I : MultispanIndex J C) [HasMulticoequalizer I] (W : C) (k : (b : J.R) → I.right b W) (h : ∀ (a : J.L), CategoryStruct.comp (I.fst a) (k (J.fst a)) = CategoryStruct.comp (I.snd a) (k (J.snd a))) (b : J.R) {Z : C} (h✝ : W Z) :

                                                                                            The multicoequalizer is isomorphic to the coequalizer of ∐ I.left ⇉ ∐ I.right.

                                                                                            Equations
                                                                                            • One or more equations did not get rendered due to their size.
                                                                                            Instances For

                                                                                              The canonical projection ∐ I.rightmulticoequalizer I.

                                                                                              Equations
                                                                                              • One or more equations did not get rendered due to their size.
                                                                                              Instances For

                                                                                                The inclusion functor WalkingMultispan (.ofLinearOrder ι) ⥤ WalkingMultispan (.prod ι).

                                                                                                Equations
                                                                                                • One or more equations did not get rendered due to their size.
                                                                                                Instances For
                                                                                                  @[simp]
                                                                                                  theorem CategoryTheory.Limits.WalkingMultispan.inclusionOfLinearOrder_map (ι : Type w) [LinearOrder ι] {x y : WalkingMultispan (MultispanShape.ofLinearOrder ι)} (f : x y) :
                                                                                                  (inclusionOfLinearOrder ι).map f = match x, y, f with | x, .(x), Hom.id .(x) => CategoryStruct.id (match x with | left a => left a | right b => right b) | .(left b), .(right ((MultispanShape.ofLinearOrder ι).fst b)), Hom.fst b => Hom.fst b | .(left b), .(right ((MultispanShape.ofLinearOrder ι).snd b)), Hom.snd b => Hom.snd b

                                                                                                  Structure expressing a symmetry of I : MultispanIndex (.prod ι) C which allows to compare the corresponding multicoequalizer to the multicoequalizer of I.toLinearOrder.

                                                                                                  Instances For

                                                                                                    The multispan index for MultispanShape.ofLinearOrder ι deduced from a multispan index for MultispanShape.prod ι when ι is linearly ordered.

                                                                                                    Equations
                                                                                                    • One or more equations did not get rendered due to their size.
                                                                                                    Instances For

                                                                                                      Given a linearly ordered type ι and I : MultispanIndex (.prod ι) C, this is the isomorphism of functors between WalkingMultispan.inclusionOfLinearOrder ι ⋙ I.multispan and I.toLinearOrder.multispan.

                                                                                                      Equations
                                                                                                      • One or more equations did not get rendered due to their size.
                                                                                                      Instances For

                                                                                                        The multicofork for I.toLinearOrder deduced from a multicofork for I : MultispanIndex (.prod ι) C when ι is linearly ordered.

                                                                                                        Equations
                                                                                                        Instances For

                                                                                                          The multicofork for I : MultispanIndex (.prod ι) C deduced from a multicofork for I.toLinearOrder when ι is linearly ordered and I is symmetric.

                                                                                                          Equations
                                                                                                          Instances For

                                                                                                            If ι is a linearly ordered type, I : MultispanIndex (.prod ι) C, and c a colimit multicofork for I, then c.toLinearOrder is a colimit multicofork for I.toLinearOrder.

                                                                                                            Equations
                                                                                                            Instances For