diff --git a/src/Categories/Bicategory/Construction/Spans.agda b/src/Categories/Bicategory/Construction/Spans.agda
new file mode 100644
index 000000000..b62a5452b
--- /dev/null
+++ b/src/Categories/Bicategory/Construction/Spans.agda
@@ -0,0 +1,374 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Categories.Category
+open import Categories.Diagram.Pullback
+
+module Categories.Bicategory.Construction.Spans {o ℓ e} {𝒞 : Category o ℓ e}
+                                                (_×ₚ_ : ∀ {X Y Z} → (f : 𝒞 [ X , Z ]) (g : 𝒞 [ Y , Z ]) → Pullback 𝒞 f g) where
+
+open import Level
+open import Function using (_$_)
+
+open import Data.Product using (Σ; _×_; _,_; proj₁; proj₂; uncurry)
+
+open import Categories.Bicategory
+open import Categories.NaturalTransformation.NaturalIsomorphism hiding (refl; sym)
+
+open import Categories.Category.Diagram.Span 𝒞
+open import Categories.Category.Construction.Spans 𝒞 renaming (Spans to Spans₁)
+
+open import Categories.Morphism
+open import Categories.Morphism.Reasoning 𝒞
+
+private
+  module Spans₁ X Y = Category (Spans₁ X Y)
+
+open Category 𝒞
+open HomReasoning
+open Equiv
+
+open Span
+open Span⇒
+open Pullback
+
+open Compositions _×ₚ_
+
+private
+  variable
+    A B C D E : Obj
+
+  --------------------------------------------------------------------------------
+  -- Proofs about span compositions
+
+⊚₁-identity : ∀ (f : Span B C) → (g : Span A B) → Spans₁ A C [ Spans₁.id B C {f} ⊚₁ Spans₁.id A B {g} ≈ Spans₁.id A C ]
+⊚₁-identity f g = ⟺ (unique ((cod g) ×ₚ (dom f)) id-comm id-comm)
+
+⊚₁-homomorphism : {f f′ f″ : Span B C} {g g′ g″ : Span A B}
+                  → (α : Span⇒ f f′) → (α′ : Span⇒ f′ f″)
+                  → (β : Span⇒ g g′) → (β′ : Span⇒ g′ g″)
+                  → Spans₁ A C [ (Spans₁ B C [ α′ ∘ α ]) ⊚₁ (Spans₁ A B [ β′ ∘ β ]) ≈ Spans₁ A C [ α′ ⊚₁ β′ ∘ α ⊚₁ β ] ]
+⊚₁-homomorphism {A} {B} {C} {f} {f′} {f″} {g} {g′} {g″} α α′ β β′ =
+  let pullback  = (cod g) ×ₚ (dom f)
+      pullback′ = (cod g′) ×ₚ(dom f′)
+      pullback″ = (cod g″) ×ₚ (dom f″)
+      α-chase = begin
+        p₂ pullback″ ∘ universal pullback″ _ ∘ universal pullback′ _ ≈⟨ pullˡ (p₂∘universal≈h₂ pullback″) ⟩
+        (arr α′ ∘ p₂ pullback′) ∘ universal pullback′ _ ≈⟨ extendˡ (p₂∘universal≈h₂ pullback′) ⟩
+        (arr α′ ∘ arr α) ∘ p₂ pullback ∎
+      β-chase = begin
+        p₁ pullback″ ∘ universal pullback″ _ ∘ universal pullback′ _            ≈⟨ pullˡ (p₁∘universal≈h₁ pullback″) ⟩
+        (arr β′ ∘ p₁ pullback′) ∘ universal pullback′ _ ≈⟨ extendˡ (p₁∘universal≈h₁ pullback′) ⟩
+        (arr β′ ∘ arr β) ∘ p₁ pullback                                          ∎
+  in ⟺ (unique pullback″ β-chase α-chase)
+
+--------------------------------------------------------------------------------
+-- Associators
+
+module _ (f : Span C D) (g : Span B C) (h : Span A B) where
+  private
+    pullback-fg    = (cod g) ×ₚ (dom f)
+    pullback-gh    = (cod h) ×ₚ (dom g)
+    pullback-⟨fg⟩h = (cod h) ×ₚ (dom (f ⊚₀ g))
+    pullback-f⟨gh⟩ = (cod (g ⊚₀ h)) ×ₚ (dom f)
+
+  ⊚-assoc : Span⇒ ((f ⊚₀ g) ⊚₀ h) (f ⊚₀ (g ⊚₀ h))
+  ⊚-assoc = record
+    { arr = universal pullback-f⟨gh⟩ {h₁ = universal pullback-gh (commute pullback-⟨fg⟩h ○ assoc)} $ begin
+        (cod g ∘ p₂ pullback-gh) ∘ universal pullback-gh _ ≈⟨ pullʳ (p₂∘universal≈h₂ pullback-gh) ⟩
+        cod g ∘ p₁ pullback-fg ∘ p₂ pullback-⟨fg⟩h         ≈⟨ extendʳ (commute pullback-fg) ⟩
+        dom f ∘ p₂ pullback-fg ∘ p₂ pullback-⟨fg⟩h         ∎
+    ; commute-dom = begin
+        ((dom h ∘ p₁ pullback-gh) ∘ p₁ pullback-f⟨gh⟩) ∘ universal pullback-f⟨gh⟩ _ ≈⟨ pullʳ (p₁∘universal≈h₁ pullback-f⟨gh⟩) ⟩
+        (dom h ∘ p₁ pullback-gh) ∘ universal pullback-gh _                          ≈⟨ pullʳ (p₁∘universal≈h₁ pullback-gh) ⟩
+        dom h ∘ p₁ pullback-⟨fg⟩h                                                   ∎
+    ; commute-cod = begin
+        (cod f ∘ p₂ pullback-f⟨gh⟩) ∘ universal pullback-f⟨gh⟩ _ ≈⟨ extendˡ (p₂∘universal≈h₂ pullback-f⟨gh⟩) ⟩
+        (cod f ∘ p₂ pullback-fg) ∘ p₂ pullback-⟨fg⟩h             ∎
+    }
+
+  ⊚-assoc⁻¹ :  Span⇒ (f ⊚₀ (g ⊚₀ h)) ((f ⊚₀ g) ⊚₀ h)
+  ⊚-assoc⁻¹ = record
+    { arr = universal pullback-⟨fg⟩h {h₁ = p₁ pullback-gh ∘ p₁ pullback-f⟨gh⟩} {h₂ = universal pullback-fg (⟺ assoc ○ commute pullback-f⟨gh⟩)} $ begin
+        cod h ∘ p₁ pullback-gh ∘ p₁ pullback-f⟨gh⟩         ≈⟨ extendʳ (commute pullback-gh) ⟩
+        dom g ∘ p₂ pullback-gh ∘ p₁ pullback-f⟨gh⟩         ≈⟨ pushʳ (⟺ (p₁∘universal≈h₁ pullback-fg)) ⟩
+        (dom g ∘ p₁ pullback-fg) ∘ universal pullback-fg _ ∎
+      ; commute-dom = begin
+        (dom h ∘ p₁ pullback-⟨fg⟩h) ∘ universal pullback-⟨fg⟩h _ ≈⟨ extendˡ (p₁∘universal≈h₁ pullback-⟨fg⟩h) ⟩
+        (dom h ∘ p₁ pullback-gh) ∘ p₁ pullback-f⟨gh⟩             ∎
+    ; commute-cod = begin
+        ((cod f ∘ p₂ pullback-fg) ∘ p₂ pullback-⟨fg⟩h) ∘ universal pullback-⟨fg⟩h _ ≈⟨ pullʳ (p₂∘universal≈h₂ pullback-⟨fg⟩h) ⟩
+        (cod f ∘ p₂ pullback-fg) ∘ universal pullback-fg _                          ≈⟨ pullʳ (p₂∘universal≈h₂ pullback-fg) ⟩
+        cod f ∘ p₂ pullback-f⟨gh⟩                                                   ∎
+    }
+
+  ⊚-assoc-iso : Iso (Spans₁ A D) ⊚-assoc ⊚-assoc⁻¹
+  ⊚-assoc-iso = record
+    { isoˡ =
+      let lemma-fgˡ = begin
+            p₁ pullback-fg ∘ universal pullback-fg _ ∘ universal pullback-f⟨gh⟩ _ ≈⟨ pullˡ (p₁∘universal≈h₁ pullback-fg) ⟩
+            (p₂ pullback-gh ∘ p₁ pullback-f⟨gh⟩) ∘ universal pullback-f⟨gh⟩ _     ≈⟨ pullʳ (p₁∘universal≈h₁ pullback-f⟨gh⟩) ⟩
+            p₂ pullback-gh ∘ universal pullback-gh _                              ≈⟨ p₂∘universal≈h₂ pullback-gh ⟩
+            p₁ pullback-fg ∘ p₂ pullback-⟨fg⟩h                                    ∎
+
+          lemma-fgʳ = begin
+            p₂ pullback-fg ∘ universal pullback-fg _ ∘ universal pullback-f⟨gh⟩ _ ≈⟨ pullˡ (p₂∘universal≈h₂ pullback-fg) ⟩
+            p₂ pullback-f⟨gh⟩ ∘ universal pullback-f⟨gh⟩ _                        ≈⟨ p₂∘universal≈h₂ pullback-f⟨gh⟩ ⟩
+            p₂ pullback-fg ∘ p₂ pullback-⟨fg⟩h                                    ∎
+
+          lemmaˡ = begin
+            p₁ pullback-⟨fg⟩h ∘ universal pullback-⟨fg⟩h _ ∘ universal pullback-f⟨gh⟩ _ ≈⟨ pullˡ (p₁∘universal≈h₁ pullback-⟨fg⟩h) ⟩
+            (p₁ pullback-gh ∘ p₁ pullback-f⟨gh⟩) ∘ universal pullback-f⟨gh⟩ _           ≈⟨ pullʳ (p₁∘universal≈h₁ pullback-f⟨gh⟩) ⟩
+            p₁ pullback-gh ∘ universal pullback-gh _                                    ≈⟨ p₁∘universal≈h₁ pullback-gh ⟩
+            p₁ pullback-⟨fg⟩h                                                           ∎
+
+          lemmaʳ = begin
+            p₂ pullback-⟨fg⟩h ∘ universal pullback-⟨fg⟩h _ ∘ universal pullback-f⟨gh⟩ _ ≈⟨ pullˡ (p₂∘universal≈h₂ pullback-⟨fg⟩h) ⟩
+            universal pullback-fg _ ∘ universal pullback-f⟨gh⟩ _                        ≈⟨ unique-diagram pullback-fg lemma-fgˡ lemma-fgʳ ⟩
+            p₂ pullback-⟨fg⟩h                                                           ∎
+      in unique pullback-⟨fg⟩h lemmaˡ lemmaʳ ○ ⟺ (Pullback.id-unique pullback-⟨fg⟩h)
+    ; isoʳ =
+      let lemma-ghˡ = begin
+            p₁ pullback-gh ∘ universal pullback-gh _ ∘ universal pullback-⟨fg⟩h _ ≈⟨  pullˡ (p₁∘universal≈h₁ pullback-gh) ⟩
+            p₁ pullback-⟨fg⟩h ∘ universal pullback-⟨fg⟩h _                        ≈⟨  p₁∘universal≈h₁ pullback-⟨fg⟩h ⟩
+            p₁ pullback-gh ∘ p₁ pullback-f⟨gh⟩                                    ∎
+
+          lemma-ghʳ = begin
+            p₂ pullback-gh ∘ universal pullback-gh _ ∘ universal pullback-⟨fg⟩h _ ≈⟨ pullˡ (p₂∘universal≈h₂ pullback-gh) ⟩
+            (p₁ pullback-fg ∘ p₂ pullback-⟨fg⟩h) ∘ universal pullback-⟨fg⟩h _     ≈⟨ pullʳ (p₂∘universal≈h₂ pullback-⟨fg⟩h) ⟩
+            p₁ pullback-fg ∘ universal pullback-fg _                              ≈⟨ p₁∘universal≈h₁ pullback-fg ⟩
+            p₂ pullback-gh ∘ p₁ pullback-f⟨gh⟩ ∎ 
+
+          lemmaˡ = begin
+            p₁ pullback-f⟨gh⟩ ∘ universal pullback-f⟨gh⟩ _ ∘ universal pullback-⟨fg⟩h _ ≈⟨ pullˡ (p₁∘universal≈h₁ pullback-f⟨gh⟩) ⟩
+            universal pullback-gh _ ∘ universal pullback-⟨fg⟩h _                        ≈⟨ unique-diagram pullback-gh lemma-ghˡ lemma-ghʳ ⟩
+            p₁ pullback-f⟨gh⟩                                                           ∎
+          lemmaʳ = begin
+            p₂ pullback-f⟨gh⟩ ∘ universal pullback-f⟨gh⟩ _ ∘ universal pullback-⟨fg⟩h _ ≈⟨ pullˡ (p₂∘universal≈h₂ pullback-f⟨gh⟩) ⟩
+            (p₂ pullback-fg ∘ p₂ pullback-⟨fg⟩h) ∘ universal pullback-⟨fg⟩h _           ≈⟨ pullʳ (p₂∘universal≈h₂ pullback-⟨fg⟩h) ⟩
+            p₂ pullback-fg ∘ universal pullback-fg _                                    ≈⟨ p₂∘universal≈h₂ pullback-fg ⟩
+            p₂ pullback-f⟨gh⟩                                                           ∎
+      in unique pullback-f⟨gh⟩ lemmaˡ lemmaʳ ○ ⟺ (Pullback.id-unique pullback-f⟨gh⟩)
+    }
+
+⊚-assoc-commute : ∀ {f f′ : Span C D} {g g′ : Span B C} {h h′ : Span A B} → (α : Span⇒ f f′) → (β : Span⇒ g g′) → (γ : Span⇒ h h′)
+            → Spans₁ A D [ Spans₁ A D [ ⊚-assoc f′ g′ h′ ∘ (α ⊚₁ β) ⊚₁ γ ] ≈ Spans₁ A D [ α ⊚₁ (β ⊚₁ γ) ∘ ⊚-assoc f g h ] ]
+⊚-assoc-commute {f = f} {f′ = f′} {g = g} {g′ = g′} {h = h} {h′ = h′} α β γ =
+  let pullback-fg     = (cod g) ×ₚ (dom f)
+      pullback-fg′    = (cod g′) ×ₚ (dom f′)
+      pullback-gh     = (cod h) ×ₚ (dom g)
+      pullback-gh′    = (cod h′) ×ₚ (dom g′)
+      pullback-f⟨gh⟩  = (cod (g ⊚₀ h)) ×ₚ (dom f)
+      pullback-f⟨gh⟩′ = (cod (g′ ⊚₀ h′)) ×ₚ (dom f′)
+      pullback-⟨fg⟩h  = (cod h) ×ₚ (dom (f ⊚₀ g))
+      pullback-⟨fg⟩h′ = (cod h′) ×ₚ (dom (f′ ⊚₀ g′))
+
+      lemma-ghˡ′ = begin
+        p₁ pullback-gh′ ∘ universal pullback-gh′ _ ∘ universal pullback-⟨fg⟩h′ _ ≈⟨ pullˡ (p₁∘universal≈h₁ pullback-gh′) ⟩
+        p₁ pullback-⟨fg⟩h′ ∘ universal pullback-⟨fg⟩h′ _                         ≈⟨ p₁∘universal≈h₁ pullback-⟨fg⟩h′ ⟩
+        arr γ ∘ p₁ pullback-⟨fg⟩h                                                ≈⟨ pushʳ (⟺ (p₁∘universal≈h₁ pullback-gh)) ⟩
+        (arr γ ∘ p₁ pullback-gh) ∘ universal pullback-gh _                       ≈⟨ pushˡ (⟺ (p₁∘universal≈h₁ pullback-gh′)) ⟩
+        p₁ pullback-gh′ ∘ universal pullback-gh′ _ ∘ universal pullback-gh _     ∎
+
+      lemma-ghʳ′ = begin
+        p₂ pullback-gh′ ∘ universal pullback-gh′ _ ∘ universal pullback-⟨fg⟩h′ _ ≈⟨ pullˡ (p₂∘universal≈h₂ pullback-gh′) ⟩
+        (p₁ pullback-fg′ ∘ p₂ pullback-⟨fg⟩h′) ∘ universal pullback-⟨fg⟩h′ _     ≈⟨ pullʳ (p₂∘universal≈h₂ pullback-⟨fg⟩h′) ⟩
+        p₁ pullback-fg′ ∘ universal pullback-fg′ _ ∘ p₂ pullback-⟨fg⟩h           ≈⟨ pullˡ (p₁∘universal≈h₁ pullback-fg′) ⟩
+        (arr β ∘ p₁ pullback-fg) ∘ p₂ pullback-⟨fg⟩h                             ≈⟨ extendˡ (⟺ (p₂∘universal≈h₂ pullback-gh)) ⟩
+        (arr β ∘ p₂ pullback-gh) ∘ universal pullback-gh _                       ≈⟨ pushˡ (⟺ (p₂∘universal≈h₂ pullback-gh′)) ⟩
+        p₂ pullback-gh′ ∘ universal pullback-gh′ _ ∘ universal pullback-gh _     ∎
+
+      lemmaˡ = begin
+        p₁ pullback-f⟨gh⟩′ ∘ universal pullback-f⟨gh⟩′ _ ∘ universal pullback-⟨fg⟩h′ _ ≈⟨ pullˡ (p₁∘universal≈h₁ pullback-f⟨gh⟩′) ⟩
+        universal pullback-gh′ _ ∘ universal pullback-⟨fg⟩h′ _                         ≈⟨ unique-diagram pullback-gh′ lemma-ghˡ′ lemma-ghʳ′ ⟩
+        universal pullback-gh′ _ ∘ universal pullback-gh _                             ≈⟨ pushʳ (⟺ (p₁∘universal≈h₁ pullback-f⟨gh⟩)) ⟩
+        (universal pullback-gh′ _ ∘ p₁ pullback-f⟨gh⟩) ∘ universal pullback-f⟨gh⟩ _    ≈⟨ pushˡ (⟺ (p₁∘universal≈h₁ pullback-f⟨gh⟩′)) ⟩
+        p₁ pullback-f⟨gh⟩′ ∘ universal pullback-f⟨gh⟩′ _ ∘ universal pullback-f⟨gh⟩ _  ∎
+
+      lemmaʳ = begin
+        p₂ pullback-f⟨gh⟩′ ∘ universal pullback-f⟨gh⟩′ _ ∘ universal pullback-⟨fg⟩h′ _ ≈⟨ pullˡ (p₂∘universal≈h₂ pullback-f⟨gh⟩′) ⟩
+        (p₂ pullback-fg′ ∘ p₂ pullback-⟨fg⟩h′) ∘ universal pullback-⟨fg⟩h′ _           ≈⟨ pullʳ (p₂∘universal≈h₂ pullback-⟨fg⟩h′) ⟩
+        p₂ pullback-fg′ ∘ universal pullback-fg′ _ ∘ p₂ pullback-⟨fg⟩h                 ≈⟨ pullˡ (p₂∘universal≈h₂ pullback-fg′) ⟩
+        (arr α ∘ p₂ pullback-fg) ∘ p₂ pullback-⟨fg⟩h                                   ≈⟨ extendˡ (⟺ (p₂∘universal≈h₂ pullback-f⟨gh⟩)) ⟩
+        (arr α ∘ p₂ pullback-f⟨gh⟩) ∘ universal pullback-f⟨gh⟩ _                       ≈⟨ pushˡ (⟺ (p₂∘universal≈h₂ pullback-f⟨gh⟩′)) ⟩
+        p₂ pullback-f⟨gh⟩′ ∘ universal pullback-f⟨gh⟩′ _ ∘ universal pullback-f⟨gh⟩ _  ∎
+
+  in unique-diagram pullback-f⟨gh⟩′ lemmaˡ lemmaʳ
+
+
+--------------------------------------------------------------------------------
+-- Unitors
+
+module _ (f : Span A B) where
+  private
+    pullback-dom-f = id ×ₚ (dom f)
+    pullback-cod-f = (cod f) ×ₚ id
+
+  ⊚-unitˡ : Span⇒ (id-span ⊚₀ f) f
+  ⊚-unitˡ = record
+    { arr = p₁ pullback-cod-f
+    ; commute-dom = refl
+    ; commute-cod = commute pullback-cod-f
+    }
+
+  ⊚-unitˡ⁻¹ : Span⇒ f (id-span ⊚₀ f)
+  ⊚-unitˡ⁻¹ = record
+    { arr = universal pullback-cod-f id-comm
+    ; commute-dom = cancelʳ (p₁∘universal≈h₁ pullback-cod-f)
+    ; commute-cod = pullʳ (p₂∘universal≈h₂ pullback-cod-f) ○ identityˡ
+    }
+
+  ⊚-unitˡ-iso : Iso (Spans₁ A B) ⊚-unitˡ ⊚-unitˡ⁻¹
+  ⊚-unitˡ-iso = record
+    { isoˡ = unique-diagram pullback-cod-f (pullˡ (p₁∘universal≈h₁ pullback-cod-f) ○ id-comm-sym) (pullˡ (p₂∘universal≈h₂ pullback-cod-f) ○ commute pullback-cod-f ○ id-comm-sym)
+    ; isoʳ = p₁∘universal≈h₁ pullback-cod-f
+    }
+
+  ⊚-unitʳ : Span⇒ (f ⊚₀ id-span) f
+  ⊚-unitʳ = record
+    { arr = p₂ pullback-dom-f
+    ; commute-dom = ⟺ (commute pullback-dom-f)
+    ; commute-cod = refl
+    }
+
+  ⊚-unitʳ⁻¹ : Span⇒ f (f ⊚₀ id-span)
+  ⊚-unitʳ⁻¹ = record
+    { arr = universal pullback-dom-f id-comm-sym
+    ; commute-dom = pullʳ (p₁∘universal≈h₁ pullback-dom-f) ○ identityˡ
+    ; commute-cod = pullʳ (p₂∘universal≈h₂ pullback-dom-f) ○ identityʳ
+    }
+
+  ⊚-unitʳ-iso : Iso (Spans₁ A B) ⊚-unitʳ ⊚-unitʳ⁻¹
+  ⊚-unitʳ-iso = record
+    { isoˡ = unique-diagram pullback-dom-f (pullˡ (p₁∘universal≈h₁ pullback-dom-f) ○ ⟺ (commute pullback-dom-f) ○ id-comm-sym) (pullˡ (p₂∘universal≈h₂ pullback-dom-f) ○ id-comm-sym)
+    ; isoʳ = p₂∘universal≈h₂ pullback-dom-f
+    }
+
+⊚-unitˡ-commute : ∀ {f f′ : Span A B} → (α : Span⇒ f f′) → Spans₁ A B [ Spans₁ A B [ ⊚-unitˡ f′ ∘ Spans₁.id B B ⊚₁ α ] ≈ Spans₁ A B [ α ∘ ⊚-unitˡ f ] ]
+⊚-unitˡ-commute {f′ = f′} α = p₁∘universal≈h₁ ((cod f′) ×ₚ id)
+
+⊚-unitʳ-commute : ∀ {f f′ : Span A B} → (α : Span⇒ f f′) → Spans₁ A B [ Spans₁ A B [ ⊚-unitʳ f′ ∘ α ⊚₁ Spans₁.id A A ] ≈ Spans₁ A B [ α ∘ ⊚-unitʳ f ] ]
+⊚-unitʳ-commute {f′ = f′} α = p₂∘universal≈h₂ (id ×ₚ (dom f′))
+
+--------------------------------------------------------------------------------
+-- Coherence Conditions
+
+triangle : (f : Span A B) → (g : Span B C) → Spans₁ A C [ Spans₁ A C [ Spans₁.id B C {g} ⊚₁ ⊚-unitˡ f ∘ ⊚-assoc g id-span f ] ≈ ⊚-unitʳ g ⊚₁ Spans₁.id A B {f} ]
+triangle f g =
+  let pullback-dom-g = id ×ₚ (dom g)
+      pullback-cod-f = (cod f) ×ₚ id
+      pullback-fg    = (cod f) ×ₚ (dom g)
+      pullback-id-fg = (cod (id-span ⊚₀ f)) ×ₚ (dom g)
+      pullback-f-id-g = (cod f) ×ₚ (dom (id-span ⊚₀ g))
+  in unique pullback-fg (pullˡ (p₁∘universal≈h₁ pullback-fg) ○ pullʳ (p₁∘universal≈h₁ pullback-id-fg) ○ p₁∘universal≈h₁ pullback-cod-f ○ ⟺ identityˡ)
+                        (pullˡ (p₂∘universal≈h₂ pullback-fg) ○ pullʳ (p₂∘universal≈h₂ pullback-id-fg) ○ identityˡ)
+
+
+pentagon : (f : Span A B) → (g : Span B C) → (h : Span C D) → (i : Span D E)
+         →  Spans₁ A E [ Spans₁ A E [ (Spans₁.id D E {i}) ⊚₁ (⊚-assoc h g f) ∘ Spans₁ A E [ ⊚-assoc i (h ⊚₀ g) f ∘ ⊚-assoc i h g ⊚₁ Spans₁.id A B {f} ] ] ≈ Spans₁ A E [ ⊚-assoc i h (g ⊚₀ f) ∘ ⊚-assoc (i ⊚₀ h) g f ] ]
+pentagon {A} {B} {C} {D} {E} f g h i =
+  let pullback-fg       = (cod f) ×ₚ (dom g)
+      pullback-gh       = (cod g) ×ₚ (dom h)
+      pullback-hi       = (cod h) ×ₚ (dom i)
+      pullback-f⟨gh⟩    = (cod f) ×ₚ (dom (h ⊚₀ g))
+      pullback-⟨fg⟩h    = (cod (g ⊚₀ f)) ×ₚ (dom h)
+      pullback-⟨gh⟩i    = (cod (h ⊚₀ g)) ×ₚ (dom i)
+      pullback-g⟨hi⟩    = (cod g) ×ₚ (dom (i ⊚₀ h))
+      pullback-⟨⟨fg⟩h⟩i = (cod (h ⊚₀ (g ⊚₀ f))) ×ₚ (dom i)
+      pullback-⟨f⟨gh⟩⟩i = (cod ((h ⊚₀ g) ⊚₀ f)) ×ₚ (dom i)
+      pullback-⟨fg⟩⟨hi⟩ = (cod (g ⊚₀ f)) ×ₚ (dom (i ⊚₀ h))
+      pullback-f⟨⟨gh⟩i⟩ = (cod f) ×ₚ (dom (i ⊚₀ (h ⊚₀ g)))
+      pullback-f⟨g⟨hi⟩⟩ = (cod f) ×ₚ (dom ((i ⊚₀ h) ⊚₀ g))
+
+      lemma-fgˡ = begin
+        p₁ pullback-fg ∘ universal pullback-fg _ ∘ universal pullback-f⟨gh⟩ _ ∘ universal pullback-f⟨⟨gh⟩i⟩ _ ≈⟨ pullˡ (p₁∘universal≈h₁ pullback-fg) ⟩
+        p₁ pullback-f⟨gh⟩ ∘ universal pullback-f⟨gh⟩ _ ∘ universal pullback-f⟨⟨gh⟩i⟩ _                        ≈⟨ pullˡ (p₁∘universal≈h₁ pullback-f⟨gh⟩) ⟩
+        p₁ pullback-f⟨⟨gh⟩i⟩ ∘ universal pullback-f⟨⟨gh⟩i⟩ _                                                  ≈⟨ p₁∘universal≈h₁ pullback-f⟨⟨gh⟩i⟩ ⟩
+        id ∘ p₁ pullback-f⟨g⟨hi⟩⟩                                                                             ≈⟨ identityˡ ⟩
+        p₁ pullback-f⟨g⟨hi⟩⟩                                                                                  ≈˘⟨ p₁∘universal≈h₁ pullback-fg ⟩
+        p₁ pullback-fg ∘ universal pullback-fg _                                                              ∎
+
+      lemma-fgʳ = begin
+        p₂ pullback-fg ∘ universal pullback-fg _ ∘ universal pullback-f⟨gh⟩ _ ∘ universal pullback-f⟨⟨gh⟩i⟩ _ ≈⟨ pullˡ (p₂∘universal≈h₂ pullback-fg) ⟩
+        (p₁ pullback-gh ∘ p₂ pullback-f⟨gh⟩) ∘ universal pullback-f⟨gh⟩ _ ∘ universal pullback-f⟨⟨gh⟩i⟩ _     ≈⟨ center (p₂∘universal≈h₂ pullback-f⟨gh⟩) ⟩
+        p₁ pullback-gh ∘ (p₁ pullback-⟨gh⟩i ∘ p₂ pullback-f⟨⟨gh⟩i⟩) ∘ universal pullback-f⟨⟨gh⟩i⟩ _           ≈⟨ center⁻¹ refl (p₂∘universal≈h₂ pullback-f⟨⟨gh⟩i⟩) ⟩
+        (p₁ pullback-gh ∘ p₁ pullback-⟨gh⟩i) ∘ universal pullback-⟨gh⟩i _ ∘ p₂ pullback-f⟨g⟨hi⟩⟩              ≈⟨ center (p₁∘universal≈h₁ pullback-⟨gh⟩i) ⟩ 
+        p₁ pullback-gh ∘ universal pullback-gh _ ∘ p₂ pullback-f⟨g⟨hi⟩⟩                                       ≈⟨ pullˡ (p₁∘universal≈h₁ pullback-gh) ⟩
+        p₁ pullback-g⟨hi⟩ ∘ p₂ pullback-f⟨g⟨hi⟩⟩                                                              ≈˘⟨ p₂∘universal≈h₂ pullback-fg ⟩
+        p₂ pullback-fg ∘ universal pullback-fg _                                                              ∎
+
+      lemma-⟨fg⟩hˡ = begin
+        p₁ pullback-⟨fg⟩h ∘ universal pullback-⟨fg⟩h _ ∘ universal pullback-f⟨gh⟩ _ ∘ universal pullback-f⟨⟨gh⟩i⟩ _ ≈⟨ pullˡ (p₁∘universal≈h₁ pullback-⟨fg⟩h) ⟩
+        universal pullback-fg _ ∘ universal pullback-f⟨gh⟩ _ ∘ universal pullback-f⟨⟨gh⟩i⟩ _                        ≈⟨ unique-diagram pullback-fg lemma-fgˡ lemma-fgʳ ⟩
+        universal pullback-fg _                                                                                     ≈˘⟨ p₁∘universal≈h₁ pullback-⟨fg⟩⟨hi⟩ ⟩
+        p₁ pullback-⟨fg⟩⟨hi⟩ ∘ universal pullback-⟨fg⟩⟨hi⟩ _                                                        ≈⟨ pushˡ (⟺ (p₁∘universal≈h₁ pullback-⟨fg⟩h)) ⟩
+        p₁ pullback-⟨fg⟩h ∘ universal pullback-⟨fg⟩h _ ∘ universal pullback-⟨fg⟩⟨hi⟩ _                              ∎
+
+      lemma-⟨fg⟩hʳ = begin
+        p₂ pullback-⟨fg⟩h ∘ universal pullback-⟨fg⟩h _ ∘ universal pullback-f⟨gh⟩ _ ∘ universal pullback-f⟨⟨gh⟩i⟩ _ ≈⟨ pullˡ (p₂∘universal≈h₂ pullback-⟨fg⟩h) ⟩
+        (p₂ pullback-gh ∘ p₂ pullback-f⟨gh⟩) ∘ universal pullback-f⟨gh⟩ _ ∘ universal pullback-f⟨⟨gh⟩i⟩ _           ≈⟨ center (p₂∘universal≈h₂ pullback-f⟨gh⟩) ⟩
+        p₂ pullback-gh ∘ (p₁ pullback-⟨gh⟩i ∘ p₂ pullback-f⟨⟨gh⟩i⟩) ∘ universal pullback-f⟨⟨gh⟩i⟩ _                 ≈⟨ center⁻¹ refl (p₂∘universal≈h₂ pullback-f⟨⟨gh⟩i⟩) ⟩
+        (p₂ pullback-gh ∘ p₁ pullback-⟨gh⟩i) ∘ universal pullback-⟨gh⟩i _ ∘ p₂ pullback-f⟨g⟨hi⟩⟩                    ≈⟨ center (p₁∘universal≈h₁ pullback-⟨gh⟩i) ⟩
+        p₂ pullback-gh ∘ universal pullback-gh _ ∘ p₂ pullback-f⟨g⟨hi⟩⟩                                             ≈⟨ extendʳ (p₂∘universal≈h₂ pullback-gh) ⟩
+        p₁ pullback-hi ∘ p₂ pullback-g⟨hi⟩ ∘ p₂ pullback-f⟨g⟨hi⟩⟩                                                   ≈⟨ pushʳ (⟺ (p₂∘universal≈h₂ pullback-⟨fg⟩⟨hi⟩)) ⟩
+        (p₁ pullback-hi ∘ p₂ pullback-⟨fg⟩⟨hi⟩) ∘ universal pullback-⟨fg⟩⟨hi⟩ _                                     ≈⟨ pushˡ (⟺ (p₂∘universal≈h₂ pullback-⟨fg⟩h)) ⟩
+        p₂ pullback-⟨fg⟩h ∘ universal pullback-⟨fg⟩h _ ∘ universal pullback-⟨fg⟩⟨hi⟩ _                              ∎
+
+      lemmaˡ = begin
+        p₁ pullback-⟨⟨fg⟩h⟩i ∘ universal pullback-⟨⟨fg⟩h⟩i _ ∘ universal pullback-⟨f⟨gh⟩⟩i _ ∘ universal pullback-f⟨⟨gh⟩i⟩ _ ≈⟨ pullˡ (p₁∘universal≈h₁ pullback-⟨⟨fg⟩h⟩i) ⟩
+        (universal pullback-⟨fg⟩h _ ∘ p₁ pullback-⟨f⟨gh⟩⟩i) ∘ universal pullback-⟨f⟨gh⟩⟩i _ ∘ universal pullback-f⟨⟨gh⟩i⟩ _  ≈⟨ center (p₁∘universal≈h₁ pullback-⟨f⟨gh⟩⟩i) ⟩
+        universal pullback-⟨fg⟩h _ ∘ universal pullback-f⟨gh⟩ _ ∘ universal pullback-f⟨⟨gh⟩i⟩ _                              ≈⟨ unique-diagram pullback-⟨fg⟩h lemma-⟨fg⟩hˡ lemma-⟨fg⟩hʳ ⟩
+        universal pullback-⟨fg⟩h _ ∘ universal pullback-⟨fg⟩⟨hi⟩ _                                                           ≈⟨ pushˡ (⟺ (p₁∘universal≈h₁ pullback-⟨⟨fg⟩h⟩i)) ⟩
+        p₁ pullback-⟨⟨fg⟩h⟩i ∘ universal pullback-⟨⟨fg⟩h⟩i _ ∘ universal pullback-⟨fg⟩⟨hi⟩ _                                 ∎
+
+      lemmaʳ = begin
+        p₂ pullback-⟨⟨fg⟩h⟩i ∘ universal pullback-⟨⟨fg⟩h⟩i _ ∘ universal pullback-⟨f⟨gh⟩⟩i _ ∘ universal pullback-f⟨⟨gh⟩i⟩ _ ≈⟨ pullˡ (p₂∘universal≈h₂ pullback-⟨⟨fg⟩h⟩i) ⟩
+        (id ∘ p₂ pullback-⟨f⟨gh⟩⟩i) ∘ universal pullback-⟨f⟨gh⟩⟩i _ ∘ universal pullback-f⟨⟨gh⟩i⟩ _                          ≈⟨ center (p₂∘universal≈h₂ pullback-⟨f⟨gh⟩⟩i) ⟩
+        id ∘ (p₂ pullback-⟨gh⟩i ∘ p₂ pullback-f⟨⟨gh⟩i⟩) ∘ universal pullback-f⟨⟨gh⟩i⟩ _                                      ≈⟨ center⁻¹ identityˡ (p₂∘universal≈h₂ pullback-f⟨⟨gh⟩i⟩) ⟩
+        p₂ pullback-⟨gh⟩i ∘ universal pullback-⟨gh⟩i _ ∘ p₂ pullback-f⟨g⟨hi⟩⟩                                                ≈⟨ pullˡ (p₂∘universal≈h₂ pullback-⟨gh⟩i) ⟩
+        (p₂ pullback-hi ∘ p₂ pullback-g⟨hi⟩) ∘ p₂ pullback-f⟨g⟨hi⟩⟩                                                          ≈⟨ extendˡ (⟺ (p₂∘universal≈h₂ pullback-⟨fg⟩⟨hi⟩)) ⟩
+        (p₂ pullback-hi ∘ p₂ pullback-⟨fg⟩⟨hi⟩) ∘ universal pullback-⟨fg⟩⟨hi⟩ _                                              ≈⟨ pushˡ (⟺ (p₂∘universal≈h₂ pullback-⟨⟨fg⟩h⟩i)) ⟩
+        p₂ pullback-⟨⟨fg⟩h⟩i ∘ universal pullback-⟨⟨fg⟩h⟩i _ ∘ universal pullback-⟨fg⟩⟨hi⟩ _                                 ∎
+
+  in unique-diagram pullback-⟨⟨fg⟩h⟩i lemmaˡ lemmaʳ
+
+Spans : Bicategory (o ⊔ ℓ) (o ⊔ ℓ ⊔ e) e o
+Spans = record
+  { enriched = record
+    { Obj = Obj
+    ; hom = Spans₁
+    ; id = λ {A} → record
+      { F₀ = λ _ → id-span
+      ; F₁ = λ _ → Spans₁.id A A
+      ; identity = refl
+      ; homomorphism = ⟺ identity²
+      ; F-resp-≈ = λ _ → refl
+      }
+    ; ⊚ = record
+      { F₀ = λ (f , g) → f ⊚₀ g
+      ; F₁ = λ (α , β) → α ⊚₁ β
+      ; identity = λ {(f , g)} → ⊚₁-identity f g
+      ; homomorphism = λ {X} {Y} {Z} {(α , α′)} {(β , β′)} → ⊚₁-homomorphism α β α′ β′
+      ; F-resp-≈ = λ {(f , g)} {(f′ , g′)} {_} {_} (α-eq , β-eq) → universal-resp-≈ ((cod g′) ×ₚ (dom f′)) (∘-resp-≈ˡ β-eq) (∘-resp-≈ˡ α-eq)
+      }
+    ; ⊚-assoc = niHelper record
+      { η = λ ((f , g) , h) → ⊚-assoc f g h
+      ; η⁻¹ = λ ((f , g) , h) → ⊚-assoc⁻¹ f g h
+      ; commute = λ ((α , β) , γ) → ⊚-assoc-commute α β γ
+      ; iso = λ ((f , g) , h) → ⊚-assoc-iso f g h
+      }
+    ; unitˡ = niHelper record
+      { η = λ (_ , f) → ⊚-unitˡ f
+      ; η⁻¹ = λ (_ , f) → ⊚-unitˡ⁻¹ f
+      ; commute = λ (_ , α) → ⊚-unitˡ-commute α
+      ; iso = λ (_ , f) → ⊚-unitˡ-iso f
+      }
+    ; unitʳ = niHelper record
+      { η = λ (f , _) → ⊚-unitʳ f
+      ; η⁻¹ = λ (f , _) → ⊚-unitʳ⁻¹ f
+      ; commute = λ (α , _) → ⊚-unitʳ-commute α
+      ; iso = λ (f , _) → ⊚-unitʳ-iso f
+      }
+    }
+  ; triangle = λ {_} {_} {_} {f} {g} → triangle f g
+  ; pentagon = λ {_} {_} {_} {_} {_} {f} {g} {h} {i} → pentagon f g h i
+  }
diff --git a/src/Categories/Category/Construction/Spans.agda b/src/Categories/Category/Construction/Spans.agda
new file mode 100644
index 000000000..f98667126
--- /dev/null
+++ b/src/Categories/Category/Construction/Spans.agda
@@ -0,0 +1,38 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Categories.Category
+
+module Categories.Category.Construction.Spans {o ℓ e} (𝒞 : Category o ℓ e) where
+
+open import Level
+
+open import Categories.Category.Diagram.Span 𝒞
+open import Categories.Morphism.Reasoning 𝒞
+
+open Category 𝒞
+open HomReasoning
+open Equiv
+
+open Span
+open Span⇒
+
+Spans : Obj → Obj → Category (o ⊔ ℓ) (o ⊔ ℓ ⊔ e) e
+Spans X Y = record
+  { Obj = Span X Y
+  ; _⇒_ = Span⇒
+  ; _≈_ = λ f g → arr f ≈ arr g
+  ; id = id-span⇒
+  ; _∘_ = _∘ₛ_
+  ; assoc = assoc
+  ; sym-assoc = sym-assoc
+  ; identityˡ = identityˡ
+  ; identityʳ = identityʳ
+  ; identity² = identity²
+  ; equiv = record
+    { refl = refl
+    ; sym = sym
+    ; trans = trans
+    }
+  ; ∘-resp-≈ = ∘-resp-≈
+  }
+
diff --git a/src/Categories/Category/Diagram/Span.agda b/src/Categories/Category/Diagram/Span.agda
new file mode 100644
index 000000000..0573208c7
--- /dev/null
+++ b/src/Categories/Category/Diagram/Span.agda
@@ -0,0 +1,108 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Categories.Category
+
+-- Some basic facts about Spans in some category 𝒞.
+--
+-- For the Category instances for these, you can look at the following modules
+--    Categories.Category.Construction.Spans
+--    Categories.Bicategory.Construction.Spans
+module Categories.Category.Diagram.Span {o ℓ e} (𝒞 : Category o ℓ e) where
+
+open import Level
+open import Function using (_$_)
+
+open import Categories.Diagram.Pullback 𝒞
+open import Categories.Morphism.Reasoning 𝒞
+
+open Category 𝒞
+open HomReasoning
+open Equiv
+
+open Pullback
+
+private
+  variable
+    A B C D E : Obj
+
+--------------------------------------------------------------------------------
+-- Spans, and Span morphisms
+
+infixr 9 _∘ₛ_
+
+record Span (X Y : Obj) : Set (o ⊔ ℓ) where
+  field
+    M : Obj
+    dom : M ⇒ X
+    cod : M ⇒ Y
+
+open Span
+
+id-span : Span A A
+id-span {A} = record
+  { M = A
+  ; dom = id
+  ; cod = id
+  }
+
+record Span⇒ {X Y} (f g : Span X Y) : Set (o ⊔ ℓ ⊔ e) where
+  field
+    arr : M f ⇒ M g
+    commute-dom : dom g ∘ arr ≈ dom f
+    commute-cod : cod g ∘ arr ≈ cod f
+
+open Span⇒
+
+id-span⇒ : ∀ {f : Span A B} → Span⇒ f f
+id-span⇒ = record
+  { arr = id
+  ; commute-dom = identityʳ
+  ; commute-cod = identityʳ
+  }
+
+_∘ₛ_ : ∀ {f g h : Span A B} → (α : Span⇒ g h) → (β : Span⇒ f g) → Span⇒ f h
+_∘ₛ_ {f = f} {g = g} {h = h} α β = record
+  { arr = arr α ∘ arr β
+  ; commute-dom = begin
+    dom h ∘ arr α ∘ arr β ≈⟨ pullˡ (commute-dom α) ⟩
+    dom g ∘ arr β ≈⟨ commute-dom β ⟩
+    dom f ∎
+  ; commute-cod = begin
+    cod h ∘ arr α ∘ arr β ≈⟨ pullˡ (commute-cod α) ⟩
+    cod g ∘ arr β ≈⟨ commute-cod β ⟩
+    cod f ∎
+  }
+
+--------------------------------------------------------------------------------
+-- Span Compositions
+
+module Compositions (_×ₚ_ : ∀ {X Y Z} (f : X ⇒ Z) → (g : Y ⇒ Z) → Pullback f g) where
+
+  _⊚₀_ : Span B C → Span A B → Span A C
+  f ⊚₀ g =
+    let g×ₚf = (cod g) ×ₚ (dom f)
+    in record
+        { M = P g×ₚf
+        ; dom = dom g ∘ p₁ g×ₚf
+        ; cod = cod f ∘ p₂ g×ₚf
+        }
+
+  _⊚₁_ : {f f′ : Span B C} {g g′ : Span A B} → Span⇒ f f′ → Span⇒ g g′ → Span⇒ (f ⊚₀ g) (f′ ⊚₀ g′)
+  _⊚₁_  {f = f} {f′ = f′} {g = g} {g′ = g′} α β =
+    let pullback = (cod g) ×ₚ (dom f)
+        pullback′ = (cod g′) ×ₚ (dom f′)
+    in record
+      { arr = universal pullback′ {h₁ = arr β ∘ p₁ pullback} {h₂ = arr α ∘ p₂ pullback} $ begin
+          cod g′ ∘ arr β ∘ p₁ pullback ≈⟨ pullˡ (commute-cod β) ⟩
+          cod g ∘ p₁ pullback          ≈⟨ commute pullback ⟩
+          dom f ∘ p₂ pullback          ≈⟨ pushˡ (⟺ (commute-dom α)) ⟩
+          dom f′ ∘ arr α ∘ p₂ pullback ∎
+      ; commute-dom = begin
+          (dom g′ ∘ p₁ pullback′) ∘ universal pullback′ _ ≈⟨ pullʳ (p₁∘universal≈h₁ pullback′) ⟩
+          dom g′ ∘ arr β ∘ p₁ pullback                    ≈⟨ pullˡ (commute-dom β) ⟩
+          dom g ∘ p₁ pullback                             ∎
+      ; commute-cod = begin
+          (cod f′ ∘ p₂ pullback′) ∘ universal pullback′ _ ≈⟨ pullʳ (p₂∘universal≈h₂ pullback′) ⟩
+          cod f′ ∘ arr α ∘ p₂ pullback                    ≈⟨ pullˡ (commute-cod α) ⟩
+          cod f ∘ p₂ pullback                             ∎
+      }