adjust imports

agda · Jun 15, 2024 · cb8c7b6 · cb8c7b6
1 parent 36af897
commit cb8c7b6
Show file tree

Hide file tree

Showing 11 changed files with 117 additions and 126 deletions.
diff --git a/src/Categories/Category/CartesianClosed/Properties.agda b/src/Categories/Category/CartesianClosed/Properties.agda
@@ -1,43 +1,38 @@
 {-# OPTIONS --without-K --safe #-}
 
+open import Categories.Category.Core using (Category)
+open import Categories.Category.CartesianClosed using (CartesianClosed; module CartesianMonoidalClosed)
+
+module Categories.Category.CartesianClosed.Properties {o ℓ e} {𝒞 : Category o ℓ e} (𝓥 : CartesianClosed 𝒞) where
 
 open import Level
+
 open import Data.Product using (Σ; _,_; Σ-syntax; proj₁; proj₂)
 
+open import Categories.Adjoint.Properties using (lapc)
 open import Categories.Category.BinaryProducts using (BinaryProducts)
 open import Categories.Category.Cartesian using (Cartesian)
-open import Categories.Category.CartesianClosed using (CartesianClosed; module CartesianMonoidalClosed)
 open import Categories.Category.Monoidal.Closed using (Closed)
-open import Categories.Category.Core using (Category)
-open import Categories.Object.Terminal
-open import Categories.Diagram.Colimit
-open import Categories.Adjoint.Properties using (lapc)
-
-import Categories.Morphism.Reasoning as MR
-
+open import Categories.Diagram.Colimit using (Colimit)
+open import Categories.Diagram.Empty 𝒞 using (empty)
 open import Categories.Functor using (Functor; _∘F_)
-
-module Categories.Category.CartesianClosed.Properties {o ℓ e} {𝒞 : Category o ℓ e} (𝓥 : CartesianClosed 𝒞) where
-
-open import Categories.Diagram.Empty 𝒞
+open import Categories.Morphism.Reasoning 𝒞 using (pullˡ)
+open import Categories.Object.Initial 𝒞 using (Initial; IsInitial)
+open import Categories.Object.Initial.Colimit 𝒞 using (⊥⇒colimit; colimit⇒⊥)
+open import Categories.Object.StrictInitial 𝒞 using (IsStrictInitial)
+open import Categories.Object.Terminal using (Terminal)
 
 open Category 𝒞
 open CartesianClosed 𝓥 using (_^_; eval′; cartesian)
 open Cartesian cartesian using (products; terminal)
+open CartesianMonoidalClosed 𝒞 𝓥 using (closedMonoidal)
 open BinaryProducts products
 open Terminal terminal using (⊤)
 open HomReasoning
-open MR 𝒞
 
-open CartesianMonoidalClosed 𝒞 𝓥 using (closedMonoidal)
 private
   module closedMonoidal = Closed closedMonoidal
 
-open import Categories.Object.Initial 𝒞
-open import Categories.Object.StrictInitial 𝒞
-open import Categories.Object.Initial.Colimit 𝒞
-
-
 PointSurjective : ∀ {A X Y : Obj} → (X ⇒ Y ^ A) → Set (ℓ ⊔ e)
 PointSurjective {A = A} {X = X} {Y = Y} ϕ =
   ∀ (f : A ⇒ Y) → Σ[ x ∈ ⊤ ⇒ X ] (∀ (a : ⊤ ⇒ A) → eval′ ∘ first ϕ ∘ ⟨ x , a ⟩  ≈ f ∘ a)

diff --git a/src/Categories/Category/Construction/Functors.agda b/src/Categories/Category/Construction/Functors.agda
@@ -188,6 +188,12 @@ uncurry {C₁ = C₁} {C₂ = C₂} {D = D} = record
           } where module t = NaturalTransformation t
                   open NaturalTransformation
 
+module uncurry {o₁ e₁ ℓ₁} {C₁ : Category o₁ e₁ ℓ₁}
+               {o₂ e₂ ℓ₂} {C₂ : Category o₂ e₂ ℓ₂}
+               {o′ e′ ℓ′} {D  : Category o′ e′ ℓ′}
+               where
+  open Functor (uncurry {C₁ = C₁} {C₂ = C₂} {D = D}) public
+
 module _ {o₁ e₁ ℓ₁} {C₁ : Category o₁ e₁ ℓ₁}
          {o₂ e₂ ℓ₂} {C₂ : Category o₂ e₂ ℓ₂}
          {o′ e′ ℓ′} {D  : Category o′ e′ ℓ′} where

diff --git a/src/Categories/Category/Construction/TwistedArrow.agda b/src/Categories/Category/Construction/TwistedArrow.agda
@@ -1,28 +1,25 @@
 {-# OPTIONS --without-K --safe #-}
-open import Data.Product using (_,_; _×_; map; zip)
-open import Function.Base using (_$_; flip)
-open import Level
-open import Relation.Binary.Core using (Rel)
 
 open import Categories.Category using (Category; module Definitions)
-open import Categories.Category.Product renaming (Product to _×ᶜ_)
-open import Categories.Functor
-
-import Categories.Morphism as M
-import Categories.Morphism.Reasoning as MR
 
 -- Definition of the "Twisted Arrow" Category of a Category 𝒞
 module Categories.Category.Construction.TwistedArrow {o ℓ e} (𝒞 : Category o ℓ e) where
 
-private
-  open module 𝒞 = Category 𝒞
+open import Level
+open import Data.Product using (_,_; _×_; map; zip)
+open import Function.Base using (_$_; flip)
+open import Relation.Binary.Core using (Rel)
 
+open import Categories.Category.Product renaming (Product to _×ᶜ_)
+open import Categories.Functor using (Functor)
+open import Categories.Morphism.Reasoning 𝒞 using (pullˡ; pullʳ )
 
-open M 𝒞
+private
+  open module 𝒞 = Category 𝒞
 open Definitions 𝒞
-open MR 𝒞
 open HomReasoning
 
+
 private
   variable
     A B C : Obj
@@ -78,14 +75,12 @@ TwistedArrow = record
 
 -- Consider TwistedArrow as the comma category * / Hom[C][-,-]
 -- We have the codomain functor TwistedArrow → C.op × C
-
-module _ where
-  open Morphism
-  open Morphism⇒
-  open Functor
-  Forget : Functor TwistedArrow (𝒞.op ×ᶜ 𝒞)
-  Forget .F₀ x = dom x , cod x
-  Forget .F₁ f = dom⇐ f , cod⇒ f
-  Forget .identity = Equiv.refl , Equiv.refl
-  Forget .homomorphism = Equiv.refl , Equiv.refl
-  Forget .F-resp-≈ e = e
+open Functor
+Codomain : Functor TwistedArrow (𝒞.op ×ᶜ 𝒞)
+Codomain .F₀ x = dom , cod
+  where open Morphism x
+Codomain .F₁ f = dom⇐ , cod⇒
+  where open Morphism⇒ f
+Codomain .identity = Equiv.refl , Equiv.refl
+Codomain .homomorphism = Equiv.refl , Equiv.refl
+Codomain .F-resp-≈ e = e
diff --git a/src/Categories/Diagram/Empty.agda b/src/Categories/Diagram/Empty.agda
@@ -1,12 +1,13 @@
 {-# OPTIONS --without-K --safe #-}
 
-open import Categories.Category
-open import Categories.Category.Lift
-open import Categories.Category.Finite.Fin.Construction.Discrete
-open import Categories.Functor.Core
+open import Categories.Category.Core using (Category)
 
 module Categories.Diagram.Empty {o ℓ e} (C : Category o ℓ e) where
 
+open import Categories.Category.Finite.Fin.Construction.Discrete using (Discrete)
+open import Categories.Category.Lift using (liftC)
+open import Categories.Functor.Core using (Functor)
+
 -- maybe (liftC o′ ℓ′ e′ (Discrete 0)) should be Categories.Category.Empty so this does not depend on liftC
 empty : ∀ o′ ℓ′ e′ → Functor (liftC o′ ℓ′ e′ (Discrete 0)) C
 empty _ _ _ = record

diff --git a/src/Categories/Diagram/End/Fubini.agda b/src/Categories/Diagram/End/Fubini.agda
@@ -1,26 +1,26 @@
 {-# OPTIONS --without-K --lossy-unification --safe #-}
 
+module Categories.Diagram.End.Fubini where
+
 open import Level
 open import Data.Product using (Σ; _,_; _×_) renaming (proj₁ to fst; proj₂ to snd)
 open import Function using (_$_)
 
-open import Categories.Category
-open import Categories.Category.Construction.Functors
-open import Categories.Category.Product renaming (Product to _×ᶜ_)
+open import Categories.Category using (Category)
+open import Categories.Category.Construction.Functors using (Functors; curry)
+open import Categories.Category.Product using (πˡ; πʳ; _⁂_; _※_; Swap) renaming (Product to _×ᶜ_)
 open import Categories.Diagram.End using () renaming (End to ∫)
-open import Categories.Diagram.End.Properties
-open import Categories.Diagram.End.Parameterized renaming (EndF to ⨏)
-open import Categories.Diagram.Wedge
-open import Categories.Functor renaming (id to idF)
-open import Categories.Functor.Bifunctor
-open import Categories.Functor.Bifunctor.Properties
+open import Categories.Diagram.End.Properties using (end-η-commute; end-unique)
+open import Categories.Diagram.End.Parameterized using () renaming (EndF to ⨏)
+open import Categories.Diagram.Wedge using (Wedge)
+open import Categories.Functor using (Functor; _∘F_) renaming (id to idF)
+open import Categories.Functor.Bifunctor using (Bifunctor; appˡ)
 open import Categories.NaturalTransformation using (NaturalTransformation)
-open import Categories.NaturalTransformation.Dinatural
+open import Categories.NaturalTransformation.Dinatural using (DinaturalTransformation; dtHelper)
 
 import Categories.Morphism as M
 import Categories.Morphism.Reasoning as MR
 
-module Categories.Diagram.End.Fubini where
 variable
   o ℓ e : Level
   C P D : Category o ℓ e
@@ -82,7 +82,7 @@ module _  (F : Bifunctor (Category.op C ×ᶜ Category.op P) (C ×ᶜ P) D)
           (F₁ ((C.id , P.id) , (C.id , s)) ∘ F₁ ((C.id , P.id) , (f , P.id)) ∘ ω.dinatural.α (p , p) c) ∘ ρ.dinatural.α p
             ≈⟨ (refl⟩∘⟨ refl⟩∘⟨ ⟺ identityʳ) ⟩∘⟨refl ⟩
           (F₁ ((C.id , P.id) , (C.id , s)) ∘ F₁ ((C.id , P.id) , (f , P.id)) ∘ ω.dinatural.α (p , p) c ∘ id) ∘ ρ.dinatural.α p
-            ≈⟨ (refl⟩∘⟨ ω.dinatural.commute (p , p) f ) ⟩∘⟨refl ⟩
+            ≈⟨ (refl⟩∘⟨ ω.dinatural.commute (p , p) f) ⟩∘⟨refl ⟩
           (F₁ ((C.id , P.id) , (C.id , s)) ∘ F₁ ((f , P.id) , (C.id , P.id)) ∘ ω.dinatural.α (p , p) d ∘ id) ∘ ρ.dinatural.α p
             ≈⟨ extendʳ (⟺ F.homomorphism ○ F-resp-≈ ((MR.id-comm C , P.Equiv.refl) , (C.Equiv.refl , MR.id-comm P)) ○ F.homomorphism) ⟩∘⟨refl ⟩
           -- now, we must show dinaturality in P
@@ -93,7 +93,7 @@ module _  (F : Bifunctor (Category.op C ×ᶜ Category.op P) (C ×ᶜ P) D)
           -- this is the hard part: we use commutativity from the bottom face of the cube.
           -- The fact that this exists (an arrow between ∫ F (p,p,- ,-) to ∫ F (p,q,- ,-)) is due to functorality of ∫ and curry₀.
           -- The square commutes by universiality of ω
-            ≈⟨ refl⟩∘⟨ extendʳ (⟺ (end-η-commute ⦃ ω (p , p) ⦄ ⦃ ω (p , q) ⦄ (curry.₀.₁ (F ′) (P.id , s)) d )) ⟩
+            ≈⟨ refl⟩∘⟨ extendʳ (⟺ (end-η-commute ⦃ ω (p , p) ⦄ ⦃ ω (p , q) ⦄ (curry.₀.₁ (F ′) (P.id , s)) d)) ⟩
           -- now we can use dinaturality in ρ, which annoyingly has an `id` tacked on the end
           F₁ ((f , P.id) , (C.id , P.id)) ∘ ω.dinatural.α (p , q) d ∘ ∫F.F₁ (P.id , s) ∘ ρ.dinatural.α p
             ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨  ⟺ identityʳ ⟩
@@ -201,6 +201,6 @@ module _ (F : Bifunctor (Category.op C ×ᶜ Category.op P) (C ×ᶜ P) D)
     eₚ′′  .∫.unique {W} {g} h = eₚ.unique F h
 
   Fubini′ : ∫.E e₁ ≅ ∫.E e₂
-  Fubini′ = ≅.trans (Fubini F {ωᴾ} {eₚ' = eₚ F} ) $
+  Fubini′ = ≅.trans (Fubini F {ωᴾ} {eₚ' = eₚ F}) $
             ≅.trans (end-unique eₚ′′ (eₚ (F ′′)))
                     (≅.sym (Fubini (F ′′) {ωᶜ} {eₚ' = eₚ (F ′′)}))
diff --git a/src/Categories/Diagram/End/Properties.agda b/src/Categories/Diagram/End/Properties.agda
@@ -2,43 +2,40 @@
 
 module Categories.Diagram.End.Properties where
 
+-- The following conventions are taken in this file: C is the 'source' category
+-- and D is the destination. If two source categories are needed, the other is
+-- called 'P' for "parameter", following MacLane. F, G and H are functors and ef,
+-- eg and eh are witnesses of their respective ends.
+
 open import Level
 open import Data.Product using (Σ; _,_)
 open import Function using (_$_)
 
-open import Categories.Category
-open import Categories.Category.Construction.Functors
-open import Categories.Category.Construction.TwistedArrow
+open import Categories.Category using (Category)
+open import Categories.Category.Construction.Functors using (Functors)
+open import Categories.Category.Construction.TwistedArrow using (Codomain)
 open import Categories.Category.Equivalence as SE using (StrongEquivalence)
-open import Categories.Category.Equivalence.Preserves
-open import Categories.Category.Product renaming (Product to _×ᶜ_)
-open import Categories.Diagram.Cone
-open import Categories.Diagram.End renaming (End to ∫)
-open import Categories.Diagram.Limit
-open import Categories.Diagram.Limit.Properties
-open import Categories.Diagram.Wedge
-open import Categories.Diagram.Wedge.Properties
-open import Categories.Functor hiding (id)
-open import Categories.Functor.Bifunctor
-open import Categories.Functor.Bifunctor.Properties
-open import Categories.Functor.Instance.Twisted
-open import Categories.Functor.Limits
-open import Categories.NaturalTransformation renaming (_∘ʳ_ to _▹ⁿ_; id to idN)
+open import Categories.Category.Equivalence.Preserves using (pres-Terminal)
+open import Categories.Category.Product using () renaming (Product to _×ᶜ_)
+open import Categories.Diagram.End using () renaming (End to ∫)
+open import Categories.Diagram.Limit using (Limit)
+open import Categories.Diagram.Limit.Properties using (≃-resp-lim)
+open import Categories.Diagram.Wedge using (Wedge; module Wedge-Morphism)
+open import Categories.Diagram.Wedge.Properties using (ConesTwist≅Wedges)
+open import Categories.Functor using (Functor; _∘F_)
+open import Categories.Functor.Bifunctor using (Bifunctor)
+open import Categories.Functor.Instance.Twisted using (Twist; Twistⁿⁱ)
+open import Categories.Functor.Limits using (Continuous)
+open import Categories.NaturalTransformation using (NaturalTransformation; _∘ᵥ_) renaming (_∘ʳ_ to _▹ⁿ_; id to idN)
 open import Categories.NaturalTransformation.Dinatural hiding (_≃_)
-open import Categories.NaturalTransformation.Equivalence renaming (_≃_ to _≃ⁿ_)
-open import Categories.NaturalTransformation.NaturalIsomorphism renaming (_≃_ to _≃ⁱ_)
-open import Categories.NaturalTransformation.NaturalIsomorphism.Properties
+open import Categories.NaturalTransformation.Equivalence using () renaming (_≃_ to _≃ⁿ_)
+open import Categories.NaturalTransformation.NaturalIsomorphism using (NaturalIsomorphism; sym-associator) renaming (_≃_ to _≃ⁱ_)
 open import Categories.Object.Terminal as Terminal
 
 import Categories.Category.Construction.Wedges as Wedges
 import Categories.Morphism as M
 import Categories.Morphism.Reasoning as MR
 
--- The following conventions are taken in this file: C is the 'source' category
--- and D is the destination. If two source categories are needed, the other is
--- called 'P' for "parameter", following MacLane. F, G and H are functors and ef,
--- eg and eh are witnesses of their respective ends.
-
 private
   variable
     o ℓ e o′ ℓ′ e′ : Level
@@ -236,14 +233,14 @@ module _ {C : Category o ℓ e}
       j-limit : Limit (Twist C D J)
       j-limit = End-yields-limit J ej
       --new-limit
-      f-limit : Limit (F ∘F (J ∘F Forget C))
+      f-limit : Limit (F ∘F (J ∘F Codomain C))
       f-limit .Limit.terminal = record
         { ⊤ = F-map-Coneˡ F (Limit.limit j-limit)
         ; ⊤-is-terminal = cont j-limit
         }
       -- for this we merely need to transport across the associator
       f-limit′ : Limit (Twist C E (F ∘F J))
-      f-limit′ = ≃-resp-lim (sym-associator (Forget C) J F) f-limit
+      f-limit′ = ≃-resp-lim (sym-associator (Codomain C) J F) f-limit
 
     -- really we want IsEnd `F.₀ (∫.E ej)` (F ∘F J)
     contF-as-end : ∫ (F ∘F J)

diff --git a/src/Categories/Functor/Bifunctor.agda b/src/Categories/Functor/Bifunctor.agda
@@ -1,4 +1,8 @@
 {-# OPTIONS --without-K --safe #-}
+
+-- Bifunctor, aka a Functor from C × D to E
+module Categories.Functor.Bifunctor where
+
 open import Level
 open import Data.Product using (_,_)
 
@@ -7,10 +11,6 @@ open import Categories.Functor
 open import Categories.Functor.Construction.Constant
 open import Categories.Category.Product
 
-module Categories.Functor.Bifunctor where
-
--- Bifunctor, aka a Functor from C × D to E
-
 private
   variable
     o ℓ e o′ ℓ′ e′ o″ ℓ″ e″ o‴ ℓ‴ e‴ o⁗ ℓ⁗ e⁗ : Level

diff --git a/src/Categories/Functor/Bifunctor/Properties.agda b/src/Categories/Functor/Bifunctor/Properties.agda
@@ -6,11 +6,8 @@ open import Level
 open import Data.Product using (Σ; _,_)
 
 open import Categories.Category
-open import Categories.Category.Product
 open import Categories.Functor
 open import Categories.Functor.Bifunctor
-open import Categories.Functor.Construction.Constant
-open import Categories.NaturalTransformation using (NaturalTransformation; _∘ˡ_) renaming (id to idN)
 
 import Categories.Morphism.Reasoning as MR
 

diff --git a/src/Categories/Functor/Instance/Twisted.agda b/src/Categories/Functor/Instance/Twisted.agda
@@ -1,39 +1,39 @@
 {-# OPTIONS --without-K --safe #-}
 
+open import Categories.Category using (Category; module Definitions)
+
+-- Definition of the "Twisted" Functor between certain Functor Categories
+module Categories.Functor.Instance.Twisted {o ℓ e o′ ℓ′ e′} (C : Category o ℓ e) (D : Category o′ ℓ′ e′)where
+
 open import Level
 open import Data.Product using (_,_)
 
-open import Categories.Category using (Category; module Definitions)
-
-open import Categories.Category.Construction.TwistedArrow
-open import Categories.Category.Product renaming (Product to _×ᶜ_)
-open import Categories.Category.Construction.Functors
-open import Categories.Functor
-open import Categories.Functor.Bifunctor
+open import Categories.Category.Construction.Functors using (Functors; product)
+open import Categories.Category.Construction.TwistedArrow using (TwistedArrow; Morphism; Morphism⇒; Codomain)
+open import Categories.Category.Product using () renaming (Product to _×ᶜ_)
+open import Categories.Functor using (Functor; _∘F_)
+open import Categories.Functor.Bifunctor using (appʳ)
+open import Categories.Functor.Limits using (Continuous)
 open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper)
 open import Categories.NaturalTransformation.NaturalIsomorphism using (_≃_; _ⓘʳ_)
-open import Categories.Functor.Limits using (Continuous)
-
-
--- Definition of the "Twisted" Functor between certain Functor Categories
-module Categories.Functor.Instance.Twisted {o ℓ e o′ ℓ′ e′} (C : Category o ℓ e) (D : Category o′ ℓ′ e′)where
 
 private
   module C = Category C
   module D = Category D
 
 open Morphism
 open Morphism⇒
+
 -- precomposition with the forgetful functor
 Twist : Functor (C.op ×ᶜ C) D → Functor (TwistedArrow C) D
-Twist F = F ∘F Forget C
+Twist F = F ∘F Codomain C
 
 Twist′ : Functor (C.op ×ᶜ C) D → Functor (Category.op (TwistedArrow C.op)) D
-Twist′ F = F ∘F (Functor.op (Forget C.op))
+Twist′ F = F ∘F (Functor.op (Codomain C.op))
 
 -- precomposition is functorial
 Twisted : Functor (Functors (C.op ×ᶜ C) D) (Functors (TwistedArrow C) D)
-Twisted = appʳ product (Forget C)
+Twisted = appʳ product (Codomain C)
 
 Twistⁿⁱ : ∀ {F G : Functor (C.op ×ᶜ C) D } → (F ≃ G) → Twist F ≃ Twist G
-Twistⁿⁱ α = α ⓘʳ Forget C
+Twistⁿⁱ α = α ⓘʳ Codomain C