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-φ∘ φ₁ φ₂
                          }

That extensionality is a postulate is an issue with type theory (with many attempted fixes), so I don't try avoiding it.

That said, as I hinted at on Twitter, both uses of ext (line 31 and line 44) could be replaced by using a new member of Functor called preserve-pointwise-eq: ∀ {f g} → f ≗ g → map f ≗ map g.

You'd need to prove it for each Functor, and I'm not sure you (always) can without extensionality — AFAICS in my head, that works easily for functors like A × —, but fails for representable functors like A → —. There, pointwise equality on arbitrary input h requires f ∘ h ≡ g ∘ h, but I fear without extensionality we can only prove f (h x) ≡ g (h x).

Since you already use extensionality, you could drop the pointwise equality from the Functor definition and use plain prop equality.

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