Agda formalisation of basic category theory

categories.agda

---
--- An exercise to get myself familiar with Agda by formalising category theory
--- to the extent that Yoneda lemma can be stated and proved.
--- (Agda version 2.6.1 and stdlib 1.3)


import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; trans; sym; cong; cong-app; subst; cong₂)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _∎) renaming (step-≡ to _≡⟨_⟩_)
import Function.Base as Func
open import Level using (Level; _⊔_; Lift; lift; lower) renaming (suc to lsuc; zero to lzero)
import Function.Equality
open Function.Equality.Π using (_⟨$⟩_)

--
-- Categories
--

record Category {l1 l2 : Level} : Set (lsuc l1 ⊔ lsuc l2) where
  field
    obj : Set l1
    hom : obj → obj → Set l2
    id  : ∀ {a : obj} → hom a a
    _∘_ : ∀ {a b c} → hom b c → hom a b → hom a c
    id-identity-r : ∀ {a b} (f : hom a b) → f ∘ id ≡ f
    id-identity-l : ∀ {a b} (f : hom a b) → id ∘ f ≡ f
    ∘-assoc : ∀ {a b c d} {f : hom a b} {g : hom b c} {h : hom c d}
                → (h ∘ (g ∘ f)) ≡ ((h ∘ g) ∘ f)

-- As an example, Agda's Set is a category assuming extensionality
import Axiom.Extensionality.Propositional as Ext
postulate
  extensionality : {a b : Level} → Ext.Extensionality a b
  extensionality-imp : {a b : Level} → Ext.ExtensionalityImplicit a b

𝕊et : ∀ {l : Level} → Category
𝕊et {l} = record {
    obj = Set l
  ; hom = λ (a b : Set l) → (a → b)
  ; id = Func.id
  ; _∘_ = λ {a b c} (g : b → c) (f : a → b) → g Func.∘ f
  ; id-identity-r = λ f → extensionality (λ x → refl)
  ; id-identity-l = λ f → extensionality (λ x → refl)
  ; ∘-assoc = λ {f} {g} {h} → refl
  }


--
-- Functors
--

record Functor {l1 l2 l3 l4 : Level}
               (C : Category {l1} {l2}) (D : Category {l3} {l4})
               : Set (l1 ⊔ l2 ⊔ l3 ⊔ l4) where
  field
    on-obj : Category.obj C → Category.obj D
    on-arrow : ∀ {a b} → Category.hom C a b
                       → Category.hom D (on-obj a) (on-obj b)
    id-preserve : ∀ {a} → on-arrow (Category.id C {a}) ≡ Category.id D {on-obj a}
    ∘-preserve : ∀ {a b c} {f : Category.hom C b c} {g : Category.hom C a b}
                 → on-arrow (Category._∘_ C f g) ≡ Category._∘_ D (on-arrow f) (on-arrow g)
open Functor

-- List is an endo-functor on 𝕊et
import Data.List as List
import Data.List.Properties as ListProp
open List using (List)

L : {l : Level} → Functor (𝕊et {l}) (𝕊et {l})
L = record {
    on-obj = List
  ; on-arrow = List.map
  ; id-preserve = extensionality ListProp.map-id
  ; ∘-preserve = extensionality ListProp.map-compose
  }

-- Maybe is an endo-functor on 𝕊et
import Data.Maybe as Maybe
import Data.Maybe.Properties as MaybeProp
open Maybe using (Maybe)
Mb : {l : Level} → Functor (𝕊et {l}) (𝕊et {l})
Mb = record {
     on-obj = Maybe
   ; on-arrow = Maybe.map
   ; id-preserve = extensionality MaybeProp.map-id
   ; ∘-preserve = extensionality MaybeProp.map-compose
   }

-- Hom functor C(a, -) : C → 𝕊et
homF : ∀ {l1 l2} {C : Category {l1} {l2}} → (a : Category.obj C) → Functor C (𝕊et {l2})
homF {C = C} a = record {
    on-obj = λ x → Category.hom C a x
  ; on-arrow = λ x y → Category._∘_ C x y
  ; id-preserve = extensionality (λ x → Category.id-identity-l C x)
  ; ∘-preserve = λ {a b c f g} → extensionality (λ x → sym (Category.∘-assoc C))
  }

-- A functor lifting 𝕊et {l1} to higher level
𝕊etLift : ∀{l1 : Level} (l2 : Level) → Functor (𝕊et {l1}) (𝕊et {l1 ⊔ l2})
𝕊etLift {l1} l2 = record {
    on-obj = Lift l2
  ; on-arrow = λ f (lift a) → lift (f a)
  ; id-preserve = refl
  ; ∘-preserve = refl
  }

-- Functors can be composed
_∘-F_ : ∀ {l1 l2 l3 l4 l5 l6 : Level} → {C : Category {l1} {l2}} → {D : Category {l3} {l4}} → {E : Category {l5} {l6}}
        → Functor D E → Functor C D → Functor C E
_∘-F_ {C = C} {D = D} {E = E} F G = record {
    on-obj = λ x → on-obj F (on-obj G x)
  ; on-arrow = λ f → on-arrow F (on-arrow G f)
  ; id-preserve =  λ {x} →
      begin
        on-arrow F (on-arrow G (Category.id C))
      ≡⟨ cong (on-arrow F) (id-preserve G) ⟩
        on-arrow F (Category.id D)
      ≡⟨ id-preserve F ⟩
        Category.id E
      ∎
  ; ∘-preserve = λ {a} {b} {c} {f} {g} →
       begin
          on-arrow F (on-arrow G (Category._∘_ C f g))
        ≡⟨ cong (on-arrow F) (∘-preserve G) ⟩
          on-arrow F (Category._∘_ D (on-arrow G f) (on-arrow G g))
        ≡⟨ ∘-preserve F ⟩
          Category._∘_ E (on-arrow F (on-arrow G f)) (on-arrow F (on-arrow G g))
        ∎
  }


--
-- Natural Transformations
--

record NatTrans {l1 l2 l3 l4 : Level}
                {C : Category {l1} {l2}} {D : Category {l3} {l4}}
                (F G : Functor C D) : Set (l1 ⊔ l2 ⊔ l3 ⊔ l4) where
  constructor mkNatTrans
  open Functor
  open Category
  field
    at : (c : obj C) → hom D (on-obj F c) (on-obj G c)
    naturality : ∀ {a b} (f : hom C a b) →
                   _∘_ D (at b) (Functor.on-arrow F f) ≡ _∘_ D (Functor.on-arrow G f) (at a)

-- Two natural transformation are the same when their components are the same
-- TODO: what's the best way to prove equality of records?
NatTrans-≡ : ∀ {l1 l2 l3 l4 : Level}
             → {C : Category {l1} {l2}} {D : Category {l3} {l4}}
             → {F G : Functor C D}
             → {σ τ : NatTrans F G}
             → NatTrans.at σ ≡ NatTrans.at τ
             → σ ≡ τ
NatTrans-≡ {l1} {l2} {l3} {l4} {C} {D} {F} {G} {mkNatTrans a b} {mkNatTrans (.a) d} refl
  = cong (mkNatTrans a) (extensionality-imp (extensionality-imp (extensionality (λ x → eq-uni (b x) (d x)))))
  where eq-uni : ∀ {l : Level} {A : Set l} {x y : A} → (a b : x ≡ y) → a ≡ b
        eq-uni refl refl = refl

-- The first element of the list is extracted, if there is one
List→Maybe : NatTrans L Mb
List→Maybe = record {
    at = extract
  ; naturality = λ f → extensionality (nat f)
  }
  where extract : (c : Set) → List c → Maybe c
        extract c List.[] = Maybe.nothing
        extract c (x List.∷ x₁) = Maybe.just x

        nat : ∀ {a b : Set} (f : a → b) → (l : List a) →
              extract b (List.map f l) ≡ Maybe.map f (extract a l)
        nat f List.[] = refl
        nat f (x List.∷ l) = refl

-- Identity natural transformation
Id-nat : ∀ {l1 l2 l3 l4} {C : Category {l1} {l2}} {D : Category {l3} {l4}}
         → (F : Functor C D) → NatTrans F F
Id-nat {C = C} {D = D} F = record {
    at = λ c → Category.id D {(Functor.on-obj F c)}
  ; naturality = λ f →
      trans (Category.id-identity-l D (Functor.on-arrow F f))
            (sym (Category.id-identity-r D (Functor.on-arrow F f)))
  }

-- Vertical composition of natural transformations
_∘-nat_ : ∀ {l1 l2 l3 l4 : Level} {C : Category {l1} {l2}} {D : Category {l3} {l4}}
            {F G H : Functor C D}
         → NatTrans G H → NatTrans F G → NatTrans F H
_∘-nat_ {D = D} {F = F} {G = G} {H = H} τ σ = record {
    at = λ c → (NatTrans.at τ c) ∘ (NatTrans.at σ c)
  ; naturality = λ {a} {b} f →
      begin
        ((NatTrans.at τ b ∘ NatTrans.at σ b) ∘ Functor.on-arrow F f)
      ≡⟨ sym ∘-assoc ⟩
        NatTrans.at τ b ∘ ((NatTrans.at σ b) ∘ Functor.on-arrow F f)
      ≡⟨ cong (_∘_ (NatTrans.at τ b)) (NatTrans.naturality σ f) ⟩
        NatTrans.at τ b ∘ (Functor.on-arrow G f ∘ NatTrans.at σ a)
      ≡⟨ ∘-assoc ⟩
        (NatTrans.at τ b ∘ Functor.on-arrow G f) ∘ NatTrans.at σ a
      ≡⟨ cong (λ f → f ∘ NatTrans.at σ a) (NatTrans.naturality τ f) ⟩
        (Functor.on-arrow H f ∘ NatTrans.at τ a) ∘ NatTrans.at σ a
      ≡⟨ sym ∘-assoc ⟩
        Functor.on-arrow H f ∘ (NatTrans.at τ a ∘ NatTrans.at σ a)
      ∎
  }
  where open Category D

-- An arrow f : b → a induces a natural transformation from C(a, -) to C(b, -)
hom-nat : ∀ {l1 l2 : Level} {C : Category {l1} {l2}} {a b : Category.obj C}
          → (f : Category.hom C b a) → NatTrans (homF {C = C} a) (homF {C = C} b)
hom-nat {C = C} f = record {
    at = λ c h → h ∘ f
  ; naturality = λ g → extensionality (λ x → sym (∘-assoc))
  }
  where open Category C

---
--- Functors from category C to D form a category with arrows natural transformations.
---
𝔽unctor : ∀ {l1 l2 l3 l4 : Level} (C : Category {l1} {l2}) (D : Category {l3} {l4}) → Category
𝔽unctor C D = record
  { obj = Functor C D
  ; hom = λ F G → NatTrans F G
  ; id = λ {F} → Id-nat F
  ; _∘_ = _∘-nat_
  ; id-identity-r = λ {F} {G} σ → NatTrans-≡ (extensionality (λ x → Category.id-identity-r D (NatTrans.at σ x)))
  ; id-identity-l = λ {F} {G} σ → NatTrans-≡ (extensionality (λ x → Category.id-identity-l D (NatTrans.at σ x)))
  ; ∘-assoc = λ {F} {G} {H} {K} {σ} {τ} {γ} → NatTrans-≡ (extensionality (λ x → Category.∘-assoc D))
  }


---
--- Product category
---
open import Data.Product using (_×_; _,_; proj₁; proj₂)
_×-cat_ : ∀ {a b c d : Level} → Category {a} {b} → Category {c} {d} → Category {a ⊔ c} {b ⊔ d}
C ×-cat D = record {
    obj = obj C × obj D
  ; hom = λ (c1 , c2) (d1 , d2)  →  hom C c1 d1 × hom D c2 d2
  ; id = (id C) , (id D)
  ; _∘_ = λ (f1 , f2) (g1 , g2) →  Category._∘_ C f1 g1 , Category._∘_ D f2 g2
  ; id-identity-r = λ f → cong₂ _,_ (id-identity-r C (proj₁ f)) (id-identity-r D (proj₂ f))
  ; id-identity-l = λ f → cong₂ _,_ (id-identity-l C (proj₁ f)) (id-identity-l D (proj₂ f))
  ; ∘-assoc = λ {a} {b} {c} {d} {(f1 , f2)} {(g1 , g2)} {(h1 , h2)}
      →  cong₂ _,_ (Category.∘-assoc C) (Category.∘-assoc D)
  }
  where open Category

---
--- Yoneda lemma:
---   For any category C and functor F : C → 𝕊et, there is a bijection
---      NatTrans(C(a, -), F) ≅ F a,
---   and this bijection is natural in a and F when viewing both sides
---   of the equation as functors from category (C × 𝔽unctor C 𝕊et) to 𝕊et.
---
open import Function.Bijection using (_⤖_; bijection; Bijection)

-- First comes the bijection and the naturality will be shown later
よ : ∀ {l1 l2 : Level}
     → {C : Category {l1} {l2}} {F : Functor C 𝕊et} {a : Category.obj C}
     → NatTrans (homF a) F ⤖ on-obj F a
よ {l1} {l2} {C} {F} {a} = bijection to from to-injective to-from
  where open NatTrans
        open Category
        to : NatTrans (homF a) F → on-obj F a
        to (mkNatTrans at nat) = at a (id C {a})

        from : on-obj F a → NatTrans (homF a) F
        from fa = mkNatTrans (λ c f → on-arrow F f fa)
                             (λ f → extensionality (λ g → cong-app (∘-preserve F) fa))

        to-from : ∀(x : on-obj F a) → to (from x) ≡ x
        to-from x rewrite id-preserve F {a} = refl

        _∘-C_ : ∀ {a b c} → hom C b c → hom C a b → hom C a c
        _∘-C_ = Category._∘_ C

        to-injective : {τ σ : NatTrans (homF a) F} → to τ ≡ to σ → τ ≡ σ
        to-injective {τ} {σ} eq = NatTrans-≡ (extensionality
          (λ (c : obj C) → extensionality
            (λ (f : hom C a c) →
              begin
                at τ c f
              ≡⟨ lemma {τ} ⟩
                (on-arrow F f) ((at τ a) (id C))
              ≡⟨ cong (on-arrow F f) eq ⟩
                (on-arrow F f) ((at σ a) (id C))
              ≡⟨ sym (lemma {σ}) ⟩
                at σ c f
              ∎ )))
              where lemma : ∀ {τ : NatTrans (homF a) F} → {c : obj C} → {f : hom C a c}
                            → at τ c f ≡ (on-arrow F f) ((at τ a) (id C))
                    lemma {τ} {c} {f} =
                      begin
                        at τ c f
                      ≡⟨ cong (at τ c) (sym (id-identity-r C f)) ⟩
                        at τ c (f ∘-C id C)
                      ≡⟨⟩
                        (Category._∘_ 𝕊et (at τ c) (_∘-C_ f)) (id C)
                      ≡⟨ cong-app (naturality τ f) (id C)⟩
                        (Category._∘_ 𝕊et (on-arrow F f) (at τ a)) (id C)
                      ≡⟨⟩
                        (on-arrow F f) ((at τ a) (id C))
                      ∎

-- Before showing the naturality of よ, we need to formalise its two sides as 𝕊et-valued functors

-- The RHS of よ is the 'functor application functor'.
App : ∀{l1 l2 l3 : Level} {C : Category {l1} {l2}} → Functor ((𝔽unctor C (𝕊et {l3}) ×-cat C)) (𝕊et {l3})
App {C = C} = record {
    on-obj = λ (f , c) → on-obj f c
  ; on-arrow = λ {(F , a)} {(G , b)} (τ , f) →  Category._∘_ 𝕊et (at τ b) (on-arrow F f)
  ; id-preserve =  λ {(F , c)} → extensionality (λ x → cong-app (id-preserve F) x)
  ; ∘-preserve = λ {(F , a)} {(G , b)} {(H , c)} {(τ , f)} {(σ , h)} → extensionality λ x →
      cong (at τ c) (
        begin
          (at σ c (on-arrow F ((C Category.∘ f) h) x))
        ≡⟨ cong (at σ c) (cong-app (∘-preserve F) x) ⟩
          (at σ c (on-arrow F f (on-arrow F h x)))
        ≡⟨ cong-app (naturality σ f) (on-arrow F h x) ⟩
          (on-arrow G f (at σ b (on-arrow F h x)))
        ∎)
  }
  where open NatTrans


-- The LHS of よ is a (bi-)functor from ((𝔽unctor C 𝕊et) ×-cat C) to 𝕊et mapping < F , c > to Nat(C(a, -), F)
YoLHS : ∀{l1 l2 : Level} {C : Category {l1} {l2}} → Functor ((𝔽unctor C (𝕊et {l2}) ×-cat C)) (𝕊et {l1 ⊔ lsuc l2})
YoLHS {l1} {l2} {C = C} = record {
    on-obj = λ (F , c) → NatTrans (homF c) F
  ; on-arrow =  λ {(F , a)} {(G , b)} (τ , f) → λ σ → τ ∘-nat (σ ∘-nat hom-nat f)
  ; id-preserve = λ {(F , c)} → extensionality (λ σ →
      begin
        (Id-nat F ∘-nat (σ ∘-nat hom-nat (id C)))
      ≡⟨ id-identity-l (𝔽unctor C 𝕊et) (σ ∘-nat hom-nat (id C)) ⟩
        σ ∘-nat hom-nat (id C)
      ≡⟨ NatTrans-≡ (extensionality (λ c → extensionality (λ f → cong (at σ c) (id-identity-r C f)))) ⟩
        σ
      ∎)
      ; ∘-preserve = λ {_} {_} {_} {(σ , f)} {(τ , h)} → extensionality (λ γ →
          NatTrans-≡ (extensionality (λ c →
            extensionality (λ k → cong (λ x → at σ c (at τ c (at γ c x))) (∘-assoc C {f = h} {g = f} {h = k})))))
  }
  where open NatTrans
        open Functor
        open Category


-- Now we are ready to prove よ is natural
よ-nat : ∀ {l1 l2 : Level} {C : Category {l1} {l2}}
         → NatTrans (YoLHS {l1} {l2} {C}) (𝕊etLift (l1 ⊔ lsuc l2) ∘-F App {l1} {l2} {l2})
よ-nat {l1} {l2} {C}=
  mkNatTrans (λ (F , c) σ → lift (Bijection.to よ ⟨$⟩ σ))
             λ {(F , c)} {(G , d)} (τ , f) → extensionality (λ σ →
                cong lift (cong (at τ d) (
                  begin
                    at (σ ∘-nat hom-nat {C = C} f) d (id C)
                  ≡⟨⟩
                    ((at σ d) Func.∘ (at (hom-nat {C = C} f) d)) (id C)
                  ≡⟨⟩
                    at σ d (at (hom-nat {C = C} f) d (id C))
                  ≡⟨ cong (at σ d) (id-identity-l C f) ⟩
                    at σ d f
                  ≡⟨ cong (at σ d) (sym (id-identity-r C f)) ⟩
                    at σ d (Category._∘_ C f (id C {a = c}))
                  ≡⟨ cong-app (naturality σ f) (id C) ⟩
                    on-arrow F f (Bijection.to よ ⟨$⟩ σ)
                  ∎)))
  where open NatTrans
        open Category