Merge pull request #350 from MiddleAdjunction/RemovingARedundantField…

…InCCC-Canonical Removing a redundant field in CartesianClosed/Canonical
agda · May 27, 2022 · 45798f8 · 45798f8
2 parents 6927a40 + 6e08750
commit 45798f8
Show file tree

Hide file tree

Showing 7 changed files with 3 additions and 13 deletions.
diff --git a/src/Categories/Category/CartesianClosed/Canonical.agda b/src/Categories/Category/CartesianClosed/Canonical.agda
@@ -93,9 +93,11 @@ record CartesianClosed : Set (levelOfTerm 𝒞) where
 
     eval-comp  : eval ∘ (curry f ⁂ id) ≈ f
 
-    curry-resp-≈ : f ≈ g → curry f ≈ curry g
     curry-unique : eval ∘ (f ⁂ id) ≈ g → f ≈ curry g
 
+  curry-resp-≈ : f ≈ g → curry f ≈ curry g
+  curry-resp-≈ f≈g = curry-unique (eval-comp ○ f≈g)
+
   -- The above defines canonical exponentials, making 𝒞 cartesian closed.
   --
   -- NOTE: below we use "⊗" to indicate "non-canonical" products.
@@ -153,7 +155,6 @@ module Equivalence where
     ; eval  = eval′
     ; curry = λg
     ; eval-comp    = β′
-    ; curry-resp-≈ = λ-cong
     ; curry-unique = λ-unique′
     }
     where

diff --git a/src/Categories/Category/Construction/Properties/Presheaves/CartesianClosed.agda b/src/Categories/Category/Construction/Properties/Presheaves/CartesianClosed.agda
@@ -145,9 +145,6 @@ module IsCartesianClosed {o} (C : Category o o o) where
       let module H  = Functor H
           module α  = NaturalTransformation α
       in Π.cong (α.η _) (H.identity eq₁ , eq₂) }
-    ; curry-resp-≈ = λ { {F} {G} eq eq₁ (eq₂ , eq₃) →
-      let module G = Functor G
-      in eq (G.F-resp-≈ eq₂ eq₁ , eq₃) }
     ; curry-unique = λ {F G H} {α β} eq {X} {x y} eq₁ → λ { {Y} {f , z} {g , w} (eq₂ , eq₃) →
       let module F = Functor F
           module G = Functor G

diff --git a/src/Categories/Category/Construction/Properties/Presheaves/FromCartesianCCC.agda b/src/Categories/Category/Construction/Properties/Presheaves/FromCartesianCCC.agda
@@ -222,10 +222,6 @@ module FromCartesianCCC {o} {C : Category o o o} (Car : Cartesian C) where
           ≈⟨ Π.cong (α.η X) (H.identity HX.refl , G.identity GX.refl) ⟩
         α.η X ⟨$⟩ (z , w)
           ∎ }
-    ; curry-resp-≈ = λ {F G H} eq eq₁ eq₂ →
-      let module G = Functor G
-          module H = Functor H
-      in eq (Π.cong (G.₁ π₁) eq₁ , Π.cong (H.₁ π₂) eq₂)
     ; curry-unique = λ {F G H} {α β} eq {X} {x y} eq₁ {Y} {z w} eq₂ →
       let module F   = Functor F
           module G   = Functor G

diff --git a/src/Categories/Category/Instance/Properties/Cats.agda b/src/Categories/Category/Instance/Properties/Cats.agda
@@ -148,7 +148,6 @@ module CanonicallyCartesianClosed {l} where
     ; eval         = eval
     ; curry        = curry.F₀
     ; eval-comp    = λ {_} {_} {_} {G} → eval-comp {G = G}
-    ; curry-resp-≈ = λ {_} {_} {_} {G} {H} → curry.resp-NI {F = G} {H}
     ; curry-unique = λ {_} {_} {_} {G} {H} → curry-unique {G = G} {H}
     }
 

diff --git a/src/Categories/Category/Instance/Properties/Posets.agda b/src/Categories/Category/Instance/Properties/Posets.agda
@@ -257,7 +257,6 @@ Posets-CanonicallyCCC = record
   ; eval         = eval
   ; curry        = curry
   ; eval-comp    = λ {_ _ _ f}   → eval-comp {f = f}
-  ; curry-resp-≈ = λ {_ _ _ f g} → curry-resp-≗ {f = f} {g}
   ; curry-unique = λ {_ _ _ f g} → curry-unique {f = f} {g}
   }
 

diff --git a/src/Categories/Category/Instance/Properties/Setoids/CCC.agda b/src/Categories/Category/Instance/Properties/Setoids/CCC.agda
@@ -47,7 +47,6 @@ module _ ℓ where
       ; cong  = λ eq₁ eq₂ → cong f (eq₁ , eq₂)
       }
     ; eval-comp    = λ {_ _ _ f} → cong f
-    ; curry-resp-≈ = λ eq₁ eq₂ eq → eq₁ (eq₂ , eq)
     ; curry-unique = λ eq₁ eq₂ eq → eq₁ (eq₂ , eq)
     }
     where

diff --git a/src/Categories/Category/Instance/Properties/Setoids/LCCC.agda b/src/Categories/Category/Instance/Properties/Setoids/LCCC.agda
@@ -363,7 +363,6 @@ module _ {o} where
           in Π.cong α.h λ { center → trans (arr₁ span-arrˡ) (eq center)
                           ; left   → eq left
                           ; right  → eq right } }
-        ; curry-resp-≈ = λ {_ _ _} {α β} → curry-resp-≈ {_} {_} {_} {α} {β}
         ; curry-unique = λ {_ _ _} {α β} → curry-unique {_} {_} {_} {α} {β}
         }