UniAgda.Categories.Natural-Transformation

Table of Contents

1 Prelude

2 Natural transformations

A natural transformation is a map between functors. We define it as a record.

record NaturalTransformation {i j k l : Level} {A : Precategory i j} {B : Precategory k l} (F G : Functor A B) : Type (i  j  l) where
  eta-equality
  module F = Functor F
  module G = Functor G
  field
    α-ob : (x : A .ob)  B .hom (F.₀ x) (G.₀ x)
    α-nat : {x y : A .ob} (f : A [ x , y ])  (α-ob y) o⟨ B  (F.₁ f)  (G.₁ f) o⟨ B  (α-ob x)

As precategories have sets of morphisms, the hom condition is a proposition. We use this later to show that there is a set of natural transformations between two functors.

  α-hom-is-prop : {x y : A .ob}
                   isProp ((f : hom A x y)  comp B (α-ob y) (F.₁ f)  comp B (G.₁ f) (α-ob x))
  α-hom-is-prop = prop-fibres-Pi-is-prop λ f₁  sets-have-prop-ids _ (B .hom-set _ _) _ _

2.1 Sigma definition and equivalence

The Σ definition of a natural transformation is presented here.

Nat-trans-sig : {i j k l : Level} {A : Precategory i j} {B : Precategory k l}
            (F G : Functor A B)
             Type (i  j  l)
Nat-trans-sig {i} {j} {k} {l} {A} {B} F G =
  let module A = Precategory A in
  let module B = Precategory B in
  let module F = Functor F in
  let module G = Functor G in
    Σ[ α-ob  ((x : A.ob)  B.hom (F.₀ x) (G.₀ x)) ] (
    {x y : A.ob} (f : A.hom x y)  B.comp (α-ob y) (F.₁ f)  B.comp (G.₁ f) (α-ob x))

Of course, we have an equivalence between the two definitions.

nat-trans-sig→rec :  {i j k l} {A : Precategory i j} {B : Precategory k l}
                     (F G : Functor A B)
                      Nat-trans-sig F G  NaturalTransformation F G
NaturalTransformation.α-ob (nat-trans-sig→rec F G (α₁ , α₂)) = α₁
NaturalTransformation.α-nat (nat-trans-sig→rec F G (α₁ , α₂)) = α₂

nat-trans-rec→sig :  {i j k l} {A : Precategory i j} {B : Precategory k l}
                       (F G : Functor A B)
                        NaturalTransformation F G  Nat-trans-sig F G
nat-trans-rec→sig F G record { α-ob = α-ob ; α-nat = α-nat } =
  α-ob ,
  α-nat

nat-trans-rec→sig→rec :  {i j k l} {A : Precategory i j} {B : Precategory k l}
                 (F G : Functor A B)
                  (α : NaturalTransformation F G)  (nat-trans-sig→rec F G o nat-trans-rec→sig F G) α  α
nat-trans-rec→sig→rec F G α = refl

nat-trans-sig→rec→sig :  {i j k l} {A : Precategory i j} {B : Precategory k l}
                 (F G : Functor A B)
                  (α : Nat-trans-sig F G)  (nat-trans-rec→sig F G o nat-trans-sig→rec F G) α  α
nat-trans-sig→rec→sig F G (a , b) = path-equiv-sigma
  (refl , refl)

Nat-trans-sig-equiv :  {i j k l} {A : Precategory i j} {B : Precategory k l}
               (F G : Functor A B)
                (Nat-trans-sig F G)  (NaturalTransformation F G)
Nat-trans-sig-equiv F G = equiv-adjointify
  (nat-trans-sig→rec F G ,
  (nat-trans-rec→sig F G) ,
  (nat-trans-rec→sig→rec F G) ,
  (nat-trans-sig→rec→sig F G))
open NaturalTransformation

3 Natural transformations properties

4 Categorical properties

We prove some useful results which will be used to show that functors form a precategory. Firstly, there is an identity natural transformation.

idⁿ :  {i j k l} {A : Precategory i j} {B : Precategory k l} {F : Functor A B}
       NaturalTransformation F F
idⁿ {i} {j} {k} {l} {A} {B} {F} =
  record { α-ob = λ x  B .Id ;
           α-nat = λ f  B .IdR (F .F₁ f)  B .IdL (F .F₁ f) ^ }

We also have (vertical) composition of natural transformations.

nat-trans-compᵛ :  {i j k l} {A : Precategory i j} {B : Precategory k l} {F G H : Functor A B}
                  (β : NaturalTransformation G H) (α : NaturalTransformation F G)
                   NaturalTransformation F H
nat-trans-compᵛ {i} {j} {k} {l} {A} {B} {F} {G} {H}
  record { α-ob = β₁ ; α-nat = β₂ }
  record { α-ob = α₁ ; α-nat = α₂ } =
    record { α-ob =  a  (β₁ a) o⟨ B  (α₁ a)) ;
             α-nat = λ { {x} {y} f  B .Assoc (F .F₁ f) (α₁ y) (β₁ y) ^ 
               precat-whiskerL B (α₂ f) (β₁ y) 
               B .Assoc (α₁ x) (G .F₁ f) (β₁ y) 
               precat-whiskerR B (β₂ f) (α₁ x) 
               B .Assoc (α₁ x) (β₁ x) (H .F₁ f) ^} }

_oᴺ_ = nat-trans-compᵛ
infixr 9 _oᴺ_

Composing with the identity is as expected.

nat-trans-id-compᵛ :  {i j k l} {A : Precategory i j} {B : Precategory k l} {F G : Functor A B}
                     (α : NaturalTransformation F G)
                      nat-trans-compᵛ idⁿ α  α
nat-trans-id-compᵛ {B = B} record { α-ob = α₁ ; α-nat = α₂ } =
  nat-trans-id (funextD λ x  B .IdR (α₁ x))


nat-trans-compᵛ-id :  {i j k l} {A : Precategory i j} {B : Precategory k l} {F G : Functor A B} (α : NaturalTransformation F G)
                      nat-trans-compᵛ  α idⁿ  α
nat-trans-compᵛ-id {B = B} record { α-ob = α₁ ; α-nat = α₂ } =
  nat-trans-id (funextD λ x  B .IdL (α₁ x))

Finally, composition is associative.

nat-trans-comp-assoc :  {i j k l} {A : Precategory i j} {B : Precategory k l} {F G H K : Functor A B}
                       (α : NaturalTransformation F G) (β : NaturalTransformation G H) (γ : NaturalTransformation H K)
                      nat-trans-compᵛ γ (nat-trans-compᵛ β α)  nat-trans-compᵛ (nat-trans-compᵛ γ β) α
nat-trans-comp-assoc {B = B}
  record { α-ob = α₁ ; α-nat = α₂ }
  record { α-ob = β₁ ; α-nat = β₂ }
  record { α-ob = γ₁ ; α-nat = γ₂ } =
         nat-trans-id
      (funextD λ x  B .Assoc (α₁ x) (β₁ x) (γ₁ x))

Author: James Leslie

Created: 2021-03-27 Sat 10:47