diff --git a/src/Categories/Bicategory/Construction/Spans/Properties.agda b/src/Categories/Bicategory/Construction/Spans/Properties.agda
new file mode 100644
index 000000000..bd73d1d92
--- /dev/null
+++ b/src/Categories/Bicategory/Construction/Spans/Properties.agda
@@ -0,0 +1,133 @@
+{-# OPTIONS --without-K --safe #-}
+
+module Categories.Bicategory.Construction.Spans.Properties where
+
+open import Level
+
+open import Data.Product using (_,_; _×_)
+open import Relation.Binary.Bundles using (Setoid)
+import Relation.Binary.Reasoning.Setoid as SR
+open import Function.Equality as SΠ renaming (id to ⟶-id)
+
+open import Categories.Category
+open import Categories.Category.Helper
+open import Categories.Category.Instance.Setoids
+open import Categories.Category.Instance.Properties.Setoids.Limits.Canonical
+
+open import Categories.Diagram.Pullback
+
+open import Categories.Bicategory
+open import Categories.Bicategory.Monad
+
+import Categories.Category.Diagram.Span as Span
+import Categories.Bicategory.Construction.Spans as Spans
+
+--------------------------------------------------------------------------------
+-- Monads in the Bicategory of Spans are Categories
+
+module _ {o ℓ : Level} (T : Monad (Spans.Spans (pullback o ℓ))) where
+
+  private
+    module T = Monad T
+
+    open Span (Setoids (o ⊔ ℓ) ℓ)
+    open Spans (pullback o ℓ)
+    open Span⇒
+    open Bicategory Spans
+
+    open Setoid renaming (_≈_ to [_][_≈_])
+
+
+  -- We can view the roof of the span as a hom set! However, we need to partition
+  -- this big set up into small chunks with known domains/codomains.
+  record Hom (X Y : Carrier T.C) : Set (o ⊔ ℓ) where
+    field
+      hom : Carrier (Span.M T.T)
+      dom-eq : [ T.C ][ Span.dom T.T ⟨$⟩ hom ≈ X ]
+      cod-eq : [ T.C ][ Span.cod T.T ⟨$⟩ hom ≈ Y ]
+
+  open Hom
+
+  private
+    ObjSetoid : Setoid (o ⊔ ℓ) ℓ
+    ObjSetoid = T.C
+
+    HomSetoid : Setoid (o ⊔ ℓ) ℓ
+    HomSetoid = Span.M T.T
+
+    module ObjSetoid = Setoid ObjSetoid
+    module HomSetoid = Setoid HomSetoid
+
+    id⇒ : (X : Carrier T.C) → Hom X X
+    id⇒ X = record
+      { hom = arr T.η ⟨$⟩ X
+      ; dom-eq = commute-dom T.η (refl T.C)
+      ; cod-eq = commute-cod T.η (refl T.C)
+      }
+
+    _×ₚ_ : ∀ {A B C} → (f : Hom B C) → (g : Hom A B) → FiberProduct (Span.cod T.T) (Span.dom T.T)
+    _×ₚ_ {B = B} f g = record
+      { elem₁ = hom g
+      ; elem₂ = hom f
+      ; commute = begin
+        Span.cod T.T ⟨$⟩ hom g ≈⟨ cod-eq g ⟩
+        B                      ≈⟨ ObjSetoid.sym (dom-eq f) ⟩
+        Span.dom T.T ⟨$⟩ hom f ∎
+      }
+      where
+        open SR ObjSetoid
+
+    _∘⇒_ : ∀ {A B C} (f : Hom B C) → (g : Hom A B) → Hom A C
+    _∘⇒_ {A = A} {C = C} f g = record
+      { hom = arr T.μ ⟨$⟩ (f ×ₚ g)
+      ; dom-eq = begin
+        Span.dom T.T ⟨$⟩ (arr T.μ ⟨$⟩ (f ×ₚ g)) ≈⟨ (commute-dom T.μ {f ×ₚ g} {f ×ₚ g} (HomSetoid.refl , HomSetoid.refl)) ⟩
+        Span.dom T.T ⟨$⟩ hom g                  ≈⟨ dom-eq g ⟩
+        A                                       ∎
+      ; cod-eq = begin
+        Span.cod T.T ⟨$⟩ (arr T.μ ⟨$⟩ (f ×ₚ g)) ≈⟨ commute-cod T.μ {f ×ₚ g} {f ×ₚ g} (HomSetoid.refl , HomSetoid.refl) ⟩
+        Span.cod T.T ⟨$⟩ hom f                  ≈⟨ cod-eq f ⟩
+        C                                       ∎
+      }
+      where
+        open SR ObjSetoid
+
+  SpanMonad⇒Category : Category (o ⊔ ℓ) (o ⊔ ℓ) ℓ
+  SpanMonad⇒Category = categoryHelper record
+    { Obj = Setoid.Carrier T.C
+    ; _⇒_ = Hom
+    ; _≈_ = λ f g → [ HomSetoid ][ hom f ≈ hom g ]
+    ; id = λ {X} → id⇒ X
+    ; _∘_ = _∘⇒_
+    ; assoc = λ {A} {B} {C} {D} {f} {g} {h} →
+      let f×ₚ⟨g×ₚh⟩ = record
+            { elem₁ = record
+              { elem₁ = hom f
+              ; elem₂ = hom g
+              ; commute = FiberProduct.commute (g ×ₚ f)
+              }
+            ; elem₂ = hom h
+            ; commute = FiberProduct.commute (h ×ₚ g)
+            }
+      in begin
+        arr T.μ ⟨$⟩ ((h ∘⇒ g) ×ₚ f) ≈⟨ cong (arr T.μ) (HomSetoid.refl , cong (arr T.μ) (HomSetoid.refl , HomSetoid.refl)) ⟩
+        arr T.μ ⟨$⟩ _                ≈⟨ T.sym-assoc {f×ₚ⟨g×ₚh⟩} {f×ₚ⟨g×ₚh⟩} ((HomSetoid.refl , HomSetoid.refl) , HomSetoid.refl) ⟩
+        arr T.μ ⟨$⟩ _                ≈⟨ (cong (arr T.μ) (cong (arr T.μ) (HomSetoid.refl , HomSetoid.refl) , HomSetoid.refl)) ⟩
+        arr T.μ ⟨$⟩ (h ×ₚ (g ∘⇒ f)) ∎
+    ; identityˡ = λ {A} {B} {f} → begin
+      arr T.μ ⟨$⟩ (id⇒ B ×ₚ f) ≈⟨ cong (arr T.μ) (HomSetoid.refl , cong (arr T.η) (ObjSetoid.sym (cod-eq f))) ⟩
+      arr T.μ ⟨$⟩ _             ≈⟨ T.identityʳ HomSetoid.refl ⟩
+      hom f                     ∎
+    ; identityʳ = λ {A} {B} {f} → begin
+      arr T.μ ⟨$⟩ (f ×ₚ id⇒ A) ≈⟨ cong (arr T.μ) (cong (arr T.η) (ObjSetoid.sym (dom-eq f)) , HomSetoid.refl) ⟩
+      arr T.μ ⟨$⟩ _             ≈⟨ T.identityˡ HomSetoid.refl ⟩
+      hom f                     ∎
+    ; equiv = record
+      { refl = HomSetoid.refl
+      ; sym = HomSetoid.sym
+      ; trans = HomSetoid.trans
+      }
+    ; ∘-resp-≈ = λ f≈h g≈i → cong (arr T.μ) (g≈i , f≈h)
+    }
+      where
+        open SR HomSetoid
diff --git a/src/Categories/Bicategory/Monad.agda b/src/Categories/Bicategory/Monad.agda
new file mode 100644
index 000000000..b78750c06
--- /dev/null
+++ b/src/Categories/Bicategory/Monad.agda
@@ -0,0 +1,27 @@
+{-# OPTIONS --without-K --safe #-}
+
+-- A Monad in a Bicategory.
+-- For the more elementary version of Monads, see 'Categories.Monad'.
+module Categories.Bicategory.Monad where
+
+open import Level
+open import Data.Product using (_,_)
+
+open import Categories.Bicategory
+import Categories.Bicategory.Extras as Bicat
+open import Categories.NaturalTransformation.NaturalIsomorphism using (NaturalIsomorphism)
+
+
+record Monad {o ℓ e t} (𝒞 : Bicategory o ℓ e t) : Set (o ⊔ ℓ ⊔ e ⊔ t) where
+  open Bicat 𝒞
+
+  field
+    C : Obj
+    T : C ⇒₁ C
+    η : id₁ ⇒₂ T
+    μ : (T ⊚₀ T) ⇒₂ T
+
+    assoc     : μ ∘ᵥ (T ▷ μ) ∘ᵥ associator.from ≈ (μ ∘ᵥ (μ ◁ T))
+    sym-assoc : μ ∘ᵥ (μ ◁ T) ∘ᵥ associator.to ≈ (μ ∘ᵥ (T ▷ μ))
+    identityˡ : μ ∘ᵥ (T ▷ η) ∘ᵥ unitorʳ.to ≈ id₂
+    identityʳ : μ ∘ᵥ (η ◁ T) ∘ᵥ unitorˡ.to ≈ id₂
diff --git a/src/Categories/Bicategory/Monad/Properties.agda b/src/Categories/Bicategory/Monad/Properties.agda
new file mode 100644
index 000000000..c4df88c1b
--- /dev/null
+++ b/src/Categories/Bicategory/Monad/Properties.agda
@@ -0,0 +1,93 @@
+{-# OPTIONS --without-K --safe #-}
+module Categories.Bicategory.Monad.Properties where
+
+open import Categories.Category
+open import Categories.Bicategory.Instance.Cats
+open import Categories.NaturalTransformation using (NaturalTransformation)
+open import Categories.Functor using (Functor)
+
+import Categories.Bicategory.Monad as BicatMonad
+import Categories.Monad as ElemMonad
+
+import Categories.Morphism.Reasoning as MR
+
+--------------------------------------------------------------------------------
+-- Bicategorical Monads in Cat are the same as the more elementary
+-- definition of Monads.
+
+CatMonad⇒Monad : ∀ {o ℓ e} → (T : BicatMonad.Monad (Cats o ℓ e)) → ElemMonad.Monad (BicatMonad.Monad.C T)
+CatMonad⇒Monad T = record
+  { F = T.T
+  ; η = T.η
+  ; μ = T.μ
+  ; assoc = λ {X} → begin
+    η T.μ X ∘ F₁ T.T (η T.μ X)               ≈⟨ intro-ids ⟩
+    (η T.μ X ∘ (F₁ T.T (η T.μ X) ∘ id) ∘ id) ≈⟨ T.assoc ⟩
+    (η T.μ X ∘ F₁ T.T id ∘ η T.μ (F₀ T.T X)) ≈⟨ ∘-resp-≈ʳ (∘-resp-≈ˡ (identity T.T) ○ identityˡ) ⟩
+    η T.μ X ∘ η T.μ (F₀ T.T X)               ∎
+  ; sym-assoc = λ {X} → begin
+    η T.μ X ∘ η T.μ (F₀ T.T X)                    ≈⟨ intro-F-ids ⟩
+    η T.μ X ∘ (F₁ T.T id ∘ η T.μ (F₀ T.T X)) ∘ id ≈⟨ T.sym-assoc ⟩
+    η T.μ X ∘ F₁ T.T (η T.μ X) ∘ id               ≈⟨ ∘-resp-≈ʳ identityʳ ⟩
+    η T.μ X ∘ F₁ T.T (η T.μ X)                    ∎
+  ; identityˡ = λ {X} → begin
+    η T.μ X ∘ F₁ T.T (η T.η X)             ≈⟨ intro-ids ⟩
+    η T.μ X ∘ (F₁ T.T (η T.η X) ∘ id) ∘ id ≈⟨ T.identityˡ ⟩
+    id                                     ∎
+  ; identityʳ = λ {X} → begin
+    η T.μ X ∘ η T.η (F₀ T.T X)                    ≈⟨ intro-F-ids ⟩
+    η T.μ X ∘ (F₁ T.T id ∘ η T.η (F₀ T.T X)) ∘ id ≈⟨ T.identityʳ ⟩
+    id                                            ∎
+  }
+  where
+    module T = BicatMonad.Monad T
+    open Category (BicatMonad.Monad.C T)
+    open HomReasoning
+    open Equiv
+    open MR (BicatMonad.Monad.C T)
+
+    open NaturalTransformation
+    open Functor
+
+    intro-ids : ∀ {X Y Z} {f : Y ⇒ Z} {g : X ⇒ Y} → f ∘ g ≈ f ∘ (g ∘ id) ∘ id
+    intro-ids = ⟺ (∘-resp-≈ʳ identityʳ) ○ ⟺ (∘-resp-≈ʳ identityʳ)
+
+    intro-F-ids : ∀ {X Y Z} {f : F₀ T.T Y ⇒ Z} {g : X ⇒ F₀ T.T Y} → f ∘ g ≈ f ∘ (F₁ T.T id ∘ g) ∘ id
+    intro-F-ids = ∘-resp-≈ʳ (⟺ identityˡ ○  ⟺ (∘-resp-≈ˡ (identity T.T))) ○ ⟺ (∘-resp-≈ʳ identityʳ)
+
+Monad⇒CatMonad : ∀ {o ℓ e} {𝒞 : Category o ℓ e} → (T : ElemMonad.Monad 𝒞) → BicatMonad.Monad (Cats o ℓ e)
+Monad⇒CatMonad {𝒞 = 𝒞} T = record
+  { C = 𝒞
+  ; T = T.F
+  ; η = T.η
+  ; μ = T.μ
+  ; assoc = λ {X} → begin
+    T.μ.η X ∘ (T.F.F₁ (T.μ.η X) ∘ id) ∘ id ≈⟨ eliminate-ids ⟩
+    T.μ.η X ∘ T.F.F₁ (T.μ.η X)             ≈⟨ T.assoc ⟩
+    T.μ.η X ∘ T.μ.η (T.F.F₀ X)             ≈⟨ ∘-resp-≈ʳ (⟺ identityˡ ○ ∘-resp-≈ˡ (⟺ T.F.identity)) ⟩
+    T.μ.η X ∘ T.F.F₁ id ∘ T.μ.η (T.F.F₀ X) ∎
+  ; sym-assoc = λ {X} → begin
+    T.μ.η X ∘ (T.F.F₁ id ∘ T.μ.η (T.F.F₀ X)) ∘ id ≈⟨ eliminate-F-ids ⟩
+    T.μ.η X ∘ T.μ.η (T.F.F₀ X)                    ≈⟨ T.sym-assoc ⟩
+    T.μ.η X ∘ T.F.F₁ (T.μ.η X)                    ≈⟨ ∘-resp-≈ʳ (⟺ identityʳ) ⟩
+    T.μ.η X ∘ T.F.F₁ (T.μ.η X) ∘ id               ∎
+  ; identityˡ = λ {X} → begin
+    T.μ.η X ∘ (T.F.F₁ (T.η.η X) ∘ id) ∘ id ≈⟨ eliminate-ids ⟩
+    T.μ.η X ∘ T.F.F₁ (T.η.η X)             ≈⟨ T.identityˡ ⟩
+    id                                     ∎
+  ; identityʳ = λ {X} → begin
+    (T.μ.η X ∘ (T.F.F₁ id ∘ T.η.η (T.F.F₀ X)) ∘ id) ≈⟨ eliminate-F-ids ⟩
+    T.μ.η X ∘ T.η.η (T.F.F₀ X)                      ≈⟨ T.identityʳ ⟩
+    id                                              ∎
+  }
+  where
+    module T = ElemMonad.Monad T
+    open Category 𝒞
+    open HomReasoning
+    open MR 𝒞
+
+    eliminate-ids : ∀ {X Y Z} {f : Y ⇒ Z} {g : X ⇒ Y} →  f ∘ (g ∘ id) ∘ id ≈ f ∘ g
+    eliminate-ids = ∘-resp-≈ʳ identityʳ ○ ∘-resp-≈ʳ identityʳ
+
+    eliminate-F-ids : ∀ {X Y Z} {f : T.F.F₀ Y ⇒ Z} {g : X ⇒ T.F.F₀ Y} →  f ∘ (T.F.F₁ id ∘ g) ∘ id ≈ f ∘ g
+    eliminate-F-ids = ∘-resp-≈ʳ identityʳ ○ ∘-resp-≈ʳ (∘-resp-≈ˡ T.F.identity ○ identityˡ)
diff --git a/src/Categories/Category/Instance/Properties/Setoids/Limits/Canonical.agda b/src/Categories/Category/Instance/Properties/Setoids/Limits/Canonical.agda
new file mode 100644
index 000000000..5d746ca2f
--- /dev/null
+++ b/src/Categories/Category/Instance/Properties/Setoids/Limits/Canonical.agda
@@ -0,0 +1,62 @@
+{-# OPTIONS --without-K --safe #-}
+
+-- A "canonical" presentation of limits in Setoid.
+--
+-- These limits are obviously isomorphic to those created by
+-- the Completeness proof, but are far less unweildy to work with.
+-- This isomorphism is witnessed by Categories.Diagram.Pullback.up-to-iso
+
+module Categories.Category.Instance.Properties.Setoids.Limits.Canonical where
+
+open import Level
+
+open import Data.Product using (_,_; _×_)
+
+open import Relation.Binary.Bundles using (Setoid)
+open import Function.Equality as SΠ renaming (id to ⟶-id)
+import Relation.Binary.Reasoning.Setoid as SR
+
+open import Categories.Diagram.Pullback
+
+open import Categories.Category.Instance.Setoids
+
+open Setoid renaming (_≈_ to [_][_≈_])
+
+--------------------------------------------------------------------------------
+-- Pullbacks
+
+record FiberProduct {o ℓ} {X Y Z : Setoid o ℓ} (f : X ⟶ Z) (g : Y ⟶ Z) : Set (o ⊔ ℓ) where
+  field
+    elem₁ : Carrier X
+    elem₂ : Carrier Y
+    commute : [ Z ][ f ⟨$⟩ elem₁ ≈ g ⟨$⟩ elem₂ ]
+
+open FiberProduct
+
+pullback : ∀ (o ℓ : Level) {X Y Z : Setoid (o ⊔ ℓ) ℓ} → (f : X ⟶ Z) → (g : Y ⟶ Z) → Pullback (Setoids (o ⊔ ℓ) ℓ) f g
+pullback _ _ {X = X} {Y = Y} {Z = Z} f g = record
+  { P = record
+    { Carrier = FiberProduct f g
+    ; _≈_ =  λ p q → [ X ][ elem₁ p ≈ elem₁ q ] × [ Y ][ elem₂ p ≈ elem₂ q ]
+    ; isEquivalence = record
+      { refl = (refl X) , (refl Y)
+      ; sym = λ (eq₁ , eq₂) → sym X eq₁ , sym Y eq₂
+      ; trans = λ (eq₁ , eq₂) (eq₁′ , eq₂′) → (trans X eq₁ eq₁′) , (trans Y eq₂ eq₂′)
+      }
+    }
+    ; p₁ = record { _⟨$⟩_ = elem₁ ; cong = λ (eq₁ , _) → eq₁ }
+    ; p₂ = record { _⟨$⟩_ = elem₂ ; cong = λ (_ , eq₂) → eq₂ }
+    ; isPullback = record
+      { commute = λ {p} {q} (eq₁ , eq₂) → trans Z (cong f eq₁) (commute q)
+      ; universal = λ {A} {h₁} {h₂} eq → record
+        { _⟨$⟩_ = λ a → record
+          { elem₁ = h₁ ⟨$⟩ a
+          ; elem₂ = h₂ ⟨$⟩ a
+          ; commute = eq (refl A)
+          }
+        ; cong = λ eq → cong h₁ eq , cong h₂ eq }
+      ; unique = λ eq₁ eq₂ x≈y → eq₁ x≈y , eq₂ x≈y
+      ; p₁∘universal≈h₁ = λ {_} {h₁} {_} eq → cong h₁ eq
+      ; p₂∘universal≈h₂ = λ {_} {_} {h₂} eq → cong h₂ eq
+      }
+    }