Rename Opposite to opposite

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 ℓ') (ℓ ⊔ ℓ')

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

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

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}

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