Category no eta equality (#1247)

* init the no-eta-equality for Category experiment

* update Category.Path to no-eta-equality

* no-eta-equality appropriate interface for Opposite categories

* weakequiv fixes

* more fixes

* get started on fixing ZFunctor stuff

* port ZFunctors to no-eta-equality

* fix whitespace

* get CommAlgebras compiling by filling in some inferred args

* more op stuff

* another op

* another one

* remove irrelevant changes

* restore comment

* revert unnecessary change

* revert unnecessary change

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,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)

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 ]

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

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

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)

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 (_＊)
 

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)

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
+

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ᴰ

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)