TOTBWF/HigherCategories.agda

## HigherCategories.agda
{-# OPTIONS --without-K --safe #-}
-- Some stuff from "Higher Operads, Higher Categories"
-- https://arxiv.org/abs/math/0305049
module MultiCategory where

open import Level
open import Data.Product using (Σ; _×_; _,_; proj₁; proj₂; uncurry)

open import Categories.Category
open import Categories.Bicategory
open import Categories.Monad
open import Categories.Diagram.Pullback

import Categories.Morphism.Reasoning as MR

HasPullbacks : ∀ {o ℓ e} (𝒞 : Category o ℓ e) → Set _
HasPullbacks 𝒞 = ∀ {X Y Z} (f : 𝒞 [ X , Z ]) (g : 𝒞 [ Y , Z ]) → Pullback 𝒞 f g

module _ {o ℓ e} {ℰ : Category o ℓ e} (has-pullbacks : HasPullbacks ℰ) (T : Monad ℰ) where
  module ℰ = Category ℰ
  module T = Monad T
  open T.F renaming (F₀ to T₀; F₁ to T₁; F-resp-≈ to T-resp-≈)
  open ℰ.HomReasoning
  open MR ℰ

  record Span (E E′ : ℰ.Obj) : Set (levelOfTerm ℰ) where
    field
      M : ℰ.Obj
      dom : ℰ [ M , T₀ E ]
      cod : ℰ [ M , E′ ]

  open Span

  record Span⇒ {E E′ : ℰ.Obj} (f g : Span E E′) : Set (levelOfTerm ℰ) where
    field
      diag : ℰ [ M f , M g ]
      commute-dom : ℰ [ ℰ [ dom g ∘ diag ] ≈ dom f ]
      commute-cod : ℰ [ ℰ [ cod g ∘ diag ] ≈ cod f ]

  open Span⇒

  ℰᵀ : Bicategory (levelOfTerm ℰ) (levelOfTerm ℰ) e o
  ℰᵀ = record
    { enriched = record
      { Obj = ℰ.Obj
      ; hom = Spans
      ; id = λ {E} → record
               { F₀ = λ _ → record
                 { M = E
                 ; dom = T.η.η E
                 ; cod = ℰ.id
                 }
               ; F₁ = λ _ → record
                 { diag = ℰ.id
                 ; commute-dom = ℰ.identityʳ
                 ; commute-cod = ℰ.identityʳ
                 }
               ; identity = ℰ.Equiv.refl
               ; homomorphism = ℰ.Equiv.sym ℰ.identity²
               ; F-resp-≈ = λ _ → ℰ.Equiv.refl
               }
      ; ⊚ = λ {E E′ E″} → {!!}
              -- record
              -- { F₀ = λ (f , g) → f ⊚₀ g
              -- ; F₁ = λ (α , β) → α ⊚₁ β
              -- ; identity = λ {(f , g)} → ⊚₁-identity f g
              -- ; homomorphism = λ {(f , g)} {(f′ , g′)} {(f″ , g″)} {(α , β)} {(α′ , β′)} → ⊚₁-homomorphism α α′ β β′
              -- ; F-resp-≈ = λ {(f , g)} {(f′ , g′)} {(α , β)} {(α′ , β′)} (α-eq , β-eq) → ⊚₁-resp-≈ α α′ β β′ α-eq β-eq
              -- }
      ; ⊚-assoc = {!!}
      ; unitˡ = {!!}
      ; unitʳ = {!!}
      }
    ; triangle = {!!}
    ; pentagon = {!!}
    }
    where
      -- The category with spans as objects, and span maps as morphisms
      Spans : ℰ.Obj → ℰ.Obj → Category (levelOfTerm ℰ) (levelOfTerm ℰ) e
      Spans E E′ = record
        { Obj = Span E E′
        ; _⇒_ = λ f g → Span⇒ f g
        ; _≈_ = λ α β → ℰ [ diag α ≈ diag β ]
        ; id = record
          { diag = ℰ.id
          ; commute-dom =  ℰ.identityʳ
          ; commute-cod = ℰ.identityʳ
          }
        ; _∘_ = λ {f g h} α β → record
          { diag = ℰ [ diag α ∘ diag β ]
          ; commute-dom = begin
            ℰ [ dom h ∘ ℰ [ diag α ∘ diag β ] ] ≈⟨ pullˡ (commute-dom α) ⟩
            ℰ [ dom g ∘ diag β ] ≈⟨ commute-dom β ⟩
            dom f ∎
          ; commute-cod = begin
            ℰ [ cod h ∘ ℰ [ diag α ∘ diag β ] ] ≈⟨ pullˡ (commute-cod α) ⟩
            ℰ [ cod g ∘ diag β ] ≈⟨ commute-cod β ⟩
            cod f ∎
          }
        ; assoc = ℰ.assoc
        ; sym-assoc = ℰ.sym-assoc
        ; identityˡ = ℰ.identityˡ
        ; identityʳ = ℰ.identityʳ
        ; identity² = ℰ.identity²
        ; equiv = record
          { refl = ℰ.Equiv.refl
          ; sym = ℰ.Equiv.sym
          ; trans = ℰ.Equiv.trans
          }
        ; ∘-resp-≈ = ℰ.∘-resp-≈
        }
      _⊚₀_ : ∀ {E E′ E″ : ℰ.Obj} → Span E′ E″ → Span E E′ → Span E E″
      _⊚₀_ {E} {E′} {E″} f g =
        let pullback : Pullback ℰ (T₁ (cod g)) (dom f)
            pullback = has-pullbacks (T₁ (cod g)) (dom f)
        in record
          { M = Pullback.P pullback
          ; dom = ℰ [ T.μ.η E ∘ ℰ [ T₁ (dom g) ∘ Pullback.p₁ pullback ] ]
          ; cod = ℰ [ cod f ∘ Pullback.p₂ pullback ]
          }

      _⊚₁_ : ∀ {E E′ E″ : ℰ.Obj} → {f f′ : Span E′ E″} → {g g′ : Span E E′} → (α : Span⇒ f f′) → (β : Span⇒ g g′) → Span⇒ (f ⊚₀ g) (f′ ⊚₀ g′)
      _⊚₁_ {E} {E′} {E″} {f} {f′} {g} {g′} α β =
        let pullback : Pullback ℰ (T₁ (cod g)) (dom f)
            pullback = has-pullbacks (T₁ (cod g)) (dom f)

            pullback′ : Pullback ℰ (T₁ (cod g′)) (dom f′)
            pullback′ = has-pullbacks (T₁ (cod g′)) (dom f′)

            chase : ℰ [ ℰ [ T₁ (cod g′) ∘ ℰ [ T₁ (diag β) ∘ Pullback.p₁ pullback ] ] ≈ ℰ [ dom f′ ∘ ℰ [ diag α ∘ Pullback.p₂ pullback ] ] ]
            chase = begin
                ℰ [ T₁ (cod g′) ∘ ℰ [ T₁ (diag β) ∘ Pullback.p₁ pullback ] ] ≈⟨ pullˡ (⟺ (T.F.homomorphism)) ⟩
                ℰ [ T₁ (ℰ [ cod g′ ∘ diag β ]) ∘ Pullback.p₁ pullback ]      ≈⟨ T-resp-≈ (commute-cod β) ⟩∘⟨refl ⟩
                ℰ [ T₁ (cod g) ∘ Pullback.p₁ pullback ]                      ≈⟨ Pullback.commute pullback ⟩
                ℰ [ dom f ∘ Pullback.p₂ pullback ]                           ≈⟨ pushˡ (⟺ (commute-dom α)) ⟩
                ℰ [ dom f′ ∘ ℰ [ diag α ∘ Pullback.p₂ pullback ] ]           ∎
        in record
          { diag = Pullback.universal pullback′ chase
          ; commute-dom = begin
            ℰ [ ℰ [ T.μ.η E ∘ ℰ [ T₁ (dom g′) ∘ Pullback.p₁ pullback′ ] ] ∘ Pullback.universal pullback′ chase ] ≈⟨ pull-last (Pullback.p₁∘universal≈h₁ pullback′) ⟩
            ℰ [ T.μ.η E ∘ ℰ [ T₁ (dom g′) ∘ ℰ [ T₁ (diag β) ∘ Pullback.p₁ pullback ] ] ]                         ≈⟨ refl⟩∘⟨ pullˡ (⟺ T.F.homomorphism) ⟩
            ℰ [ T.μ.η E ∘ ℰ [ T₁ (ℰ [ dom g′ ∘ diag β ]) ∘ Pullback.p₁ pullback ] ]                              ≈⟨ refl⟩∘⟨ (T-resp-≈ (commute-dom β)) ⟩∘⟨refl ⟩
            ℰ [ T.μ.η E ∘ ℰ [ T₁ (dom g) ∘ Pullback.p₁ pullback ] ]                                              ∎
          ; commute-cod = begin
            ℰ [ ℰ [ cod f′ ∘ Pullback.p₂ pullback′ ] ∘ Pullback.universal pullback′ chase ] ≈⟨ pullʳ (Pullback.p₂∘universal≈h₂ pullback′) ⟩
            ℰ [ cod f′ ∘ ℰ [ diag α ∘ Pullback.p₂ pullback ] ]                              ≈⟨ pullˡ (commute-cod α) ⟩
            ℰ [ cod f ∘ Pullback.p₂ pullback ]                                              ∎
          }

      ⊚₁-identity : ∀ {E E′ E″ : ℰ.Obj} → (f : Span E′ E″) → (g : Span E E′) → Spans E E″ [ Category.id (Spans E′ E″) {f} ⊚₁ Category.id (Spans E E′) {g} ≈ Category.id (Spans E E″) ]
      ⊚₁-identity {E} {E′} {E″} f g =
        let pullback = has-pullbacks (T₁ (cod g)) (dom f)
        in begin
          Pullback.universal pullback _ ≈˘⟨ Pullback.unique pullback (ℰ.identityʳ ○ introˡ T.F.identity) id-comm ⟩
          ℰ.id ∎

      ⊚₁-homomorphism : ∀ {E E′ E″ : ℰ.Obj} {f f′ f″ : Span E′ E″} {g g′ g″ : Span E E′}
                        → (α : Span⇒ f f′) → (α′ : Span⇒ f′ f″) → (β : Span⇒ g g′) → (β′ : Span⇒ g′ g″)
                        → Spans E E″ [ (Spans E′ E″ [ α′ ∘ α ]) ⊚₁ (Spans E E′ [ β′ ∘ β ]) ≈ Spans E E″ [ α′ ⊚₁ β′ ∘ α ⊚₁ β ] ]
      ⊚₁-homomorphism {E} {E′} {E″} {f} {f′} {f″} {g} {g′} {g″} α α′ β β′ =
        let pullback = has-pullbacks (T₁ (cod g)) (dom f)
            pullback′ = has-pullbacks (T₁ (cod g′)) (dom f′)
            pullback″ = has-pullbacks (T₁ (cod g″)) (dom f″)

            β-chase = begin
              ℰ [ Pullback.p₁ pullback″ ∘ ℰ [ Pullback.universal pullback″ _ ∘ Pullback.universal pullback′ _ ] ] ≈⟨ pullˡ (Pullback.p₁∘universal≈h₁ pullback″) ⟩
              ℰ [ ℰ [ T₁ (diag β′) ∘ Pullback.p₁ pullback′ ] ∘ Pullback.universal pullback′ _ ]                   ≈⟨ pullʳ (Pullback.p₁∘universal≈h₁ pullback′) ⟩
              ℰ [ T₁ (diag β′) ∘ ℰ [ T₁ (diag β) ∘ Pullback.p₁ pullback ] ]                                       ≈⟨ pullˡ (⟺ T.F.homomorphism) ⟩
              ℰ [ T₁ (diag (Spans E E′ [ β′ ∘ β ])) ∘ Pullback.p₁ pullback ]                                      ∎

            α-chase = begin
              ℰ [ Pullback.p₂ pullback″ ∘ ℰ [ Pullback.universal pullback″ _ ∘ Pullback.universal pullback′ _ ] ] ≈⟨ pullˡ (Pullback.p₂∘universal≈h₂ pullback″) ⟩
              ℰ [ ℰ [ diag α′ ∘ Pullback.p₂ pullback′ ] ∘ Pullback.universal pullback′ _ ]                        ≈⟨ pullʳ (Pullback.p₂∘universal≈h₂ pullback′) ⟩
              ℰ [ diag α′ ∘ ℰ [ diag α ∘ Pullback.p₂ pullback ] ]                                                 ≈⟨ ℰ.sym-assoc ⟩
              ℰ [ ℰ [ diag α′ ∘ diag α ] ∘ Pullback.p₂ pullback ]                                                 ∎

        in begin
          Pullback.universal pullback″ _ ≈˘⟨ Pullback.unique pullback″ β-chase α-chase ⟩
          ℰ [ Pullback.universal pullback″ _ ∘ Pullback.universal pullback′ _ ] ∎

      ⊚₁-resp-≈ : ∀ {E E′ E″ : ℰ.Obj} {f f′ : Span E′ E″} {g g′ : Span E E′} (α α′ : Span⇒ f f′) (β β′ : Span⇒ g g′)
                  → (α-eq : Spans E′ E″ [ α ≈ α′ ]) → (β-eq : Spans E E′ [ β ≈ β′ ]) → Spans E E″ [ α ⊚₁ β ≈ α′ ⊚₁ β′ ]
      ⊚₁-resp-≈ {E} {E′} {E″} {f} {f′} {g} {g′} α α′ β β′ α-eq β-eq =
        let pullback′ = has-pullbacks (T₁ (cod g′)) (dom f′)
        in Pullback.universal-resp-≈ pullback′ (ℰ.∘-resp-≈ˡ (T-resp-≈ β-eq)) (ℰ.∘-resp-≈ˡ α-eq)
	{-# OPTIONS --without-K --safe #-}
	-- Some stuff from "Higher Operads, Higher Categories"
	-- https://arxiv.org/abs/math/0305049
	module MultiCategory where

	open import Level
	open import Data.Product using (Σ; _×_; _,_; proj₁; proj₂; uncurry)

	open import Categories.Category
	open import Categories.Bicategory
	open import Categories.Monad
	open import Categories.Diagram.Pullback

	import Categories.Morphism.Reasoning as MR

	HasPullbacks : ∀ {o ℓ e} (𝒞 : Category o ℓ e) → Set _
	HasPullbacks 𝒞 = ∀ {X Y Z} (f : 𝒞 [ X , Z ]) (g : 𝒞 [ Y , Z ]) → Pullback 𝒞 f g

	module _ {o ℓ e} {ℰ : Category o ℓ e} (has-pullbacks : HasPullbacks ℰ) (T : Monad ℰ) where
	module ℰ = Category ℰ
	module T = Monad T
	open T.F renaming (F₀ to T₀; F₁ to T₁; F-resp-≈ to T-resp-≈)
	open ℰ.HomReasoning
	open MR ℰ

	record Span (E E′ : ℰ.Obj) : Set (levelOfTerm ℰ) where
	field
	M : ℰ.Obj
	dom : ℰ [ M , T₀ E ]
	cod : ℰ [ M , E′ ]

	open Span

	record Span⇒ {E E′ : ℰ.Obj} (f g : Span E E′) : Set (levelOfTerm ℰ) where
	field
	diag : ℰ [ M f , M g ]
	commute-dom : ℰ [ ℰ [ dom g ∘ diag ] ≈ dom f ]
	commute-cod : ℰ [ ℰ [ cod g ∘ diag ] ≈ cod f ]

	open Span⇒

	ℰᵀ : Bicategory (levelOfTerm ℰ) (levelOfTerm ℰ) e o
	ℰᵀ = record
	{ enriched = record
	{ Obj = ℰ.Obj
	; hom = Spans
	; id = λ {E} → record
	{ F₀ = λ _ → record
	{ M = E
	; dom = T.η.η E
	; cod = ℰ.id
	}
	; F₁ = λ _ → record
	{ diag = ℰ.id
	; commute-dom = ℰ.identityʳ
	; commute-cod = ℰ.identityʳ
	}
	; identity = ℰ.Equiv.refl
	; homomorphism = ℰ.Equiv.sym ℰ.identity²
	; F-resp-≈ = λ _ → ℰ.Equiv.refl
	}
	; ⊚ = λ {E E′ E″} → {!!}
	-- record
	-- { F₀ = λ (f , g) → f ⊚₀ g
	-- ; F₁ = λ (α , β) → α ⊚₁ β
	-- ; identity = λ {(f , g)} → ⊚₁-identity f g
	-- ; homomorphism = λ {(f , g)} {(f′ , g′)} {(f″ , g″)} {(α , β)} {(α′ , β′)} → ⊚₁-homomorphism α α′ β β′
	-- ; F-resp-≈ = λ {(f , g)} {(f′ , g′)} {(α , β)} {(α′ , β′)} (α-eq , β-eq) → ⊚₁-resp-≈ α α′ β β′ α-eq β-eq
	-- }
	; ⊚-assoc = {!!}
	; unitˡ = {!!}
	; unitʳ = {!!}
	}
	; triangle = {!!}
	; pentagon = {!!}
	}
	where
	-- The category with spans as objects, and span maps as morphisms
	Spans : ℰ.Obj → ℰ.Obj → Category (levelOfTerm ℰ) (levelOfTerm ℰ) e
	Spans E E′ = record
	{ Obj = Span E E′
	; _⇒_ = λ f g → Span⇒ f g
	; _≈_ = λ α β → ℰ [ diag α ≈ diag β ]
	; id = record
	{ diag = ℰ.id
	; commute-dom = ℰ.identityʳ
	; commute-cod = ℰ.identityʳ
	}
	; _∘_ = λ {f g h} α β → record
	{ diag = ℰ [ diag α ∘ diag β ]
	; commute-dom = begin
	ℰ [ dom h ∘ ℰ [ diag α ∘ diag β ] ] ≈⟨ pullˡ (commute-dom α) ⟩
	ℰ [ dom g ∘ diag β ] ≈⟨ commute-dom β ⟩
	dom f ∎
	; commute-cod = begin
	ℰ [ cod h ∘ ℰ [ diag α ∘ diag β ] ] ≈⟨ pullˡ (commute-cod α) ⟩
	ℰ [ cod g ∘ diag β ] ≈⟨ commute-cod β ⟩
	cod f ∎
	}
	; assoc = ℰ.assoc
	; sym-assoc = ℰ.sym-assoc
	; identityˡ = ℰ.identityˡ
	; identityʳ = ℰ.identityʳ
	; identity² = ℰ.identity²
	; equiv = record
	{ refl = ℰ.Equiv.refl
	; sym = ℰ.Equiv.sym
	; trans = ℰ.Equiv.trans
	}
	; ∘-resp-≈ = ℰ.∘-resp-≈
	}
	_⊚₀_ : ∀ {E E′ E″ : ℰ.Obj} → Span E′ E″ → Span E E′ → Span E E″
	_⊚₀_ {E} {E′} {E″} f g =
	let pullback : Pullback ℰ (T₁ (cod g)) (dom f)
	pullback = has-pullbacks (T₁ (cod g)) (dom f)
	in record
	{ M = Pullback.P pullback
	; dom = ℰ [ T.μ.η E ∘ ℰ [ T₁ (dom g) ∘ Pullback.p₁ pullback ] ]
	; cod = ℰ [ cod f ∘ Pullback.p₂ pullback ]
	}

	_⊚₁_ : ∀ {E E′ E″ : ℰ.Obj} → {f f′ : Span E′ E″} → {g g′ : Span E E′} → (α : Span⇒ f f′) → (β : Span⇒ g g′) → Span⇒ (f ⊚₀ g) (f′ ⊚₀ g′)
	_⊚₁_ {E} {E′} {E″} {f} {f′} {g} {g′} α β =
	let pullback : Pullback ℰ (T₁ (cod g)) (dom f)
	pullback = has-pullbacks (T₁ (cod g)) (dom f)

	pullback′ : Pullback ℰ (T₁ (cod g′)) (dom f′)
	pullback′ = has-pullbacks (T₁ (cod g′)) (dom f′)

	chase : ℰ [ ℰ [ T₁ (cod g′) ∘ ℰ [ T₁ (diag β) ∘ Pullback.p₁ pullback ] ] ≈ ℰ [ dom f′ ∘ ℰ [ diag α ∘ Pullback.p₂ pullback ] ] ]
	chase = begin
	ℰ [ T₁ (cod g′) ∘ ℰ [ T₁ (diag β) ∘ Pullback.p₁ pullback ] ] ≈⟨ pullˡ (⟺ (T.F.homomorphism)) ⟩
	ℰ [ T₁ (ℰ [ cod g′ ∘ diag β ]) ∘ Pullback.p₁ pullback ] ≈⟨ T-resp-≈ (commute-cod β) ⟩∘⟨refl ⟩
	ℰ [ T₁ (cod g) ∘ Pullback.p₁ pullback ] ≈⟨ Pullback.commute pullback ⟩
	ℰ [ dom f ∘ Pullback.p₂ pullback ] ≈⟨ pushˡ (⟺ (commute-dom α)) ⟩
	ℰ [ dom f′ ∘ ℰ [ diag α ∘ Pullback.p₂ pullback ] ] ∎
	in record
	{ diag = Pullback.universal pullback′ chase
	; commute-dom = begin
	ℰ [ ℰ [ T.μ.η E ∘ ℰ [ T₁ (dom g′) ∘ Pullback.p₁ pullback′ ] ] ∘ Pullback.universal pullback′ chase ] ≈⟨ pull-last (Pullback.p₁∘universal≈h₁ pullback′) ⟩
	ℰ [ T.μ.η E ∘ ℰ [ T₁ (dom g′) ∘ ℰ [ T₁ (diag β) ∘ Pullback.p₁ pullback ] ] ] ≈⟨ refl⟩∘⟨ pullˡ (⟺ T.F.homomorphism) ⟩
	ℰ [ T.μ.η E ∘ ℰ [ T₁ (ℰ [ dom g′ ∘ diag β ]) ∘ Pullback.p₁ pullback ] ] ≈⟨ refl⟩∘⟨ (T-resp-≈ (commute-dom β)) ⟩∘⟨refl ⟩
	ℰ [ T.μ.η E ∘ ℰ [ T₁ (dom g) ∘ Pullback.p₁ pullback ] ] ∎
	; commute-cod = begin
	ℰ [ ℰ [ cod f′ ∘ Pullback.p₂ pullback′ ] ∘ Pullback.universal pullback′ chase ] ≈⟨ pullʳ (Pullback.p₂∘universal≈h₂ pullback′) ⟩
	ℰ [ cod f′ ∘ ℰ [ diag α ∘ Pullback.p₂ pullback ] ] ≈⟨ pullˡ (commute-cod α) ⟩
	ℰ [ cod f ∘ Pullback.p₂ pullback ] ∎
	}

	⊚₁-identity : ∀ {E E′ E″ : ℰ.Obj} → (f : Span E′ E″) → (g : Span E E′) → Spans E E″ [ Category.id (Spans E′ E″) {f} ⊚₁ Category.id (Spans E E′) {g} ≈ Category.id (Spans E E″) ]
	⊚₁-identity {E} {E′} {E″} f g =
	let pullback = has-pullbacks (T₁ (cod g)) (dom f)
	in begin
	Pullback.universal pullback _ ≈˘⟨ Pullback.unique pullback (ℰ.identityʳ ○ introˡ T.F.identity) id-comm ⟩
	ℰ.id ∎

	⊚₁-homomorphism : ∀ {E E′ E″ : ℰ.Obj} {f f′ f″ : Span E′ E″} {g g′ g″ : Span E E′}
	→ (α : Span⇒ f f′) → (α′ : Span⇒ f′ f″) → (β : Span⇒ g g′) → (β′ : Span⇒ g′ g″)
	→ Spans E E″ [ (Spans E′ E″ [ α′ ∘ α ]) ⊚₁ (Spans E E′ [ β′ ∘ β ]) ≈ Spans E E″ [ α′ ⊚₁ β′ ∘ α ⊚₁ β ] ]
	⊚₁-homomorphism {E} {E′} {E″} {f} {f′} {f″} {g} {g′} {g″} α α′ β β′ =
	let pullback = has-pullbacks (T₁ (cod g)) (dom f)
	pullback′ = has-pullbacks (T₁ (cod g′)) (dom f′)
	pullback″ = has-pullbacks (T₁ (cod g″)) (dom f″)

	β-chase = begin
	ℰ [ Pullback.p₁ pullback″ ∘ ℰ [ Pullback.universal pullback″ _ ∘ Pullback.universal pullback′ _ ] ] ≈⟨ pullˡ (Pullback.p₁∘universal≈h₁ pullback″) ⟩
	ℰ [ ℰ [ T₁ (diag β′) ∘ Pullback.p₁ pullback′ ] ∘ Pullback.universal pullback′ _ ] ≈⟨ pullʳ (Pullback.p₁∘universal≈h₁ pullback′) ⟩
	ℰ [ T₁ (diag β′) ∘ ℰ [ T₁ (diag β) ∘ Pullback.p₁ pullback ] ] ≈⟨ pullˡ (⟺ T.F.homomorphism) ⟩
	ℰ [ T₁ (diag (Spans E E′ [ β′ ∘ β ])) ∘ Pullback.p₁ pullback ] ∎

	α-chase = begin
	ℰ [ Pullback.p₂ pullback″ ∘ ℰ [ Pullback.universal pullback″ _ ∘ Pullback.universal pullback′ _ ] ] ≈⟨ pullˡ (Pullback.p₂∘universal≈h₂ pullback″) ⟩
	ℰ [ ℰ [ diag α′ ∘ Pullback.p₂ pullback′ ] ∘ Pullback.universal pullback′ _ ] ≈⟨ pullʳ (Pullback.p₂∘universal≈h₂ pullback′) ⟩
	ℰ [ diag α′ ∘ ℰ [ diag α ∘ Pullback.p₂ pullback ] ] ≈⟨ ℰ.sym-assoc ⟩
	ℰ [ ℰ [ diag α′ ∘ diag α ] ∘ Pullback.p₂ pullback ] ∎

	in begin
	Pullback.universal pullback″ _ ≈˘⟨ Pullback.unique pullback″ β-chase α-chase ⟩
	ℰ [ Pullback.universal pullback″ _ ∘ Pullback.universal pullback′ _ ] ∎

	⊚₁-resp-≈ : ∀ {E E′ E″ : ℰ.Obj} {f f′ : Span E′ E″} {g g′ : Span E E′} (α α′ : Span⇒ f f′) (β β′ : Span⇒ g g′)
	→ (α-eq : Spans E′ E″ [ α ≈ α′ ]) → (β-eq : Spans E E′ [ β ≈ β′ ]) → Spans E E″ [ α ⊚₁ β ≈ α′ ⊚₁ β′ ]
	⊚₁-resp-≈ {E} {E′} {E″} {f} {f′} {g} {g′} α α′ β β′ α-eq β-eq =
	let pullback′ = has-pullbacks (T₁ (cod g′)) (dom f′)
	in Pullback.universal-resp-≈ pullback′ (ℰ.∘-resp-≈ˡ (T-resp-≈ β-eq)) (ℰ.∘-resp-≈ˡ α-eq)