[Agda] Associativity for free!

[Alan Jeffrey]

OK, that's pretty cool.

One thing which did occur to me (though I didn't persue it very far) is 
that there's a connection with n-categorical machinery.

Recall that the equivalence (ok : f ≡ _++_ as) had to be declared 
irrelevant, because otherwise its proof objects were causing 
associativity to fail. Well, we could (of course, who would do anything 
else :-) do the same trick one level up, and replace ok by a function 
something like (ok1 : ∀ bs g → (g ≡ _++_ bs) → ((g ◦ f) ≡ _++_ (g as))), 
that is ok1 proves that composition with f transforms 
appending-functions to appending-functions. In particular, ok is (ok1 [] 
id refl).

Oh, but now we're not isomorphic to lists any more, because there's too 
many ok1 functions, so we need an ok2 which says that ok1 is "the 
obvious proof given ok". Ah, but then ok2 needs to be irrelevant. Or we 
play the same trick again and define ok3 (etc. etc. etc.)

This all has the flavor of an n-category where you have n levels of 
canonical isomorphisms, with a base case of definitional equality.

It would take a braver person than I to try to persuade Agda of this though.

A.

On 10/27/2011 08:47 AM, James Chapman wrote:
> 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
>