[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