open import Cat.Instances.Product
open import Cat.Functor.Constant
open import Cat.Functor.Compose
open import Cat.Prelude

import Cat.Functor.Reasoning
import Cat.Reasoning

open Precategory
open Functor
open _=>_

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 is univalent, then so is the category of functors 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 

open import Cat.Functor.Univalence public

Constant diagramsπŸ”—

There is a functor from to that takes an object to the constant functor 

module _ {o β„“ o' β„“'} {C : Precategory o β„“} {J : Precategory o' β„“'} where
  private module C = Precategory C
  private module J = Precategory J

  ConstD : Functor C Cat[ J , C ]
  ConstD .Fβ‚€ x = Const x
  ConstD .F₁ f = constⁿ f
  ConstD .F-id = ext Ξ» _ β†’ refl
  ConstD .F-∘ f g = ext Ξ» _ β†’ 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)
        (ext Ξ» x β†’ isom.invl #β‚š _)
        (ext Ξ» 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)
        (ext Ξ» x β†’ F.annihilate (isom.invl Ξ·β‚š _))
        (ext Ξ» 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 α))
  (reext! (Isoⁿ.invl α)) (reext! (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 Κ» x ≃ G Κ» x
  natural-iso→equiv eta x =
    Isoⁿ.to eta .η x ,
    natural-iso-to-is-equiv eta x