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