Category.idr

The category of functors and natural transformations

Because vertical composition has the shape f =>> g -> g =>> h -> f =>> h, we can use it to define the category of functors as objects and natural transformations as morphisms using vertical composition to stitch natural transformations together. The objects of this category are functors, it is parameterised by two categories c and d that will remain fixed such that every object is an instance of a functor from c to d. The identity morphism is given by the identity natural transformation. It remains to prove this statement, which we do programmatically. First, we pin down the parameters that are not going to change, that is, the categories $\mathcal{C}$ and $\mathcal{D}$, and the functors $f,g:\mathcal{C}\to \mathcal{D}$

parameters
  {0 o1, o2 : Type}
  {0 c : Category o1} {0 d : Category o2}
  {f, g : c ->> d}

To help with type inference, we define an alias for function composition that is specialied to the category $\mathcal{D}$.

  0
  (|>>) : {x, y, z : o2} -> x ~> y -> y ~> z -> x ~> z
  (|>>) = (|:>) d
  private infixr 2 |>>

Then we prove the three lemmas that need to hold for this to form a category

Lemma

The identity natural transformation is neutral on the right side of vertical composition.

  public export
  ntIdentityRight :
    (n : f =>> g) -> NTEq (n ⨾⨾⨾ identity {f = g}) n
  ntIdentityRight nt = MkNTEq $ \vx => Calc $
      |~ nt.component vx |>> g.mapHom vx vx (c.id vx)
      ~~ nt.component vx |>> d.id (g.mapObj vx)
         ...(cong (nt.component vx |>>) (g.presId vx))
      ~~ nt.component vx
         ...((d.idRight _ _ _))

Lemma

The identity natural transformation is neutral on the left side of vertical composition.

  public export
  0 ntIdentityLeft :
    (n : f =>> g) -> NTEq (NaturalTransformation.identity ⨾⨾⨾ n) n
  ntIdentityLeft nt = MkNTEq $ \v =>
      Calc $ |~ f.mapHom v v (c.id v) |>> nt.component v
             ~~ d.id (f.mapObj v)     |>> nt.component v
                ...(cong (|>> nt.component v) (f.presId v))
             ~~ nt.component v
                ...(d.idLeft _ _ (nt.component v))

Lemma

Vertical composition of natural transformations is associative.

  public export
  0 ntAssoc :
      {h, i : c ->> d} ->
      (n1 : f =>> g) -> (n2 : g =>> h) -> (n3 : h =>> i) ->
      NTEq (n1 ⨾⨾⨾ (n2 ⨾⨾⨾ n3)) ((n1 ⨾⨾⨾ n2) ⨾⨾⨾ n3)
  ntAssoc (MkNT n1 p1) (MkNT n2 p2) (MkNT n3 p3) = MkNTEq $ \v =>
      (d.compAssoc _ _ _ _ (n1 v) (n2 v) (n3 v))

Using those lemma we can build the functor category parameterised over two categories $\mathcal{C}$ and $\mathcal{D}$. The objects are functors $\mathcal{C}\to \mathcal{D}$ and morphisms are natural transformation.

Proposition

Given categories $\mathcal{C}$ and $\mathcal{D}$, we define the category of functors as objets and natural transformations as morphisms, composed via vertical composition.

FunctorCat : (c1 : Category a) -> (c2 : Category b) -> Category (c1 ->> c2)
FunctorCat c1 c2 = MkCategory
    (=>>)
    (\f => identity {f})
    (⨾⨾⨾)
    (\f, g, n => ntEqToEq $ ntIdentityRight n)
    (\f, g, n => ntEqToEq $ ntIdentityLeft n)
    (\f, g, h, i, nt1, nt2, nt3 =>
        ntEqToEq $ ntAssoc nt1 nt2 nt3
    )