From f0beec1530b428713ff177068566a7d845ea112a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Sun, 25 Feb 2018 15:23:33 +0100
Subject: [PATCH] Rename Opposite to opposite

---
 src/Cat/Categories/Fun.agda      | 2 +-
 src/Cat/Categories/Sets.agda     | 4 ++--
 src/Cat/Category.agda            | 2 +-
 src/Cat/Category/Properties.agda | 2 +-
 src/Cat/CwF.agda                 | 2 +-
 5 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/src/Cat/Categories/Fun.agda b/src/Cat/Categories/Fun.agda
index ac7fd8a..2af9e55 100644
--- a/src/Cat/Categories/Fun.agda
+++ b/src/Cat/Categories/Fun.agda
@@ -108,7 +108,7 @@ module Fun {ℓc ℓc' ℓd ℓd' : Level} (ℂ : Category ℓc ℓc') (𝔻 : C
 
 module _ {ℓ ℓ' : Level} (ℂ : Category ℓ ℓ') where
   open import Cat.Categories.Sets
-  open NaturalTransformation (Opposite ℂ) (𝓢𝓮𝓽 ℓ')
+  open NaturalTransformation (opposite ℂ) (𝓢𝓮𝓽 ℓ')
 
   -- Restrict the functors to Presheafs.
   RawPresh : RawCategory (ℓ ⊔ lsuc ℓ') (ℓ ⊔ ℓ')
diff --git a/src/Cat/Categories/Sets.agda b/src/Cat/Categories/Sets.agda
index 035c743..0ed99a3 100644
--- a/src/Cat/Categories/Sets.agda
+++ b/src/Cat/Categories/Sets.agda
@@ -88,7 +88,7 @@ module _ {ℓa ℓb : Level} where
 
     -- Contravariant Presheaf
     Presheaf : Set (ℓa ⊔ lsuc ℓb)
-    Presheaf = Functor (Opposite ℂ) (𝓢𝓮𝓽 ℓb)
+    Presheaf = Functor (opposite ℂ) (𝓢𝓮𝓽 ℓb)
 
   -- The "co-yoneda" embedding.
   representable : {ℂ : Category ℓa ℓb} → Category.Object ℂ → Representable ℂ
@@ -106,7 +106,7 @@ module _ {ℓa ℓb : Level} where
       open Category ℂ
 
   -- Alternate name: `yoneda`
-  presheaf : {ℂ : Category ℓa ℓb} → Category.Object (Opposite ℂ) → Presheaf ℂ
+  presheaf : {ℂ : Category ℓa ℓb} → Category.Object (opposite ℂ) → Presheaf ℂ
   presheaf {ℂ = ℂ} B = record
     { raw = record
       { func* = λ A → ℂ [ A , B ] , arrowsAreSets
diff --git a/src/Cat/Category.agda b/src/Cat/Category.agda
index 7ba7eb9..d70fc65 100644
--- a/src/Cat/Category.agda
+++ b/src/Cat/Category.agda
@@ -336,4 +336,4 @@ module Opposite {ℓa ℓb : Level} where
     Category.raw        (oppositeIsInvolution i) = rawInv i
     Category.isCategory (oppositeIsInvolution x) = {!!}
 
-open Opposite public renaming (opposite to Opposite)
+open Opposite public
diff --git a/src/Cat/Category/Properties.agda b/src/Cat/Category/Properties.agda
index 957b31f..5462f13 100644
--- a/src/Cat/Category/Properties.agda
+++ b/src/Cat/Category/Properties.agda
@@ -22,7 +22,7 @@ module _ {ℓ : Level} {ℂ : Category ℓ ℓ} (unprovable : IsCategory (RawCat
   open import Cat.Category.Exponential
   open Functor
   𝓢 = Sets ℓ
-  open Fun (Opposite ℂ) 𝓢
+  open Fun (opposite ℂ) 𝓢
   private
     Catℓ : Category _ _
     Catℓ = record { raw = RawCat ℓ ℓ ; isCategory = unprovable}
diff --git a/src/Cat/CwF.agda b/src/Cat/CwF.agda
index 3954ea5..584268d 100644
--- a/src/Cat/CwF.agda
+++ b/src/Cat/CwF.agda
@@ -22,7 +22,7 @@ module _ {ℓa ℓb : Level} where
     Substitutions = Arrow ℂ
     field
       -- A functor T
-      T : Functor (Opposite ℂ) (Fam ℓa ℓb)
+      T : Functor (opposite ℂ) (Fam ℓa ℓb)
       -- Empty context
       [] : Terminal ℂ
     private