UniAgda.Categories.Functor

Table of Contents

1 Prelude

2 Definition

We introduce functors between precategories as a record, giving the sigma type and equivalence later.

record Functor {i j k l} (A : Precategory i j) (B : Precategory k l) : Type (i  j  k  l) where
  eta-equality
  private module A = Precategory A
  private module B = Precategory B
  field
    F₀ : A .ob  B .ob
    F₁ : {a b : A .ob}  A [ a , b ]   B [ (F₀ a) , (F₀ b) ]
    F-id : {a : A .ob}  F₁ (A .Id {a})  (B .Id {F₀ a})
    F-comp : {a b c : A .ob} (g : A [ b , c ]) (f : A [ a , b ])  F₁ (g o⟨ A  f)  (F₁ g) o⟨ B  (F₁ f)

   = F₀
   = F₁

2.1 Sigma definition and equivalence

Functor-sig :  {i j k l}
          (A : Precategory i j) (B : Precategory k l)
           Type (i  j  k  l)
Functor-sig {i} {j} {k} {l} A B =
  let module A = Precategory A in
    let module B = Precategory B in
      Σ[ F₀  ((A.ob)  (B.ob))] (
        Σ[ F₁  ({a b : A.ob}  A.hom a b  B.hom (F₀ a) (F₀ b))] (
          Σ[ F-id  ({a : A.ob}  F₁ (A.Id {a})  (B.Id {F₀ a}))] (
            ({a b c : A.ob} (g : A.hom b c) (f : A.hom a b)  F₁ (A.comp g f)  B.comp (F₁ g) (F₁ f)))))

functor-sig→rec :  {i j k l}
                  (A : Precategory i j) (B : Precategory k l)
                   Functor-sig A B  Functor A B
functor-sig→rec A B (F₀ , F₁ , F-id , F-comp) =
  record { F₀ = F₀ ; F₁ = F₁ ; F-id = F-id ; F-comp = F-comp }

functor-rec→sig :  {i j k l}
                  (A : Precategory i j) (B : Precategory k l)
                   Functor A B  Functor-sig A B
functor-rec→sig A B record { F₀ = F₀ ; F₁ = F₁ ; F-id = F-id ; F-comp = F-comp } =
  (F₀ ,
  F₁ ,
  F-id ,
  F-comp)

functor-rec→sig→rec :  {i j k l}
                      (A : Precategory i j) (B : Precategory k l)
                       (F : Functor A B)  (functor-sig→rec A B o functor-rec→sig A B) F  F
functor-rec→sig→rec A B F = refl

functor-sig→rec→sig :  {i j k l}
                      (A : Precategory i j) (B : Precategory k l)
                       (F : Functor-sig A B)  (functor-rec→sig A B o functor-sig→rec A B) F  F
functor-sig→rec→sig A B (F₀ , F₁ , F-id , F-comp) =
  path-equiv-sigma (refl ,
    (path-equiv-sigma (refl ,
      (path-equiv-sigma (refl ,
        refl)))))

Functor-sig-Equiv :  {i j k l}
                    (A : Precategory i j) (B : Precategory k l)
                     Functor-sig A B  Functor A B
Functor-sig-Equiv A B = equiv-adjointify
  (functor-sig→rec A B ,
  functor-rec→sig A B ,
  functor-rec→sig→rec A B ,
  functor-sig→rec→sig A B)
open Functor

3 Paths between functors

4 Functor composition

5 Identity functor

Author: James Leslie

Created: 2021-03-27 Sat 10:47