module Cat.Instances.Functor where

private variable
  o h o₁ h₁ oβ‚‚ hβ‚‚ : Level
  B C D E : Precategory o h
  F G : Functor C D

Functor (pre)categoriesπŸ”—

open import Cat.Functor.Base public

Functor categoriesπŸ”—

When the codomain category DD is univalent, then so is the category of functors [C,D][C,D]. Essentially, this can be read as saying that β€œnaturally isomorphic functors are identified”. We begin by proving that the components of a natural isomorphism (a natural transformation with natural inverse) are themselves isomorphisms in DD.

open import Cat.Functor.Univalence public

CurryingπŸ”—

There is an equivalence between the spaces of bifunctors CΓ—Dβ†’E\mathcal{C} \times \mathcal{D} \to E and the space of functors Cβ†’[D,E]\mathcal{C} \to [\mathcal{D},E]. We refer to the image of a functor under this equivalence as its exponential transpose, and we refer to the map in the β€œforwards” direction (as in the text above) as currying:

Curry : Functor (C Γ—αΆœ D) E β†’ Functor C Cat[ D , E ]
Curry {C = C} {D = D} {E = E} F = curried where
  open import Cat.Functor.Bifunctor {C = C} {D = D} {E = E} F

  curried : Functor C Cat[ D , E ]
  curried .Fβ‚€ = Right
  curried .F₁ xβ†’y = NT (Ξ» f β†’ first xβ†’y) Ξ» x y f β†’
       sym (F-∘ F _ _)
    Β·Β· ap (F₁ F) (Ξ£-pathp (C .idr _ βˆ™ sym (C .idl _)) (D .idl _ βˆ™ sym (D .idr _)))
    ·· F-∘ F _ _
  curried .F-id = Nat-path Ξ» x β†’ F-id F
  curried .F-∘ f g = Nat-path Ξ» x β†’
    ap (Ξ» x β†’ F₁ F (_ , x)) (sym (D .idl _)) βˆ™ F-∘ F _ _

Uncurry : Functor C Cat[ D , E ] β†’ Functor (C Γ—αΆœ D) E
Uncurry {C = C} {D = D} {E = E} F = uncurried where
  import Cat.Reasoning C as C
  import Cat.Reasoning D as D
  import Cat.Reasoning E as E
  module F = Functor F

  uncurried : Functor (C Γ—αΆœ D) E
  uncurried .Fβ‚€ (c , d) = Fβ‚€ (F.β‚€ c) d
  uncurried .F₁ (f , g) = F.₁ f .Ξ· _ E.∘ F₁ (F.β‚€ _) g

  uncurried .F-id {x = x , y} = path where abstract
    path : E ._∘_ (F.₁ (C .id) .Ξ· y) (F₁ (F.β‚€ x) (D .id)) ≑ E .id
    path =
      F.₁ C.id .Ξ· y E.∘ F₁ (F.β‚€ x) D.id β‰‘βŸ¨ E.elimr (F-id (F.β‚€ x)) βŸ©β‰‘
      F.₁ C.id .Ξ· y                     β‰‘βŸ¨ (Ξ» i β†’ F.F-id i .Ξ· y) βŸ©β‰‘
      E.id                              ∎

  uncurried .F-∘ (f , g) (f' , g') = path where abstract
    path : uncurried .F₁ (f C.∘ f' , g D.∘ g')
         ≑ uncurried .F₁ (f , g) E.∘ uncurried .F₁ (f' , g')
    path =
      F.₁ (f C.∘ f') .Ξ· _ E.∘ F₁ (F.β‚€ _) (g D.∘ g')                       β‰‘Λ˜βŸ¨ E.pulll (Ξ» i β†’ F.F-∘ f f' (~ i) .Ξ· _) βŸ©β‰‘Λ˜
      F.₁ f .Ξ· _ E.∘ F.₁ f' .Ξ· _ E.∘ ⌜ F₁ (F.β‚€ _) (g D.∘ g') ⌝            β‰‘βŸ¨ ap! (F-∘ (F.β‚€ _) _ _) βŸ©β‰‘
      F.₁ f .Ξ· _ E.∘ F.₁ f' .Ξ· _ E.∘ F₁ (F.β‚€ _) g E.∘ F₁ (F.β‚€ _) g'       β‰‘βŸ¨ cat! E βŸ©β‰‘
      F.₁ f .Ξ· _ E.∘ ⌜ F.₁ f' .Ξ· _ E.∘ F₁ (F.β‚€ _) g ⌝ E.∘ F₁ (F.β‚€ _) g'   β‰‘βŸ¨ ap! (F.₁ f' .is-natural _ _ _) βŸ©β‰‘
      F.₁ f .Ξ· _ E.∘ (F₁ (F.β‚€ _) g E.∘ F.₁ f' .Ξ· _) E.∘ F₁ (F.β‚€ _) g'     β‰‘βŸ¨ cat! E βŸ©β‰‘
      ((F.₁ f .Ξ· _ E.∘ F₁ (F.β‚€ _) g) E.∘ (F.₁ f' .Ξ· _ E.∘ F₁ (F.β‚€ _) g')) ∎

Constant diagramsπŸ”—

There is a functor from C\mathcal{C} to [J,C][\mathcal{J}, \mathcal{C}] that takes an object x:Cx : \mathcal{C} to the constant functor j↦xj \mapsto x.

  ConstD : Functor C Cat[ J , C ]
  ConstD .Fβ‚€ x = Const x
  ConstD .F₁ f = const-nt f
  ConstD .F-id = Nat-path (Ξ» _ β†’ refl)
  ConstD .F-∘ f g = Nat-path (Ξ» _ β†’ refl)
F∘-assoc
  : βˆ€ {o β„“ o' β„“' o'' β„“'' o₃ ℓ₃}
      {C : Precategory o β„“} {D : Precategory o' β„“'} {E : Precategory o'' β„“''} {F : Precategory o₃ ℓ₃}
      {F : Functor E F} {G : Functor D E} {H : Functor C D}
  β†’ F F∘ (G F∘ H) ≑ (F F∘ G) F∘ H
F∘-assoc = Functor-path (Ξ» x β†’ refl) Ξ» x β†’ refl

F∘-idl
  : βˆ€ {o'' β„“'' o₃ ℓ₃}
      {E : Precategory o'' β„“''} {E' : Precategory o₃ ℓ₃}
      {F : Functor E E'}
  β†’ Id F∘ F ≑ F
F∘-idl = Functor-path (Ξ» x β†’ refl) Ξ» x β†’ refl

F∘-idr
  : βˆ€ {o'' β„“'' o₃ ℓ₃}
      {E : Precategory o'' β„“''} {E' : Precategory o₃ ℓ₃}
      {F : Functor E E'}
  β†’ F F∘ Id ≑ F
F∘-idr = Functor-path (Ξ» x β†’ refl) Ξ» x β†’ refl

module
  _ {o β„“ o' β„“' o'' β„“''}
    {C : Precategory o β„“} {D : Precategory o' β„“'} {E : Precategory o'' β„“''}
  where
    private
      module CD = Cat.Reasoning Cat[ C , D ]
      module DE = Cat.Reasoning Cat[ D , E ]
      module CE = Cat.Reasoning Cat[ C , E ]

    F∘-iso-l : {F F' : Functor D E} {G : Functor C D}
             β†’ F DE.β‰… F' β†’ (F F∘ G) CE.β‰… (F' F∘ G)
    F∘-iso-l {F} {F'} {G} isom =
      CE.make-iso (isom.to β—‚ G) (isom.from β—‚ G)
        (Nat-path Ξ» x β†’ isom.invl Ξ·β‚š _)
        (Nat-path Ξ» x β†’ isom.invr Ξ·β‚š _)
      where
        module isom = DE._β‰…_ isom

    F∘-iso-r : {F : Functor D E} {G G' : Functor C D}
             β†’ G CD.β‰… G' β†’ (F F∘ G) CE.β‰… (F F∘ G')
    F∘-iso-r {F} {G} {G'} isom =
      CE.make-iso (F β–Έ isom.to) (F β–Έ isom.from)
        (Nat-path Ξ» x β†’ F.annihilate (isom.invl Ξ·β‚š _))
        (Nat-path Ξ» x β†’ F.annihilate (isom.invr Ξ·β‚š _))
      where
        module isom = CD._β‰…_ isom
        module F = Cat.Functor.Reasoning F

open import Cat.Functor.Naturality public

module
  _ {o β„“ o' β„“'}
    {C : Precategory o β„“} {D : Precategory o' β„“'}
  where

  private
    module DD = Cat.Reasoning Cat[ D , D ]
    module CD = Cat.Reasoning Cat[ C , D ]
    module D = Cat.Reasoning D
    module C = Cat.Reasoning C

  F∘-iso-id-l
    : {F : Functor D D} {G : Functor C D}
    β†’ F ≅ⁿ Id β†’ (F F∘ G) ≅ⁿ G
  F∘-iso-id-l {F} {G} isom = subst ((F F∘ G) CD.β‰…_) F∘-idl (F∘-iso-l isom)

open _=>_

_ni^op : F ≅ⁿ G β†’ Functor.op F ≅ⁿ Functor.op G
_ni^op Ξ± =
  Cat.Reasoning.make-iso _
    (_=>_.op (Isoⁿ.from α))
    (_=>_.op (Isoⁿ.to α))
    (Nat-path Ξ» j β†’ Isoⁿ.invl Ξ± Ξ·β‚š _)
    (Nat-path Ξ» j β†’ Isoⁿ.invr Ξ± Ξ·β‚š _)

module _ {o β„“ ΞΊ} {C : Precategory o β„“} where
  open Functor
  open _=>_

  natural-iso-to-is-equiv
    : {F G : Functor C (Sets ΞΊ)}
    β†’ (eta : F ≅ⁿ G)
    β†’ βˆ€ x β†’ is-equiv (Isoⁿ.to eta .Ξ· x)
  natural-iso-to-is-equiv eta x =
    is-iso→is-equiv $
      iso (Isoⁿ.from eta .η x)
          (Ξ» x i β†’ Isoⁿ.invl eta i .Ξ· _ x)
          (Ξ» x i β†’ Isoⁿ.invr eta i .Ξ· _ x)

  natural-iso-from-is-equiv
    : {F G : Functor C (Sets ΞΊ)}
    β†’ (eta : F ≅ⁿ G)
    β†’ βˆ€ x β†’ is-equiv (Isoⁿ.from eta .Ξ· x)
  natural-iso-from-is-equiv eta x =
    is-iso→is-equiv $
      iso (Isoⁿ.to eta .η x)
          (Ξ» x i β†’ Isoⁿ.invr eta i .Ξ· _ x)
          (Ξ» x i β†’ Isoⁿ.invl eta i .Ξ· _ x)

  natural-iso→equiv
    : {F G : Functor C (Sets ΞΊ)}
    β†’ (eta : F ≅ⁿ G)
    β†’ βˆ€ x β†’ ∣ F .Fβ‚€ x ∣ ≃ ∣ G .Fβ‚€ x ∣
  natural-iso→equiv eta x =
    Isoⁿ.to eta .η x ,
    natural-iso-to-is-equiv eta x