Functors compose

Compose.agda

module Compose where

open import Level
open import Function
open import Relation.Binary.PropositionalEquality

record Functor {α} (T : Set α → Set α) : Set (suc α) where
  field
    map : ∀ {A B : Set α} → (A → B) → T A → T B
    identity : ∀ {A : Set α} → map id ≡ id {A = T A}
    composition : ∀ {A B C : Set α} → (f : B → C) → (g : A → B) → map (f ∘ g) ≡ map f ∘ map g

open Functor
open ≡-Reasoning

map-φ∘ : ∀ {α} {F G : Set α → Set α} {A B : Set α} → Functor F → Functor G → (A → B) → (F ∘ G) A → (F ∘ G) B
map-φ∘ f g = map f ∘ map g

identity-φ∘ : ∀ {α} {F G : Set α → Set α} {A : Set α} →
              (φ₁ : Functor F) → (φ₂ : Functor G) →
              map-φ∘ φ₁ φ₂ id ≡ id {A = (F ∘ G) A}
identity-φ∘ {A = A} φ₁ φ₂ = begin
  map φ₁ (map φ₂ id)  ≡⟨ cong (map φ₁) (identity φ₂) ⟩
  map φ₁ id           ≡⟨ identity φ₁ ⟩
  id                  ∎

composition-φ∘ : ∀ {α} {F G : Set α → Set α} {A B C : Set α} →
                 (φ₁ : Functor F) → (φ₂ : Functor G) →
                 (f : B → C) → (g : A → B) →
                 map-φ∘ φ₁ φ₂ (f ∘ g) ≡ map-φ∘ φ₁ φ₂ f ∘ map-φ∘ φ₁ φ₂ g
composition-φ∘ φ₁ φ₂ f g = begin
  map φ₁ (map φ₂ (f ∘ g))                ≡⟨ cong (map φ₁) (composition φ₂ f g) ⟩
  map φ₁ (map φ₂ f ∘ map φ₂ g)           ≡⟨ composition φ₁ (map φ₂ f) (map φ₂ g) ⟩
  map φ₁ (map φ₂ f) ∘ map φ₁ (map φ₂ g)  ∎

functor-φ∘ : ∀ {α} {F G : Set α → Set α} → Functor F → Functor G → Functor (F ∘ G)
functor-φ∘ φ₁ φ₂ = record { map = map φ₁ ∘ map φ₂
                          ; identity = identity-φ∘ φ₁ φ₂
                          ; composition = composition-φ∘ φ₁ φ₂
                          }

@AndrasKovacs thanks! I was also able to remove the need for extensionality by removing pointwise equality.