diff --git a/Cubical/AlgebraicGeometry/Functorial/ZFunctors/Base.agda b/Cubical/AlgebraicGeometry/Functorial/ZFunctors/Base.agda
index 46b1f4bcf4..d3a07111c9 100644
--- a/Cubical/AlgebraicGeometry/Functorial/ZFunctors/Base.agda
+++ b/Cubical/AlgebraicGeometry/Functorial/ZFunctors/Base.agda
@@ -43,6 +43,7 @@ open import Cubical.Categories.Instances.Sets
 open import Cubical.Categories.Instances.CommRings
 open import Cubical.Categories.Instances.Functors
 open import Cubical.Categories.NaturalTransformation
+open import Cubical.Categories.Presheaf
 open import Cubical.Categories.Yoneda
 open import Cubical.Categories.Site.Sheaf
 open import Cubical.Categories.Site.Instances.ZariskiCommRing
@@ -60,16 +61,19 @@ module _ {ℓ : Level} where
   open CommRingStr ⦃...⦄
   open IsCommRingHom
 
+  Aff : Category (ℓ-suc ℓ) ℓ
+  Aff = CommRingsCategory {ℓ = ℓ} ^op
 
   -- using the naming conventions of Demazure & Gabriel
-  ℤFunctor = Functor (CommRingsCategory {ℓ = ℓ}) (SET ℓ)
-  ℤFUNCTOR = FUNCTOR (CommRingsCategory {ℓ = ℓ}) (SET ℓ)
+  ℤFunctor = Presheaf Aff ℓ
+  ℤFUNCTOR = PresheafCategory Aff ℓ
 
   -- Yoneda in the notation of Demazure & Gabriel,
   -- uses that double op is original category definitionally
-  Sp : Functor (CommRingsCategory {ℓ = ℓ} ^op) ℤFUNCTOR
-  Sp = YO {C = (CommRingsCategory {ℓ = ℓ} ^op)}
+  Sp : Functor Aff ℤFUNCTOR
+  Sp = YO
 
+  -- TODO: should probably just be hasUniversalElement
   isAffine : (X : ℤFunctor) → Type (ℓ-suc ℓ)
   isAffine X = ∃[ A ∈ CommRing ℓ ] NatIso (Sp .F-ob A) X
   -- TODO: 𝔸¹ ≅ Sp ℤ[x] and 𝔾ₘ ≅ Sp ℤ[x,x⁻¹] ≅ D(x) ↪ 𝔸¹ as first examples of affine schemes
@@ -82,7 +86,7 @@ module _ {ℓ : Level} where
   -- aka the affine line
   -- (aka the representable of ℤ[x])
   𝔸¹ : ℤFunctor
-  𝔸¹ = ForgetfulCommRing→Set
+  𝔸¹ = ForgetfulCommRing→Set ∘F fromOpOp
 
   -- the global sections functor
   𝓞 : Functor ℤFUNCTOR (CommRingsCategory {ℓ = ℓ-suc ℓ} ^op)
diff --git a/Cubical/Categories/Category/Base.agda b/Cubical/Categories/Category/Base.agda
index 578e7f446d..5191bd4c4e 100644
--- a/Cubical/Categories/Category/Base.agda
+++ b/Cubical/Categories/Category/Base.agda
@@ -12,7 +12,8 @@ private
 
 -- Categories with hom-sets
 record Category ℓ ℓ' : Type (ℓ-suc (ℓ-max ℓ ℓ')) where
-  -- no-eta-equality ; NOTE: need eta equality for `opop`
+  -- TODO: document the impetus for this change
+  no-eta-equality
   field
     ob : Type ℓ
     Hom[_,_] : ob → ob → Type ℓ'
@@ -137,6 +138,7 @@ isPropIsUnivalent =
   (isPropΠ2 λ _ _ → isPropIsEquiv _ )
 
 -- Opposite category
+-- TODO: move all of this to Constructions.Opposite?
 _^op : Category ℓ ℓ' → Category ℓ ℓ'
 ob (C ^op)           = ob C
 Hom[_,_] (C ^op) x y = C [ y , x ]
diff --git a/Cubical/Categories/Category/Path.agda b/Cubical/Categories/Category/Path.agda
index 74cc93e22a..9313937d50 100644
--- a/Cubical/Categories/Category/Path.agda
+++ b/Cubical/Categories/Category/Path.agda
@@ -79,40 +79,42 @@ module _ {C C' : Category ℓ ℓ'} where
   id≡ c = cong id pa
   ⋆≡ c = cong _⋆_ pa
 
- CategoryPathIso : Iso (CategoryPath C C') (C ≡ C')
- Iso.fun CategoryPathIso = CategoryPath.mk≡
- Iso.inv CategoryPathIso = ≡→CategoryPath
- Iso.rightInv CategoryPathIso b i j = c
-  where
-  cp = ≡→CategoryPath b
-  b' = CategoryPath.mk≡ cp
-  module _ (j : I) where
-    module c' = Category (b j)
-
-  c : Category ℓ ℓ'
-  ob c = c'.ob j
-  Hom[_,_] c = c'.Hom[_,_] j
-  id c = c'.id j
-  _⋆_ c = c'._⋆_ j
-  ⋆IdL c = isProp→SquareP (λ i j →
+
+ module _ (b : C ≡ C') where
+   private
+     cp = ≡→CategoryPath b
+     b' = CategoryPath.mk≡ cp
+
+   CategoryPathIsoRightInv : mk≡ (≡→CategoryPath b) ≡ b
+   CategoryPathIsoRightInv i j .ob = b j .ob
+   CategoryPathIsoRightInv i j .Hom[_,_] = b j .Hom[_,_]
+   CategoryPathIsoRightInv i j .id = b j .id
+   CategoryPathIsoRightInv i j ._⋆_ = b j ._⋆_
+   CategoryPathIsoRightInv i j .⋆IdL = isProp→SquareP (λ i j →
       isPropImplicitΠ2 λ x y → isPropΠ λ f →
         (isSetHom≡ cp j {x} {y})
-         (c'._⋆_ j (c'.id j) f) f)
-      refl refl (λ j → b' j .⋆IdL) (λ j → c'.⋆IdL j) i j
-  ⋆IdR c = isProp→SquareP (λ i j →
+         (b j ._⋆_ (b j .id) f) f)
+      refl refl (λ j → b' j .⋆IdL) (λ j → b j .⋆IdL) i j
+   CategoryPathIsoRightInv i j .⋆IdR = isProp→SquareP (λ i j →
       isPropImplicitΠ2 λ x y → isPropΠ λ f →
         (isSetHom≡ cp j {x} {y})
-         (c'._⋆_ j f (c'.id j)) f)
-      refl refl (λ j → b' j .⋆IdR) (λ j → c'.⋆IdR j) i j
-  ⋆Assoc c = isProp→SquareP (λ i j →
+         (b j ._⋆_ f (b j .id)) f)
+      refl refl (λ j → b' j .⋆IdR) (λ j → b j .⋆IdR) i j
+   CategoryPathIsoRightInv i j .⋆Assoc = isProp→SquareP (λ i j →
       isPropImplicitΠ4 λ x y z w → isPropΠ3 λ f g h →
         (isSetHom≡ cp j {x} {w})
-         (c'._⋆_ j (c'._⋆_ j {x} {y} {z} f g) h)
-         (c'._⋆_ j f (c'._⋆_ j g h)))
-      refl refl (λ j → b' j .⋆Assoc) (λ j → c'.⋆Assoc j) i j
-  isSetHom c = isProp→SquareP (λ i j →
-      isPropImplicitΠ2 λ x y → isPropIsSet {A = c'.Hom[_,_] j x y})
-      refl refl (λ j → b' j .isSetHom) (λ j → c'.isSetHom j) i j
+         (b j ._⋆_ (b j ._⋆_ {x} {y} {z} f g) h)
+         (b j ._⋆_ f (b j ._⋆_ g h)))
+      refl refl (λ j → b' j .⋆Assoc) (λ j → b j .⋆Assoc) i j
+   CategoryPathIsoRightInv i j .isSetHom = isProp→SquareP (λ i j →
+      isPropImplicitΠ2 λ x y → isPropIsSet {A = b j .Hom[_,_] x y})
+      refl refl (λ j → b' j .isSetHom) (λ j → b j .isSetHom) i j
+
+ CategoryPathIso : Iso (CategoryPath C C') (C ≡ C')
+ Iso.fun CategoryPathIso = CategoryPath.mk≡
+ Iso.inv CategoryPathIso = ≡→CategoryPath
+ Iso.rightInv CategoryPathIso = CategoryPathIsoRightInv
+
  ob≡ (Iso.leftInv CategoryPathIso a i) = ob≡ a
  Hom≡ (Iso.leftInv CategoryPathIso a i) = Hom≡ a
  id≡ (Iso.leftInv CategoryPathIso a i) = id≡ a
diff --git a/Cubical/Categories/Category/Properties.agda b/Cubical/Categories/Category/Properties.agda
index e693d332fb..fcefca4396 100644
--- a/Cubical/Categories/Category/Properties.agda
+++ b/Cubical/Categories/Category/Properties.agda
@@ -29,9 +29,10 @@ module _ {C : Category ℓ ℓ'} where
   isSetHomP2r = isOfHLevel→isOfHLevelDep 2 (λ a → isSetHom C {y = a})
 
 
--- opposite of opposite is definitionally equal to itself
-involutiveOp : ∀ {C : Category ℓ ℓ'} → C ^op ^op ≡ C
-involutiveOp = refl
+-- opposite of opposite is *not* definitionally equal to itself.
+-- The following does *not* type check because of no-eta-equality.
+-- involutiveOp : ∀ {C : Category ℓ ℓ'} → C ^op ^op ≡ C
+-- involutiveOp = refl
 
 module _ {C : Category ℓ ℓ'} where
   -- Other useful operations on categories
diff --git a/Cubical/Categories/Constructions/Opposite.agda b/Cubical/Categories/Constructions/Opposite.agda
index c4fe24d0f1..b7e3dfccf0 100644
--- a/Cubical/Categories/Constructions/Opposite.agda
+++ b/Cubical/Categories/Constructions/Opposite.agda
@@ -23,17 +23,16 @@ module _ {C : Category ℓC ℓC'} (isUnivC : isUnivalent C) where
     J (λ y p → op-Iso (pathToIso {C = C} p) ≡ pathToIso {C = C ^op} p)
       (CatIso≡ _ _ refl)
 
-  op-Iso-pathToIso' : ∀ {x y : C .ob} (p : x ≡ y)
-                   → op-Iso (pathToIso {C = C ^op} p) ≡ pathToIso {C = C} p
-  op-Iso-pathToIso' =
-    J (λ y p → op-Iso (pathToIso {C = C ^op} p) ≡ pathToIso {C = C} p)
-      (CatIso≡ _ _ refl)
+  op-Iso⁻-pathToIso : ∀ {x y : C .ob} (p : x ≡ y)
+                   → op-Iso⁻ (pathToIso {C = C ^op} p) ≡ pathToIso {C = C} p
+  op-Iso⁻-pathToIso =
+    J (λ _ p → op-Iso⁻ (pathToIso p) ≡ pathToIso p) (CatIso≡ _ _ refl)
 
   isUnivalentOp : isUnivalent (C ^op)
   isUnivalentOp .univ x y = isIsoToIsEquiv
-    ( (λ f^op → CatIsoToPath isUnivC (op-Iso f^op))
+    ( (λ f^op → CatIsoToPath isUnivC (op-Iso⁻ f^op))
     , (λ f^op → CatIso≡ _ _
-        (cong fst
-        (cong op-Iso ((secEq (univEquiv isUnivC _ _) (op-Iso f^op))))))
-    , λ p → cong (CatIsoToPath isUnivC) (op-Iso-pathToIso' p)
+      (cong fst (cong op-Iso (secEq (univEquiv isUnivC _ _) (op-Iso⁻ f^op)))))
+    , λ p →
+        cong (CatIsoToPath isUnivC) (op-Iso⁻-pathToIso p)
         ∙ retEq (univEquiv isUnivC _ _) p)
diff --git a/Cubical/Categories/Constructions/Slice/Functor.agda b/Cubical/Categories/Constructions/Slice/Functor.agda
index baf166bc00..d87fdc1850 100644
--- a/Cubical/Categories/Constructions/Slice/Functor.agda
+++ b/Cubical/Categories/Constructions/Slice/Functor.agda
@@ -26,7 +26,6 @@ private
   variable
     ℓ ℓ' : Level
     C D : Category ℓ ℓ'
-    c d : C .ob
 
 infix 39 _F/_
 infix 40 ∑_
@@ -79,7 +78,7 @@ module _ (Pbs : Pullbacks C) where
  open _⊣₂_
 
 
- module _ (𝑓 : C [ c , d ]) where
+ module _ {c d}(𝑓 : C [ c , d ]) where
 
   open BaseChange 𝑓 hiding (_＊)
 
diff --git a/Cubical/Categories/Constructions/TwistedArrow.agda b/Cubical/Categories/Constructions/TwistedArrow.agda
index 53d0aaa3fb..af70ce1a41 100644
--- a/Cubical/Categories/Constructions/TwistedArrow.agda
+++ b/Cubical/Categories/Constructions/TwistedArrow.agda
@@ -22,7 +22,7 @@ TwistedEnds : (C : Category ℓ ℓ') → Functor (TwistedArrowCategory C) (C ^o
 TwistedEnds C = ForgetElements (HomFunctor C)
 
 TwistedDom : (C : Category ℓ ℓ') → Functor ((TwistedArrowCategory C) ^op) C
-TwistedDom C = ((Fst (C ^op) C) ^opF) ∘F (ForgetElements (HomFunctor C) ^opF)
+TwistedDom C = recOp (Fst _ _ ∘F ForgetElements (HomFunctor C))
 
 TwistedCod : (C : Category ℓ ℓ') → Functor (TwistedArrowCategory C) C
 TwistedCod C = (Snd (C ^op) C) ∘F ForgetElements (HomFunctor C)
diff --git a/Cubical/Categories/Displayed/Constructions/Weaken/Base.agda b/Cubical/Categories/Displayed/Constructions/Weaken/Base.agda
index 2b2f801097..342f8a3bbc 100644
--- a/Cubical/Categories/Displayed/Constructions/Weaken/Base.agda
+++ b/Cubical/Categories/Displayed/Constructions/Weaken/Base.agda
@@ -10,6 +10,7 @@ open import Cubical.Data.Sigma
 
 open import Cubical.Categories.Category.Base
 open import Cubical.Categories.Functor
+open import Cubical.Categories.Constructions.BinProduct
 
 open import Cubical.Categories.Displayed.Base
 open import Cubical.Categories.Displayed.Section.Base
@@ -42,6 +43,9 @@ module _ (C : Category ℓC ℓC') (D : Category ℓD ℓD') where
   weakenΠ .F-id = refl
   weakenΠ .F-seq _ _ = refl
 
+  ∫weaken→×C : Functor (∫C weaken) (C ×C D)
+  ∫weaken→×C = TC.Fst ,F weakenΠ
+
 module _ {C : Category ℓC ℓC'}
          {D : Category ℓD ℓD'}
          {E : Category ℓE ℓE'}
@@ -95,3 +99,4 @@ module _ {B : Category ℓB ℓB'} {C : Category ℓC ℓC'} where
   weakenF G .F-homᴰ = G .F-hom
   weakenF G .F-idᴰ = G .F-id
   weakenF G .F-seqᴰ = G .F-seq
+
diff --git a/Cubical/Categories/Displayed/Functor.agda b/Cubical/Categories/Displayed/Functor.agda
index 2531aa39ea..763ef96c4c 100644
--- a/Cubical/Categories/Displayed/Functor.agda
+++ b/Cubical/Categories/Displayed/Functor.agda
@@ -143,13 +143,36 @@ module _ {C : Category ℓC ℓC'} {D : Category ℓD ℓD'} {F : Functor C D}
 
 -- Displayed opposite functor
 module _ {C : Category ℓC ℓC'} {D : Category ℓD ℓD'}
-  {F : Functor C D} {Cᴰ : Categoryᴰ C ℓCᴰ ℓCᴰ'} {Dᴰ : Categoryᴰ D ℓDᴰ ℓDᴰ'}
-  (Fᴰ : Functorᴰ F Cᴰ Dᴰ)
+  {Cᴰ : Categoryᴰ C ℓCᴰ ℓCᴰ'} {Dᴰ : Categoryᴰ D ℓDᴰ ℓDᴰ'}
   where
   open Functorᴰ
-  _^opFᴰ : Functorᴰ (F ^opF) (Cᴰ ^opᴰ) (Dᴰ ^opᴰ)
-  _^opFᴰ .F-obᴰ = Fᴰ .F-obᴰ
-  _^opFᴰ .F-homᴰ = Fᴰ .F-homᴰ
-  _^opFᴰ .F-idᴰ = Fᴰ .F-idᴰ
-  _^opFᴰ .F-seqᴰ fᴰ gᴰ = Fᴰ .F-seqᴰ gᴰ fᴰ
 
+  -- TODO: move to Displayed.Constructions.Opposite
+  introOpᴰ : ∀ {F} → Functorᴰ F (Cᴰ ^opᴰ) Dᴰ → Functorᴰ (introOp F) Cᴰ (Dᴰ ^opᴰ)
+  introOpᴰ Fᴰ .F-obᴰ = Fᴰ .F-obᴰ
+  introOpᴰ Fᴰ .F-homᴰ = Fᴰ .F-homᴰ
+  introOpᴰ Fᴰ .F-idᴰ = Fᴰ .F-idᴰ
+  introOpᴰ Fᴰ .F-seqᴰ fᴰ gᴰ = Fᴰ .F-seqᴰ gᴰ fᴰ
+
+  recOpᴰ : ∀ {F} → Functorᴰ F Cᴰ (Dᴰ ^opᴰ) → Functorᴰ (recOp F) (Cᴰ ^opᴰ) Dᴰ
+  recOpᴰ Fᴰ .F-obᴰ = Fᴰ .F-obᴰ
+  recOpᴰ Fᴰ .F-homᴰ = Fᴰ .F-homᴰ
+  recOpᴰ Fᴰ .F-idᴰ = Fᴰ .F-idᴰ
+  recOpᴰ Fᴰ .F-seqᴰ fᴰ gᴰ = Fᴰ .F-seqᴰ gᴰ fᴰ
+module _ {C : Category ℓC ℓC'} {Cᴰ : Categoryᴰ C ℓCᴰ ℓCᴰ'} where
+  toOpOpᴰ : Functorᴰ toOpOp Cᴰ ((Cᴰ ^opᴰ) ^opᴰ)
+  toOpOpᴰ = introOpᴰ 𝟙ᴰ⟨ _ ⟩
+
+  fromOpOpᴰ : Functorᴰ fromOpOp ((Cᴰ ^opᴰ) ^opᴰ) Cᴰ
+  fromOpOpᴰ = recOpᴰ 𝟙ᴰ⟨ _ ⟩
+module _ {C : Category ℓC ℓC'} {D : Category ℓD ℓD'}
+  {Cᴰ : Categoryᴰ C ℓCᴰ ℓCᴰ'} {Dᴰ : Categoryᴰ D ℓDᴰ ℓDᴰ'}
+  where
+
+  _^opFᴰ : ∀ {F} → Functorᴰ F Cᴰ Dᴰ
+                 → Functorᴰ (F ^opF) (Cᴰ ^opᴰ) (Dᴰ ^opᴰ)
+  Fᴰ ^opFᴰ = recOpᴰ (toOpOpᴰ ∘Fᴰ Fᴰ)
+
+  _^opF⁻ᴰ : ∀ {F} → Functorᴰ F (Cᴰ ^opᴰ) (Dᴰ ^opᴰ)
+                 → Functorᴰ (F ^opF⁻) Cᴰ Dᴰ
+  Fᴰ ^opF⁻ᴰ = fromOpOpᴰ ∘Fᴰ introOpᴰ Fᴰ
diff --git a/Cubical/Categories/Displayed/Section/Base.agda b/Cubical/Categories/Displayed/Section/Base.agda
index 3ce2460398..03fbfb8775 100644
--- a/Cubical/Categories/Displayed/Section/Base.agda
+++ b/Cubical/Categories/Displayed/Section/Base.agda
@@ -316,3 +316,38 @@ module _ {C : Category ℓC ℓC'}
   compFunctorᴰGlobalSection : Functorᴰ F Cᴰ Dᴰ → GlobalSection Cᴰ → Section F Dᴰ
   compFunctorᴰGlobalSection Fᴰ Gᴰ = reindS' (Eq.refl , Eq.refl)
     (compFunctorᴰSection Fᴰ Gᴰ)
+
+module _ {C : Category ℓC ℓC'}
+         {D : Category ℓD ℓD'}
+         {Dᴰ : Categoryᴰ D ℓDᴰ ℓDᴰ'}
+          where
+
+  open Section
+  introOpS : ∀ {F : Functor (C ^op) _}
+    → Section F Dᴰ
+    → Section (introOp F) (Dᴰ ^opᴰ)
+  introOpS S .F-obᴰ = S .F-obᴰ
+  introOpS S .F-homᴰ = S .F-homᴰ
+  introOpS S .F-idᴰ = S .F-idᴰ
+  introOpS S .F-seqᴰ f g = S .F-seqᴰ g f
+
+  recOpS : ∀ {F : Functor C _}
+    → Section F (Dᴰ ^opᴰ)
+    → Section (recOp F) Dᴰ
+  recOpS S .F-obᴰ = S .F-obᴰ
+  recOpS S .F-homᴰ = S .F-homᴰ
+  recOpS S .F-idᴰ = S .F-idᴰ
+  recOpS S .F-seqᴰ f g = S .F-seqᴰ g f
+
+module _ {C : Category ℓC ℓC'}
+         {D : Category ℓD ℓD'}
+         {Dᴰ : Categoryᴰ D ℓDᴰ ℓDᴰ'}
+          where
+
+  _^opS : ∀ {F : Functor C _} → Section F Dᴰ → Section (F ^opF) (Dᴰ ^opᴰ)
+  S ^opS = recOpS (compFunctorᴰSection toOpOpᴰ S)
+
+  _^opS⁻ : ∀ {F : Functor (C ^op) _}
+    → Section F (Dᴰ ^opᴰ)
+    → Section (F ^opF⁻) Dᴰ
+  S ^opS⁻ = compFunctorᴰSection fromOpOpᴰ (introOpS S)
diff --git a/Cubical/Categories/Functor/Base.agda b/Cubical/Categories/Functor/Base.agda
index 0e95d761f2..4c658b965c 100644
--- a/Cubical/Categories/Functor/Base.agda
+++ b/Cubical/Categories/Functor/Base.agda
@@ -142,25 +142,37 @@ funcCompOb≡ : ∀ (G : Functor D E) (F : Functor C D) (c : ob C)
             → funcComp G F .F-ob c ≡ G .F-ob (F .F-ob c)
 funcCompOb≡ G F c = refl
 
+-- TODO: move all of this to Constructions.Opposite?
+introOp : Functor (C ^op) D → Functor C (D ^op)
+introOp F .F-ob = F .F-ob
+introOp F .F-hom = F .F-hom
+introOp F .F-id = F .F-id
+introOp F .F-seq f g = F .F-seq g f
+
+recOp : Functor C (D ^op) → Functor (C ^op) D
+recOp F .F-ob = F .F-ob
+recOp F .F-hom = F .F-hom
+recOp F .F-id = F .F-id
+recOp F .F-seq f g = F .F-seq g f
+
+toOpOp : Functor C ((C ^op) ^op)
+toOpOp = introOp Id
+
+fromOpOp : Functor ((C ^op) ^op) C
+fromOpOp = recOp Id
 
 _^opF  : Functor C D → Functor (C ^op) (D ^op)
-(F ^opF) .F-ob      = F .F-ob
-(F ^opF) .F-hom     = F .F-hom
-(F ^opF) .F-id      = F .F-id
-(F ^opF) .F-seq f g = F .F-seq g f
+F ^opF = recOp (toOpOp ∘F F)
+
+_^opF⁻ : Functor (C ^op) (D ^op) → Functor C D
+F ^opF⁻ = fromOpOp ∘F introOp F
 
 open Iso
 Iso^opF : Iso (Functor C D) (Functor (C ^op) (D ^op))
-fun Iso^opF = _^opF
-inv Iso^opF = _^opF
-F-ob (rightInv Iso^opF b i) = F-ob b
-F-hom (rightInv Iso^opF b i) = F-hom b
-F-id (rightInv Iso^opF b i) = F-id b
-F-seq (rightInv Iso^opF b i) = F-seq b
-F-ob (leftInv Iso^opF a i) = F-ob a
-F-hom (leftInv Iso^opF a i) = F-hom a
-F-id (leftInv Iso^opF a i) = F-id a
-F-seq (leftInv Iso^opF a i) = F-seq a
+Iso^opF .fun = _^opF
+Iso^opF .inv = _^opF⁻
+Iso^opF .rightInv F = Functor≡ (λ _ → refl) (λ _ → refl)
+Iso^opF .leftInv F = Functor≡ (λ _ → refl) (λ _ → refl)
 
 ^opFEquiv : Functor C D ≃ Functor (C ^op) (D ^op)
 ^opFEquiv = isoToEquiv Iso^opF
diff --git a/Cubical/Categories/Functor/ComposeProperty.agda b/Cubical/Categories/Functor/ComposeProperty.agda
index 3533acf387..8e0be0eeec 100644
--- a/Cubical/Categories/Functor/ComposeProperty.agda
+++ b/Cubical/Categories/Functor/ComposeProperty.agda
@@ -1,5 +1,3 @@
-{-# OPTIONS --lossy-unification #-}
-
 module Cubical.Categories.Functor.ComposeProperty where
 
 open import Cubical.Foundations.Prelude
@@ -98,6 +96,7 @@ module _ {ℓC ℓC' ℓD ℓD' ℓE ℓE'}
       → F .F-hom (f ⋆⟨ D ⟩ g ⋆⟨ D ⟩ h) ≡ F .F-hom f ⋆⟨ E ⟩ F .F-hom g ⋆⟨ E ⟩ F .F-hom h
     F-seq3 F = F .F-seq _ _ ∙ cong (λ x → x ⋆⟨ E ⟩ _) (F .F-seq _ _)
 
+    module E = Category E
     ext : NatTrans A B
     ext .N-ob d = isContrMor d .fst .fst
     ext .N-hom {x = d} {y = d'} f = Prop.rec2 (E .isSetHom _ _)
@@ -106,11 +105,10 @@ module _ {ℓC ℓC' ℓD ℓD' ℓE ℓE'}
             (λ i → A .F-hom f ⋆⟨ E ⟩ mor-eq d' c' h' i)
           ∙ cong (λ x → A .F-hom f ⋆⟨ E ⟩ x) (E .⋆Assoc _ _ _)
           ∙ sym (E .⋆Assoc _ _ _) ∙ sym (E .⋆Assoc _ _ _)
-          ∙ cong (λ x → x ⋆⟨ E ⟩ _ ⋆⟨ E ⟩ _) (sym (E .⋆IdL _))
-          ∙ cong (λ x → x ⋆⟨ E ⟩ _ ⋆⟨ E ⟩ _ ⋆⟨ E ⟩ _) (sym (F-Iso {F = A} h .snd .sec))
+          ∙ E.⟨ E.⟨ sym (E.⋆IdL _) ∙ E.⟨ sym (F-Iso {F = A} h .snd .sec) ⟩⋆⟨ refl ⟩ ⟩⋆⟨ refl ⟩ ⟩⋆⟨ refl ⟩
           ∙ cong (λ x → x ⋆⟨ E ⟩ _ ⋆⟨ E ⟩ _) (E .⋆Assoc _ _ _)
           ∙ cong (λ x → _ ⋆⟨ E ⟩ x ⋆⟨ E ⟩ _ ⋆⟨ E ⟩ _) (sym (E .⋆Assoc _ _ _))
-          ∙ cong (λ x → _ ⋆⟨ E ⟩ x ⋆⟨ E ⟩ _ ⋆⟨ E ⟩ _) (sym (F-seq3 A))
+          ∙ E.⟨ E.⟨ E.⟨ refl ⟩⋆⟨ E.⟨ sym (A .F-seq _ _) ⟩⋆⟨ refl ⟩ ∙ sym (A .F-seq _ _) ⟩ ⟩⋆⟨ refl ⟩ ⟩⋆⟨ refl ⟩
           ∙ cong (λ x → A .F-hom (invIso h .fst) ⋆⟨ E ⟩ x ⋆⟨ E ⟩ _ ⋆⟨ E ⟩ _) (sym (cong (A .F-hom) p))
           ∙ cong (λ x → x ⋆⟨ E ⟩ _) (E .⋆Assoc _ _ _)
           ∙ cong (λ x → _ ⋆⟨ E ⟩ x ⋆⟨ E ⟩ _) (α .N-hom k)
@@ -140,7 +138,6 @@ module _ {ℓC ℓC' ℓD ℓD' ℓE ℓE'}
     isFull+Faithful→isFullyFaithful {F = precomposeF E F}
       (isEssSurj+Full→isFullPrecomp surj full) (isEssSurj→isFaithfulPrecomp surj)
 
-
 module _ {ℓC ℓC' ℓD ℓD' ℓE ℓE'}
   {C : Category ℓC ℓC'} {D : Category ℓD ℓD'}
   {E : Category ℓE ℓE'} (isUnivE : isUnivalent E)
diff --git a/Cubical/Categories/Instances/CommAlgebras.agda b/Cubical/Categories/Instances/CommAlgebras.agda
index 23453db42d..1156e6c686 100644
--- a/Cubical/Categories/Instances/CommAlgebras.agda
+++ b/Cubical/Categories/Instances/CommAlgebras.agda
@@ -674,10 +674,9 @@ module PreSheafFromUniversalProp (C : Category ℓ ℓ') (P : ob C → Type ℓ)
     assocDiagPath : Forgetful ∘F (universalPShf ∘F D) ≡ 𝓖 ∘F D
     assocDiagPath = F-assoc
 
-    conePathPCR : PathP (λ i → Cone (assocDiagPath i) (F-ob 𝓖 c))
+    conePathPCR : PathP (λ i → Cone {C = CommRingsCategory} (assocDiagPath i) (F-ob 𝓖 c))
                    (F-cone Forgetful (F-cone universalPShf cc)) (F-cone 𝓖 cc)
-    conePathPCR = conePathPDiag (λ v _ → 𝓖 .F-hom (cc .coneOut v))
-
+    conePathPCR = conePathPDiag {c = 𝓖 .F-ob c} {p = assocDiagPath} (λ v _ → 𝓖 .F-hom (cc .coneOut v))
 
    toLimCone : isLimCone _ _ (F-cone 𝓖 cc)
    toLimCone = transport (λ i → isLimCone _ _ (conePathPCR i))
diff --git a/Cubical/Categories/Instances/Functors.agda b/Cubical/Categories/Instances/Functors.agda
index 0877a3c7db..8e735ae52f 100644
--- a/Cubical/Categories/Instances/Functors.agda
+++ b/Cubical/Categories/Instances/Functors.agda
@@ -136,4 +136,3 @@ module _ (C : Category ℓC ℓC') (D : Category ℓD ℓD') where
     β .N-ob e ∘⟨ D ⟩ (G .F-hom g ∘⟨ D ⟩ (α .N-ob d ∘⟨ D ⟩ F .F-hom f))
       ≡⟨ D .⋆Assoc _ _ _ ⟩
     (β .N-ob e ∘⟨ D ⟩ G .F-hom g) ∘⟨ D ⟩ (α .N-ob d ∘⟨ D ⟩ F .F-hom f) ∎
-
diff --git a/Cubical/Categories/Isomorphism.agda b/Cubical/Categories/Isomorphism.agda
index d9b384df63..389796b9c7 100644
--- a/Cubical/Categories/Isomorphism.agda
+++ b/Cubical/Categories/Isomorphism.agda
@@ -204,6 +204,11 @@ module _ {C : Category ℓC ℓC'} where
   op-Iso f .snd .sec = f .snd .sec
   op-Iso f .snd .ret = f .snd .ret
 
+  op-Iso⁻ : {x y : C .ob} → CatIso (C ^op) x y → CatIso C x y
+  op-Iso⁻ f .fst = f .snd .inv
+  op-Iso⁻ f .snd .inv = f .fst
+  op-Iso⁻ f .snd .sec = f .snd .sec
+  op-Iso⁻ f .snd .ret = f .snd .ret
 
 module _ {C : Category ℓC ℓC'}{D : Category ℓD ℓD'}{F : Functor C D} where
 
diff --git a/Cubical/Categories/Site/Sheafification/UniversalProperty.agda b/Cubical/Categories/Site/Sheafification/UniversalProperty.agda
index 69c022f3f2..05c1586997 100644
--- a/Cubical/Categories/Site/Sheafification/UniversalProperty.agda
+++ b/Cubical/Categories/Site/Sheafification/UniversalProperty.agda
@@ -173,7 +173,7 @@ module UniversalProperty
     sheafificationIsUniversal :
       isUniversal
         (SheafCategory J ℓP ^op)
-        ((C^ [ P ,-]) ∘F FullInclusion C^ (isSheaf J))
+        ((C^ [ P ,-]) ∘F FullInclusion C^ (isSheaf J) ∘F fromOpOp)
         (sheafification , isSheafSheafification)
         η
     sheafificationIsUniversal (G , isSheafG) = record