diff --git a/src/Cat/Instances/Product.lagda.md b/src/Cat/Instances/Product.lagda.md
index 02d538f29..7c38c0db3 100644
--- a/src/Cat/Instances/Product.lagda.md
+++ b/src/Cat/Instances/Product.lagda.md
@@ -135,7 +135,6 @@ _nt×_ α β .is-natural (c , d) (c' , d') (f , g) = Σ-pathp
 ```
 -->
 
-
 ## Univalence
 
 Isomorphisms in functor categories admit a short description, too: They
diff --git a/src/Cat/Instances/Product/Opposite.lagda.md b/src/Cat/Instances/Product/Opposite.lagda.md
new file mode 100644
index 000000000..8ea746955
--- /dev/null
+++ b/src/Cat/Instances/Product/Opposite.lagda.md
@@ -0,0 +1,46 @@
+<!--
+```agda
+open import Cat.Functor.Equivalence
+open import Cat.Functor.Properties
+open import Cat.Instances.Product
+open import Cat.Functor.Base
+open import Cat.Prelude
+
+import Cat.Reasoning
+```
+-->
+
+```agda
+module Cat.Instances.Product.Opposite {o₁ h₁ o₂ h₂ : Level} 
+  {C : Precategory o₁ h₁} {D : Precategory o₁ h₁}
+  where
+```
+
+<!--
+```agda
+open Precategory
+open Functor
+```
+-->
+
+# Opposite product category {defines="opposite-product-category"}
+
+As one might expect, taking the [[opposite category]] of a [[product category]]
+agrees with the product of opposite categories. Rather than showing 
+equality we construct an [[isomorphism of precategories]].
+
+```agda
+×^op : Functor ((C ×ᶜ D)^op) (C ^op ×ᶜ D ^op)
+×^op .F₀ x = x
+×^op .F₁ f = f 
+×^op .F-id = refl
+×^op .F-∘ f g = refl
+
+×^op-is-iso : is-precat-iso ×^op
+×^op-is-iso = iso has-is-ff has-is-iso where 
+  has-is-ff : Cat.Functor.Properties.is-fully-faithful ×^op
+  has-is-ff = id-equiv
+
+  has-is-iso : is-equiv (F₀ ×^op)
+  has-is-iso = id-equiv
+```