UniAgda.Categories.FunctorCat

Table of Contents

1 Prelude

2 Functor Precategories

3 Natural isomorphisms

One of the first results about natural transformations that one proves, is that a natural transformation is an isomorphism if and only if each component is an isomorphism. We prove that now, hiding each direction in a "private" environment. The forward direction is straightforward, we just need to convert the paths between records into a path between Σ types. Then it is easy to show that we do have an isomorphism.

private
  lemma9-2-4i :  {i₁ i₂ i₃ i₄} {A : Precategory i₁ i₂} {B : Precategory i₃ i₄} {F G : (B ^ A) .ob}
                  (γ : (B ^ A) .hom F G)
                   isIso (B ^ A) γ  ((a : A .ob)  isIso B (γ .α-ob a))
  lemma9-2-4i {B = B} {F = F} {G = G} γ (α , p , q) a =
    let q' = ap (nat-trans-rec→sig F F) q
        p' = ap (nat-trans-rec→sig G G) p in
    (α .α-ob a) ,
    happlyD (pr₁ (path-sigma p')) a ,
    happlyD (pr₁ (path-sigma q')) a

The reverse direction mainly consists of some path algebra. It is mathematically straightforward, but due to associativity, can be unsightly in the details.

  lemma9-2-4ii :  {i₁ i₂ i₃ i₄} {A : Precategory i₁ i₂} {B : Precategory i₃ i₄} {F G : (B ^ A) .ob}
                  (γ : (B ^ A) .hom F G)
                    ((a : A .ob)  isIso B (γ .α-ob a))  isIso (B ^ A) γ
  lemma9-2-4ii {B = B} {F = F} {G = G} record { α-ob = γ₁ ; α-nat = γ₂ } δ =
    record { α-ob = λ a  pr₁ (δ a) ;
             α-nat = λ { {a} {b} f 
               (((((((IdL B (pr₁ (δ b) o⟨ B  G .F₁ f) ^
                  precat-whiskerL B (pr₁ (pr₂ (δ a)) ^) (pr₁ (δ b) o⟨ B  G .F₁ f))
                  Assoc B (pr₁ (δ a)) (γ₁ a) (pr₁ (δ b) o⟨ B  G .F₁ f))
                  precat-whiskerR B (Assoc B (γ₁ a) (G .F₁ f) (pr₁ (δ b)) ^) (pr₁ (δ a)))
                  precat-whiskerR B (precat-whiskerL B (γ₂ f ^) (pr₁ (δ b))) (pr₁ (δ a)))
                  precat-whiskerR B (Assoc B (F .F₁ f) (γ₁ b) (pr₁ (δ b)) ) (pr₁ (δ a)))
                  (Assoc B (pr₁ (δ a)) (F .F₁ f) ((pr₁ (δ b)) o⟨ B  (γ₁ b)) ^))
                ap  Z  comp B (Z) (comp' B (F .F₁ f) (pr₁ (δ a)))) (pr₂ (pr₂ (δ b))))
                IdR B (F .F₁ f o⟨ B  pr₁ (δ a))} } ,
    (nat-trans-id (funextD λ x  pr₁ (pr₂ (δ x)))) ,
    (nat-trans-id (funextD λ x  pr₂ (pr₂ (δ x))))

Combining the above results, we get the desired proof.

nat-trans-iso-components :  {i₁ i₂ i₃ i₄} {A : Precategory i₁ i₂} {B : Precategory i₃ i₄} {F G : (B ^ A) .ob}
                             (γ : (B ^ A) .hom F G)
                              isIso (B ^ A) γ  ((a : A .ob)  isIso B (γ .α-ob a))
nat-trans-iso-components γ =
  (lemma9-2-4i γ) ,
  (lemma9-2-4ii γ)

4 Functor Categories

Author: James Leslie

Created: 2021-03-27 Sat 10:47