diff --git a/doc/implementation.tex b/doc/implementation.tex
index d94f033..75f2df7 100644
--- a/doc/implementation.tex
+++ b/doc/implementation.tex
@@ -10,19 +10,20 @@ Name & Link \\
 \hline
 Categories & \sourcelink{Cat.Category} \\
 Functors & \sourcelink{Cat.Category.Functor} \\
-Products & \sourcelink{Cat.Category.Products} \\
-Exponentials & \sourcelink{Cat.Category.Exponentials} \\
+Products & \sourcelink{Cat.Category.Product} \\
+Exponentials & \sourcelink{Cat.Category.Exponential} \\
 Cartesian closed categories & \sourcelink{Cat.Category.CartesianClosed} \\
 Natural transformations & \sourcelink{Cat.Category.NaturalTransformation} \\
 Yoneda embedding & \sourcelink{Cat.Category.Yoneda} \\
-Monads & \sourcelink{Cat.Category.Monads} \\
+Monads & \sourcelink{Cat.Category.Monad} \\
+Kleisli Monads & \sourcelink{Cat.Category.Monad.Kleisli} \\
+Monoidal Monads & \sourcelink{Cat.Category.Monad.Monoidal} \\
+Voevodsky's construction & \sourcelink{Cat.Category.Monad.Voevodsky} \\
 %% Categories & \null \\
 %%
-Opposite category &
-\href{\sourcebasepath Cat.Category.html#22744}{\texttt{Cat.Category.Opposite}} \\
+Opposite category & \sourcelink{Cat.Categories.Opposite} \\
 Category of sets & \sourcelink{Cat.Categories.Sets} \\
-Span category &
-\href{\sourcebasepath Cat.Category.Product.html#2919}{\texttt{Cat.Category.Product.Span}} \\
+Span category & \sourcelink{Cat.Categories.Span} \\
   %%
 \end{tabular}
 \end{center}
diff --git a/src/Cat.agda b/src/Cat.agda
index fca9c99..a2d73e8 100644
--- a/src/Cat.agda
+++ b/src/Cat.agda
@@ -14,6 +14,7 @@ open import Cat.Category.Monad.Monoidal
 open import Cat.Category.Monad.Kleisli
 open import Cat.Category.Monad.Voevodsky
 
+open import Cat.Categories.Opposite
 open import Cat.Categories.Sets
 open import Cat.Categories.Cat
 open import Cat.Categories.Rel
diff --git a/src/Cat/Categories/CwF.agda b/src/Cat/Categories/CwF.agda
index 1a491ec..9c1fc6d 100644
--- a/src/Cat/Categories/CwF.agda
+++ b/src/Cat/Categories/CwF.agda
@@ -5,6 +5,7 @@ open import Cat.Prelude
 open import Cat.Category
 open import Cat.Category.Functor
 open import Cat.Categories.Fam
+open import Cat.Categories.Opposite
 
 module _ {ℓa ℓb : Level} where
   record CwF : Set (lsuc (ℓa ⊔ ℓb)) where
diff --git a/src/Cat/Categories/Fun.agda b/src/Cat/Categories/Fun.agda
index eb861e7..bcfb508 100644
--- a/src/Cat/Categories/Fun.agda
+++ b/src/Cat/Categories/Fun.agda
@@ -3,11 +3,11 @@ module Cat.Categories.Fun where
 
 open import Cat.Prelude
 open import Cat.Equivalence
-
 open import Cat.Category
 open import Cat.Category.Functor
 import Cat.Category.NaturalTransformation
   as NaturalTransformation
+open import Cat.Categories.Opposite
 
 module Fun {ℓc ℓc' ℓd ℓd' : Level} (ℂ : Category ℓc ℓc') (𝔻 : Category ℓd ℓd') where
   open NaturalTransformation ℂ 𝔻 public hiding (module Properties)
diff --git a/src/Cat/Categories/Opposite.agda b/src/Cat/Categories/Opposite.agda
new file mode 100644
index 0000000..ef2fa33
--- /dev/null
+++ b/src/Cat/Categories/Opposite.agda
@@ -0,0 +1,96 @@
+{-# OPTIONS --cubical #-}
+module Cat.Categories.Opposite where
+
+open import Cat.Prelude
+open import Cat.Equivalence
+open import Cat.Category
+
+-- | The opposite category
+--
+-- The opposite category is the category where the direction of the arrows are
+-- flipped.
+module _ {ℓa ℓb : Level} where
+  module _ (ℂ : Category ℓa ℓb) where
+    private
+      module _ where
+        module ℂ = Category ℂ
+        opRaw : RawCategory ℓa ℓb
+        RawCategory.Object   opRaw = ℂ.Object
+        RawCategory.Arrow    opRaw = flip ℂ.Arrow
+        RawCategory.identity opRaw = ℂ.identity
+        RawCategory._<<<_    opRaw = ℂ._>>>_
+
+        open RawCategory opRaw
+
+        isPreCategory : IsPreCategory opRaw
+        IsPreCategory.isAssociative isPreCategory = sym ℂ.isAssociative
+        IsPreCategory.isIdentity    isPreCategory = swap ℂ.isIdentity
+        IsPreCategory.arrowsAreSets isPreCategory = ℂ.arrowsAreSets
+
+      open IsPreCategory isPreCategory
+
+      module _ {A B : ℂ.Object} where
+        open Σ (toIso _ _ (ℂ.univalent {A} {B}))
+          renaming (fst to idToIso* ; snd to inv*)
+        open AreInverses {f = ℂ.idToIso A B} {idToIso*} inv*
+
+        shuffle : A ≊ B → A ℂ.≊ B
+        shuffle (f , g , inv) = g , f , inv
+
+        shuffle~ : A ℂ.≊ B → A ≊ B
+        shuffle~ (f , g , inv) = g , f , inv
+
+        lem : (p : A ≡ B) → idToIso A B p ≡ shuffle~ (ℂ.idToIso A B p)
+        lem p = isoEq refl
+
+        isoToId* : A ≊ B → A ≡ B
+        isoToId* = idToIso* ∘ shuffle
+
+        inv : AreInverses (idToIso A B) isoToId*
+        inv =
+          ( funExt (λ x → begin
+            (isoToId* ∘ idToIso A B) x
+              ≡⟨⟩
+            (idToIso*  ∘ shuffle ∘ idToIso A B) x
+              ≡⟨ cong (λ φ → φ x) (cong (λ φ → idToIso* ∘ shuffle ∘ φ) (funExt lem)) ⟩
+            (idToIso*  ∘ shuffle ∘ shuffle~ ∘ ℂ.idToIso A B) x
+              ≡⟨⟩
+            (idToIso*  ∘ ℂ.idToIso A B) x
+              ≡⟨ (λ i → verso-recto i x) ⟩
+            x ∎)
+          , funExt (λ x → begin
+            (idToIso A B ∘ idToIso* ∘ shuffle) x
+              ≡⟨ cong (λ φ → φ x) (cong (λ φ → φ ∘ idToIso* ∘ shuffle) (funExt lem)) ⟩
+            (shuffle~ ∘ ℂ.idToIso A B ∘ idToIso* ∘ shuffle) x
+              ≡⟨ cong (λ φ → φ x) (cong (λ φ → shuffle~ ∘ φ ∘ shuffle) recto-verso) ⟩
+            (shuffle~ ∘ shuffle) x
+              ≡⟨⟩
+            x ∎)
+          )
+
+      isCategory : IsCategory opRaw
+      IsCategory.isPreCategory isCategory = isPreCategory
+      IsCategory.univalent     isCategory
+        = univalenceFromIsomorphism (isoToId* , inv)
+
+    opposite : Category ℓa ℓb
+    Category.raw        opposite = opRaw
+    Category.isCategory opposite = isCategory
+
+  -- As demonstrated here a side-effect of having no-eta-equality on constructors
+  -- means that we need to pick things apart to show that things are indeed
+  -- definitionally equal. I.e; a thing that would normally be provable in one
+  -- line now takes 13!! Admittedly it's a simple proof.
+  module _ {ℂ : Category ℓa ℓb} where
+    open Category ℂ
+    private
+      -- Since they really are definitionally equal we just need to pick apart
+      -- the data-type.
+      rawInv : Category.raw (opposite (opposite ℂ)) ≡ raw
+      RawCategory.Object   (rawInv _) = Object
+      RawCategory.Arrow    (rawInv _) = Arrow
+      RawCategory.identity (rawInv _) = identity
+      RawCategory._<<<_    (rawInv _) = _<<<_
+
+    oppositeIsInvolution : opposite (opposite ℂ) ≡ ℂ
+    oppositeIsInvolution = Category≡ rawInv
diff --git a/src/Cat/Categories/Sets.agda b/src/Cat/Categories/Sets.agda
index e707b55..e25f148 100644
--- a/src/Cat/Categories/Sets.agda
+++ b/src/Cat/Categories/Sets.agda
@@ -3,11 +3,11 @@
 module Cat.Categories.Sets where
 
 open import Cat.Prelude as P
-
+open import Cat.Equivalence
 open import Cat.Category
 open import Cat.Category.Functor
 open import Cat.Category.Product
-open import Cat.Equivalence
+open import Cat.Categories.Opposite
 
 _⊙_ : {ℓa ℓb ℓc : Level} {A : Set ℓa} {B : Set ℓb} {C : Set ℓc} → (A ≃ B) → (B ≃ C) → A ≃ C
 eqA ⊙ eqB = Equivalence.compose eqA eqB
diff --git a/src/Cat/Categories/Span.agda b/src/Cat/Categories/Span.agda
new file mode 100644
index 0000000..3573266
--- /dev/null
+++ b/src/Cat/Categories/Span.agda
@@ -0,0 +1,173 @@
+{-# OPTIONS --cubical --caching #-}
+module Cat.Categories.Span where
+
+open import Cat.Prelude as P hiding (_×_ ; fst ; snd)
+open import Cat.Equivalence
+open import Cat.Category
+
+module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb)
+  (let module ℂ = Category ℂ) (𝒜 ℬ : ℂ.Object) where
+
+  open P
+
+  private
+    module _ where
+      raw : RawCategory _ _
+      raw = record
+        { Object = Σ[ X ∈ ℂ.Object ] ℂ.Arrow X 𝒜 × ℂ.Arrow X ℬ
+        ; Arrow = λ{ (A , a0 , a1) (B , b0 , b1)
+          → Σ[ f ∈ ℂ.Arrow A B ]
+              ℂ [ b0 ∘ f ] ≡ a0
+            × ℂ [ b1 ∘ f ] ≡ a1
+            }
+        ; identity = λ{ {X , f , g} → ℂ.identity {X} , ℂ.rightIdentity , ℂ.rightIdentity}
+        ; _<<<_ = λ { {_ , a0 , a1} {_ , b0 , b1} {_ , c0 , c1} (f , f0 , f1) (g , g0 , g1)
+          → (f ℂ.<<< g)
+            , (begin
+                ℂ [ c0 ∘ ℂ [ f ∘ g ] ] ≡⟨ ℂ.isAssociative ⟩
+                ℂ [ ℂ [ c0 ∘ f ] ∘ g ] ≡⟨ cong (λ φ → ℂ [ φ ∘ g ]) f0 ⟩
+                ℂ [ b0 ∘ g ] ≡⟨ g0 ⟩
+                a0 ∎
+              )
+            , (begin
+               ℂ [ c1 ∘ ℂ [ f ∘ g ] ] ≡⟨ ℂ.isAssociative ⟩
+               ℂ [ ℂ [ c1 ∘ f ] ∘ g ] ≡⟨ cong (λ φ → ℂ [ φ ∘ g ]) f1 ⟩
+               ℂ [ b1 ∘ g ] ≡⟨ g1 ⟩
+                a1 ∎
+              )
+          }
+        }
+
+      module _ where
+        open RawCategory raw
+
+        propEqs : ∀ {X' : Object}{Y' : Object} (let X , xa , xb = X') (let Y , ya , yb = Y')
+                    → (xy : ℂ.Arrow X Y) → isProp (ℂ [ ya ∘ xy ] ≡ xa × ℂ [ yb ∘ xy ] ≡ xb)
+        propEqs xs = propSig (ℂ.arrowsAreSets _ _) (\ _ → ℂ.arrowsAreSets _ _)
+
+        arrowEq : {X Y : Object} {f g : Arrow X Y} → fst f ≡ fst g → f ≡ g
+        arrowEq {X} {Y} {f} {g} p = λ i → p i , lemPropF propEqs p {snd f} {snd g} i
+
+        isAssociative : IsAssociative
+        isAssociative {f = f , f0 , f1} {g , g0 , g1} {h , h0 , h1} = arrowEq ℂ.isAssociative
+
+        isIdentity : IsIdentity identity
+        isIdentity {AA@(A , a0 , a1)} {BB@(B , b0 , b1)} {f , f0 , f1} = arrowEq ℂ.leftIdentity , arrowEq ℂ.rightIdentity
+
+        arrowsAreSets : ArrowsAreSets
+        arrowsAreSets {X , x0 , x1} {Y , y0 , y1}
+          = sigPresSet ℂ.arrowsAreSets λ a → propSet (propEqs _)
+
+        isPreCat : IsPreCategory raw
+        IsPreCategory.isAssociative isPreCat = isAssociative
+        IsPreCategory.isIdentity    isPreCat = isIdentity
+        IsPreCategory.arrowsAreSets isPreCat = arrowsAreSets
+
+      open IsPreCategory isPreCat
+
+      module _ {𝕏 𝕐 : Object} where
+        open Σ 𝕏 renaming (fst to X ; snd to x)
+        open Σ x renaming (fst to xa ; snd to xb)
+        open Σ 𝕐 renaming (fst to Y ; snd to y)
+        open Σ y renaming (fst to ya ; snd to yb)
+        open import Cat.Equivalence using (composeIso) renaming (_≅_ to _≅_)
+        step0
+          : ((X , xa , xb) ≡ (Y , ya , yb))
+          ≅ (Σ[ p ∈ (X ≡ Y) ] (PathP (λ i → ℂ.Arrow (p i) 𝒜) xa ya) × (PathP (λ i → ℂ.Arrow (p i) ℬ) xb yb))
+        step0
+          = (λ p → cong fst p , cong-d (fst ∘ snd) p , cong-d (snd ∘ snd) p)
+          -- , (λ x  → λ i → fst x i , (fst (snd x) i) , (snd (snd x) i))
+          , (λ{ (p , q , r) → Σ≡ p λ i → q i , r i})
+          , funExt (λ{ p → refl})
+          , funExt (λ{ (p , q , r) → refl})
+
+        step1
+          : (Σ[ p ∈ (X ≡ Y) ] (PathP (λ i → ℂ.Arrow (p i) 𝒜) xa ya) × (PathP (λ i → ℂ.Arrow (p i) ℬ) xb yb))
+          ≅ Σ (X ℂ.≊ Y) (λ iso
+            → let p = ℂ.isoToId iso
+            in
+            ( PathP (λ i → ℂ.Arrow (p i) 𝒜) xa ya)
+            × PathP (λ i → ℂ.Arrow (p i) ℬ) xb yb
+            )
+        step1
+          = symIso
+              (isoSigFst
+                {A = (X ℂ.≊ Y)}
+                {B = (X ≡ Y)}
+                (ℂ.groupoidObject _ _)
+                {Q = \ p → (PathP (λ i → ℂ.Arrow (p i) 𝒜) xa ya) × (PathP (λ i → ℂ.Arrow (p i) ℬ) xb yb)}
+                ℂ.isoToId
+                (symIso (_ , ℂ.asTypeIso {X} {Y}) .snd)
+              )
+
+        step2
+          : Σ (X ℂ.≊ Y) (λ iso
+            → let p = ℂ.isoToId iso
+            in
+            ( PathP (λ i → ℂ.Arrow (p i) 𝒜) xa ya)
+            × PathP (λ i → ℂ.Arrow (p i) ℬ) xb yb
+            )
+          ≅ ((X , xa , xb) ≊ (Y , ya , yb))
+        step2
+          = ( λ{ (iso@(f , f~ , inv-f) , p , q)
+              → ( f  , sym (ℂ.domain-twist-sym  iso p) , sym (ℂ.domain-twist-sym iso q))
+              , ( f~ , sym (ℂ.domain-twist      iso p) , sym (ℂ.domain-twist     iso q))
+              , arrowEq (fst inv-f)
+              , arrowEq (snd inv-f)
+              }
+            )
+          , (λ{ (f , f~ , inv-f , inv-f~) →
+            let
+              iso : X ℂ.≊ Y
+              iso = fst f , fst f~ , cong fst inv-f , cong fst inv-f~
+              p : X ≡ Y
+              p = ℂ.isoToId iso
+              pA : ℂ.Arrow X 𝒜 ≡ ℂ.Arrow Y 𝒜
+              pA = cong (λ x → ℂ.Arrow x 𝒜) p
+              pB : ℂ.Arrow X ℬ ≡ ℂ.Arrow Y ℬ
+              pB = cong (λ x → ℂ.Arrow x ℬ) p
+              k0 = begin
+                coe pB xb ≡⟨ ℂ.coe-dom iso ⟩
+                xb ℂ.<<< fst f~ ≡⟨ snd (snd f~) ⟩
+                yb ∎
+              k1 = begin
+                coe pA xa ≡⟨ ℂ.coe-dom iso ⟩
+                xa ℂ.<<< fst f~ ≡⟨ fst (snd f~) ⟩
+                ya ∎
+            in iso , coe-lem-inv k1 , coe-lem-inv k0})
+          , funExt (λ x → lemSig
+              (λ x → propSig prop0 (λ _ → prop1))
+              _ _
+              (Σ≡ refl (ℂ.propIsomorphism _ _ _)))
+          , funExt (λ{ (f , _) → lemSig propIsomorphism _ _ (Σ≡ refl (propEqs _ _ _))})
+            where
+            prop0 : ∀ {x} → isProp (PathP (λ i → ℂ.Arrow (ℂ.isoToId x i) 𝒜) xa ya)
+            prop0 {x} = pathJ (λ y p → ∀ x → isProp (PathP (λ i → ℂ.Arrow (p i) 𝒜) xa x)) (λ x → ℂ.arrowsAreSets _ _) Y (ℂ.isoToId x) ya
+            prop1 : ∀ {x} → isProp (PathP (λ i → ℂ.Arrow (ℂ.isoToId x i) ℬ) xb yb)
+            prop1 {x} = pathJ (λ y p → ∀ x → isProp (PathP (λ i → ℂ.Arrow (p i) ℬ) xb x)) (λ x → ℂ.arrowsAreSets _ _) Y (ℂ.isoToId x) yb
+        -- One thing to watch out for here is that the isomorphisms going forwards
+        -- must compose to give idToIso
+        iso
+          : ((X , xa , xb) ≡ (Y , ya , yb))
+          ≅ ((X , xa , xb) ≊ (Y , ya , yb))
+        iso = step0 ⊙ step1 ⊙ step2
+          where
+          infixl 5 _⊙_
+          _⊙_ = composeIso
+        equiv1
+          : ((X , xa , xb) ≡ (Y , ya , yb))
+          ≃ ((X , xa , xb) ≊ (Y , ya , yb))
+        equiv1 = _ , fromIso _ _ (snd iso)
+
+      univalent : Univalent
+      univalent = univalenceFrom≃ equiv1
+
+      isCat : IsCategory raw
+      IsCategory.isPreCategory isCat = isPreCat
+      IsCategory.univalent     isCat = univalent
+
+  span : Category _ _
+  span = record
+    { raw = raw
+    ; isCategory = isCat
+    }
diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda
index 274f94e..139fba9 100644
--- a/src/Cat/Category.agda
+++ b/src/Cat/Category.agda
@@ -631,95 +631,3 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
 
   _[_∘_] : {A B C : Object} → (g : Arrow B C) → (f : Arrow A B) → Arrow A C
   _[_∘_] = _<<<_
-
--- | The opposite category
---
--- The opposite category is the category where the direction of the arrows are
--- flipped.
-module Opposite {ℓa ℓb : Level} where
-  module _ (ℂ : Category ℓa ℓb) where
-    private
-      module _ where
-        module ℂ = Category ℂ
-        opRaw : RawCategory ℓa ℓb
-        RawCategory.Object   opRaw = ℂ.Object
-        RawCategory.Arrow    opRaw = flip ℂ.Arrow
-        RawCategory.identity opRaw = ℂ.identity
-        RawCategory._<<<_    opRaw = ℂ._>>>_
-
-        open RawCategory opRaw
-
-        isPreCategory : IsPreCategory opRaw
-        IsPreCategory.isAssociative isPreCategory = sym ℂ.isAssociative
-        IsPreCategory.isIdentity    isPreCategory = swap ℂ.isIdentity
-        IsPreCategory.arrowsAreSets isPreCategory = ℂ.arrowsAreSets
-
-      open IsPreCategory isPreCategory
-
-      module _ {A B : ℂ.Object} where
-        open Σ (toIso _ _ (ℂ.univalent {A} {B}))
-          renaming (fst to idToIso* ; snd to inv*)
-        open AreInverses {f = ℂ.idToIso A B} {idToIso*} inv*
-
-        shuffle : A ≊ B → A ℂ.≊ B
-        shuffle (f , g , inv) = g , f , inv
-
-        shuffle~ : A ℂ.≊ B → A ≊ B
-        shuffle~ (f , g , inv) = g , f , inv
-
-        lem : (p : A ≡ B) → idToIso A B p ≡ shuffle~ (ℂ.idToIso A B p)
-        lem p = isoEq refl
-
-        isoToId* : A ≊ B → A ≡ B
-        isoToId* = idToIso* ∘ shuffle
-
-        inv : AreInverses (idToIso A B) isoToId*
-        inv =
-          ( funExt (λ x → begin
-            (isoToId* ∘ idToIso A B) x
-              ≡⟨⟩
-            (idToIso*  ∘ shuffle ∘ idToIso A B) x
-              ≡⟨ cong (λ φ → φ x) (cong (λ φ → idToIso* ∘ shuffle ∘ φ) (funExt lem)) ⟩
-            (idToIso*  ∘ shuffle ∘ shuffle~ ∘ ℂ.idToIso A B) x
-              ≡⟨⟩
-            (idToIso*  ∘ ℂ.idToIso A B) x
-              ≡⟨ (λ i → verso-recto i x) ⟩
-            x ∎)
-          , funExt (λ x → begin
-            (idToIso A B ∘ idToIso* ∘ shuffle) x
-              ≡⟨ cong (λ φ → φ x) (cong (λ φ → φ ∘ idToIso* ∘ shuffle) (funExt lem)) ⟩
-            (shuffle~ ∘ ℂ.idToIso A B ∘ idToIso* ∘ shuffle) x
-              ≡⟨ cong (λ φ → φ x) (cong (λ φ → shuffle~ ∘ φ ∘ shuffle) recto-verso) ⟩
-            (shuffle~ ∘ shuffle) x
-              ≡⟨⟩
-            x ∎)
-          )
-
-      isCategory : IsCategory opRaw
-      IsCategory.isPreCategory isCategory = isPreCategory
-      IsCategory.univalent     isCategory
-        = univalenceFromIsomorphism (isoToId* , inv)
-
-    opposite : Category ℓa ℓb
-    Category.raw        opposite = opRaw
-    Category.isCategory opposite = isCategory
-
-  -- As demonstrated here a side-effect of having no-eta-equality on constructors
-  -- means that we need to pick things apart to show that things are indeed
-  -- definitionally equal. I.e; a thing that would normally be provable in one
-  -- line now takes 13!! Admittedly it's a simple proof.
-  module _ {ℂ : Category ℓa ℓb} where
-    open Category ℂ
-    private
-      -- Since they really are definitionally equal we just need to pick apart
-      -- the data-type.
-      rawInv : Category.raw (opposite (opposite ℂ)) ≡ raw
-      RawCategory.Object   (rawInv _) = Object
-      RawCategory.Arrow    (rawInv _) = Arrow
-      RawCategory.identity (rawInv _) = identity
-      RawCategory._<<<_    (rawInv _) = _<<<_
-
-    oppositeIsInvolution : opposite (opposite ℂ) ≡ ℂ
-    oppositeIsInvolution = Category≡ rawInv
-
-open Opposite public
diff --git a/src/Cat/Category/Product.agda b/src/Cat/Category/Product.agda
index 4856668..41d10e2 100644
--- a/src/Cat/Category/Product.agda
+++ b/src/Cat/Category/Product.agda
@@ -55,286 +55,122 @@ module _ {ℓa ℓb : Level} (ℂ : Category ℓa ℓb) where
         ×  ℂ [ g ∘ snd ]
         ]
 
-module _ {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} {A B : Category.Object ℂ} where
+module _ {ℓa ℓb : Level} {ℂ : Category ℓa ℓb}
+  (let module ℂ = Category ℂ) {𝒜 ℬ : ℂ.Object} where
   private
-    open Category ℂ
-    module _ (raw : RawProduct ℂ A B) where
-      module _ (x y : IsProduct ℂ A B raw) where
-        private
-          module x = IsProduct x
-          module y = IsProduct y
+    module _ (raw : RawProduct ℂ 𝒜 ℬ) where
+      private
+        open Category ℂ hiding (raw)
+        module _ (x y : IsProduct ℂ 𝒜 ℬ raw) where
+          private
+            module x = IsProduct x
+            module y = IsProduct y
 
-        module _ {X : Object} (f : ℂ [ X , A ]) (g : ℂ [ X , B ]) where
-          module _ (f×g : Arrow X y.object) where
-            help : isProp (∀{y} → (ℂ [ y.fst ∘ y ] ≡ f) P.× (ℂ [ y.snd ∘ y ] ≡ g) → f×g ≡ y)
-            help = propPiImpl (λ _ → propPi (λ _ → arrowsAreSets _ _))
+          module _ {X : Object} (f : ℂ [ X , 𝒜 ]) (g : ℂ [ X , ℬ ]) where
+            module _ (f×g : Arrow X y.object) where
+              help : isProp (∀{y} → (ℂ [ y.fst ∘ y ] ≡ f) P.× (ℂ [ y.snd ∘ y ] ≡ g) → f×g ≡ y)
+              help = propPiImpl (λ _ → propPi (λ _ → arrowsAreSets _ _))
 
-          res = ∃-unique (x.ump f g) (y.ump f g)
+            res = ∃-unique (x.ump f g) (y.ump f g)
 
-          prodAux : x.ump f g ≡ y.ump f g
-          prodAux = lemSig ((λ f×g → propSig (propSig (arrowsAreSets _ _) λ _ → arrowsAreSets _ _) (λ _ → help f×g))) _ _ res
+            prodAux : x.ump f g ≡ y.ump f g
+            prodAux = lemSig ((λ f×g → propSig (propSig (arrowsAreSets _ _) λ _ → arrowsAreSets _ _) (λ _ → help f×g))) _ _ res
 
-        propIsProduct' : x ≡ y
-        propIsProduct' i = record { ump = λ f g → prodAux f g i }
+          propIsProduct' : x ≡ y
+          propIsProduct' i = record { ump = λ f g → prodAux f g i }
 
-      propIsProduct : isProp (IsProduct ℂ A B raw)
+      propIsProduct : isProp (IsProduct ℂ 𝒜 ℬ raw)
       propIsProduct = propIsProduct'
 
-  Product≡ : {x y : Product ℂ A B} → (Product.raw x ≡ Product.raw y) → x ≡ y
-  Product≡ {x} {y} p i = record { raw = p i ; isProduct = q i }
-    where
-    q : (λ i → IsProduct ℂ A B (p i)) [ Product.isProduct x ≡ Product.isProduct y ]
-    q = lemPropF propIsProduct p
+    Product≡ : {x y : Product ℂ 𝒜 ℬ} → (Product.raw x ≡ Product.raw y) → x ≡ y
+    Product≡ {x} {y} p i = record { raw = p i ; isProduct = q i }
+      where
+      q : (λ i → IsProduct ℂ 𝒜 ℬ (p i)) [ Product.isProduct x ≡ Product.isProduct y ]
+      q = lemPropF propIsProduct p
 
-module Try0 {ℓa ℓb : Level} {ℂ : Category ℓa ℓb}
-  (let module ℂ = Category ℂ) {𝒜 ℬ : ℂ.Object} where
+    open P
+    open import Cat.Categories.Span
 
-  open P
+    open Category (span ℂ 𝒜 ℬ)
 
-  module _ where
-    raw : RawCategory _ _
-    raw = record
-      { Object = Σ[ X ∈ ℂ.Object ] ℂ.Arrow X 𝒜 × ℂ.Arrow X ℬ
-      ; Arrow = λ{ (A , a0 , a1) (B , b0 , b1)
-        → Σ[ f ∈ ℂ.Arrow A B ]
-            ℂ [ b0 ∘ f ] ≡ a0
-          × ℂ [ b1 ∘ f ] ≡ a1
-          }
-      ; identity = λ{ {X , f , g} → ℂ.identity {X} , ℂ.rightIdentity , ℂ.rightIdentity}
-      ; _<<<_ = λ { {_ , a0 , a1} {_ , b0 , b1} {_ , c0 , c1} (f , f0 , f1) (g , g0 , g1)
-        → (f ℂ.<<< g)
-          , (begin
-              ℂ [ c0 ∘ ℂ [ f ∘ g ] ] ≡⟨ ℂ.isAssociative ⟩
-              ℂ [ ℂ [ c0 ∘ f ] ∘ g ] ≡⟨ cong (λ φ → ℂ [ φ ∘ g ]) f0 ⟩
-              ℂ [ b0 ∘ g ] ≡⟨ g0 ⟩
-              a0 ∎
-            )
-          , (begin
-             ℂ [ c1 ∘ ℂ [ f ∘ g ] ] ≡⟨ ℂ.isAssociative ⟩
-             ℂ [ ℂ [ c1 ∘ f ] ∘ g ] ≡⟨ cong (λ φ → ℂ [ φ ∘ g ]) f1 ⟩
-             ℂ [ b1 ∘ g ] ≡⟨ g1 ⟩
-              a1 ∎
-            )
-        }
-      }
-
-    module _ where
-      open RawCategory raw
-
-      propEqs : ∀ {X' : Object}{Y' : Object} (let X , xa , xb = X') (let Y , ya , yb = Y')
-                  → (xy : ℂ.Arrow X Y) → isProp (ℂ [ ya ∘ xy ] ≡ xa × ℂ [ yb ∘ xy ] ≡ xb)
-      propEqs xs = propSig (ℂ.arrowsAreSets _ _) (\ _ → ℂ.arrowsAreSets _ _)
-
-      arrowEq : {X Y : Object} {f g : Arrow X Y} → fst f ≡ fst g → f ≡ g
-      arrowEq {X} {Y} {f} {g} p = λ i → p i , lemPropF propEqs p {snd f} {snd g} i
-
-      private
-        isAssociative : IsAssociative
-        isAssociative {f = f , f0 , f1} {g , g0 , g1} {h , h0 , h1} = arrowEq ℂ.isAssociative
-
-        isIdentity : IsIdentity identity
-        isIdentity {AA@(A , a0 , a1)} {BB@(B , b0 , b1)} {f , f0 , f1} = arrowEq ℂ.leftIdentity , arrowEq ℂ.rightIdentity
-
-        arrowsAreSets : ArrowsAreSets
-        arrowsAreSets {X , x0 , x1} {Y , y0 , y1}
-          = sigPresSet ℂ.arrowsAreSets λ a → propSet (propEqs _)
-
-      isPreCat : IsPreCategory raw
-      IsPreCategory.isAssociative isPreCat = isAssociative
-      IsPreCategory.isIdentity    isPreCat = isIdentity
-      IsPreCategory.arrowsAreSets isPreCat = arrowsAreSets
-
-    open IsPreCategory isPreCat
-
-    module _ {𝕏 𝕐 : Object} where
-      open Σ 𝕏 renaming (fst to X ; snd to x)
-      open Σ x renaming (fst to xa ; snd to xb)
-      open Σ 𝕐 renaming (fst to Y ; snd to y)
-      open Σ y renaming (fst to ya ; snd to yb)
-      open import Cat.Equivalence using (composeIso) renaming (_≅_ to _≅_)
-      step0
-        : ((X , xa , xb) ≡ (Y , ya , yb))
-        ≅ (Σ[ p ∈ (X ≡ Y) ] (PathP (λ i → ℂ.Arrow (p i) 𝒜) xa ya) × (PathP (λ i → ℂ.Arrow (p i) ℬ) xb yb))
-      step0
-        = (λ p → cong fst p , cong-d (fst ∘ snd) p , cong-d (snd ∘ snd) p)
-        -- , (λ x  → λ i → fst x i , (fst (snd x) i) , (snd (snd x) i))
-        , (λ{ (p , q , r) → Σ≡ p λ i → q i , r i})
-        , funExt (λ{ p → refl})
-        , funExt (λ{ (p , q , r) → refl})
-
-      step1
-        : (Σ[ p ∈ (X ≡ Y) ] (PathP (λ i → ℂ.Arrow (p i) 𝒜) xa ya) × (PathP (λ i → ℂ.Arrow (p i) ℬ) xb yb))
-        ≅ Σ (X ℂ.≊ Y) (λ iso
-          → let p = ℂ.isoToId iso
-          in
-          ( PathP (λ i → ℂ.Arrow (p i) 𝒜) xa ya)
-          × PathP (λ i → ℂ.Arrow (p i) ℬ) xb yb
-          )
-      step1
-        = symIso
-            (isoSigFst
-              {A = (X ℂ.≊ Y)}
-              {B = (X ≡ Y)}
-              (ℂ.groupoidObject _ _)
-              {Q = \ p → (PathP (λ i → ℂ.Arrow (p i) 𝒜) xa ya) × (PathP (λ i → ℂ.Arrow (p i) ℬ) xb yb)}
-              ℂ.isoToId
-              (symIso (_ , ℂ.asTypeIso {X} {Y}) .snd)
-            )
-
-      step2
-        : Σ (X ℂ.≊ Y) (λ iso
-          → let p = ℂ.isoToId iso
-          in
-          ( PathP (λ i → ℂ.Arrow (p i) 𝒜) xa ya)
-          × PathP (λ i → ℂ.Arrow (p i) ℬ) xb yb
-          )
-        ≅ ((X , xa , xb) ≊ (Y , ya , yb))
-      step2
-        = ( λ{ (iso@(f , f~ , inv-f) , p , q)
-            → ( f  , sym (ℂ.domain-twist-sym  iso p) , sym (ℂ.domain-twist-sym iso q))
-            , ( f~ , sym (ℂ.domain-twist      iso p) , sym (ℂ.domain-twist     iso q))
-            , arrowEq (fst inv-f)
-            , arrowEq (snd inv-f)
-            }
-          )
-        , (λ{ (f , f~ , inv-f , inv-f~) →
-          let
-            iso : X ℂ.≊ Y
-            iso = fst f , fst f~ , cong fst inv-f , cong fst inv-f~
-            p : X ≡ Y
-            p = ℂ.isoToId iso
-            pA : ℂ.Arrow X 𝒜 ≡ ℂ.Arrow Y 𝒜
-            pA = cong (λ x → ℂ.Arrow x 𝒜) p
-            pB : ℂ.Arrow X ℬ ≡ ℂ.Arrow Y ℬ
-            pB = cong (λ x → ℂ.Arrow x ℬ) p
-            k0 = begin
-              coe pB xb ≡⟨ ℂ.coe-dom iso ⟩
-              xb ℂ.<<< fst f~ ≡⟨ snd (snd f~) ⟩
-              yb ∎
-            k1 = begin
-              coe pA xa ≡⟨ ℂ.coe-dom iso ⟩
-              xa ℂ.<<< fst f~ ≡⟨ fst (snd f~) ⟩
-              ya ∎
-          in iso , coe-lem-inv k1 , coe-lem-inv k0})
-        , funExt (λ x → lemSig
-            (λ x → propSig prop0 (λ _ → prop1))
-            _ _
-            (Σ≡ refl (ℂ.propIsomorphism _ _ _)))
-        , funExt (λ{ (f , _) → lemSig propIsomorphism _ _ (Σ≡ refl (propEqs _ _ _))})
-          where
-          prop0 : ∀ {x} → isProp (PathP (λ i → ℂ.Arrow (ℂ.isoToId x i) 𝒜) xa ya)
-          prop0 {x} = pathJ (λ y p → ∀ x → isProp (PathP (λ i → ℂ.Arrow (p i) 𝒜) xa x)) (λ x → ℂ.arrowsAreSets _ _) Y (ℂ.isoToId x) ya
-          prop1 : ∀ {x} → isProp (PathP (λ i → ℂ.Arrow (ℂ.isoToId x i) ℬ) xb yb)
-          prop1 {x} = pathJ (λ y p → ∀ x → isProp (PathP (λ i → ℂ.Arrow (p i) ℬ) xb x)) (λ x → ℂ.arrowsAreSets _ _) Y (ℂ.isoToId x) yb
-      -- One thing to watch out for here is that the isomorphisms going forwards
-      -- must compose to give idToIso
-      iso
-        : ((X , xa , xb) ≡ (Y , ya , yb))
-        ≅ ((X , xa , xb) ≊ (Y , ya , yb))
-      iso = step0 ⊙ step1 ⊙ step2
+    lemma : Terminal ≃ Product ℂ 𝒜 ℬ
+    lemma = fromIsomorphism Terminal (Product ℂ 𝒜 ℬ) (f , g , inv)
+      where
+      f : Terminal → Product ℂ 𝒜 ℬ
+      f ((X , x0 , x1) , uniq) = p
         where
-        infixl 5 _⊙_
-        _⊙_ = composeIso
-      equiv1
-        : ((X , xa , xb) ≡ (Y , ya , yb))
-        ≃ ((X , xa , xb) ≊ (Y , ya , yb))
-      equiv1 = _ , fromIso _ _ (snd iso)
-
-    univalent : Univalent
-    univalent = univalenceFrom≃ equiv1
-
-    isCat : IsCategory raw
-    IsCategory.isPreCategory isCat = isPreCat
-    IsCategory.univalent     isCat = univalent
-
-    cat : Category _ _
-    cat = record
-      { raw = raw
-      ; isCategory = isCat
-      }
-
-  open Category cat
-
-  lemma : Terminal ≃ Product ℂ 𝒜 ℬ
-  lemma = fromIsomorphism Terminal (Product ℂ 𝒜 ℬ) (f , g , inv)
-  -- C-x 8 RET MATHEMATICAL BOLD SCRIPT CAPITAL A
-  -- 𝒜
-    where
-    f : Terminal → Product ℂ 𝒜 ℬ
-    f ((X , x0 , x1) , uniq) = p
-      where
-      rawP : RawProduct ℂ 𝒜 ℬ
-      rawP = record
-        { object = X
-        ; fst = x0
-        ; snd = x1
-        }
-      -- open RawProduct rawP renaming (fst to x0 ; snd to x1)
-      module _ {Y : ℂ.Object} (p0 : ℂ [ Y , 𝒜 ]) (p1 : ℂ [ Y , ℬ ]) where
-        uy : isContr (Arrow (Y , p0 , p1) (X , x0 , x1))
-        uy = uniq {Y , p0 , p1}
-        open Σ uy renaming (fst to Y→X ; snd to contractible)
-        open Σ Y→X renaming (fst to p0×p1 ; snd to cond)
-        ump : ∃![ f×g ] (ℂ [ x0 ∘ f×g ] ≡ p0 P.× ℂ [ x1 ∘ f×g ] ≡ p1)
-        ump = p0×p1 , cond , λ {f} cond-f → cong fst (contractible (f , cond-f))
-      isP : IsProduct ℂ 𝒜 ℬ rawP
-      isP = record { ump = ump }
-      p : Product ℂ 𝒜 ℬ
-      p = record
-        { raw = rawP
-        ; isProduct = isP
-        }
-    g : Product ℂ 𝒜 ℬ → Terminal
-    g p = 𝒳 , t
-      where
-      open Product p renaming (object to X ; fst to x₀ ; snd to x₁) using ()
-      module p = Product p
-      module isp = IsProduct p.isProduct
-      𝒳 : Object
-      𝒳 = X , x₀ , x₁
-      module _ {𝒴 : Object} where
-        open Σ 𝒴 renaming (fst to Y)
-        open Σ (snd 𝒴) renaming (fst to y₀ ; snd to y₁)
-        ump = p.ump y₀ y₁
-        open Σ ump renaming (fst to f')
-        open Σ (snd ump) renaming (fst to f'-cond)
-        𝒻 : Arrow 𝒴 𝒳
-        𝒻 = f' , f'-cond
-        contractible : (f : Arrow 𝒴 𝒳) → 𝒻 ≡ f
-        contractible ff@(f , f-cond) = res
-          where
-          k : f' ≡ f
-          k = snd (snd ump) f-cond
-          prp : (a : ℂ.Arrow Y X) → isProp
-            ( (ℂ [ x₀ ∘ a ] ≡ y₀)
-            × (ℂ [ x₁ ∘ a ] ≡ y₁)
-            )
-          prp f f0 f1 = Σ≡
-            (ℂ.arrowsAreSets _ _ (fst f0) (fst f1))
-            (ℂ.arrowsAreSets _ _ (snd f0) (snd f1))
-          h :
-            ( λ i
-              → ℂ [ x₀ ∘ k i ] ≡ y₀
-              × ℂ [ x₁ ∘ k i ] ≡ y₁
-            ) [ f'-cond ≡ f-cond ]
-          h = lemPropF prp k
-          res : (f' , f'-cond) ≡ (f , f-cond)
-          res = Σ≡ k h
-      t : IsTerminal 𝒳
-      t {𝒴} = 𝒻 , contractible
-    ve-re : ∀ x → g (f x) ≡ x
-    ve-re x = Propositionality.propTerminal _ _
-    re-ve : ∀ p → f (g p) ≡ p
-    re-ve p = Product≡ e
-      where
-      module p = Product p
-      -- RawProduct does not have eta-equality.
-      e : Product.raw (f (g p)) ≡ Product.raw p
-      RawProduct.object (e i) = p.object
-      RawProduct.fst (e i) = p.fst
-      RawProduct.snd (e i) = p.snd
-    inv : AreInverses f g
-    inv = funExt ve-re , funExt re-ve
+        rawP : RawProduct ℂ 𝒜 ℬ
+        rawP = record
+          { object = X
+          ; fst = x0
+          ; snd = x1
+          }
+        -- open RawProduct rawP renaming (fst to x0 ; snd to x1)
+        module _ {Y : ℂ.Object} (p0 : ℂ [ Y , 𝒜 ]) (p1 : ℂ [ Y , ℬ ]) where
+          uy : isContr (Arrow (Y , p0 , p1) (X , x0 , x1))
+          uy = uniq {Y , p0 , p1}
+          open Σ uy renaming (fst to Y→X ; snd to contractible)
+          open Σ Y→X renaming (fst to p0×p1 ; snd to cond)
+          ump : ∃![ f×g ] (ℂ [ x0 ∘ f×g ] ≡ p0 P.× ℂ [ x1 ∘ f×g ] ≡ p1)
+          ump = p0×p1 , cond , λ {f} cond-f → cong fst (contractible (f , cond-f))
+        isP : IsProduct ℂ 𝒜 ℬ rawP
+        isP = record { ump = ump }
+        p : Product ℂ 𝒜 ℬ
+        p = record
+          { raw = rawP
+          ; isProduct = isP
+          }
+      g : Product ℂ 𝒜 ℬ → Terminal
+      g p = 𝒳 , t
+        where
+        open Product p renaming (object to X ; fst to x₀ ; snd to x₁) using ()
+        module p = Product p
+        module isp = IsProduct p.isProduct
+        𝒳 : Object
+        𝒳 = X , x₀ , x₁
+        module _ {𝒴 : Object} where
+          open Σ 𝒴 renaming (fst to Y)
+          open Σ (snd 𝒴) renaming (fst to y₀ ; snd to y₁)
+          ump = p.ump y₀ y₁
+          open Σ ump renaming (fst to f')
+          open Σ (snd ump) renaming (fst to f'-cond)
+          𝒻 : Arrow 𝒴 𝒳
+          𝒻 = f' , f'-cond
+          contractible : (f : Arrow 𝒴 𝒳) → 𝒻 ≡ f
+          contractible ff@(f , f-cond) = res
+            where
+            k : f' ≡ f
+            k = snd (snd ump) f-cond
+            prp : (a : ℂ.Arrow Y X) → isProp
+              ( (ℂ [ x₀ ∘ a ] ≡ y₀)
+              × (ℂ [ x₁ ∘ a ] ≡ y₁)
+              )
+            prp f f0 f1 = Σ≡
+              (ℂ.arrowsAreSets _ _ (fst f0) (fst f1))
+              (ℂ.arrowsAreSets _ _ (snd f0) (snd f1))
+            h :
+              ( λ i
+                → ℂ [ x₀ ∘ k i ] ≡ y₀
+                × ℂ [ x₁ ∘ k i ] ≡ y₁
+              ) [ f'-cond ≡ f-cond ]
+            h = lemPropF prp k
+            res : (f' , f'-cond) ≡ (f , f-cond)
+            res = Σ≡ k h
+        t : IsTerminal 𝒳
+        t {𝒴} = 𝒻 , contractible
+      ve-re : ∀ x → g (f x) ≡ x
+      ve-re x = Propositionality.propTerminal _ _
+      re-ve : ∀ p → f (g p) ≡ p
+      re-ve p = Product≡ e
+        where
+        module p = Product p
+        -- RawProduct does not have eta-equality.
+        e : Product.raw (f (g p)) ≡ Product.raw p
+        RawProduct.object (e i) = p.object
+        RawProduct.fst (e i) = p.fst
+        RawProduct.snd (e i) = p.snd
+      inv : AreInverses f g
+      inv = funExt ve-re , funExt re-ve
 
   propProduct : isProp (Product ℂ 𝒜 ℬ)
   propProduct = equivPreservesNType {n = ⟨-1⟩} lemma Propositionality.propTerminal
@@ -348,10 +184,7 @@ module _ {ℓa ℓb : Level} {ℂ : Category ℓa ℓb} {A B : Category.Object 
         module y = HasProducts y
 
       productEq : x.product ≡ y.product
-      productEq = funExt λ A → funExt λ B → Try0.propProduct _ _
+      productEq = funExt λ A → funExt λ B → propProduct _ _
 
   propHasProducts : isProp (HasProducts ℂ)
   propHasProducts x y i = record { product = productEq x y i }
-
-fmap≡ : {A : Set} {a0 a1 : A} {B : Set} → (f : A → B) → Path a0 a1 → Path (f a0) (f a1)
-fmap≡ = cong
diff --git a/src/Cat/Category/Yoneda.agda b/src/Cat/Category/Yoneda.agda
index c02274b..1fbe990 100644
--- a/src/Cat/Category/Yoneda.agda
+++ b/src/Cat/Category/Yoneda.agda
@@ -9,9 +9,9 @@ open import Cat.Category.Functor
 open import Cat.Category.NaturalTransformation
   renaming (module Properties to F)
   using ()
-
-open import Cat.Categories.Fun using (module Fun)
+open import Cat.Categories.Opposite
 open import Cat.Categories.Sets hiding (presheaf)
+open import Cat.Categories.Fun using (module Fun)
 
 -- There is no (small) category of categories. So we won't use _⇑_ from
 -- `HasExponential`