Explode Cat.Instances.Functor

src/Algebra/Group/Cat/Base.lagda.md

@@ -4,6 +4,7 @@ open import Algebra.Prelude
 open import Algebra.Group
 
 open import Cat.Displayed.Univalence.Thin
+open import Cat.Functor.Properties
 open import Cat.Prelude
 ```
 -->

src/Algebra/Group/Cat/Monadic.lagda.md

@@ -9,8 +9,8 @@ open import Algebra.Group
 open import Cat.Functor.Adjoint.Monadic
 open import Cat.Functor.Adjoint.Monad
 open import Cat.Functor.Equivalence
+open import Cat.Functor.Properties
 open import Cat.Diagram.Monad
-open import Cat.Functor.Base
 
 import Algebra.Group.Cat.Base as Grp
 

src/Algebra/Monoid/Category.lagda.md

@@ -8,8 +8,8 @@ open import Cat.Displayed.Univalence.Thin
 open import Cat.Functor.Adjoint.Monadic
 open import Cat.Functor.Equivalence
 open import Cat.Instances.Delooping
+open import Cat.Functor.Properties
 open import Cat.Functor.Adjoint
-open import Cat.Functor.Base
 open import Cat.Prelude
 
 open import Data.List

src/Cat/Base.lagda.md

@@ -466,6 +466,18 @@ Natural transformations also dualize. The opposite of $\eta : F
 
 <!--
 ```agda
+{-# INLINE NT #-}
+
+is-natural-transformation
+  : ∀ {o ℓ o′ ℓ′} {C : Precategory o ℓ} {D : Precategory o′ ℓ′}
+  → (F G : Functor C D)
+  → (η : ∀ x → D .Precategory.Hom (F .Functor.F₀ x) (G .Functor.F₀ x))
+  → Type _
+is-natural-transformation {C = C} {D = D} F G η =
+  ∀ x y (f : C .Precategory.Hom x y) → η y D.∘ F .F₁ f ≡ G .F₁ f D.∘ η x
+  where module D = Precategory D
+        open Functor
+
 module _ where
   open Precategory
   open Functor

src/Cat/Bi/Base.lagda.md

@@ -1,7 +1,8 @@
 <!--
 ```agda
-open import Cat.Instances.Functor.Compose renaming (_◆_ to _◇_)
-open import Cat.Instances.Functor
+open import Cat.Functor.Compose renaming (_◆_ to _◇_)
+open import Cat.Functor.Naturality
+open import Cat.Functor.Base
 open import Cat.Instances.Product
 open import Cat.Functor.Hom
 open import Cat.Prelude

src/Cat/Bi/Instances/InternalCats.lagda.md

@@ -57,7 +57,7 @@ the identity internal natural isomorphism as-is.
 
 ```agda
   ƛ : ∀ {A B : Internal-cat}
-    → natural-iso Id (Right (Fi∘-functor A B B) Idi)
+    → Id ≅ⁿ Right (Fi∘-functor A B B) Idi
   ƛ {B = B} = to-natural-iso ni where
     open Cat.Internal.Reasoning B
     ni : make-natural-iso _ _
@@ -77,7 +77,7 @@ the identity internal natural isomorphism as-is.
       idri _ ∙ id-commi
 
   ρ : ∀ {A B : Internal-cat}
-    → natural-iso Id (Left (Fi∘-functor A A B) Idi)
+    → Id ≅ⁿ Left (Fi∘-functor A A B) Idi
   ρ {B = B} = to-natural-iso ni where
     open Cat.Internal.Reasoning B
     ni : make-natural-iso _ _
@@ -97,7 +97,7 @@ the identity internal natural isomorphism as-is.
       idri _ ∙ ap (_∘i _) (G .Fi-id)
 
   α : {A B C D : Internal-cat}
-    → natural-iso
+    → _≅ⁿ_
        {C = Internal-functors _ C D ×ᶜ Internal-functors _ B C ×ᶜ Internal-functors _ A B}
        (compose-assocˡ (λ {A} {B} {C} → Fi∘-functor A B C))
        (compose-assocʳ λ {A} {B} {C} → Fi∘-functor A B C)

src/Cat/Diagram/Colimit/Base.lagda.md

@@ -405,7 +405,7 @@ module _ {o₁ h₁ o₂ h₂ : _} {J : Precategory o₁ h₁} {C : Precategory
 <!--
 ```agda
   colimits→inversesp {f = f} {g = g} f-factor g-factor =
-    natural-inverses→inverses
+    inversesⁿ→inverses
       {α = hom→⊤-natural-trans f}
       {β = hom→⊤-natural-trans g}
       (Lan-unique.σ-inversesp Cx Cy
@@ -414,7 +414,7 @@ module _ {o₁ h₁ o₂ h₂ : _} {J : Precategory o₁ h₁} {C : Precategory
       tt
 
   colimits→invertiblep {f = f} f-factor =
-    is-natural-invertible→invertible
+    is-invertibleⁿ→is-invertible
       {α = hom→⊤-natural-trans f}
       (Lan-unique.σ-is-invertiblep
         Cx
@@ -428,8 +428,7 @@ module _ {o₁ h₁ o₂ h₂ : _} {J : Precategory o₁ h₁} {C : Precategory
   colimits→invertible =
     colimits→invertiblep (Cx.factors Cy.ψ Cy.commutes)
 
-  colimits-unique =
-    Nat-iso→Iso (Lan-unique.unique Cx Cy) tt
+  colimits-unique = isoⁿ→iso (Lan-unique.unique Cx Cy) tt
 ```
 -->
 
@@ -477,7 +476,7 @@ module _ {o₁ h₁ o₂ h₂ : _} {J : Precategory o₁ h₁} {C : Precategory
     → is-lan !F D K' eta
   is-invertible→is-colimitp {K' = K'} {eta = eta} eps p q invert =
     generalize-colimitp
-      (is-invertible→is-lan Cy $ componentwise-invertible→invertible _ λ _ → invert)
+      (is-invertible→is-lan Cy $ invertible→invertibleⁿ _ λ _ → invert)
       q
 ```
 
@@ -488,8 +487,8 @@ coapex of $C$ is also a colimit of $Dia'$.
 ```agda
   natural-iso-diagram→is-colimitp
     : ∀ {D′ : Functor J C} {eta : D′ => K F∘ !F}
-    → (isos : natural-iso D D′)
-    → (∀ {j} →  Cy.ψ j C.∘ natural-iso.from isos .η j ≡ eta .η j)
+    → (isos : D ≅ⁿ D′)
+    → (∀ {j} →  Cy.ψ j C.∘ Isoⁿ.from isos .η j ≡ eta .η j)
     → is-lan !F D′ K eta
   natural-iso-diagram→is-colimitp {D′ = D′} isos q = generalize-colimitp
     (natural-iso-of→is-lan Cy isos)
@@ -501,11 +500,9 @@ coapex of $C$ is also a colimit of $Dia'$.
 module _ {o₁ h₁ o₂ h₂ : _} {J : Precategory o₁ h₁} {C : Precategory o₂ h₂}
          {D D′ : Functor J C} where
   natural-iso→colimit
-    : natural-iso D D′
-    → Colimit D
-    → Colimit D′
+    : D ≅ⁿ D′ → Colimit D → Colimit D′
   natural-iso→colimit isos C .Lan.Ext = Lan.Ext C
-  natural-iso→colimit isos C .Lan.eta = Lan.eta C ∘nt natural-iso.from isos
+  natural-iso→colimit isos C .Lan.eta = Lan.eta C ∘nt Isoⁿ.from isos
   natural-iso→colimit isos C .Lan.has-lan = natural-iso-of→is-lan (Lan.has-lan C) isos
 ```
 -->
@@ -618,7 +615,7 @@ module _ {J : Precategory o₁ h₁} {C : Precategory o₂ h₂} {D : Precategor
     open _=>_
 
   natural-iso→preserves-colimits
-    : natural-iso F F'
+    : F ≅ⁿ F'
     → preserves-colimit F Dia
     → preserves-colimit F' Dia
   natural-iso→preserves-colimits α F-preserves {K = K} {eps} colim =
@@ -631,7 +628,7 @@ module _ {J : Precategory o₁ h₁} {C : Precategory o₂ h₂} {D : Precategor
         F' .F₁ (eps .η j) ∎)
       (F-preserves colim)
     where
-      module α = natural-iso α
+      module α = Isoⁿ α
 ```
 -->
 

src/Cat/Diagram/Colimit/Representable.lagda.md

@@ -1,7 +1,7 @@
 <!--
 ```agda
 open import Cat.Functor.Hom.Representable
-open import Cat.Instances.Functor.Compose
+open import Cat.Functor.Compose
 open import Cat.Instances.Shape.Terminal
 open import Cat.Instances.Sets.Complete
 open import Cat.Diagram.Colimit.Base
@@ -63,10 +63,10 @@ conditions.
 
   represents→is-colimit
     : ∀ {c : C.Ob} {eta : Dia => Const c}
-    → is-natural-invertible (Hom-into-inj eta)
+    → is-invertibleⁿ (Hom-into-inj eta)
     → is-colimit Dia c eta
   represents→is-colimit {c} {eta} nat-inv = colim where
-    module nat-inv = is-natural-invertible nat-inv
+    module nat-inv = is-invertibleⁿ nat-inv
 
     colim : is-colimit Dia c eta
     colim .σ {M} α =

src/Cat/Diagram/Limit/Base.lagda.md

@@ -2,8 +2,9 @@
 ```agda
 open import Cat.Instances.Shape.Terminal
 open import Cat.Functor.Kan.Unique
+open import Cat.Functor.Naturality
 open import Cat.Functor.Coherence
-open import Cat.Instances.Functor
+open import Cat.Functor.Base
 open import Cat.Functor.Kan.Base
 open import Cat.Prelude
 
@@ -509,7 +510,7 @@ with the 2 limits, then $f$ and $g$ are inverses.
     → (∀ {j : J.Ob} → Lx.ψ j C.∘ g ≡ Ly.ψ j)
     → C.Inverses f g
   limits→inversesp {f = f} {g = g} f-factor g-factor =
-    natural-inverses→inverses
+    inversesⁿ→inverses
       {α = hom→⊤-natural-trans f}
       {β = hom→⊤-natural-trans g}
       (Ran-unique.σ-inversesp Ly Lx
@@ -527,7 +528,7 @@ must be invertible.
     → (∀ {j : J.Ob} → Ly.ψ j C.∘ f ≡ Lx.ψ j)
     → C.is-invertible f
   limits→invertiblep {f = f} f-factor =
-    is-natural-invertible→invertible
+    is-invertibleⁿ→is-invertible
       {α = hom→⊤-natural-trans f}
       (Ran-unique.σ-is-invertiblep
         Ly
@@ -553,8 +554,7 @@ Finally, we can bundle this data up to show that the apexes are isomorphic.
 
 ```agda
   limits-unique : x C.≅ y
-  limits-unique =
-    Nat-iso→Iso (Ran-unique.unique Lx Ly) tt
+  limits-unique = isoⁿ→iso (Ran-unique.unique Lx Ly) tt
 ```
 
 
@@ -598,7 +598,7 @@ module _ {o₁ h₁ o₂ h₂ : _} {J : Precategory o₁ h₁} {C : Precategory
     → is-ran !F D K' eps
   is-invertible→is-limitp {K' = K'} eta p q invert =
     generalize-limitp
-      (is-invertible→is-ran Ly $ componentwise-invertible→invertible _ (λ _ → invert))
+      (is-invertible→is-ran Ly $ invertible→invertibleⁿ _ (λ _ → invert))
       q
 ```
 
@@ -609,8 +609,8 @@ apex of $L$ is also a limit of $Dia'$.
 ```agda
   natural-iso-diagram→is-limitp
     : ∀ {D′ : Functor J C} {eps : K F∘ !F => D′}
-    → (isos : natural-iso D D′)
-    → (∀ {j} → natural-iso.to isos .η j C.∘ Ly.ψ j ≡ eps .η j)
+    → (isos : D ≅ⁿ D′)
+    → (∀ {j} → Isoⁿ.to isos .η j C.∘ Ly.ψ j ≡ eps .η j)
     → is-ran !F D′ K eps
   natural-iso-diagram→is-limitp {D′ = D′} isos p =
     generalize-limitp
@@ -624,12 +624,9 @@ module _ {o₁ h₁ o₂ h₂ : _} {J : Precategory o₁ h₁} {C : Precategory
          {D D′ : Functor J C}
          where
 
-  natural-iso→limit
-    : natural-iso D D′
-    → Limit D
-    → Limit D′
+  natural-iso→limit : D ≅ⁿ D′ → Limit D → Limit D′
   natural-iso→limit isos L .Ran.Ext = Ran.Ext L
-  natural-iso→limit isos L .Ran.eps = natural-iso.to isos ∘nt Ran.eps L
+  natural-iso→limit isos L .Ran.eps = Isoⁿ.to isos ∘nt Ran.eps L
   natural-iso→limit isos L .Ran.has-ran = natural-iso-of→is-ran (Ran.has-ran L) isos
 ```
 -->
@@ -762,7 +759,7 @@ module _ {J : Precategory o₁ h₁} {C : Precategory o₂ h₂} {D : Precategor
     open _=>_
 
   natural-iso→preserves-limits
-    : natural-iso F F'
+    : F ≅ⁿ F'
     → preserves-limit F Dia
     → preserves-limit F' Dia
   natural-iso→preserves-limits α F-preserves {K = K} {eps} lim =
@@ -775,7 +772,7 @@ module _ {J : Precategory o₁ h₁} {C : Precategory o₂ h₂} {D : Precategor
           F' .F₁ (eps .η j)                                                         ∎)
         (F-preserves lim)
     where
-      module α = natural-iso α
+      module α = Isoⁿ α
 ```
 -->
 

src/Cat/Diagram/Monad.lagda.md

@@ -1,7 +1,7 @@
 <!--
 ```agda
+open import Cat.Functor.Properties
 open import Cat.Functor.Adjoint
-open import Cat.Functor.Base
 open import Cat.Prelude
 
 open Functor

src/Cat/Displayed/Cartesian/Weak.lagda.md

@@ -530,7 +530,7 @@ between $\cE_{u}(-,y')$ and $\cE_{x}(-,u^{*}(y'))$.
 ```agda
   weak-fibration→hom-iso-into
     : ∀ {x y y′} (u : Hom x y)
-    → natural-iso (Hom-over-into ℰ u y′) (Hom-into (Fibre ℰ x) (weak-lift.x′ u y′))
+    → Hom-over-into ℰ u y′ ≅ⁿ Hom-into (Fibre ℰ x) (weak-lift.x′ u y′)
   weak-fibration→hom-iso-into {x} {y} {y′} u = to-natural-iso mi where
     open make-natural-iso
 
@@ -642,15 +642,15 @@ module _ (U : ∀ {x y} → Hom x y → Functor (Fibre ℰ y) (Fibre ℰ x)) whe
 
   hom-iso→weak-fibration
     : (∀ {x y y′} (u : Hom x y)
-       → natural-iso (Hom-over-into ℰ u y′) (Hom-into (Fibre ℰ x) (U u .F₀ y′)))
+       → Hom-over-into ℰ u y′ ≅ⁿ Hom-into (Fibre ℰ x) (U u .F₀ y′))
     → is-weak-cartesian-fibration
   hom-iso→weak-fibration hom-iso =
     vertical-equiv→weak-fibration
       (λ u → U u .F₀)
-      (λ u′ → natural-iso.to (hom-iso _) .η _ u′)
+      (λ u′ → Isoⁿ.to (hom-iso _) .η _ u′)
       (natural-iso-to-is-equiv (hom-iso _) _)
       λ f′ g′ → to-pathp⁻ $
-        happly (natural-iso.to (hom-iso _) .is-natural _ _ g′) f′
+        happly (Isoⁿ.to (hom-iso _) .is-natural _ _ g′) f′
 ```
 -->
 
@@ -669,9 +669,7 @@ module _ (fib : Cartesian-fibration) where
 
   fibration→hom-iso-from
     : ∀ {x y x′} (u : Hom x y)
-    → natural-iso
-      (Hom-over-from ℰ u x′)
-      (Hom-from (Fibre ℰ x) x′ F∘ base-change u)
+    → Hom-over-from ℰ u x′ ≅ⁿ Hom-from (Fibre ℰ x) x′ F∘ base-change u
   fibration→hom-iso-from {x} {y} {x′} u = to-natural-iso mi where
     open make-natural-iso
 
@@ -711,9 +709,7 @@ module _ (fib : Cartesian-fibration) where
 
   fibration→hom-iso-into
     : ∀ {x y y′} (u : Hom x y)
-    → natural-iso
-      (Hom-over-into ℰ u y′)
-      (Hom-into (Fibre ℰ x) (has-lift.x′ u y′))
+    → Hom-over-into ℰ u y′ ≅ⁿ Hom-into (Fibre ℰ x) (has-lift.x′ u y′)
   fibration→hom-iso-into u =
     weak-fibration→hom-iso-into (fibration→weak-fibration fib) u
 ```
@@ -725,13 +721,13 @@ a natural iso between $\cE_{u}(-,-)$ and $\cE_{id}(-,u^{*}(-))$.
 ```agda
   fibration→hom-iso
     : ∀ {x y} (u : Hom x y)
-    → natural-iso (Hom-over ℰ u) (Hom[-,-] (Fibre ℰ x) F∘ (Id F× base-change u))
+    → Hom-over ℰ u ≅ⁿ Hom[-,-] (Fibre ℰ x) F∘ (Id F× base-change u)
   fibration→hom-iso {x = x} u = to-natural-iso mi where
     open make-natural-iso
     open _=>_
 
-    module into-iso {y′} = natural-iso (fibration→hom-iso-into {y′ = y′} u)
-    module from-iso {x′} = natural-iso (fibration→hom-iso-from {x′ = x′} u)
+    module into-iso {y′} = Isoⁿ (fibration→hom-iso-into {y′ = y′} u)
+    module from-iso {x′} = Isoⁿ (fibration→hom-iso-from {x′ = x′} u)
 
     mi : make-natural-iso (Hom-over ℰ u) (Hom[-,-] (Fibre ℰ x) F∘ (Id F× base-change u))
     mi .eta x u′ = has-lift.universalv u _ u′