port ZFunctors to no-eta-equality

Author: maxsnew

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,29 +61,32 @@ 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*
+  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
 
   -- a ℤ-functor that is a sheaf wrt the Zariski coverage is called local
   isLocal : ℤFunctor → Type (ℓ-suc ℓ)
-  isLocal X = isSheaf zariskiCoverage (X ∘F fromOpOp)
+  isLocal X = isSheaf zariskiCoverage X
 
   -- the forgetful functor
   -- 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)
@@ -191,7 +195,7 @@ module AdjBij {ℓ : Level} where
 
     -- the other direction is just precomposition modulo Yoneda
     _♯ : X ⇒ Sp .F-ob A → CommRingHom A (𝓞 .F-ob X)
-    fst (α ♯) a = α ●ᵛ {!yoneda 𝔸¹ A .inv a!} -- α ●ᵛ yonedaᴾ 𝔸¹ A .inv a
+    fst (α ♯) a = α ●ᵛ yonedaᴾ 𝔸¹ A .inv a
 
     pres0 (snd (α ♯)) = makeNatTransPath (funExt₂ λ B x → α .N-ob B x .snd .pres0)
     pres1 (snd (α ♯)) = makeNatTransPath (funExt₂ λ B x → α .N-ob B x .snd .pres1)
@@ -236,10 +240,10 @@ module AdjBij {ℓ : Level} where
     where
     theIso : Iso (A .fst) ((𝓞 ∘F Sp) .F-ob A .fst)
     fun theIso = ε A .fst
-    inv theIso = {!!} -- yonedaᴾ 𝔸¹ A .fun
-    rightInv theIso α = {!!} -- ℤFUNCTOR .⋆IdL _ ∙ yonedaᴾ 𝔸¹ A .leftInv α
-    leftInv theIso a = {!!} -- path -- I get yellow otherwise
-      -- where
-      -- path : yonedaᴾ 𝔸¹ A .fun ((idTrans (Sp .F-ob A)) ●ᵛ yonedaᴾ 𝔸¹ A .inv a) ≡ a
-      -- path = cong (yonedaᴾ 𝔸¹ A .fun) (ℤFUNCTOR .⋆IdL _) ∙ yonedaᴾ 𝔸¹ A .rightInv a
+    inv theIso = yonedaᴾ 𝔸¹ A .fun
+    rightInv theIso α = ℤFUNCTOR .⋆IdL _ ∙ yonedaᴾ 𝔸¹ A .leftInv α
+    leftInv theIso a = path
+      where
+      path : yonedaᴾ 𝔸¹ A .fun ((idTrans (Sp .F-ob A)) ●ᵛ yonedaᴾ 𝔸¹ A .inv a) ≡ a
+      path = cong (yonedaᴾ 𝔸¹ A .fun) (ℤFUNCTOR .⋆IdL _) ∙ yonedaᴾ 𝔸¹ A .rightInv a
   snd (𝓞⊣SpCounitEquiv A) = ε A .snd