another one

Author: maxsnew

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