[Agda] Associativity for free!

James Chapman james at cs.ioc.ee
Thu Oct 27 15:47:01 CEST 2011


Next I wondered if we can generalize this from monoids to categories. For this we need Yoneda's lemma (a.k.a. Cayley's theorem on steroids).

First an even bigger pile of suspicious looking machinery:

{-# OPTIONS --type-in-type #-}
module Yoneda where

data _≡_ {A : Set}(a : A) : {A' : Set} → A' → Set where
  refl : a ≡ a

sym : ∀{A A' : Set}{a : A}{a' : A'} → a ≡ a' → a' ≡ a
sym refl = refl

trans : ∀{A A' A'' : Set}{a : A}{a' : A'}{a'' : A''} →
        a ≡ a' → a' ≡ a'' → a ≡ a''
trans refl p = p

funnycong : ∀{A}{B : A → Set}{C : Set}{a a' : A} → a ≡ a' →
            .{b : B a} → .{b' : B a'} →
	    (f : (a : A) → .(B a) → C) → f a b ≡ f a' b'
funnycong refl f = refl

cong : {A B : Set}(f : A → B){a a' : A} → a ≡ a' → f a ≡ f a'
cong f refl = refl

fcong : ∀{A}{B : A → Set}{f f' : (x : A) → B x}(a : A) → f ≡ f' → f a ≡ f' a
fcong a refl = refl

ifcong : ∀{A}{B : A → Set}{f f' : {x : A} → B x}(a : A) →
         _≡_ { {x : A} → B x} f { {x : A} → B x} f' → f {a} ≡ f' {a}
ifcong a refl = refl

ir : ∀{A A'}{a : A}{a' : A'}{p q : a ≡ a'} → p ≡ q
ir {p = refl} {q = refl} = refl

fixtypes : ∀{A A' : Set}{a a' : A}{a'' a''' : A'}
           {p : a ≡ a'}{q : a'' ≡ a'''} → a ≡ a'' → a' ≡ a''' → p ≡ q
fixtypes refl refl = ir

postulate ext : {X Y : Set}{f g : X → Y} → (∀ x → f x ≡ g x) → f ≡ g

postulate iext : {A : Set}{B B' : A → Set}{f : ∀ {a} → B a}{g : ∀{a} → B' a} →
                 (∀ a → f {a} ≡ g {a}) →
                 _≡_ { {a : A} → B a} f { {a : A} → B' a} g

id : {X : Set} → X → X
id = λ x → x

_◦_ : {X Y Z : Set} → (Y → Z) → (X → Y) → X → Z
f ◦ g = λ x → f (g x)

Ok, now we define a category as follows:

record Cat : Set where
  field Obj  : Set
        Hom  : Obj → Obj → Set
        iden : ∀{X} → Hom X X
        comp : ∀{X Y Z} → Hom Y Z → Hom X Y → Hom X Z
        idl  : ∀{X Y}{f : Hom X Y} → comp iden f ≡ f
        idr  : ∀{X Y}{f : Hom X Y} → comp f iden ≡ f
        ass  : ∀{W X Y Z}{f : Hom Y Z}{g : Hom X Y}{h : Hom W X} →
               comp (comp f g) h ≡ comp f (comp g h)
open Cat

Now, Yoneda's embedding says that we can view morphism in C as the following polymorphic function:

Y : ∀{C A B} → Hom C A B → (∀ Z → Hom C B Z → Hom C A Z)                        
Y {C} f = λ Z g → comp C g f                                                    

and we can convert back again:                                                                                

Y-1 : ∀{C A B} → (∀ Z → Hom C B Z → Hom C A Z) → Hom C A B                      
Y-1 {C}{A}{B} α = α B (iden C)                                                  

Given any category we can transform it like so:
                                                                                
CatY : Cat → Cat                                                                
CatY C = record {                                                               
  Obj  = Obj C;                                                                 
  Hom  = λ X Y → ∀ Z → Hom C Y Z → Hom C X Z;                                   
  iden = λ X → id;                                                              
  comp = λ α β Z → β Z ◦ α Z;                                                   
  idl  = refl;                                                                  
  idr  = refl;                                                                  
  ass  = refl}                                                                  

Notice we get the identities, and associativity for free.

We're sort of done unless we'd like to actually prove the isomorphism between the homsets in these categories (Yoneda's lemma).

If we actually want to prove Yoneda's lemma we need to consider natural transformations instead of just polymorphic functions and some more machinery:

Functors:

record Fun (C D : Cat) : Set where
  field OMap  : Obj C → Obj D
        HMap  : ∀{X Y} → Hom C X Y → Hom D (OMap X) (OMap Y)
        fid   : ∀{X} → HMap (iden C {X}) ≡ iden D {OMap X}
        fcomp : ∀{X Y Z}{f : Hom C Y Z}{g : Hom C X Y} →
                HMap (comp C f g) ≡ comp D (HMap f) (HMap g)
open Fun

The category of sets:

Sets : Cat
Sets = record{
  Obj  = Set;
  Hom  = λ X Y → X → Y;
  iden = id;
  comp = λ f g → f ◦ g;
  idl  = refl;
  idr  = refl;
  ass  = refl}

Notice the laws come from free in Sets.

Hom functors:

HomF : {C : Cat} → (A : Obj C) → Fun C Sets
HomF {C} A = record {
  OMap  = Hom C A;
  HMap  = comp C;
  fid   = ext λ _ → idl C;
  fcomp = ext λ _ → ass C}

Natural transformations:

record NatT {C D}(F G : Fun C D) : Set where
  field cmp : ∀ {X} → Hom D (OMap F X) (OMap G X)
        .nat : ∀{X Y}{f : Hom C X Y} →
              comp D (HMap G f) cmp ≡ comp D cmp (HMap F f)

open NatT

we also define this handy principle which says that two NatTs are equal if their components are equal:

NatTEq : {C D : Cat}{F G : Fun C D}{α β : NatT F G} →
         (λ {X : Obj C} → cmp α {X}) ≡ (λ {X : Obj C} → cmp β {X}) → α ≡ β
NatTEq {C}{D}{F}{G} {α} {β} p = funnycong
  {∀ {X} → Hom D (OMap F X) (OMap G X)}
  {λ cmp → ∀{X Y}{f : Hom C X Y} →
    comp D (HMap G f) cmp ≡ comp D cmp (HMap F f)}
  {NatT F G}
  p
  {λ{X}{Y}{f} → nat α {X}{Y}{f}}{λ{X}{Y}{f} → nat β {X}{Y}{f}}
  λ x y → record{cmp = x;nat = y}

Now we can redefine Y and Y-1 properly:

Y : ∀{C A B} → Hom C A B → NatT {C} (HomF B) (HomF A)
Y {C} f = record {
  cmp = λ g → comp C g f;
  nat = ext λ h → sym (ass C)}

Y-1 : ∀{C A B} → (NatT {C} (HomF B) (HomF A)) → Hom C A B
Y-1 {C} α = cmp α (iden C)

and prove Yoneda's lemma:

Yoneda : ∀ C A B → Iso (Hom C A B) (NatT {C} (HomF B) (HomF A))
Yoneda C A B = record {
  fun = Y {C};
  inv = Y-1 {C};
  left = ext λ α → NatTEq (iext λ Z → ext λ g → trans (fcong (iden C) (nat α))
                                                      (cong (cmp α) (idr C)));
  right = ext λ x → idl C}

Ok, I'm cheating a little, we should also prove that it is natural in A and B. Here we just proved it is an isomorphism.

I would like to get associativity and the identities for free for composition of natural transformations, I can't have this in general as it composition uses composition in the target category of the functors which may not come for free. But, if the target category is Sets (if we have natural transformations between pre sheaves, which hom functors are, then it is) then we do get this stuff for free:

idNat : ∀{C}{F : Fun C Sets} → NatT F F
idNat {C}{F} = record {
  cmp = id;
  nat = refl}

compNat : ∀{C}{F G H : Fun C Sets} → NatT G H → NatT F G → NatT F H
compNat {C}{F}{G}{H} α β = record {
  cmp = cmp α ◦ cmp β;
  nat = λ{X}{Y}{f} → ext λ Z → trans (fcong (cmp β Z) (nat α {f = f}))
                                     (cong (cmp α) (fcong Z (nat β {f = f})))}

idlNat : ∀{C}{F G : Fun C Sets}{α : NatT F G} → compNat idNat α ≡ α
idlNat {C} = refl

idrNat : ∀{C}{F G : Fun C Sets}{α : NatT F G} → compNat α idNat ≡ α
idrNat {C}{D} = refl

assNat : ∀{C}{E F G H : Fun C Sets}{α : NatT G H}{β : NatT F G}{η : NatT E F}
         → compNat (compNat α β) η ≡ compNat α (compNat β η)
assNat {C}{D} = refl

I can fold this all up into a category CatY where the laws hold definitionally:

CatY : Cat → Cat
CatY C = record {
  Obj  = Obj C;
  Hom  = λ A B → NatT {C} (HomF B) (HomF A);
  iden = idNat;
  comp = λ α β → compNat β α;
  idl  = refl;
  idr  = refl;
  ass  = refl}

Best wishes,

James

On Oct 27, 2011, at 12:46 PM, James Chapman wrote:

> It strikes me that this trick works because difference lists are an embodyment of Cayley's theorem for monoids.
> 
> First some machinery:
> 
> {-# OPTIONS --type-in-type #-}
> 
> module Cayley where
> 
> data _≡_ {A : Set}(a : A) : {A' : Set} → A' → Set where
>  refl : a ≡ a
> 
> sym : ∀{A A' : Set}{a : A}{a' : A'} → a ≡ a' → a' ≡ a
> sym refl = refl
> 
> ir : ∀{A A'}{a : A}{a' : A'}{p q : a ≡ a'} → p ≡ q
> ir {p = refl} {q = refl} = refl
> 
> fixtypes : ∀{A A' : Set}{a a' : A}{a'' a''' : A'}{p : a ≡ a'}{q : a'' ≡ a'''} → a ≡ a'\
> ' → a' ≡ a''' → p ≡ q
> fixtypes refl refl = ir
> 
> cong : {X Y : Set}(f : X → Y){x x' : X} → x ≡ x' → f x ≡ f x'
> cong f refl = refl
> 
> id : {X : Set} → X → X
> id = λ x → x
> 
> _◦_ : {X Y Z : Set} → (Y → Z) → (X → Y) → X → Z
> f ◦ g = λ x → f (g x)
> 
> Given any monoid (M) where the monoid laws hold propositionally:
> 
> record Monoid : Set1 where
>  field set : Set
>        ε   : set
>        _•_ : set → set → set
>        lid : ∀{m} → (ε • m) ≡ m
>        rid : ∀{m} → (m • ε) ≡ m
>        ass : ∀{m m' m''} → (m • (m' • m'')) ≡ ((m • m') • m'')
> open Monoid
> 
> We can define a monoid (MorphMon M) where the monoid laws hold definitionally by using functions (where the monoidal structure given by identity and composition holds definitionally).
> Morph : Monoid → Set
> Morph M = set M → set M
> 
> MorphMon : Monoid → Monoid
> MorphMon M = record {
>  set = Morph M;
>  ε   = id;
>  _•_ = _◦_;
>  lid = refl;
>  rid = refl;
>  ass = refl}
> 
> Any Monoid (M, ε, _•_) is isomorphic to a subset of Morph M where the function is given by _•_ m for some m : M.
> 
> Here's a proof:
> 
> record Σ (A : Set)(P : A → Set) : Set where
>  constructor _,_
>  field fst : A
>        snd : P fst
> 
> open Σ
> 
> eqΣ : {I : Set}{i : I}{A A' : I -> Set}{a : A i}{i' : I}{a' : A' i'} ->
>          i ≡ i' -> A ≡ A' -> a ≡ a' -> _≡_ {Σ I A}(i , a) {Σ I A'}  (i' , a')
> eqΣ refl refl refl = refl
> 
> record Iso (X Y : Set) : Set where
>  field fun   : X → Y
>        inv   : Y → X
>        left  : (fun ◦ inv) ≡ id {Y}
>        right : (inv ◦ fun) ≡ id {X}
> 
> postulate ext : {X Y : Set}{f g : X → Y} → (∀ x → f x ≡ g x) → f ≡ g
> 
> Cayley : ∀ M → Iso (set M) (Σ (Morph M) λ morphM → Σ (set M) λ m → morphM ≡ _•_ M m)
> Cayley M = record {
>  fun   = λ m → (_•_ M m) , (m , refl);
>  inv   = λ p → fst (snd p);
>  left  = ext λ x → let y = sym (snd (snd x)) in eqΣ y refl (eqΣ refl (ext λ x' → cong (λ x → x ≡ (_•_ M x')) y) (fixtypes y refl));
>  right = refl}
> 
> I wonder if we can use this trick for groups as well as monoids and get difference integers, difference 'nats (mod n)' etc. For groups we should represent them as isomorphisms (automorphims) not functions so we would need isos to have a monodical structure which holds definitionally. But the do if we mark the field left and right above as irrelevant:
> 
> _·_ : ∀{X Y Z} → Iso Y Z → Iso X Y → Iso X Z
> f · g = record {
>  fun   =  fun f ◦ fun g ;
>  inv   = inv g ◦ inv f;
>  left  = trans (cong (λ id → (fun f ◦ id) ◦ inv f) (left g)) (left f) ;
>  right = trans (cong (λ id → (inv g ◦ id) ◦ fun g) (right f)) (right g)}
> 
> idI : ∀{X} → Iso X X
> idI {X} = record {
>  fun   = id;
>  inv   = id;
>  left  = refl;
>  right = refl}
> 
> ridI : ∀{X Y}(f : Iso X Y) → (f · idI) ≡ f
> ridI f = refl
> 
> lidI : ∀{X Y}(f : Iso X Y) → (idI · f) ≡ f
> lidI f = refl
> 
> assI : ∀{W X Y Z}(f : Iso Y Z)(g : Iso X Y)(h : Iso W X) →
>       (f · (g · h)) ≡ ((f · g) · h)
> assI f g h = refl
> 
> So, it looks promising so far.
> 
> Regards,
> 
> James



More information about the Agda mailing list