26 Oct 2011 16:48

```Hi everyone,

A quick note about a trick for representing lists (or any other monoid)
up to associativity. Am I reinventing a wheel here?

I've been doing some mucking around recently with proofs about
lambda-calculi and was hitting annoying problems with associativity
on lists. A prototypical example is:

weakening : ∀ {A a} (as bs cs : List A) →
(a ∈ (as ++ cs)) → (a ∈ (as ++ bs ++ cs))

It's easy to prove that ++ is associative, but making use of that fact
is rather painful, as there's lots of manual wiring with subst and cong,
for example:

weaken2 : ∀ {A a} (as bs cs ds : List A) →
(a ∈ (as ++ bs ++ ds)) → (a ∈ (as ++ bs ++ cs ++ ds))
weaken2 {A} {a} as bs cs ds a∈es =
subst (λ X → (a ∈ X)) (++-assoc as bs (cs ++ ds))
(weakening (as ++ bs) cs ds
(subst (λ X → (a ∈ X)) (sym (++-assoc as bs ds)) a∈es))

This gets tiresome pretty rapidly. Oh if only there were a data
structure which represented lists, but for which ++ was associative up
to beta reduction... Oh look there already is one, it's called
difference lists. Quoting the standard library:

DiffList : Set → Set
DiffList a = List a → List a
```

26 Oct 2011 19:32

Hi Alan,

I'm not aware of any prior art, but this is really nice. A few questions, based on my attempt to repeat your work. I'm a bit of a novice in Agda, so bear with me.

1. I couldn't use your definitions as-is without postulating extensional equality (i.e point wise equality = propositional functional equality) . Rephrasing your ok type as follows:

.ok : {x : List A} → (fun x ≡ (list ++ x))

Solves this problem (and doesn't break anything, as far as I can tell). Perhaps I am missing something obvious?

2. I could not come up with a satisfactory way to define your "case" function, even with =-relevant. Care to share your implementation? Once again, I could just be being thick.

Cheers, this looks really cool!

Liam O'Connor

On Thursday, 27 October 2011 at 1:48 AM, Alan Jeffrey wrote:

Hi everyone,

A quick note about a trick for representing lists (or any other monoid)
up to associativity. Am I reinventing a wheel here?

I've been doing some mucking around recently with proofs about
lambda-calculi and was hitting annoying problems with associativity
on lists. A prototypical example is:

weakening : ∀ {A a} (as bs cs : List A) →
(a ∈ (as ++ cs)) → (a ∈ (as ++ bs ++ cs))

It's easy to prove that ++ is associative, but making use of that fact
is rather painful, as there's lots of manual wiring with subst and cong,
for example:

weaken2 : ∀ {A a} (as bs cs ds : List A) →
(a ∈ (as ++ bs ++ ds)) → (a ∈ (as ++ bs ++ cs ++ ds))
weaken2 {A} {a} as bs cs ds a∈es =
subst (λ X → (a ∈ X)) (++-assoc as bs (cs ++ ds))
(weakening (as ++ bs) cs ds
(subst (λ X → (a ∈ X)) (sym (++-assoc as bs ds)) a∈es))

This gets tiresome pretty rapidly. Oh if only there were a data
structure which represented lists, but for which ++ was associative up
to beta reduction... Oh look there already is one, it's called
difference lists. Quoting the standard library:

DiffList : Set → Set
DiffList a = List a → List a

_++_ : ∀ {a} → DiffList a → DiffList a → DiffList a
xs ++ ys = λ k → xs (ys k)

Unfortunately, difference lists are not isomorphic to lists: there's a
lot more functions on lists than just concatenation functions. This
causes headaches (e.g. writing inductive functions on difference lists).

A first shot at fixing this is to write a data structure for those
difference lists which are concatenations:

record Seq (A : Set) : Set where
constructor seq
field
list : List A
fun : List A → List A
ok : fun ≡ _++_ list -- Broken

It's pretty straightforward to define the monoidal structure for Seq:

ε : ∀ {A} → Seq A
ε = seq [] id refl

_+_ : ∀ {A} → Seq A → Seq A → Seq A
(seq as f f✓) + (seq bs g g✓) = seq (f bs) (f ∘ g) (...easy lemma...)

Unfortunately, we're back to square one again, because + is only
associative up to propositional equality, not beta reduction. This time,
it's the ok field that gets in the way. So we can fix that, and just
make the ok field irrelevant, that is:

record Seq (A : Set) : Set where
constructor seq
field
list : List A
fun : List A → List A
.ok : fun ≡ _++_ list -- Fixed

open Seq public renaming (list to [_])

Hooray, + is now associative up to beta reduction:

+-assoc : ∀ {A} (as bs cs : Seq A) →
((as + bs) + cs) ≡ (as + (bs + cs))
+-assoc as bs cs = refl

≡-relevant : ∀ {A : Set} {a b : A} → .(a ≡ b) → (a ≡ b)

we can define:

data Case {A : Set} : Seq A → Set where
[] : Case ε
_∷_ : ∀ a as → Case (a ◁ as)

case : ∀ {A} (as : Seq A) → Case as

and this gives us recursive functions over Seq (which somewhat to my
surprise actually get past the termination checker), for example:

ids : ∀ {A} → Seq A → Seq A
ids as with case as
ids .(a ◁ as) | a ∷ as = a ◁ ids as
ids .ε | [] = ε

For example, we can now define weakening:

weakening : ∀ {A a} (as bs cs : Seq A) →
(a ∈ [ as + cs ]) → (a ∈ [ as + bs + cs ])

and use it up to associativity without worrying hand-coded wiring:

weaken2 : ∀ {A a} (as bs cs ds : Seq A) →
(a ∈ [ as + bs + ds ]) → (a ∈ [ as + bs + cs + ds ])
weaken2 as bs = weakening (as + bs)

Hooray, cake! Eating it!

I suspect this trick works for most any monoid, so you can do
associativity on naturals, vectors, partial orders with join, etc. etc.

The idea of using difference lists to represent lists is standard, but
as far as I know, this use of irrelevant equalities to get structural
recursion is new. Anyone know of any prior art?

A.
_______________________________________________
Agda mailing list

```_______________________________________________
Agda mailing list
Agda@...
https://lists.chalmers.se/mailman/listinfo/agda
```
26 Oct 2011 23:01

```Hi Alan,

I too have encountered this problem, rather than tackling it head on here are two ways of tiptoeing around it.

1. A trivial solution for your example is simply to make _++_ associate to the left:

data List (X : Set) : Set where
[]   : List X
_::_ : X → List X → List X

_++_ : ∀{X} → List X → List X → List X
[]        ++ xs' = xs'
(x :: xs) ++ xs' = x :: (xs ++ xs')

infixl 5 _++_

postulate P : ∀{X} → List X → Set

postulate weakening : ∀ {A} (as bs cs : List A) →
P (as ++ cs) → P (as ++ bs ++ cs)

weaken2 : ∀ {A} (as bs cs ds : List A) →
P (as ++ bs ++ ds) → P (as ++ bs ++ cs ++ ds)
weaken2 as bs cs ds p = weakening (as ++ bs) cs ds p

This may sound silly and perhaps you might somewhere else need append to associate to the right. Nisse told
me that in a recent implementation of a dependently typed lambda calculus he defined both versions and
didn't end up needing them both at the same time. Do you need both at the same time?

2. I guess you run into the this problem where ++ is an operation on contexts right? Another solution I learnt
from Conor (exercise 15, his AFP notes http://www.strictlypositive.org/epigram-notes.ps.gz) is
simply to avoid it. Instead of giving weakening this type, give a first order presentation of weakenings
(functions from a context to the same context with more stuff chucked in arbitrary places). For  lists this
function space would be the following inductively defined sublist relation:

data _≤_ {X : Set} : List X → List X → Set where
done : [] ≤ []
keep : ∀{x}{xs xs'} → xs ≤ xs' → (x :: xs) ≤ (x :: xs')
skip : ∀{x}{xs xs'} → xs ≤ xs' → xs ≤ (x :: xs')

Then, weakening would be something like:

weakening : ∀{X}{xs xs' : List X} → P xs → xs ≤ xs' → P xs'

By doing this ++ never appears in the types, so we don't have to use subst. I used this technique (called order
preserving embeddings) in chapter 4 of my thesis (http://www.cs.ioc.ee/~james/papers/thesis.pdf )
and it was much more pleasant than using ++ as we did in our Big-step normalization paper
(http://www.cs.ioc.ee/~james/papers/tait2.pdf) on which this chapter was based.

Best wishes,

James
```
27 Oct 2011 02:48

```On 10/26/2011 04:01 PM, James Chapman wrote:
> 1. A trivial solution for your example is simply to make _++_ associate to the left:

Indeed. Unfortunately, sometimes it's convenient one way round, and
sometimes the other. No matter which way you pick, it'll go wrong half
the time

> 2. Another solution I learnt from Conor (exercise 15, his AFP notes
http://www.strictlypositive.org/epigram-notes.ps.gz) is simply to avoid it.

Hmm, I can see that this might work, though some lemmas (e.g.
substitution commuting with weakening) would need a bit of work. Of
course at this point having hacked out a version of lists with
associativity, I'd like to keep pushing on it to see if I can get the
properties I need to go through.

> Alan: neat trick!

Thanks!

A.
```
27 Oct 2011 11:46

```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```
27 Oct 2011 15:47

```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}

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
```
27 Oct 2011 21:06

```Hi all,

Real cool trick!

I offer you: Cartesian categories

The object language has distinguished product objects now:

data Obj (Base : Set) : Set where
▹ : Base -> Obj Base
_×_ : (X Y : Obj Base) -> Obj Base
⊤ : Obj Base

We just add the fields for products:

record Cat : Set where
field Base  : Set
Hom   : Obj Base → Obj Base → 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)
π₁    : ∀ {X Y} → Hom (X × Y) X
π₂    : ∀ {X Y} → Hom (X × Y) Y
pair  : ∀ {X Y Z} → Hom X Y → Hom X Z → Hom X (Y × Z)
π₁β   : ∀ {X Y Z}{f : Hom X Y}{g : Hom X Z} -> comp π₁ (pair f g) ≡ f
π₂β   : ∀ {X Y Z}{f : Hom X Y}{g : Hom X Z} -> comp π₂ (pair f g) ≡ g
η     : ∀ {X Y Z}{f : Hom X (Y × Z)} -> f ≡ (pair (comp π₁ f)
(comp π₂ f))
!     : ∀ {X} -> Hom X ⊤
!η    : ∀ {X}{f g : Hom X ⊤} -> f ≡ g
open Cat

we define Homs which give us the β and η laws from Agda's products:

HomI : ∀ C (X Y : Obj (Base C)) -> Set
HomI C X (▹ B) = Hom C X (▹ B)
HomI C X (Y1 × Y2) = (HomI C X Y1) * (HomI C X Y2)
HomI C X ⊤ = Unit

Add the transformations to the Yoneda embedding; use HomI from above:

CatY : Cat → Cat
CatY C = record {
Base  = Base C;
Hom   = λ X Y → ∀ Z → HomI C Z X → HomI C Z Y;
iden  = λ Z -> id;
comp  = λ α β Z → (α Z) ◦ (β Z);
idl   = refl;
idr   = refl;
ass   = refl;
π₁    = λ Z -> _*_.fst;
π₂    = λ Z -> _*_.snd;
pair  = λ f g Z x → (f Z x , g Z x);
π₁β   = refl;
π₂β   = refl;
η     = refl;
!     = λ Z x → tt;
!η    = refl
}

After much fighting with implicit arguments, realizing I don't know
how to use modules properly, setting up some definitions instead, etc,
it managed to prove a nasty example:

test : ∀ {Γ Δ S T} {σ : HomY Δ Γ} {N : HomY Γ T} {M : HomY (Γ × T) S}
-> (M ∘ ([ id , N ] ∘ σ)) ≡ ((M ∘ [ σ ∘ π1 , π2 ]) ∘ [ id , (N ∘ σ) ])
test = refl

This example comes from the proof of the substitution lemma for object
languages with dependent types. Next goal is to see if I can harness
this...

Regards,
Andrew

On Thu, Oct 27, 2011 at 9:47 AM, James Chapman <james@...> 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}
>
>
> 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
>
> _______________________________________________
> Agda mailing list
> Agda@...
> https://lists.chalmers.se/mailman/listinfo/agda
>
```
27 Oct 2011 23:41

```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}
>
>
> 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
>
```
28 Oct 2011 17:26

```On 10/27/11 3:47 PM, James Chapman wrote:
> 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)

Is that the glorious Yoneda lemma?  Trivial in the language of types.
Just subtract the categorical waffle and every programmer understands it...

Cheers,
Andreas

--

--
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel@...
http://www2.tcs.ifi.lmu.de/~abel/
```
28 Oct 2011 19:55

```That's the Glorious Yoneda Lemma's action on homs, you are also expected
to prove a bunch of coherence properties. I suspect that if we assumed
parametricity of Agda, then many of the coherence properties would come
out in the wash.

I prefer categorical waffles to burned toast, which is often the
alternative.

A.

On 10/28/2011 10:26 AM, Andreas Abel wrote:
> On 10/27/11 3:47 PM, James Chapman wrote:
>> 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)
>
> Is that the glorious Yoneda lemma?  Trivial in the language of types.
> Just subtract the categorical waffle and every programmer understands it...
>
> Cheers,
> Andreas
>
```
28 Oct 2011 20:23

```Have a look at

http://www.cse.chalmers.se/~peterd/papers/nbe.html/Coherence_Monoidal.pdf

I think it is related.
Peter

________________________________________
From: agda-bounces@...
[agda-bounces@...] On Behalf Of Alan Jeffrey [ajeffrey@...]
Sent: Friday, October 28, 2011 7:55 PM
To: Andreas Abel
Cc: Agda mailing list

That's the Glorious Yoneda Lemma's action on homs, you are also expected
to prove a bunch of coherence properties. I suspect that if we assumed
parametricity of Agda, then many of the coherence properties would come
out in the wash.

I prefer categorical waffles to burned toast, which is often the
alternative.

A.

On 10/28/2011 10:26 AM, Andreas Abel wrote:
> On 10/27/11 3:47 PM, James Chapman wrote:
>> 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)
>
> Is that the glorious Yoneda lemma?  Trivial in the language of types.
> Just subtract the categorical waffle and every programmer understands it...
>
> Cheers,
> Andreas
>
_______________________________________________
Agda mailing list
Agda@...
https://lists.chalmers.se/mailman/listinfo/agda
```
28 Oct 2011 20:39

That link looks broken, but http://www.cse.chalmers.se/~peterd/papers/Coherence_Monoidal.pdf seemed to work :)

2011/10/28 Peter Dybjer
Have a look at

http://www.cse.chalmers.se/~peterd/papers/nbe.html/Coherence_Monoidal.pdf

I think it is related.
Peter

________________________________________
From: agda-bounces <at> lists.chalmers.se [agda-bounces-TrQ0NnR75azkdzWRgU60H7NAH6kLmebB@public.gmane.org] On Behalf Of Alan Jeffrey [ajeffrey-zWi12Q5vYqaakBO8gow8eQ@public.gmane.org]
Sent: Friday, October 28, 2011 7:55 PM
To: Andreas Abel
Cc: Agda mailing list

That's the Glorious Yoneda Lemma's action on homs, you are also expected
to prove a bunch of coherence properties. I suspect that if we assumed
parametricity of Agda, then many of the coherence properties would come
out in the wash.

I prefer categorical waffles to burned toast, which is often the
alternative.

A.

On 10/28/2011 10:26 AM, Andreas Abel wrote:
> On 10/27/11 3:47 PM, James Chapman wrote:
>> 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)
>
> Is that the glorious Yoneda lemma?  Trivial in the language of types.
> Just subtract the categorical waffle and every programmer understands it...
>
> Cheers,
> Andreas
>
_______________________________________________
Agda mailing list
Agda-TrQ0NnR75azkdzWRgU60H7NAH6kLmebB@public.gmane.org
https://lists.chalmers.se/mailman/listinfo/agda
_______________________________________________
Agda mailing list
Agda-TrQ0NnR75azkdzWRgU60H7NAH6kLmebB@public.gmane.org
https://lists.chalmers.se/mailman/listinfo/agda

```_______________________________________________
Agda mailing list
Agda@...
https://lists.chalmers.se/mailman/listinfo/agda
```
28 Oct 2011 20:49

```Oops, URL typo...

http://www.cse.chalmers.se/~peterd/papers/Coherence_Monoidal.pdf

I had a quick read through, and it is indeed related, but (I believe)
is, given any monoid (resp. monoidal category) M, building a strict
monoid (resp. strict monoidal category) N and a morphism (resp. monoidal
functor) J : M -> N such that (a ~ b in M) iff (J a = J b).

This is indeed related. The thing I think might be new is using
irrelevance as a way to build the subset of N such that J forms an
isomorphism.

A.

On 10/28/2011 01:23 PM, Peter Dybjer wrote:
> Have a look at
>
> http://www.cse.chalmers.se/~peterd/papers/nbe.html/Coherence_Monoidal.pdf
>
> I think it is related.
> Peter
>
> ________________________________________
> From: agda-bounces@...
[agda-bounces@...] On Behalf Of Alan Jeffrey [ajeffrey@...]
> Sent: Friday, October 28, 2011 7:55 PM
> To: Andreas Abel
> Cc: Agda mailing list
>
> That's the Glorious Yoneda Lemma's action on homs, you are also expected
> to prove a bunch of coherence properties. I suspect that if we assumed
> parametricity of Agda, then many of the coherence properties would come
> out in the wash.
>
> I prefer categorical waffles to burned toast, which is often the
> alternative.
>
> A.
>
> On 10/28/2011 10:26 AM, Andreas Abel wrote:
>> On 10/27/11 3:47 PM, James Chapman wrote:
>>> 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)
>>
>> Is that the glorious Yoneda lemma?  Trivial in the language of types.
>> Just subtract the categorical waffle and every programmer understands it...
>>
>> Cheers,
>> Andreas
>>
> _______________________________________________
> Agda mailing list
> Agda@...
> https://lists.chalmers.se/mailman/listinfo/agda
```
28 Oct 2011 21:40

```Hmm, thinking of which, this means that adding:

≡-relevant : ∀ {A} {a b : A} → .(a ≡ b) → (a ≡ b)

means that given f : A → B, we can define a subset of B isomorphic to
the image of f as:

record Image {A B : Set} (f : A → B) : Set where
b : B
.b✓ : ∃ (λ a → f a ≡ b)

The "assoiativity for free" construction for a monoid (_+_ : A → A → A)
is just (Image _+_).

A.

On 10/28/2011 01:49 PM, Jeffrey, Alan S A (Alan) wrote:
> Oops, URL typo...
>
>     http://www.cse.chalmers.se/~peterd/papers/Coherence_Monoidal.pdf
>
> I had a quick read through, and it is indeed related, but (I believe)
> is, given any monoid (resp. monoidal category) M, building a strict
> monoid (resp. strict monoidal category) N and a morphism (resp. monoidal
> functor) J : M ->  N such that (a ~ b in M) iff (J a = J b).
>
> This is indeed related. The thing I think might be new is using
> irrelevance as a way to build the subset of N such that J forms an
> isomorphism.
>
> A.
>
> On 10/28/2011 01:23 PM, Peter Dybjer wrote:
>> Have a look at
>>
>> http://www.cse.chalmers.se/~peterd/papers/nbe.html/Coherence_Monoidal.pdf
>>
>> I think it is related.
>> Peter
>>
>> ________________________________________
>> From: agda-bounces@...
[agda-bounces@...] On Behalf Of Alan Jeffrey [ajeffrey@...]
>> Sent: Friday, October 28, 2011 7:55 PM
>> To: Andreas Abel
>> Cc: Agda mailing list
>>
>> That's the Glorious Yoneda Lemma's action on homs, you are also expected
>> to prove a bunch of coherence properties. I suspect that if we assumed
>> parametricity of Agda, then many of the coherence properties would come
>> out in the wash.
>>
>> I prefer categorical waffles to burned toast, which is often the
>> alternative.
>>
>> A.
>>
>> On 10/28/2011 10:26 AM, Andreas Abel wrote:
>>> On 10/27/11 3:47 PM, James Chapman wrote:
>>>> 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)
>>>
>>> Is that the glorious Yoneda lemma?  Trivial in the language of types.
>>> Just subtract the categorical waffle and every programmer understands it...
>>>
>>> Cheers,
>>> Andreas
>>>
>> _______________________________________________
>> Agda mailing list
>> Agda@...
>> https://lists.chalmers.se/mailman/listinfo/agda
```
1 Nov 2011 13:57

```Dear Andreas,

surely, what James described is a part of (gateway to?) Yoneda lemma.

I think you are right in saying that it is trivial.  The whole body of
Yoneda lemma is trivial.  I recall Peter Freyd wrote something which
means that many theorems in category theory are trivial, but it is not
trivial to find a setting which makes those things trivial.  I am sure
Freyd's original wording was much better.  I once read it in some
mailing list, was impressed by it, talked about it with several
people, lost the article and have never found it again.  I miss it...

Yoshiki.
--
Yoshiki Kinoshita, D.Sc.
Principal Research Scientist
Information Technology Research Insititute
National Institute of Advanced Industrial Science and Technology (AIST)
3-11-46 Nakoji, Amagasaki-shi
Hyogo, 661-0974, Japan
Phone: 06-6494-8017  Fax:
E-mail: yoshiki <at> m.aist.go.jp

From: Andreas Abel <andreas.abel <at> ifi.lmu.de>
Date: Fri, 28 Oct 2011 17:26:54 +0200
Message-ID: <4EAAC9BE.9010208 <at> ifi.lmu.de>

andreas.abel> On 10/27/11 3:47 PM, James Chapman wrote:
andreas.abel> > Now, Yoneda's embedding says that we can view morphism in C as the following polymorphic function:
andreas.abel> >
andreas.abel> > Y : ∀{C A B} → Hom C A B → (∀ Z → Hom C B Z → Hom C A Z)
andreas.abel> > Y {C} f = λ Z g → comp C g f
andreas.abel> >
andreas.abel> > and we can convert back again:
andreas.abel> >
andreas.abel> > Y-1 : ∀{C A B} → (∀ Z → Hom C B Z → Hom C A Z) → Hom C A B
andreas.abel> > Y-1 {C}{A}{B} α = α B (iden C)
andreas.abel>
andreas.abel> Is that the glorious Yoneda lemma?  Trivial in the language of types.
andreas.abel> Just subtract the categorical waffle and every programmer understands it...
andreas.abel>
andreas.abel> Cheers,
andreas.abel> Andreas
andreas.abel>
andreas.abel> --
andreas.abel> Andreas Abel  <><      Du bist der geliebte Mensch.
andreas.abel>
andreas.abel> Theoretical Computer Science, University of Munich
andreas.abel> Oettingenstr. 67, D-80538 Munich, GERMANY
andreas.abel>
andreas.abel> andreas.abel <at> ifi.lmu.de
andreas.abel> http://www2.tcs.ifi.lmu.de/~abel/

andreas.abel> _______________________________________________
andreas.abel> Agda mailing list
andreas.abel> Agda <at> lists.chalmers.se
andreas.abel> https://lists.chalmers.se/mailman/listinfo/agda

andreas.abel>
```
```_______________________________________________
Agda mailing list
Agda@...
https://lists.chalmers.se/mailman/listinfo/agda
```
2 Nov 2011 18:48

```Dear Yoshiki,

my colleague Ulrich Schoepp always told me the Yoneda lemma was
"trivial", meaning "easy", but me being not so fluent in category theory
usually got lost trying to understand the statement.  However, I can

Cheers,
Andreas

On 11/1/11 1:57 PM, KINOSHITA Yoshiki wrote:
> Dear Andreas,
>
> surely, what James described is a part of (gateway to?) Yoneda lemma.
>
> I think you are right in saying that it is trivial.  The whole body of
> Yoneda lemma is trivial.  I recall Peter Freyd wrote something which
> means that many theorems in category theory are trivial, but it is not
> trivial to find a setting which makes those things trivial.  I am sure
> Freyd's original wording was much better.  I once read it in some
> mailing list, was impressed by it, talked about it with several
> people, lost the article and have never found it again.  I miss it...
>
> Yoshiki.
> --
> Yoshiki Kinoshita, D.Sc.
> Principal Research Scientist
> Information Technology Research Insititute
> National Institute of Advanced Industrial Science and Technology (AIST)
> 3-11-46 Nakoji, Amagasaki-shi
> Hyogo, 661-0974, Japan
> Phone: 06-6494-8017  Fax:
> E-mail: yoshiki <at> m.aist.go.jp
>
>
> From: Andreas Abel<andreas.abel@...>
> Date: Fri, 28 Oct 2011 17:26:54 +0200
> Message-ID:<4EAAC9BE.9010208@...>
>
> andreas.abel>  On 10/27/11 3:47 PM, James Chapman wrote:
> andreas.abel>  >  Now, Yoneda's embedding says that we can view morphism in C as the following polymorphic function:
> andreas.abel>  >
> andreas.abel>  >  Y : ∀{C A B} → Hom C A B → (∀ Z → Hom C B Z → Hom C A Z)
> andreas.abel>  >  Y {C} f = λ Z g → comp C g f
> andreas.abel>  >
> andreas.abel>  >  and we can convert back again:
> andreas.abel>  >
> andreas.abel>  >  Y-1 : ∀{C A B} → (∀ Z → Hom C B Z → Hom C A Z) → Hom C A B
> andreas.abel>  >  Y-1 {C}{A}{B} α = α B (iden C)
> andreas.abel>
> andreas.abel>  Is that the glorious Yoneda lemma?  Trivial in the language of types.
> andreas.abel>  Just subtract the categorical waffle and every programmer understands it...
> andreas.abel>
> andreas.abel>  Cheers,
> andreas.abel>  Andreas
> andreas.abel>
> andreas.abel>  --
> andreas.abel>  Andreas Abel<><       Du bist der geliebte Mensch.
> andreas.abel>
> andreas.abel>  Theoretical Computer Science, University of Munich
> andreas.abel>  Oettingenstr. 67, D-80538 Munich, GERMANY
> andreas.abel>
> andreas.abel>  andreas.abel@...
> andreas.abel>  http://www2.tcs.ifi.lmu.de/~abel/
> andreas.abel>  _______________________________________________
> andreas.abel>  Agda mailing list
> andreas.abel>  Agda@...
> andreas.abel>  https://lists.chalmers.se/mailman/listinfo/agda
> andreas.abel>

--

--
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel@...
http://www2.tcs.ifi.lmu.de/~abel/
```
2 Nov 2011 21:12

```
> my colleague Ulrich Schoepp always told me the Yoneda lemma was
> "trivial", meaning "easy", but me being not so fluent in category
> theory usually got lost trying to understand the statement. However,
> I can read type signatures...

My supervisor, Robin Gandy, an old-school logician, once said to me
(approximately...): "I've stared at it several times.  Sometimes I feel it is
completely trivial; and at other times I feel it is totally mysterious."

I have to admit I often feel the same about things in category theory.

By the way, for the record, the Yoneda lemma says that the natural transformations
from the functor Hom[A,_] for A : C to some random functor F : C -> Set have
the same cardinal as F(A).  Maybe Andreas can translate that into a type signature?

Hank
```
3 Nov 2011 02:25

```Dear Anderas,

andreas.abel> my colleague Ulrich Schoepp always told me the Yoneda
andreas.abel> lemma was "trivial", meaning "easy", but me being not so
andreas.abel> fluent in category theory usually got lost trying to
andreas.abel> understand the statement.  However, I can read type
andreas.abel> signatures...

You might be interested in looking at the Agda code for the proof of
Yoneda lemma which I posted after the last AIM.  It is in "Libraries
and other developments" page of Agda wiki.  I have already started to
forget what are in it, but I just checked not only the proposition
attributed to Yoneda in MacLane's book but also the definition of
Yoneda embedding is there.

Yoshiki.
```
3 Nov 2011 10:39

```On 28 Oct 2011, at 16:26, Andreas Abel wrote:

> On 10/27/11 3:47 PM, James Chapman wrote:
>> 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)
>
> Is that the glorious Yoneda lemma?  Trivial in the language of types. Just subtract the categorical waffle
and every programmer understands it...

Indeed, I have been pushing this for a while. Actually given F : Set -> Set a functor, Yoneda just says for any A
: Set:

((X : Set) -> (A -> X) -> F X) ~ F A

where ~ is isomorphism (or equality f we accept univalence). And yes this is a consequence of parametricity
or more precisely of the assumption that (X : Set) -> H X X is a coend (where H : Set^op -> Set -> Set is a bifunctor).

One interesting aspect of this equation is that the left hand side is actually large (in Set_1) while the
right hand side is small. So it is a "resizing axiom" which enables to make big things small.

There are many nice applications of the Yoneda lemma. One of my favourites is the derivation of the
exponential of endofunctors (i.e. the function space in Set -> Set) which is actually a categorical
generalisation of Kripke semantics.

Given F,G : Set -> Set (functors) and exponential F=>G if it exists must satisfy

((X : Set) -> (H x F) X -> G X) ~ ((X : Set) -> H X -> (F => G) X)		(1)

and it is easy to see that (H x F) X = H X x F X (products are constructed pointwise).

Hence we can calculate

(F => G) A
~ (X : Set) (A -> X) -> (F => G) X		(Yoneda)
~ (X : Set) (A -> X) x F X -> G X			(1)
~ (X : Set) (A -> X) -> F X -> G X		(currying)

The relation to Kripke semantics becomes clear if we read (A -> X) as X is a future of A. Actually we should
really use the contravariant version then we can read -> as implication.

It is a generalisation because it is an isomorphism as opposed to a logical equivalence.

So, yes, functional programmers should be aware of the Yoneda lemma. Ralph Hinze recently wrote a nice
paper expressing the same sentiment (after I showed him the little proof above).

Obviously, Yoneda is much more general than what I wrote above. As indicated it also works for covariant
functors and there also is a version with SIgma types instead of Pi types.

Cheers,
Thorsten

>
> Cheers,
> Andreas
>
> --
> Andreas Abel  <><      Du bist der geliebte Mensch.
>
> Theoretical Computer Science, University of Munich
> Oettingenstr. 67, D-80538 Munich, GERMANY
>
> andreas.abel@...
> http://www2.tcs.ifi.lmu.de/~abel/
> _______________________________________________
> Agda mailing list
> Agda@...
> https://lists.chalmers.se/mailman/listinfo/agda
```
3 Nov 2011 11:50

```P.S. Just remembered that I forgot one thing:

On 3 Nov 2011, at 09:39, Thorsten Altenkirch wrote:

> On 28 Oct 2011, at 16:26, Andreas Abel wrote:
>
>> On 10/27/11 3:47 PM, James Chapman wrote:
>>> 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)
>>
>> Is that the glorious Yoneda lemma?  Trivial in the language of types. Just subtract the categorical
waffle and every programmer understands it...
>
> Indeed, I have been pushing this for a while. Actually given F : Set -> Set a functor, Yoneda just says for any
A : Set:
>
> ((X : Set) -> (A -> X) -> F X) ~ F A
>
> where ~ is isomorphism (or equality f we accept univalence). And yes this is a consequence of
parametricity or more precisely of the assumption that (X : Set) -> H X X is a coend (where H : Set^op -> Set ->
Set is a bifunctor).
>
> One interesting aspect of this equation is that the left hand side is actually large (in Set_1) while the
right hand side is small. So it is a "resizing axiom" which enables to make big things small.
>
> There are many nice applications of the Yoneda lemma. One of my favourites is the derivation of the
exponential of endofunctors (i.e. the function space in Set -> Set) which is actually a categorical
generalisation of Kripke semantics.
>
> Given F,G : Set -> Set (functors) and exponential F=>G if it exists must satisfy
>
> 	((X : Set) -> (H x F) X -> G X) ~ ((X : Set) -> H X -> (F => G) X)		(1)
>
> and it is easy to see that (H x F) X = H X x F X (products are constructed pointwise).
>
> Hence we can calculate
>
> 	(F => G) A
> 	~ (X : Set) (A -> X) -> (F => G) X		(Yoneda)
> 	~ (X : Set) (A -> X) x F X -> G X			(1)
> 	~ (X : Set) (A -> X) -> F X -> G X		(currying)
>
> The relation to Kripke semantics becomes clear if we read (A -> X) as X is a future of A. Actually we should
really use the contravariant version then we can read -> as implication.

Don't forget that I said *if* it exists the exponential looks like this. However, we have no reason to assume
that in general
(X : Set) (A -> X) -> F X -> G X : Set. It is the case if we assume that F and G are containers (see our CIE paper from
last year).

>
> It is a generalisation because it is an isomorphism as opposed to a logical equivalence.
>
> So, yes, functional programmers should be aware of the Yoneda lemma. Ralph Hinze recently wrote a nice
paper expressing the same sentiment (after I showed him the little proof above).
>
> Obviously, Yoneda is much more general than what I wrote above. As indicated it also works for covariant
functors and there also is a version with SIgma types instead of Pi types.
>
> Cheers,
> Thorsten
>
>
>
>
>>
>> Cheers,
>> Andreas
>>
>> --
>> Andreas Abel  <><      Du bist der geliebte Mensch.
>>
>> Theoretical Computer Science, University of Munich
>> Oettingenstr. 67, D-80538 Munich, GERMANY
>>
>> andreas.abel@...
>> http://www2.tcs.ifi.lmu.de/~abel/
>> _______________________________________________
>> Agda mailing list
>> Agda@...
>> https://lists.chalmers.se/mailman/listinfo/agda
>
> _______________________________________________
> Agda mailing list
> Agda@...
> https://lists.chalmers.se/mailman/listinfo/agda
```
26 Oct 2011 23:34

```> 2. [...] Another solution I learnt from Conor [...]
>
> data _≤_ {X : Set} : List X → List X → Set where
>  done : [] ≤ []
>  keep : ∀{x}{xs xs'} → xs ≤ xs' → (x :: xs) ≤ (x :: xs')
>  skip : ∀{x}{xs xs'} → xs ≤ xs' → xs ≤ (x :: xs')

I think you will find this approach for weakening (of PTS typing) used
already in Geuvers and Nederhof, JAR 1991 (widely circulated by 1989).
Following Geuvers and Nederhof, this approach is used in many papers
that mentions weakening of a type system or a logic since that time
(e.g. McKinna/Pollack, Pitts, Urban, ...).

Best,
Randy
---
On Wed, Oct 26, 2011 at 5:01 PM, James Chapman <james@...> wrote:
> Hi Alan,
>
> I too have encountered this problem, rather than tackling it head on here are two ways of tiptoeing around it.
>
> 1. A trivial solution for your example is simply to make _++_ associate to the left:
>
> data List (X : Set) : Set where
>  []   : List X
>  _::_ : X → List X → List X
>
> _++_ : ∀{X} → List X → List X → List X
> []        ++ xs' = xs'
> (x :: xs) ++ xs' = x :: (xs ++ xs')
>
> infixl 5 _++_
>
> postulate P : ∀{X} → List X → Set
>
> postulate weakening : ∀ {A} (as bs cs : List A) →
>                      P (as ++ cs) → P (as ++ bs ++ cs)
>
> weaken2 : ∀ {A} (as bs cs ds : List A) →
>   P (as ++ bs ++ ds) → P (as ++ bs ++ cs ++ ds)
> weaken2 as bs cs ds p = weakening (as ++ bs) cs ds p
>
> This may sound silly and perhaps you might somewhere else need append to associate to the right. Nisse told
me that in a recent implementation of a dependently typed lambda calculus he defined both versions and
didn't end up needing them both at the same time. Do you need both at the same time?
>
> 2. I guess you run into the this problem where ++ is an operation on contexts right? Another solution I
learnt from Conor (exercise 15, his AFP notes
http://www.strictlypositive.org/epigram-notes.ps.gz) is simply to avoid it. Instead of giving
weakening this type, give a first order presentation of weakenings (functions from a context to the same
context with more stuff chucked in arbitrary places). For  lists this function space would be the
following inductively defined sublist relation:
>
> data _≤_ {X : Set} : List X → List X → Set where
>  done : [] ≤ []
>  keep : ∀{x}{xs xs'} → xs ≤ xs' → (x :: xs) ≤ (x :: xs')
>  skip : ∀{x}{xs xs'} → xs ≤ xs' → xs ≤ (x :: xs')
>
> Then, weakening would be something like:
>
> weakening : ∀{X}{xs xs' : List X} → P xs → xs ≤ xs' → P xs'
>
> By doing this ++ never appears in the types, so we don't have to use subst. I used this technique (called
order preserving embeddings) in chapter 4 of my thesis
(http://www.cs.ioc.ee/~james/papers/thesis.pdf ) and it was much more pleasant than using ++ as we did
in our Big-step normalization paper (http://www.cs.ioc.ee/~james/papers/tait2.pdf) on which this
chapter was based.
>
> Best wishes,
>
> James
>
>
> _______________________________________________
> Agda mailing list
> Agda@...
> https://lists.chalmers.se/mailman/listinfo/agda
>
>
```
26 Oct 2011 23:45

```Thanks for the references Randy.

I also forgot to say before…

Alan: neat trick!

Best,

James

On Oct 27, 2011, at 12:34 AM, Randy Pollack wrote:

>> 2. [...] Another solution I learnt from Conor [...]
>>
>> data _≤_ {X : Set} : List X → List X → Set where
>> done : [] ≤ []
>> keep : ∀{x}{xs xs'} → xs ≤ xs' → (x :: xs) ≤ (x :: xs')
>> skip : ∀{x}{xs xs'} → xs ≤ xs' → xs ≤ (x :: xs')
>
> I think you will find this approach for weakening (of PTS typing) used
> already in Geuvers and Nederhof, JAR 1991 (widely circulated by 1989).
> Following Geuvers and Nederhof, this approach is used in many papers
> that mentions weakening of a type system or a logic since that time
> (e.g. McKinna/Pollack, Pitts, Urban, ...).
>
> Best,
> Randy
> ---
> On Wed, Oct 26, 2011 at 5:01 PM, James Chapman <james@...> wrote:
>> Hi Alan,
>>
>> I too have encountered this problem, rather than tackling it head on here are two ways of tiptoeing around it.
>>
>> 1. A trivial solution for your example is simply to make _++_ associate to the left:
>>
>> data List (X : Set) : Set where
>>  []   : List X
>>  _::_ : X → List X → List X
>>
>> _++_ : ∀{X} → List X → List X → List X
>> []        ++ xs' = xs'
>> (x :: xs) ++ xs' = x :: (xs ++ xs')
>>
>> infixl 5 _++_
>>
>> postulate P : ∀{X} → List X → Set
>>
>> postulate weakening : ∀ {A} (as bs cs : List A) →
>>                      P (as ++ cs) → P (as ++ bs ++ cs)
>>
>> weaken2 : ∀ {A} (as bs cs ds : List A) →
>>   P (as ++ bs ++ ds) → P (as ++ bs ++ cs ++ ds)
>> weaken2 as bs cs ds p = weakening (as ++ bs) cs ds p
>>
>> This may sound silly and perhaps you might somewhere else need append to associate to the right. Nisse
told me that in a recent implementation of a dependently typed lambda calculus he defined both versions
and didn't end up needing them both at the same time. Do you need both at the same time?
>>
>> 2. I guess you run into the this problem where ++ is an operation on contexts right? Another solution I
learnt from Conor (exercise 15, his AFP notes
http://www.strictlypositive.org/epigram-notes.ps.gz) is simply to avoid it. Instead of giving
weakening this type, give a first order presentation of weakenings (functions from a context to the same
context with more stuff chucked in arbitrary places). For  lists this function space would be the
following inductively defined sublist relation:
>>
>> data _≤_ {X : Set} : List X → List X → Set where
>>  done : [] ≤ []
>>  keep : ∀{x}{xs xs'} → xs ≤ xs' → (x :: xs) ≤ (x :: xs')
>>  skip : ∀{x}{xs xs'} → xs ≤ xs' → xs ≤ (x :: xs')
>>
>> Then, weakening would be something like:
>>
>> weakening : ∀{X}{xs xs' : List X} → P xs → xs ≤ xs' → P xs'
>>
>> By doing this ++ never appears in the types, so we don't have to use subst. I used this technique (called
order preserving embeddings) in chapter 4 of my thesis
(http://www.cs.ioc.ee/~james/papers/thesis.pdf ) and it was much more pleasant than using ++ as we did
in our Big-step normalization paper (http://www.cs.ioc.ee/~james/papers/tait2.pdf) on which this
chapter was based.
>>
>> Best wishes,
>>
>> James
>>
>>
>> _______________________________________________
>> Agda mailing list
>> Agda@...
>> https://lists.chalmers.se/mailman/listinfo/agda
>>
>>
```
4 Nov 2011 11:28

```On 2011-10-26 23:01, James Chapman wrote:
> This may sound silly and perhaps you might somewhere else need append
> to associate to the right. Nisse told me that in a recent
> implementation of a dependently typed lambda calculus he defined both
> versions and didn't end up needing them both at the same time.

Contexts:

data Ctxt : Set where
ε   : Ctxt
_▻_ : (Γ : Ctxt) (σ : Type Γ) → Ctxt

Cons-based context extensions:

data Ctxt₊ (Γ : Ctxt) : Set where
ε   : Ctxt₊ Γ
_◅_ : (σ : Type Γ) (Γ₊ : Ctxt₊ (Γ ▻ σ)) → Ctxt₊ Γ

Snoc-based context extensions:

data Ctxt⁺ (Γ : Ctxt) : Set where
ε   : Ctxt⁺ Γ
_▻_ : (Γ⁺ : Ctxt⁺ Γ) (σ : Type (Γ ++⁺ Γ⁺)) → Ctxt⁺ Γ

The cons-based extensions are convenient if you want to define something
like weakening for a Kripke model, because

(Γ ▻ σ) ++₊ Γ₊

is by definition equal to

Γ ++₊ (σ ◅ Γ₊).

On the other hand, the snoc-based extensions are convenient if you want
to go under many lambdas, because

(Γ ++⁺ Γ⁺) ▻ σ

is by definition equal to

Γ ++⁺ (Γ⁺ ▻ σ).

For more details (work in progress):

--

--
```
26 Oct 2011 23:28

```On Wed, Oct 26, 2011 at 4:48 PM, Alan Jeffrey <ajeffrey@...> wrote:
> Hi everyone,
>
> A quick note about a trick for representing lists (or any other monoid) up
> to associativity. Am I reinventing a wheel here?

Well done, nice trick!

I've just tried on natural numbers using difference nats, then vectors based
on these nats and finally associativity of ++ goes well.

module diffnat-assoc where

open import Data.Nat
open import Function
open import Relation.Binary.PropositionalEquality

record D : Set where
constructor mk
field
n    : ℕ
f     : ℕ → ℕ
.f✓ : f ≡ _+_ n

_ᴰ : ℕ → D
n ᴰ = mk n (_+_ n) refl

_+ᴰ_ : D → D → D
mk m f f✓ +ᴰ mk n g g✓ = mk (f n) (f ∘ g) (f∘g✓ f f✓ g g✓)
where
assoc : ∀ m {n} → (λ x → m + (n + x)) ≡ _+_ (m + n)
assoc zero    = refl
assoc (suc m) = cong (_∘_ suc) (assoc m)

.f∘g✓ : ∀ f (f✓ : f ≡ _+_ m) g (g✓ : g ≡ _+_ n) → f ∘ g ≡ _+_ (f n)
f∘g✓ ._ refl ._ refl = assoc m

0ᴰ : D
0ᴰ = 0 ᴰ

1ᴰ : D
1ᴰ = 1 ᴰ

sucᴰ : D → D
sucᴰ = _+ᴰ_ 1ᴰ

free-assoc : ∀ {m n o} → m +ᴰ (n +ᴰ o) ≡ (m +ᴰ n) +ᴰ o
free-assoc = refl

data Vec (A : Set) : D → Set where
[] : Vec A 0ᴰ
_∷_ : ∀ {n} (x : A) (xs : Vec A n) → Vec A (sucᴰ n)

_++_ : ∀ {A m n} → Vec A m → Vec A n → Vec A (m +ᴰ n)
[]       ++ ys = ys
(x ∷ xs) ++ ys = x ∷ (xs ++ ys)

free-Vec-assoc : ∀ {A m n o} → Vec A ((m +ᴰ n) +ᴰ o) ≡ Vec A (m +ᴰ (n +ᴰ o))
free-Vec-assoc = refl

-- With usual vectors one can't even state this
-- lemma using homogeneous equality.
++-assoc : ∀ {A m n o} (xs : Vec A m) (ys : Vec A n) (zs : Vec A o) →
(xs ++ ys) ++ zs ≡ xs ++ (ys ++ zs)
++-assoc []       ys zs = refl
++-assoc (x ∷ xs) ys zs = cong (_∷_ x) (++-assoc xs ys zs)

--

--
Nicolas Pouillard
http://nicolaspouillard.fr
```
27 Oct 2011 02:58

```Cool! For your next trick, difference vectors over difference naturals,

A.

On 10/26/2011 04:28 PM, Nicolas Pouillard wrote:
> On Wed, Oct 26, 2011 at 4:48 PM, Alan Jeffrey<ajeffrey@...>  wrote:
>> Hi everyone,
>>
>> A quick note about a trick for representing lists (or any other monoid) up
>> to associativity. Am I reinventing a wheel here?
>
> Well done, nice trick!
>
> I've just tried on natural numbers using difference nats, then vectors based
> on these nats and finally associativity of ++ goes well.
>
> module diffnat-assoc where
>
> open import Data.Nat
> open import Function
> open import Relation.Binary.PropositionalEquality
>
> record D : Set where
>    constructor mk
>    field
>      n    : ℕ
>      f     : ℕ → ℕ
>      .f✓ : f ≡ _+_ n
>
> _ᴰ : ℕ → D
> n ᴰ = mk n (_+_ n) refl
>
> _+ᴰ_ : D → D → D
> mk m f f✓ +ᴰ mk n g g✓ = mk (f n) (f ∘ g) (f∘g✓ f f✓ g g✓)
>   where
>    assoc : ∀ m {n} → (λ x → m + (n + x)) ≡ _+_ (m + n)
>    assoc zero    = refl
>    assoc (suc m) = cong (_∘_ suc) (assoc m)
>
>    .f∘g✓ : ∀ f (f✓ : f ≡ _+_ m) g (g✓ : g ≡ _+_ n) → f ∘ g ≡ _+_ (f n)
>    f∘g✓ ._ refl ._ refl = assoc m
>
> 0ᴰ : D
> 0ᴰ = 0 ᴰ
>
> 1ᴰ : D
> 1ᴰ = 1 ᴰ
>
> sucᴰ : D → D
> sucᴰ = _+ᴰ_ 1ᴰ
>
> free-assoc : ∀ {m n o} → m +ᴰ (n +ᴰ o) ≡ (m +ᴰ n) +ᴰ o
> free-assoc = refl
>
> data Vec (A : Set) : D → Set where
>    [] : Vec A 0ᴰ
>    _∷_ : ∀ {n} (x : A) (xs : Vec A n) → Vec A (sucᴰ n)
>
> _++_ : ∀ {A m n} → Vec A m → Vec A n → Vec A (m +ᴰ n)
> []       ++ ys = ys
> (x ∷ xs) ++ ys = x ∷ (xs ++ ys)
>
> free-Vec-assoc : ∀ {A m n o} → Vec A ((m +ᴰ n) +ᴰ o) ≡ Vec A (m +ᴰ (n +ᴰ o))
> free-Vec-assoc = refl
>
> -- With usual vectors one can't even state this
> -- lemma using homogeneous equality.
> ++-assoc : ∀ {A m n o} (xs : Vec A m) (ys : Vec A n) (zs : Vec A o) →
>               (xs ++ ys) ++ zs ≡ xs ++ (ys ++ zs)
> ++-assoc []       ys zs = refl
> ++-assoc (x ∷ xs) ys zs = cong (_∷_ x) (++-assoc xs ys zs)
>
>
```
2 Nov 2011 17:26

```Hi everyone,

lambda-calculi. I've now worked through some of the details, and here is
the syntax of the simply-typed lambda-calculus:

> https://github.com/agda/agda-frp-js/blob/master/src/agda/FRP/JS/Model/STLambdaC/Exp.agda

The interesting thing is weakening, with type:

weaken+ : ∀ B Γ Δ {T} → Exp (B ++ Δ) T → Exp (B ++ Γ ++ Δ) T

and (news just in!) weakening commutes with itself (up to propositional
equality):

weaken+ Φ Ψ (B ++ Γ ++ Δ) (weaken+ (Φ ++ B) Γ Δ M)
≡ weaken+ (Φ ++ Ψ ++ B) Γ Δ (weaken+ Φ Ψ (B ++ Δ) M)

Note that you can't even state this property without associativity on
the nose, since the lhs has type (Φ ++ Ψ ++ (B ++ Γ ++ Δ)) and the rhs
has type ((Φ ++ Ψ ++ B) ++ Γ ++ Δ).

The proof makes use of a list-membership type, defined in:

> https://github.com/agda/agda-frp-js/blob/master/src/agda/FRP/JS/DList.agda

It satisfies weakening on the left and right:

_≪_ : ∀ {A a as} → (a ∈ as) → ∀ bs → (a ∈ (as ++ bs))
_≫_ : ∀ {A a bs} → ∀ as → (a ∈ bs) → (a ∈ (as ++ bs))

and moreover has left and right units and associativity properties, all
up to beta-equivalence (that is, all these properties have proof refl):

(a∈as ≪ []) ≡ a∈as
([] ≫ a∈as) ≡ a∈as
(a∈as ≪ bs ≪ cs) ≡ (a∈as ≪ bs ++ cs)
((as ≫ a∈bs) ≪ cs) ≡ (as ≫ (a∈bs ≪ cs))
(as ≫ bs ≫ a∈cs) ≡ (as ≫ bs ≫ a∈cs)

Under the hood, this is implemented in terms of difference naturals
(that is an implementation of ℕ where + and ♯0 form a monoid up to
beta-equivalence), and an implementation of difference lists such that
the length function is a monoid homomorphism up to beta-equivalence:

(len (as ++ bs) ≡ (len as + len bs))
(len [] ≡ ♯0)

With all that in place, the proof of weakening is pretty
straightforward. The only case which requires any work is variables, and
a typical case is:

begin
xweaken+ Φ Ψ (B ++ Γ ++ Δ) (case Φ (B ++ Γ ++ Δ) (Φ ≫ x ≪ Γ ≪ Δ))
≡⟨ cong (xweaken+ Φ Ψ (B ++ Γ ++ Δ)) (case-≫ Φ (x ≪ Γ ≪ Δ)) ⟩
(Φ ≫ Ψ ≫ x ≪ Γ ≪ Δ)
≡⟨ cong (xweaken+ (Φ ++ Ψ ++ B) Γ Δ) (sym (case-≪ (Φ ≫ Ψ ≫ x) Δ)) ⟩
xweaken+ (Φ ++ Ψ ++ B) Γ Δ (case (Φ ++ Ψ ++ B) Δ (Φ ≫ Ψ ≫ x ≪ Δ))
∎

I don't really want to think about what this proof would look like with
all the associativity wiring made explicit.

There is still a bit of annoying associativity left, because I can't see
how to get coproducts to associate on the nose, so there's lots of gore
needed to define a case function:

data Case {A} a (as bs : List A) : Set where
inj₁ : (a∈as : a ∈ as) → Case a as bs
inj₂ : (a∈bs : a ∈ bs) → Case a as bs

case : ∀ {A a} as bs → (a ∈ (as ++ bs)) → Case {A} a as bs

and then prove that it satisfies associativity (up to propositional
equality, not beta-equivalence).

A.

On 10/26/2011 09:48 AM, Jeffrey, Alan S A (Alan) wrote:
> Hi everyone,
>
> A quick note about a trick for representing lists (or any other monoid)
> up to associativity. Am I reinventing a wheel here?
>
> I've been doing some mucking around recently with proofs about
> lambda-calculi and was hitting annoying problems with associativity
> on lists. A prototypical example is:
>
>     weakening : ∀ {A a} (as bs cs : List A) →
>      (a ∈ (as ++ cs)) → (a ∈ (as ++ bs ++ cs))
>
> It's easy to prove that ++ is associative, but making use of that fact
> is rather painful, as there's lots of manual wiring with subst and cong,
> for example:
>
>     weaken2 : ∀ {A a} (as bs cs ds : List A) →
>       (a ∈ (as ++ bs ++ ds)) → (a ∈ (as ++ bs ++ cs ++ ds))
>     weaken2 {A} {a} as bs cs ds a∈es =
>       subst (λ X → (a ∈ X)) (++-assoc as bs (cs ++ ds))
>         (weakening (as ++ bs) cs ds
>           (subst (λ X → (a ∈ X)) (sym (++-assoc as bs ds)) a∈es))
>
> This gets tiresome pretty rapidly. Oh if only there were a data
> structure which represented lists, but for which ++ was associative up
> to beta reduction... Oh look there already is one, it's called
> difference lists. Quoting the standard library:
>
>     DiffList : Set → Set
>     DiffList a = List a → List a
>
>     _++_ : ∀ {a} → DiffList a → DiffList a → DiffList a
>     xs ++ ys = λ k → xs (ys k)
>
> Unfortunately, difference lists are not isomorphic to lists: there's a
> lot more functions on lists than just concatenation functions. This
> causes headaches (e.g. writing inductive functions on difference lists).
>
> A first shot at fixing this is to write a data structure for those
> difference lists which are concatenations:
>
>     record Seq (A : Set) : Set where
>       constructor seq
>       field
>         list : List A
>         fun : List A → List A
>         ok : fun ≡ _++_ list  -- Broken
>
> It's pretty straightforward to define the monoidal structure for Seq:
>
>     ε : ∀ {A} → Seq A
>     ε = seq [] id refl
>
>      _+_ : ∀ {A} → Seq A → Seq A → Seq A
>     (seq as f f✓) + (seq bs g g✓) = seq (f bs) (f ∘ g) (...easy lemma...)
>
> Unfortunately, we're back to square one again, because + is only
> associative up to propositional equality, not beta reduction. This time,
> it's the ok field that gets in the way. So we can fix that, and just
> make the ok field irrelevant, that is:
>
>     record Seq (A : Set) : Set where
>       constructor seq
>       field
>         list : List A
>         fun : List A → List A
>         .ok : fun ≡ _++_ list  -- Fixed
>
>     open Seq public renaming (list to [_])
>
> Hooray, + is now associative up to beta reduction:
>
>     +-assoc : ∀ {A} (as bs cs : Seq A) →
>       ((as + bs) + cs) ≡ (as + (bs + cs))
>     +-assoc as bs cs = refl
>
>
>     ≡-relevant : ∀ {A : Set} {a b : A} → .(a ≡ b) → (a ≡ b)
>
> we can define:
>
>     data Case {A : Set} : Seq A → Set where
>       [] : Case ε
>       _∷_ : ∀ a as → Case (a ◁ as)
>
>     case : ∀ {A} (as : Seq A) → Case as
>
> and this gives us recursive functions over Seq (which somewhat to my
> surprise actually get past the termination checker), for example:
>
>     ids : ∀ {A} → Seq A → Seq A
>     ids as        with case as
>     ids .(a ◁ as) | a ∷ as = a ◁ ids as
>     ids .ε        | []     = ε
>
> For example, we can now define weakening:
>
>     weakening : ∀ {A a} (as bs cs : Seq A) →
>       (a ∈ [ as + cs ]) → (a ∈ [ as + bs + cs ])
>
> and use it up to associativity without worrying hand-coded wiring:
>
>     weaken2 : ∀ {A a} (as bs cs ds : Seq A) →
>       (a ∈ [ as + bs + ds ]) → (a ∈ [ as + bs + cs + ds ])
>     weaken2 as bs = weakening (as + bs)
>
> Hooray, cake! Eating it!
>
> I suspect this trick works for most any monoid, so you can do
> associativity on naturals, vectors, partial orders with join, etc. etc.
>
> The idea of using difference lists to represent lists is standard, but
> as far as I know, this use of irrelevant equalities to get structural
> recursion is new. Anyone know of any prior art?
>
> A.
```
2 Nov 2011 18:46

```Hi Alan,

you might be interested in a trick how to fuse weakening and
substitution into a single operation.  I have done this for
non-wellscoped de Bruijn terms in Agda:

http://www2.tcs.ifi.lmu.de/~abel/ParallelSubstitution.agda

but Thorsten and Conor deserve the credit for it (pointers in the .agda
file).

Looking at your code I wonder whether substitution (substn+) could not
be a bit less general, since N remains in the same context always.
Usually I prove the substitution lemma like this:

Gamma, x : T, Delta |- M : U
Gamma               |- N : T
----------------------------
Gamma, Delta   |- M[N/x] : U

Your statement has a more general context form for N, but I wonder
whether this is necessary.

Cheers,
Andreas

On 11/2/11 5:26 PM, Alan Jeffrey wrote:
> Hi everyone,
>
> lambda-calculi. I've now worked through some of the details, and here is
> the syntax of the simply-typed lambda-calculus:
>
>> https://github.com/agda/agda-frp-js/blob/master/src/agda/FRP/JS/Model/STLambdaC/Exp.agda
>>
>
> The interesting thing is weakening, with type:
>
> weaken+ : ∀ B Γ Δ {T} → Exp (B ++ Δ) T → Exp (B ++ Γ ++ Δ) T
>
> and (news just in!) weakening commutes with itself (up to propositional
> equality):
>
> weaken+ Φ Ψ (B ++ Γ ++ Δ) (weaken+ (Φ ++ B) Γ Δ M)
> ≡ weaken+ (Φ ++ Ψ ++ B) Γ Δ (weaken+ Φ Ψ (B ++ Δ) M)
>
> Note that you can't even state this property without associativity on
> the nose, since the lhs has type (Φ ++ Ψ ++ (B ++ Γ ++ Δ)) and the rhs
> has type ((Φ ++ Ψ ++ B) ++ Γ ++ Δ).
>
> The proof makes use of a list-membership type, defined in:
>
>> https://github.com/agda/agda-frp-js/blob/master/src/agda/FRP/JS/DList.agda
>>
>
> It satisfies weakening on the left and right:
>
> _≪_ : ∀ {A a as} → (a ∈ as) → ∀ bs → (a ∈ (as ++ bs))
> _≫_ : ∀ {A a bs} → ∀ as → (a ∈ bs) → (a ∈ (as ++ bs))
>
> and moreover has left and right units and associativity properties, all
> up to beta-equivalence (that is, all these properties have proof refl):
>
> (a∈as ≪ []) ≡ a∈as
> ([] ≫ a∈as) ≡ a∈as
> (a∈as ≪ bs ≪ cs) ≡ (a∈as ≪ bs ++ cs)
> ((as ≫ a∈bs) ≪ cs) ≡ (as ≫ (a∈bs ≪ cs))
> (as ≫ bs ≫ a∈cs) ≡ (as ≫ bs ≫ a∈cs)
>
> Under the hood, this is implemented in terms of difference naturals
> (that is an implementation of ℕ where + and ♯0 form a monoid up to
> beta-equivalence), and an implementation of difference lists such that
> the length function is a monoid homomorphism up to beta-equivalence:
>
> (len (as ++ bs) ≡ (len as + len bs))
> (len [] ≡ ♯0)
>
> With all that in place, the proof of weakening is pretty
> straightforward. The only case which requires any work is variables, and
> a typical case is:
>
> begin
> xweaken+ Φ Ψ (B ++ Γ ++ Δ) (case Φ (B ++ Γ ++ Δ) (Φ ≫ x ≪ Γ ≪ Δ))
> ≡⟨ cong (xweaken+ Φ Ψ (B ++ Γ ++ Δ)) (case-≫ Φ (x ≪ Γ ≪ Δ)) ⟩
> (Φ ≫ Ψ ≫ x ≪ Γ ≪ Δ)
> ≡⟨ cong (xweaken+ (Φ ++ Ψ ++ B) Γ Δ) (sym (case-≪ (Φ ≫ Ψ ≫ x) Δ)) ⟩
> xweaken+ (Φ ++ Ψ ++ B) Γ Δ (case (Φ ++ Ψ ++ B) Δ (Φ ≫ Ψ ≫ x ≪ Δ))
> ∎
>
> I don't really want to think about what this proof would look like with
> all the associativity wiring made explicit.
>
> There is still a bit of annoying associativity left, because I can't see
> how to get coproducts to associate on the nose, so there's lots of gore
> needed to define a case function:
>
> data Case {A} a (as bs : List A) : Set where
> inj₁ : (a∈as : a ∈ as) → Case a as bs
> inj₂ : (a∈bs : a ∈ bs) → Case a as bs
>
> case : ∀ {A a} as bs → (a ∈ (as ++ bs)) → Case {A} a as bs
>
> and then prove that it satisfies associativity (up to propositional
> equality, not beta-equivalence).
>
> A.
>
> On 10/26/2011 09:48 AM, Jeffrey, Alan S A (Alan) wrote:
>> Hi everyone,
>>
>> A quick note about a trick for representing lists (or any other monoid)
>> up to associativity. Am I reinventing a wheel here?
>>
>> I've been doing some mucking around recently with proofs about
>> lambda-calculi and was hitting annoying problems with associativity
>> on lists. A prototypical example is:
>>
>> weakening : ∀ {A a} (as bs cs : List A) →
>> (a ∈ (as ++ cs)) → (a ∈ (as ++ bs ++ cs))
>>
>> It's easy to prove that ++ is associative, but making use of that fact
>> is rather painful, as there's lots of manual wiring with subst and cong,
>> for example:
>>
>> weaken2 : ∀ {A a} (as bs cs ds : List A) →
>> (a ∈ (as ++ bs ++ ds)) → (a ∈ (as ++ bs ++ cs ++ ds))
>> weaken2 {A} {a} as bs cs ds a∈es =
>> subst (λ X → (a ∈ X)) (++-assoc as bs (cs ++ ds))
>> (weakening (as ++ bs) cs ds
>> (subst (λ X → (a ∈ X)) (sym (++-assoc as bs ds)) a∈es))
>>
>> This gets tiresome pretty rapidly. Oh if only there were a data
>> structure which represented lists, but for which ++ was associative up
>> to beta reduction... Oh look there already is one, it's called
>> difference lists. Quoting the standard library:
>>
>> DiffList : Set → Set
>> DiffList a = List a → List a
>>
>> _++_ : ∀ {a} → DiffList a → DiffList a → DiffList a
>> xs ++ ys = λ k → xs (ys k)
>>
>> Unfortunately, difference lists are not isomorphic to lists: there's a
>> lot more functions on lists than just concatenation functions. This
>> causes headaches (e.g. writing inductive functions on difference lists).
>>
>> A first shot at fixing this is to write a data structure for those
>> difference lists which are concatenations:
>>
>> record Seq (A : Set) : Set where
>> constructor seq
>> field
>> list : List A
>> fun : List A → List A
>> ok : fun ≡ _++_ list -- Broken
>>
>> It's pretty straightforward to define the monoidal structure for Seq:
>>
>> ε : ∀ {A} → Seq A
>> ε = seq [] id refl
>>
>> _+_ : ∀ {A} → Seq A → Seq A → Seq A
>> (seq as f f✓) + (seq bs g g✓) = seq (f bs) (f ∘ g) (...easy lemma...)
>>
>> Unfortunately, we're back to square one again, because + is only
>> associative up to propositional equality, not beta reduction. This time,
>> it's the ok field that gets in the way. So we can fix that, and just
>> make the ok field irrelevant, that is:
>>
>> record Seq (A : Set) : Set where
>> constructor seq
>> field
>> list : List A
>> fun : List A → List A
>> .ok : fun ≡ _++_ list -- Fixed
>>
>> open Seq public renaming (list to [_])
>>
>> Hooray, + is now associative up to beta reduction:
>>
>> +-assoc : ∀ {A} (as bs cs : Seq A) →
>> ((as + bs) + cs) ≡ (as + (bs + cs))
>> +-assoc as bs cs = refl
>>
>>
>> ≡-relevant : ∀ {A : Set} {a b : A} → .(a ≡ b) → (a ≡ b)
>>
>> we can define:
>>
>> data Case {A : Set} : Seq A → Set where
>> [] : Case ε
>> _∷_ : ∀ a as → Case (a ◁ as)
>>
>> case : ∀ {A} (as : Seq A) → Case as
>>
>> and this gives us recursive functions over Seq (which somewhat to my
>> surprise actually get past the termination checker), for example:
>>
>> ids : ∀ {A} → Seq A → Seq A
>> ids as with case as
>> ids .(a ◁ as) | a ∷ as = a ◁ ids as
>> ids .ε | [] = ε
>>
>> For example, we can now define weakening:
>>
>> weakening : ∀ {A a} (as bs cs : Seq A) →
>> (a ∈ [ as + cs ]) → (a ∈ [ as + bs + cs ])
>>
>> and use it up to associativity without worrying hand-coded wiring:
>>
>> weaken2 : ∀ {A a} (as bs cs ds : Seq A) →
>> (a ∈ [ as + bs + ds ]) → (a ∈ [ as + bs + cs + ds ])
>> weaken2 as bs = weakening (as + bs)
>>
>> Hooray, cake! Eating it!
>>
>> I suspect this trick works for most any monoid, so you can do
>> associativity on naturals, vectors, partial orders with join, etc. etc.
>>
>> The idea of using difference lists to represent lists is standard, but
>> as far as I know, this use of irrelevant equalities to get structural
>> recursion is new. Anyone know of any prior art?
>>
>> A.
> _______________________________________________
> Agda mailing list
> Agda@...
> https://lists.chalmers.se/mailman/listinfo/agda
>

--

--
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel@...
http://www2.tcs.ifi.lmu.de/~abel/
```
2 Nov 2011 22:10

```I'll have a look at it, thanks for the pointer!

I'm going to be needing the general form of substitution later (in stuff
I've not committed yet, which does normalization by evaluation). That's
not to say I couldn't derive the general form from substitution and
weakening, but I think it's swings and roundabouts.

A.

On 11/02/2011 12:46 PM, Andreas Abel wrote:
> Hi Alan,
>
> you might be interested in a trick how to fuse weakening and
> substitution into a single operation.  I have done this for
> non-wellscoped de Bruijn terms in Agda:
>
>     http://www2.tcs.ifi.lmu.de/~abel/ParallelSubstitution.agda
>
> but Thorsten and Conor deserve the credit for it (pointers in the .agda
> file).
>
> Looking at your code I wonder whether substitution (substn+) could not
> be a bit less general, since N remains in the same context always.
> Usually I prove the substitution lemma like this:
>
>     Gamma, x : T, Delta |- M : U
>     Gamma               |- N : T
>     ----------------------------
>     Gamma, Delta   |- M[N/x] : U
>
> Your statement has a more general context form for N, but I wonder
> whether this is necessary.
>
> Cheers,
> Andreas
>
> On 11/2/11 5:26 PM, Alan Jeffrey wrote:
>> Hi everyone,
>>
>> lambda-calculi. I've now worked through some of the details, and here is
>> the syntax of the simply-typed lambda-calculus:
>>
>>> https://github.com/agda/agda-frp-js/blob/master/src/agda/FRP/JS/Model/STLambdaC/Exp.agda
>>>
>>
>> The interesting thing is weakening, with type:
>>
>> weaken+ : ∀ B Γ Δ {T} → Exp (B ++ Δ) T → Exp (B ++ Γ ++ Δ) T
>>
>> and (news just in!) weakening commutes with itself (up to propositional
>> equality):
>>
>> weaken+ Φ Ψ (B ++ Γ ++ Δ) (weaken+ (Φ ++ B) Γ Δ M)
>> ≡ weaken+ (Φ ++ Ψ ++ B) Γ Δ (weaken+ Φ Ψ (B ++ Δ) M)
>>
>> Note that you can't even state this property without associativity on
>> the nose, since the lhs has type (Φ ++ Ψ ++ (B ++ Γ ++ Δ)) and the rhs
>> has type ((Φ ++ Ψ ++ B) ++ Γ ++ Δ).
>>
>> The proof makes use of a list-membership type, defined in:
>>
>>> https://github.com/agda/agda-frp-js/blob/master/src/agda/FRP/JS/DList.agda
>>>
>>
>> It satisfies weakening on the left and right:
>>
>> _≪_ : ∀ {A a as} → (a ∈ as) → ∀ bs → (a ∈ (as ++ bs))
>> _≫_ : ∀ {A a bs} → ∀ as → (a ∈ bs) → (a ∈ (as ++ bs))
>>
>> and moreover has left and right units and associativity properties, all
>> up to beta-equivalence (that is, all these properties have proof refl):
>>
>> (a∈as ≪ []) ≡ a∈as
>> ([] ≫ a∈as) ≡ a∈as
>> (a∈as ≪ bs ≪ cs) ≡ (a∈as ≪ bs ++ cs)
>> ((as ≫ a∈bs) ≪ cs) ≡ (as ≫ (a∈bs ≪ cs))
>> (as ≫ bs ≫ a∈cs) ≡ (as ≫ bs ≫ a∈cs)
>>
>> Under the hood, this is implemented in terms of difference naturals
>> (that is an implementation of ℕ where + and ♯0 form a monoid up to
>> beta-equivalence), and an implementation of difference lists such that
>> the length function is a monoid homomorphism up to beta-equivalence:
>>
>> (len (as ++ bs) ≡ (len as + len bs))
>> (len [] ≡ ♯0)
>>
>> With all that in place, the proof of weakening is pretty
>> straightforward. The only case which requires any work is variables, and
>> a typical case is:
>>
>> begin
>> xweaken+ Φ Ψ (B ++ Γ ++ Δ) (case Φ (B ++ Γ ++ Δ) (Φ ≫ x ≪ Γ ≪ Δ))
>> ≡⟨ cong (xweaken+ Φ Ψ (B ++ Γ ++ Δ)) (case-≫ Φ (x ≪ Γ ≪ Δ)) ⟩
>> (Φ ≫ Ψ ≫ x ≪ Γ ≪ Δ)
>> ≡⟨ cong (xweaken+ (Φ ++ Ψ ++ B) Γ Δ) (sym (case-≪ (Φ ≫ Ψ ≫ x) Δ)) ⟩
>> xweaken+ (Φ ++ Ψ ++ B) Γ Δ (case (Φ ++ Ψ ++ B) Δ (Φ ≫ Ψ ≫ x ≪ Δ))
>> ∎
>>
>> I don't really want to think about what this proof would look like with
>> all the associativity wiring made explicit.
>>
>> There is still a bit of annoying associativity left, because I can't see
>> how to get coproducts to associate on the nose, so there's lots of gore
>> needed to define a case function:
>>
>> data Case {A} a (as bs : List A) : Set where
>> inj₁ : (a∈as : a ∈ as) → Case a as bs
>> inj₂ : (a∈bs : a ∈ bs) → Case a as bs
>>
>> case : ∀ {A a} as bs → (a ∈ (as ++ bs)) → Case {A} a as bs
>>
>> and then prove that it satisfies associativity (up to propositional
>> equality, not beta-equivalence).
>>
>> A.
>>
>> On 10/26/2011 09:48 AM, Jeffrey, Alan S A (Alan) wrote:
>>> Hi everyone,
>>>
>>> A quick note about a trick for representing lists (or any other monoid)
>>> up to associativity. Am I reinventing a wheel here?
>>>
>>> I've been doing some mucking around recently with proofs about
>>> lambda-calculi and was hitting annoying problems with associativity
>>> on lists. A prototypical example is:
>>>
>>> weakening : ∀ {A a} (as bs cs : List A) →
>>> (a ∈ (as ++ cs)) → (a ∈ (as ++ bs ++ cs))
>>>
>>> It's easy to prove that ++ is associative, but making use of that fact
>>> is rather painful, as there's lots of manual wiring with subst and cong,
>>> for example:
>>>
>>> weaken2 : ∀ {A a} (as bs cs ds : List A) →
>>> (a ∈ (as ++ bs ++ ds)) → (a ∈ (as ++ bs ++ cs ++ ds))
>>> weaken2 {A} {a} as bs cs ds a∈es =
>>> subst (λ X → (a ∈ X)) (++-assoc as bs (cs ++ ds))
>>> (weakening (as ++ bs) cs ds
>>> (subst (λ X → (a ∈ X)) (sym (++-assoc as bs ds)) a∈es))
>>>
>>> This gets tiresome pretty rapidly. Oh if only there were a data
>>> structure which represented lists, but for which ++ was associative up
>>> to beta reduction... Oh look there already is one, it's called
>>> difference lists. Quoting the standard library:
>>>
>>> DiffList : Set → Set
>>> DiffList a = List a → List a
>>>
>>> _++_ : ∀ {a} → DiffList a → DiffList a → DiffList a
>>> xs ++ ys = λ k → xs (ys k)
>>>
>>> Unfortunately, difference lists are not isomorphic to lists: there's a
>>> lot more functions on lists than just concatenation functions. This
>>> causes headaches (e.g. writing inductive functions on difference lists).
>>>
>>> A first shot at fixing this is to write a data structure for those
>>> difference lists which are concatenations:
>>>
>>> record Seq (A : Set) : Set where
>>> constructor seq
>>> field
>>> list : List A
>>> fun : List A → List A
>>> ok : fun ≡ _++_ list -- Broken
>>>
>>> It's pretty straightforward to define the monoidal structure for Seq:
>>>
>>> ε : ∀ {A} → Seq A
>>> ε = seq [] id refl
>>>
>>> _+_ : ∀ {A} → Seq A → Seq A → Seq A
>>> (seq as f f✓) + (seq bs g g✓) = seq (f bs) (f ∘ g) (...easy lemma...)
>>>
>>> Unfortunately, we're back to square one again, because + is only
>>> associative up to propositional equality, not beta reduction. This time,
>>> it's the ok field that gets in the way. So we can fix that, and just
>>> make the ok field irrelevant, that is:
>>>
>>> record Seq (A : Set) : Set where
>>> constructor seq
>>> field
>>> list : List A
>>> fun : List A → List A
>>> .ok : fun ≡ _++_ list -- Fixed
>>>
>>> open Seq public renaming (list to [_])
>>>
>>> Hooray, + is now associative up to beta reduction:
>>>
>>> +-assoc : ∀ {A} (as bs cs : Seq A) →
>>> ((as + bs) + cs) ≡ (as + (bs + cs))
>>> +-assoc as bs cs = refl
>>>
>>>
>>> ≡-relevant : ∀ {A : Set} {a b : A} → .(a ≡ b) → (a ≡ b)
>>>
>>> we can define:
>>>
>>> data Case {A : Set} : Seq A → Set where
>>> [] : Case ε
>>> _∷_ : ∀ a as → Case (a ◁ as)
>>>
>>> case : ∀ {A} (as : Seq A) → Case as
>>>
>>> and this gives us recursive functions over Seq (which somewhat to my
>>> surprise actually get past the termination checker), for example:
>>>
>>> ids : ∀ {A} → Seq A → Seq A
>>> ids as with case as
>>> ids .(a ◁ as) | a ∷ as = a ◁ ids as
>>> ids .ε | [] = ε
>>>
>>> For example, we can now define weakening:
>>>
>>> weakening : ∀ {A a} (as bs cs : Seq A) →
>>> (a ∈ [ as + cs ]) → (a ∈ [ as + bs + cs ])
>>>
>>> and use it up to associativity without worrying hand-coded wiring:
>>>
>>> weaken2 : ∀ {A a} (as bs cs ds : Seq A) →
>>> (a ∈ [ as + bs + ds ]) → (a ∈ [ as + bs + cs + ds ])
>>> weaken2 as bs = weakening (as + bs)
>>>
>>> Hooray, cake! Eating it!
>>>
>>> I suspect this trick works for most any monoid, so you can do
>>> associativity on naturals, vectors, partial orders with join, etc. etc.
>>>
>>> The idea of using difference lists to represent lists is standard, but
>>> as far as I know, this use of irrelevant equalities to get structural
>>> recursion is new. Anyone know of any prior art?
>>>
>>> A.
>> _______________________________________________
>> Agda mailing list
>> Agda@...
>> https://lists.chalmers.se/mailman/listinfo/agda
>>
>
```
4 Nov 2011 12:06

```By the way you get to write both weakening and substitution as special
cases of the bind operator for the right monad:

https://github.com/Saizan/agda-frp-js/commit/07bd98c30a8669d2c5dd3d69aa4a12bf566c7ae0

(and then i proved a bunch of not so relevant stuff in the middle)

-- Andrea

On Wed, Nov 2, 2011 at 10:10 PM, Alan Jeffrey <ajeffrey@...> wrote:
> I'll have a look at it, thanks for the pointer!
>
> I'm going to be needing the general form of substitution later (in stuff
> I've not committed yet, which does normalization by evaluation). That's not
> to say I couldn't derive the general form from substitution and weakening,
> but I think it's swings and roundabouts.
>
> A.
>
> On 11/02/2011 12:46 PM, Andreas Abel wrote:
>>
>> Hi Alan,
>>
>> you might be interested in a trick how to fuse weakening and
>> substitution into a single operation.  I have done this for
>> non-wellscoped de Bruijn terms in Agda:
>>
>>    http://www2.tcs.ifi.lmu.de/~abel/ParallelSubstitution.agda
>>
>> but Thorsten and Conor deserve the credit for it (pointers in the .agda
>> file).
>>
>> Looking at your code I wonder whether substitution (substn+) could not
>> be a bit less general, since N remains in the same context always.
>> Usually I prove the substitution lemma like this:
>>
>>    Gamma, x : T, Delta |- M : U
>>    Gamma               |- N : T
>>    ----------------------------
>>    Gamma, Delta   |- M[N/x] : U
>>
>> Your statement has a more general context form for N, but I wonder
>> whether this is necessary.
>>
>> Cheers,
>> Andreas
>>
>> On 11/2/11 5:26 PM, Alan Jeffrey wrote:
>>>
>>> Hi everyone,
>>>
>>> lambda-calculi. I've now worked through some of the details, and here is
>>> the syntax of the simply-typed lambda-calculus:
>>>
>>>>
>>>> https://github.com/agda/agda-frp-js/blob/master/src/agda/FRP/JS/Model/STLambdaC/Exp.agda
>>>>
>>>
>>> The interesting thing is weakening, with type:
>>>
>>> weaken+ : ∀ B Γ Δ {T} → Exp (B ++ Δ) T → Exp (B ++ Γ ++ Δ) T
>>>
>>> and (news just in!) weakening commutes with itself (up to propositional
>>> equality):
>>>
>>> weaken+ Φ Ψ (B ++ Γ ++ Δ) (weaken+ (Φ ++ B) Γ Δ M)
>>> ≡ weaken+ (Φ ++ Ψ ++ B) Γ Δ (weaken+ Φ Ψ (B ++ Δ) M)
>>>
>>> Note that you can't even state this property without associativity on
>>> the nose, since the lhs has type (Φ ++ Ψ ++ (B ++ Γ ++ Δ)) and the rhs
>>> has type ((Φ ++ Ψ ++ B) ++ Γ ++ Δ).
>>>
>>> The proof makes use of a list-membership type, defined in:
>>>
>>>>
>>>> https://github.com/agda/agda-frp-js/blob/master/src/agda/FRP/JS/DList.agda
>>>>
>>>
>>> It satisfies weakening on the left and right:
>>>
>>> _≪_ : ∀ {A a as} → (a ∈ as) → ∀ bs → (a ∈ (as ++ bs))
>>> _≫_ : ∀ {A a bs} → ∀ as → (a ∈ bs) → (a ∈ (as ++ bs))
>>>
>>> and moreover has left and right units and associativity properties, all
>>> up to beta-equivalence (that is, all these properties have proof refl):
>>>
>>> (a∈as ≪ []) ≡ a∈as
>>> ([] ≫ a∈as) ≡ a∈as
>>> (a∈as ≪ bs ≪ cs) ≡ (a∈as ≪ bs ++ cs)
>>> ((as ≫ a∈bs) ≪ cs) ≡ (as ≫ (a∈bs ≪ cs))
>>> (as ≫ bs ≫ a∈cs) ≡ (as ≫ bs ≫ a∈cs)
>>>
>>> Under the hood, this is implemented in terms of difference naturals
>>> (that is an implementation of ℕ where + and ♯0 form a monoid up to
>>> beta-equivalence), and an implementation of difference lists such that
>>> the length function is a monoid homomorphism up to beta-equivalence:
>>>
>>> (len (as ++ bs) ≡ (len as + len bs))
>>> (len [] ≡ ♯0)
>>>
>>> With all that in place, the proof of weakening is pretty
>>> straightforward. The only case which requires any work is variables, and
>>> a typical case is:
>>>
>>> begin
>>> xweaken+ Φ Ψ (B ++ Γ ++ Δ) (case Φ (B ++ Γ ++ Δ) (Φ ≫ x ≪ Γ ≪ Δ))
>>> ≡⟨ cong (xweaken+ Φ Ψ (B ++ Γ ++ Δ)) (case-≫ Φ (x ≪ Γ ≪ Δ)) ⟩
>>> (Φ ≫ Ψ ≫ x ≪ Γ ≪ Δ)
>>> ≡⟨ cong (xweaken+ (Φ ++ Ψ ++ B) Γ Δ) (sym (case-≪ (Φ ≫ Ψ ≫ x) Δ)) ⟩
>>> xweaken+ (Φ ++ Ψ ++ B) Γ Δ (case (Φ ++ Ψ ++ B) Δ (Φ ≫ Ψ ≫ x ≪ Δ))
>>> ∎
>>>
>>> I don't really want to think about what this proof would look like with
>>> all the associativity wiring made explicit.
>>>
>>> There is still a bit of annoying associativity left, because I can't see
>>> how to get coproducts to associate on the nose, so there's lots of gore
>>> needed to define a case function:
>>>
>>> data Case {A} a (as bs : List A) : Set where
>>> inj₁ : (a∈as : a ∈ as) → Case a as bs
>>> inj₂ : (a∈bs : a ∈ bs) → Case a as bs
>>>
>>> case : ∀ {A a} as bs → (a ∈ (as ++ bs)) → Case {A} a as bs
>>>
>>> and then prove that it satisfies associativity (up to propositional
>>> equality, not beta-equivalence).
>>>
>>> A.
>>>
>>> On 10/26/2011 09:48 AM, Jeffrey, Alan S A (Alan) wrote:
>>>>
>>>> Hi everyone,
>>>>
>>>> A quick note about a trick for representing lists (or any other monoid)
>>>> up to associativity. Am I reinventing a wheel here?
>>>>
>>>> I've been doing some mucking around recently with proofs about
>>>> lambda-calculi and was hitting annoying problems with associativity
>>>> on lists. A prototypical example is:
>>>>
>>>> weakening : ∀ {A a} (as bs cs : List A) →
>>>> (a ∈ (as ++ cs)) → (a ∈ (as ++ bs ++ cs))
>>>>
>>>> It's easy to prove that ++ is associative, but making use of that fact
>>>> is rather painful, as there's lots of manual wiring with subst and cong,
>>>> for example:
>>>>
>>>> weaken2 : ∀ {A a} (as bs cs ds : List A) →
>>>> (a ∈ (as ++ bs ++ ds)) → (a ∈ (as ++ bs ++ cs ++ ds))
>>>> weaken2 {A} {a} as bs cs ds a∈es =
>>>> subst (λ X → (a ∈ X)) (++-assoc as bs (cs ++ ds))
>>>> (weakening (as ++ bs) cs ds
>>>> (subst (λ X → (a ∈ X)) (sym (++-assoc as bs ds)) a∈es))
>>>>
>>>> This gets tiresome pretty rapidly. Oh if only there were a data
>>>> structure which represented lists, but for which ++ was associative up
>>>> to beta reduction... Oh look there already is one, it's called
>>>> difference lists. Quoting the standard library:
>>>>
>>>> DiffList : Set → Set
>>>> DiffList a = List a → List a
>>>>
>>>> _++_ : ∀ {a} → DiffList a → DiffList a → DiffList a
>>>> xs ++ ys = λ k → xs (ys k)
>>>>
>>>> Unfortunately, difference lists are not isomorphic to lists: there's a
>>>> lot more functions on lists than just concatenation functions. This
>>>> causes headaches (e.g. writing inductive functions on difference lists).
>>>>
>>>> A first shot at fixing this is to write a data structure for those
>>>> difference lists which are concatenations:
>>>>
>>>> record Seq (A : Set) : Set where
>>>> constructor seq
>>>> field
>>>> list : List A
>>>> fun : List A → List A
>>>> ok : fun ≡ _++_ list -- Broken
>>>>
>>>> It's pretty straightforward to define the monoidal structure for Seq:
>>>>
>>>> ε : ∀ {A} → Seq A
>>>> ε = seq [] id refl
>>>>
>>>> _+_ : ∀ {A} → Seq A → Seq A → Seq A
>>>> (seq as f f✓) + (seq bs g g✓) = seq (f bs) (f ∘ g) (...easy lemma...)
>>>>
>>>> Unfortunately, we're back to square one again, because + is only
>>>> associative up to propositional equality, not beta reduction. This time,
>>>> it's the ok field that gets in the way. So we can fix that, and just
>>>> make the ok field irrelevant, that is:
>>>>
>>>> record Seq (A : Set) : Set where
>>>> constructor seq
>>>> field
>>>> list : List A
>>>> fun : List A → List A
>>>> .ok : fun ≡ _++_ list -- Fixed
>>>>
>>>> open Seq public renaming (list to [_])
>>>>
>>>> Hooray, + is now associative up to beta reduction:
>>>>
>>>> +-assoc : ∀ {A} (as bs cs : Seq A) →
>>>> ((as + bs) + cs) ≡ (as + (bs + cs))
>>>> +-assoc as bs cs = refl
>>>>
>>>>
>>>> ≡-relevant : ∀ {A : Set} {a b : A} → .(a ≡ b) → (a ≡ b)
>>>>
>>>> we can define:
>>>>
>>>> data Case {A : Set} : Seq A → Set where
>>>> [] : Case ε
>>>> _∷_ : ∀ a as → Case (a ◁ as)
>>>>
>>>> case : ∀ {A} (as : Seq A) → Case as
>>>>
>>>> and this gives us recursive functions over Seq (which somewhat to my
>>>> surprise actually get past the termination checker), for example:
>>>>
>>>> ids : ∀ {A} → Seq A → Seq A
>>>> ids as with case as
>>>> ids .(a ◁ as) | a ∷ as = a ◁ ids as
>>>> ids .ε | [] = ε
>>>>
>>>> For example, we can now define weakening:
>>>>
>>>> weakening : ∀ {A a} (as bs cs : Seq A) →
>>>> (a ∈ [ as + cs ]) → (a ∈ [ as + bs + cs ])
>>>>
>>>> and use it up to associativity without worrying hand-coded wiring:
>>>>
>>>> weaken2 : ∀ {A a} (as bs cs ds : Seq A) →
>>>> (a ∈ [ as + bs + ds ]) → (a ∈ [ as + bs + cs + ds ])
>>>> weaken2 as bs = weakening (as + bs)
>>>>
>>>> Hooray, cake! Eating it!
>>>>
>>>> I suspect this trick works for most any monoid, so you can do
>>>> associativity on naturals, vectors, partial orders with join, etc. etc.
>>>>
>>>> The idea of using difference lists to represent lists is standard, but
>>>> as far as I know, this use of irrelevant equalities to get structural
>>>> recursion is new. Anyone know of any prior art?
>>>>
>>>> A.
>>>
>>> _______________________________________________
>>> Agda mailing list
>>> Agda@...
>>> https://lists.chalmers.se/mailman/listinfo/agda
>>>
>>
> _______________________________________________
> Agda mailing list
> Agda@...
> https://lists.chalmers.se/mailman/listinfo/agda
>
```
4 Nov 2011 19:07

```OK, that was very helful, a lot of boilerplate code that was duplicated
between substitutions and weakening has vanished.

> https://github.com/agda/agda-frp-js/blob/master/src/agda/FRP/JS/Model/STLambdaC/Exp.agda

A.

On 11/02/2011 12:46 PM, Andreas Abel wrote:
> Hi Alan,
>
> you might be interested in a trick how to fuse weakening and
> substitution into a single operation.  I have done this for
> non-wellscoped de Bruijn terms in Agda:
>
>     http://www2.tcs.ifi.lmu.de/~abel/ParallelSubstitution.agda
>
> but Thorsten and Conor deserve the credit for it (pointers in the .agda
> file).
>
> Looking at your code I wonder whether substitution (substn+) could not
> be a bit less general, since N remains in the same context always.
> Usually I prove the substitution lemma like this:
>
>     Gamma, x : T, Delta |- M : U
>     Gamma               |- N : T
>     ----------------------------
>     Gamma, Delta   |- M[N/x] : U
>
> Your statement has a more general context form for N, but I wonder
> whether this is necessary.
>
> Cheers,
> Andreas
>
> On 11/2/11 5:26 PM, Alan Jeffrey wrote:
>> Hi everyone,
>>
>> lambda-calculi. I've now worked through some of the details, and here is
>> the syntax of the simply-typed lambda-calculus:
>>
>>> https://github.com/agda/agda-frp-js/blob/master/src/agda/FRP/JS/Model/STLambdaC/Exp.agda
>>>
>>
>> The interesting thing is weakening, with type:
>>
>> weaken+ : ∀ B Γ Δ {T} → Exp (B ++ Δ) T → Exp (B ++ Γ ++ Δ) T
>>
>> and (news just in!) weakening commutes with itself (up to propositional
>> equality):
>>
>> weaken+ Φ Ψ (B ++ Γ ++ Δ) (weaken+ (Φ ++ B) Γ Δ M)
>> ≡ weaken+ (Φ ++ Ψ ++ B) Γ Δ (weaken+ Φ Ψ (B ++ Δ) M)
>>
>> Note that you can't even state this property without associativity on
>> the nose, since the lhs has type (Φ ++ Ψ ++ (B ++ Γ ++ Δ)) and the rhs
>> has type ((Φ ++ Ψ ++ B) ++ Γ ++ Δ).
>>
>> The proof makes use of a list-membership type, defined in:
>>
>>> https://github.com/agda/agda-frp-js/blob/master/src/agda/FRP/JS/DList.agda
>>>
>>
>> It satisfies weakening on the left and right:
>>
>> _≪_ : ∀ {A a as} → (a ∈ as) → ∀ bs → (a ∈ (as ++ bs))
>> _≫_ : ∀ {A a bs} → ∀ as → (a ∈ bs) → (a ∈ (as ++ bs))
>>
>> and moreover has left and right units and associativity properties, all
>> up to beta-equivalence (that is, all these properties have proof refl):
>>
>> (a∈as ≪ []) ≡ a∈as
>> ([] ≫ a∈as) ≡ a∈as
>> (a∈as ≪ bs ≪ cs) ≡ (a∈as ≪ bs ++ cs)
>> ((as ≫ a∈bs) ≪ cs) ≡ (as ≫ (a∈bs ≪ cs))
>> (as ≫ bs ≫ a∈cs) ≡ (as ≫ bs ≫ a∈cs)
>>
>> Under the hood, this is implemented in terms of difference naturals
>> (that is an implementation of ℕ where + and ♯0 form a monoid up to
>> beta-equivalence), and an implementation of difference lists such that
>> the length function is a monoid homomorphism up to beta-equivalence:
>>
>> (len (as ++ bs) ≡ (len as + len bs))
>> (len [] ≡ ♯0)
>>
>> With all that in place, the proof of weakening is pretty
>> straightforward. The only case which requires any work is variables, and
>> a typical case is:
>>
>> begin
>> xweaken+ Φ Ψ (B ++ Γ ++ Δ) (case Φ (B ++ Γ ++ Δ) (Φ ≫ x ≪ Γ ≪ Δ))
>> ≡⟨ cong (xweaken+ Φ Ψ (B ++ Γ ++ Δ)) (case-≫ Φ (x ≪ Γ ≪ Δ)) ⟩
>> (Φ ≫ Ψ ≫ x ≪ Γ ≪ Δ)
>> ≡⟨ cong (xweaken+ (Φ ++ Ψ ++ B) Γ Δ) (sym (case-≪ (Φ ≫ Ψ ≫ x) Δ)) ⟩
>> xweaken+ (Φ ++ Ψ ++ B) Γ Δ (case (Φ ++ Ψ ++ B) Δ (Φ ≫ Ψ ≫ x ≪ Δ))
>> ∎
>>
>> I don't really want to think about what this proof would look like with
>> all the associativity wiring made explicit.
>>
>> There is still a bit of annoying associativity left, because I can't see
>> how to get coproducts to associate on the nose, so there's lots of gore
>> needed to define a case function:
>>
>> data Case {A} a (as bs : List A) : Set where
>> inj₁ : (a∈as : a ∈ as) → Case a as bs
>> inj₂ : (a∈bs : a ∈ bs) → Case a as bs
>>
>> case : ∀ {A a} as bs → (a ∈ (as ++ bs)) → Case {A} a as bs
>>
>> and then prove that it satisfies associativity (up to propositional
>> equality, not beta-equivalence).
>>
>> A.
>>
>> On 10/26/2011 09:48 AM, Jeffrey, Alan S A (Alan) wrote:
>>> Hi everyone,
>>>
>>> A quick note about a trick for representing lists (or any other monoid)
>>> up to associativity. Am I reinventing a wheel here?
>>>
>>> I've been doing some mucking around recently with proofs about
>>> lambda-calculi and was hitting annoying problems with associativity
>>> on lists. A prototypical example is:
>>>
>>> weakening : ∀ {A a} (as bs cs : List A) →
>>> (a ∈ (as ++ cs)) → (a ∈ (as ++ bs ++ cs))
>>>
>>> It's easy to prove that ++ is associative, but making use of that fact
>>> is rather painful, as there's lots of manual wiring with subst and cong,
>>> for example:
>>>
>>> weaken2 : ∀ {A a} (as bs cs ds : List A) →
>>> (a ∈ (as ++ bs ++ ds)) → (a ∈ (as ++ bs ++ cs ++ ds))
>>> weaken2 {A} {a} as bs cs ds a∈es =
>>> subst (λ X → (a ∈ X)) (++-assoc as bs (cs ++ ds))
>>> (weakening (as ++ bs) cs ds
>>> (subst (λ X → (a ∈ X)) (sym (++-assoc as bs ds)) a∈es))
>>>
>>> This gets tiresome pretty rapidly. Oh if only there were a data
>>> structure which represented lists, but for which ++ was associative up
>>> to beta reduction... Oh look there already is one, it's called
>>> difference lists. Quoting the standard library:
>>>
>>> DiffList : Set → Set
>>> DiffList a = List a → List a
>>>
>>> _++_ : ∀ {a} → DiffList a → DiffList a → DiffList a
>>> xs ++ ys = λ k → xs (ys k)
>>>
>>> Unfortunately, difference lists are not isomorphic to lists: there's a
>>> lot more functions on lists than just concatenation functions. This
>>> causes headaches (e.g. writing inductive functions on difference lists).
>>>
>>> A first shot at fixing this is to write a data structure for those
>>> difference lists which are concatenations:
>>>
>>> record Seq (A : Set) : Set where
>>> constructor seq
>>> field
>>> list : List A
>>> fun : List A → List A
>>> ok : fun ≡ _++_ list -- Broken
>>>
>>> It's pretty straightforward to define the monoidal structure for Seq:
>>>
>>> ε : ∀ {A} → Seq A
>>> ε = seq [] id refl
>>>
>>> _+_ : ∀ {A} → Seq A → Seq A → Seq A
>>> (seq as f f✓) + (seq bs g g✓) = seq (f bs) (f ∘ g) (...easy lemma...)
>>>
>>> Unfortunately, we're back to square one again, because + is only
>>> associative up to propositional equality, not beta reduction. This time,
>>> it's the ok field that gets in the way. So we can fix that, and just
>>> make the ok field irrelevant, that is:
>>>
>>> record Seq (A : Set) : Set where
>>> constructor seq
>>> field
>>> list : List A
>>> fun : List A → List A
>>> .ok : fun ≡ _++_ list -- Fixed
>>>
>>> open Seq public renaming (list to [_])
>>>
>>> Hooray, + is now associative up to beta reduction:
>>>
>>> +-assoc : ∀ {A} (as bs cs : Seq A) →
>>> ((as + bs) + cs) ≡ (as + (bs + cs))
>>> +-assoc as bs cs = refl
>>>
>>>
>>> ≡-relevant : ∀ {A : Set} {a b : A} → .(a ≡ b) → (a ≡ b)
>>>
>>> we can define:
>>>
>>> data Case {A : Set} : Seq A → Set where
>>> [] : Case ε
>>> _∷_ : ∀ a as → Case (a ◁ as)
>>>
>>> case : ∀ {A} (as : Seq A) → Case as
>>>
>>> and this gives us recursive functions over Seq (which somewhat to my
>>> surprise actually get past the termination checker), for example:
>>>
>>> ids : ∀ {A} → Seq A → Seq A
>>> ids as with case as
>>> ids .(a ◁ as) | a ∷ as = a ◁ ids as
>>> ids .ε | [] = ε
>>>
>>> For example, we can now define weakening:
>>>
>>> weakening : ∀ {A a} (as bs cs : Seq A) →
>>> (a ∈ [ as + cs ]) → (a ∈ [ as + bs + cs ])
>>>
>>> and use it up to associativity without worrying hand-coded wiring:
>>>
>>> weaken2 : ∀ {A a} (as bs cs ds : Seq A) →
>>> (a ∈ [ as + bs + ds ]) → (a ∈ [ as + bs + cs + ds ])
>>> weaken2 as bs = weakening (as + bs)
>>>
>>> Hooray, cake! Eating it!
>>>
>>> I suspect this trick works for most any monoid, so you can do
>>> associativity on naturals, vectors, partial orders with join, etc. etc.
>>>
>>> The idea of using difference lists to represent lists is standard, but
>>> as far as I know, this use of irrelevant equalities to get structural
>>> recursion is new. Anyone know of any prior art?
>>>
>>> A.
>> _______________________________________________
>> Agda mailing list
>> Agda@...
>> https://lists.chalmers.se/mailman/listinfo/agda
>>
>
```
4 Nov 2011 12:29

```Dear Alan + all,

On Wed, Nov 2, 2011 at 6:26 PM, Alan Jeffrey <ajeffrey@...> wrote:
> lambda-calculi. I've now worked through some of the details, and here is the
> syntax of the simply-typed lambda-calculus.

For contrast, here's renaming and substitution for well typed lambda
terms. Renamings are just functions from variables to variables,
substitutions are just functions form variables to terms. No clever
representations here, no clever getting them both as a instance of a
more general operation, I just wanted to use the interface to
substitution suggested by the (relative) monadic nature of well-typed
terms. The proof is a simplification of the paper proof in Altenkirch
and Reus' paper "Monadic presentations of lambda terms using
generalized inductive types" and follows the approximately the same
structure. The development goes up to proving that the substitution
operation commutes with composition of substitutions (just composition
of functions) -- the third monad law. It's about 170 lines in all
including the utilities prelude.

module WellTypedTerms where

-- Utilities
data _≅_ {A : Set} : {A' : Set} → A → A' → Set where
refl : {a : A} → a ≅ a

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

sym : ∀{A A'}{a : A}{a' : A'} → a ≅ a' → a' ≅ a
sym refl = refl

resp : ∀{A}{B : A → Set}(f : ∀ a → B a){a a' : A} → a ≅ a' → f a ≅ f a'
resp f refl = refl

resp2 : ∀{A}{B : A → Set}{C : (x : A) → B x → Set}(f : (x : A)(y : B
x) → C x y){a a' : A} → a ≅ a' → {b : B a}{b' : B a'} → b ≅ b' → f a b
≅ f a' b'
resp2 f refl refl = refl

_•_ : {A : Set}{B : A → Set}{C : (a : A) → B a → Set} →
(∀{a} b → C a b) → (g : (∀ a → B a)) → ∀ a → C a (g a)
f • g = λ a → f (g a)

id : {A : Set} → A → A
id a = a

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} { {a : A} → B' a} f g

postulate ext : {A : Set}{B B' : A → Set}{f : ∀ a → B a}{g : ∀ a → B' a} →
(∀ a → f a ≅ g a) → f ≅ g

--Well type lambda terms

data Ty : Set where
ι   : Ty
_⇒_ : Ty → Ty → Ty

data Con : Set where
ε   : Con
_<_ : Con → Ty → Con

data Var : Con → Ty → Set where
vz : ∀{Γ σ} → Var (Γ < σ) σ
vs : ∀{Γ σ τ} → Var Γ σ → Var (Γ < τ) σ

data Tm : Con → Ty → Set where
var : ∀{Γ σ} → Var Γ σ → Tm Γ σ
app : ∀{Γ σ τ} → Tm Γ (σ ⇒ τ) → Tm Γ σ → Tm Γ τ
lam : ∀{Γ σ τ} → Tm (Γ < σ) τ → Tm Γ (σ ⇒ τ)

-- Renaming

Ren : Con → Con → Set
Ren Γ Δ = ∀ {σ} → Var Γ σ → Var Δ σ

renId : ∀{Γ} → Ren Γ Γ
renId = id

renComp : ∀{B Γ Δ} → Ren Γ Δ → Ren B Γ → Ren B Δ
renComp f g = f • g

wk : ∀{Γ Δ σ} → Ren Γ Δ → Ren (Γ < σ) (Δ < σ)
wk f vz     = vz
wk f (vs i) = vs (f i)

ren : ∀{Γ Δ} → Ren Γ Δ → ∀ {σ} → Tm Γ σ → Tm Δ σ
ren f (var x)   = var (f x)
ren f (app t u) = app (ren f t) (ren f u)
ren f (lam t)   = lam (ren (wk f) t)

wkid : ∀{Γ σ τ}(x : Var (Γ < τ) σ) → wk renId x ≅ renId x
wkid vz     = refl
wkid (vs x) = refl

renid : ∀{Γ σ}(t : Tm Γ σ) → ren renId t ≅ id t
renid (var x)   = refl
renid (app t u) = resp2 app (renid t) (renid u)
renid (lam t) = resp lam (trans (resp (λ (f : Ren _ _) → ren f t)
(iext (λ _ → ext wkid)))
(renid t))

wkcomp : ∀ {B Γ Δ}(f : Ren Γ Δ)(g : Ren B Γ){σ τ}(x : Var (B < σ) τ) →
wk (renComp f g) x ≅ renComp (wk f) (wk g) x
wkcomp f g vz     = refl
wkcomp f g (vs i) = refl

rencomp : ∀ {B Γ Δ}(f : Ren Γ Δ)(g : Ren B Γ){σ}(t : Tm B σ) →
ren (renComp f g) t ≅ (ren f • ren g) t
rencomp f g (var x)   = refl
rencomp f g (app t u) = resp2 app (rencomp f g t) (rencomp f g u)
rencomp f g (lam t)   = resp lam (trans (resp (λ (f : Ren _ _) → ren f t)
(iext λ _ → ext (wkcomp f g)))
(rencomp (wk f) (wk g) t))

-- Substitutions

Sub : Con → Con → Set
Sub Γ Δ = ∀{σ} → Var Γ σ → Tm Δ σ

lift : ∀{Γ Δ σ} → Sub Γ Δ → Sub (Γ < σ) (Δ < σ)
lift f vz     = var vz
lift f (vs x) = ren vs (f x)

sub : ∀{Γ Δ} → Sub Γ Δ → ∀{σ} → Tm Γ σ → Tm Δ σ
sub f (var x)   = f x
sub f (app t u) = app (sub f t) (sub f u)
sub f (lam t)   = lam (sub (lift f) t)

subId : ∀{Γ} → Sub Γ Γ
subId = var

subComp : ∀{B Γ Δ} → Sub Γ Δ → Sub B Γ → Sub B Δ
subComp f g = sub f • g

liftid : ∀{Γ σ τ}(x : Var (Γ < σ) τ) → lift subId x ≅ subId x
liftid vz     = refl
liftid (vs x) = refl

-- first monad law, the second holds definitionally
subid : ∀{Γ σ}(t : Tm Γ σ) → sub subId t ≅ id t
subid (var x)   = refl
subid (app t u) = resp2 app (subid t) (subid u)
subid (lam t)   = resp lam (trans (resp (λ (f : Sub _ _) → sub f t)
(iext λ _ → ext liftid))
(subid t))

liftwk : ∀{B Γ Δ}(f : Sub Γ Δ)(g : Ren B Γ){σ τ}(x : Var (B < σ) τ) →
(lift f • wk g) x ≅ lift (f • g) x
liftwk f g vz     = refl
liftwk f g (vs x) = refl

subren : ∀{B Γ Δ}(f : Sub Γ Δ)(g : Ren B Γ){σ}(t : Tm B σ) →
(sub f • ren g) t ≅ sub (f • g) t
subren f g (var x)   = refl
subren f g (app t u) = resp2 app (subren f g t) (subren f g u)
subren f g (lam t)   = resp lam (trans (subren (lift f) (wk g) t)
(resp (λ (f : Sub _ _) → sub f t)
(iext λ _ → ext (liftwk f g))))

renwklift : ∀{B Γ Δ}(f : Ren Γ Δ)(g : Sub B Γ){σ τ}(x : Var (B < σ) τ) →
(ren (wk f) • lift g) x ≅ lift (ren f • g) x
renwklift f g vz     = refl
renwklift f g (vs x) = trans (sym (rencomp (wk f) vs (g x)))
(rencomp vs f (g x))

rensub : ∀{B Γ Δ}(f : Ren Γ Δ)(g : Sub B Γ){σ}(t : Tm B σ) →
(ren f •  sub g) t ≅ sub (ren f • g) t
rensub f g (var x)   = refl
rensub f g (app t u) = resp2 app (rensub f g t) (rensub f g u)
rensub f g (lam t)   = resp lam (trans (rensub (wk f) (lift g) t)
(resp (λ (f : Sub _ _) → sub f t)
(iext λ _ →
ext (renwklift f g))))

liftcomp : ∀{B Γ Δ}(f : Sub Γ Δ)(g : Sub B Γ){σ τ}(x : Var (B < σ) τ) →
lift (subComp f g) x ≅ subComp (lift f) (lift g) x
liftcomp f g vz     = refl
liftcomp f g (vs x) = trans (rensub vs f (g x))
(sym (subren (lift f) vs (g x)))

subcomp : ∀{B Γ Δ}(f : Sub Γ Δ)(g : Sub B Γ){σ}(t : Tm B σ) →
sub (subComp f g) t ≅ (sub f • sub g) t
subcomp f g (var x)   = refl
subcomp f g (app t u) = resp2 app (subcomp f g t) (subcomp f g u)
subcomp f g (lam t)   = resp lam (trans (resp (λ (f : Sub _ _) → sub f t)
(iext λ _ → ext (liftcomp f g)))
(subcomp (lift f) (lift g) t))

Regards,

James
```
4 Nov 2011 13:14

```There's also a tutorial account of this representation, aimed at the working Coqeur, in

N Benton, C-K Hur, A Kennedy and C McBride. Strongly Typed Term Representations in Coq.
Journal of Automated Reasoning, special issue on Theory and Applications of Abstraction, Substitution
and Naming.
Published Online March 2011.

Nick

-----Original Message-----
From: agda-bounces <at> lists.chalmers.se [mailto:agda-bounces <at> lists.chalmers.se] On Behalf Of James Chapman
Sent: 04 November 2011 11:30
To: Alan Jeffrey
Cc: agda list

Dear Alan + all,

On Wed, Nov 2, 2011 at 6:26 PM, Alan Jeffrey <ajeffrey <at> bell-labs.com> wrote:
> lambda-calculi. I've now worked through some of the details, and here is the
> syntax of the simply-typed lambda-calculus.

For contrast, here's renaming and substitution for well typed lambda
terms. Renamings are just functions from variables to variables,
substitutions are just functions form variables to terms. No clever
representations here, no clever getting them both as a instance of a
more general operation, I just wanted to use the interface to
substitution suggested by the (relative) monadic nature of well-typed
terms. The proof is a simplification of the paper proof in Altenkirch
and Reus' paper "Monadic presentations of lambda terms using
generalized inductive types" and follows the approximately the same
structure. The development goes up to proving that the substitution
operation commutes with composition of substitutions (just composition
of functions) -- the third monad law. It's about 170 lines in all
including the utilities prelude.

module WellTypedTerms where

-- Utilities
data _≅_ {A : Set} : {A' : Set} → A → A' → Set where
refl : {a : A} → a ≅ a

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

sym : ∀{A A'}{a : A}{a' : A'} → a ≅ a' → a' ≅ a
sym refl = refl

resp : ∀{A}{B : A → Set}(f : ∀ a → B a){a a' : A} → a ≅ a' → f a ≅ f a'
resp f refl = refl

resp2 : ∀{A}{B : A → Set}{C : (x : A) → B x → Set}(f : (x : A)(y : B
x) → C x y){a a' : A} → a ≅ a' → {b : B a}{b' : B a'} → b ≅ b' → f a b
≅ f a' b'
resp2 f refl refl = refl

_•_ : {A : Set}{B : A → Set}{C : (a : A) → B a → Set} →
(∀{a} b → C a b) → (g : (∀ a → B a)) → ∀ a → C a (g a)
f • g = λ a → f (g a)

id : {A : Set} → A → A
id a = a

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} { {a : A} → B' a} f g

postulate ext : {A : Set}{B B' : A → Set}{f : ∀ a → B a}{g : ∀ a → B' a} →
(∀ a → f a ≅ g a) → f ≅ g

--Well type lambda terms

data Ty : Set where
ι   : Ty
_⇒_ : Ty → Ty → Ty

data Con : Set where
ε   : Con
_<_ : Con → Ty → Con

data Var : Con → Ty → Set where
vz : ∀{Γ σ} → Var (Γ < σ) σ
vs : ∀{Γ σ τ} → Var Γ σ → Var (Γ < τ) σ

data Tm : Con → Ty → Set where
var : ∀{Γ σ} → Var Γ σ → Tm Γ σ
app : ∀{Γ σ τ} → Tm Γ (σ ⇒ τ) → Tm Γ σ → Tm Γ τ
lam : ∀{Γ σ τ} → Tm (Γ < σ) τ → Tm Γ (σ ⇒ τ)

-- Renaming

Ren : Con → Con → Set
Ren Γ Δ = ∀ {σ} → Var Γ σ → Var Δ σ

renId : ∀{Γ} → Ren Γ Γ
renId = id

renComp : ∀{B Γ Δ} → Ren Γ Δ → Ren B Γ → Ren B Δ
renComp f g = f • g

wk : ∀{Γ Δ σ} → Ren Γ Δ → Ren (Γ < σ) (Δ < σ)
wk f vz     = vz
wk f (vs i) = vs (f i)

ren : ∀{Γ Δ} → Ren Γ Δ → ∀ {σ} → Tm Γ σ → Tm Δ σ
ren f (var x)   = var (f x)
ren f (app t u) = app (ren f t) (ren f u)
ren f (lam t)   = lam (ren (wk f) t)

wkid : ∀{Γ σ τ}(x : Var (Γ < τ) σ) → wk renId x ≅ renId x
wkid vz     = refl
wkid (vs x) = refl

renid : ∀{Γ σ}(t : Tm Γ σ) → ren renId t ≅ id t
renid (var x)   = refl
renid (app t u) = resp2 app (renid t) (renid u)
renid (lam t) = resp lam (trans (resp (λ (f : Ren _ _) → ren f t)
(iext (λ _ → ext wkid)))
(renid t))

wkcomp : ∀ {B Γ Δ}(f : Ren Γ Δ)(g : Ren B Γ){σ τ}(x : Var (B < σ) τ) →
wk (renComp f g) x ≅ renComp (wk f) (wk g) x
wkcomp f g vz     = refl
wkcomp f g (vs i) = refl

rencomp : ∀ {B Γ Δ}(f : Ren Γ Δ)(g : Ren B Γ){σ}(t : Tm B σ) →
ren (renComp f g) t ≅ (ren f • ren g) t
rencomp f g (var x)   = refl
rencomp f g (app t u) = resp2 app (rencomp f g t) (rencomp f g u)
rencomp f g (lam t)   = resp lam (trans (resp (λ (f : Ren _ _) → ren f t)
(iext λ _ → ext (wkcomp f g)))
(rencomp (wk f) (wk g) t))

-- Substitutions

Sub : Con → Con → Set
Sub Γ Δ = ∀{σ} → Var Γ σ → Tm Δ σ

lift : ∀{Γ Δ σ} → Sub Γ Δ → Sub (Γ < σ) (Δ < σ)
lift f vz     = var vz
lift f (vs x) = ren vs (f x)

sub : ∀{Γ Δ} → Sub Γ Δ → ∀{σ} → Tm Γ σ → Tm Δ σ
sub f (var x)   = f x
sub f (app t u) = app (sub f t) (sub f u)
sub f (lam t)   = lam (sub (lift f) t)

subId : ∀{Γ} → Sub Γ Γ
subId = var

subComp : ∀{B Γ Δ} → Sub Γ Δ → Sub B Γ → Sub B Δ
subComp f g = sub f • g

liftid : ∀{Γ σ τ}(x : Var (Γ < σ) τ) → lift subId x ≅ subId x
liftid vz     = refl
liftid (vs x) = refl

-- first monad law, the second holds definitionally
subid : ∀{Γ σ}(t : Tm Γ σ) → sub subId t ≅ id t
subid (var x)   = refl
subid (app t u) = resp2 app (subid t) (subid u)
subid (lam t)   = resp lam (trans (resp (λ (f : Sub _ _) → sub f t)
(iext λ _ → ext liftid))
(subid t))

liftwk : ∀{B Γ Δ}(f : Sub Γ Δ)(g : Ren B Γ){σ τ}(x : Var (B < σ) τ) →
(lift f • wk g) x ≅ lift (f • g) x
liftwk f g vz     = refl
liftwk f g (vs x) = refl

subren : ∀{B Γ Δ}(f : Sub Γ Δ)(g : Ren B Γ){σ}(t : Tm B σ) →
(sub f • ren g) t ≅ sub (f • g) t
subren f g (var x)   = refl
subren f g (app t u) = resp2 app (subren f g t) (subren f g u)
subren f g (lam t)   = resp lam (trans (subren (lift f) (wk g) t)
(resp (λ (f : Sub _ _) → sub f t)
(iext λ _ → ext (liftwk f g))))

renwklift : ∀{B Γ Δ}(f : Ren Γ Δ)(g : Sub B Γ){σ τ}(x : Var (B < σ) τ) →
(ren (wk f) • lift g) x ≅ lift (ren f • g) x
renwklift f g vz     = refl
renwklift f g (vs x) = trans (sym (rencomp (wk f) vs (g x)))
(rencomp vs f (g x))

rensub : ∀{B Γ Δ}(f : Ren Γ Δ)(g : Sub B Γ){σ}(t : Tm B σ) →
(ren f •  sub g) t ≅ sub (ren f • g) t
rensub f g (var x)   = refl
rensub f g (app t u) = resp2 app (rensub f g t) (rensub f g u)
rensub f g (lam t)   = resp lam (trans (rensub (wk f) (lift g) t)
(resp (λ (f : Sub _ _) → sub f t)
(iext λ _ →
ext (renwklift f g))))

liftcomp : ∀{B Γ Δ}(f : Sub Γ Δ)(g : Sub B Γ){σ τ}(x : Var (B < σ) τ) →
lift (subComp f g) x ≅ subComp (lift f) (lift g) x
liftcomp f g vz     = refl
liftcomp f g (vs x) = trans (rensub vs f (g x))
(sym (subren (lift f) vs (g x)))

subcomp : ∀{B Γ Δ}(f : Sub Γ Δ)(g : Sub B Γ){σ}(t : Tm B σ) →
sub (subComp f g) t ≅ (sub f • sub g) t
subcomp f g (var x)   = refl
subcomp f g (app t u) = resp2 app (subcomp f g t) (subcomp f g u)
subcomp f g (lam t)   = resp lam (trans (resp (λ (f : Sub _ _) → sub f t)
(iext λ _ → ext (liftcomp f g)))
(subcomp (lift f) (lift g) t))

Regards,

James
_______________________________________________
Agda mailing list
Agda <at> lists.chalmers.se
https://lists.chalmers.se/mailman/listinfo/agda

```
```_______________________________________________
Agda mailing list
Agda@...
https://lists.chalmers.se/mailman/listinfo/agda
```
4 Nov 2011 14:22

```I should have said this follows the structure of Altenkirch and Reus' proof for untyped terms.

Also, this agda proof is described in the accepted draft paper "Relative Monads formalized"
(http://www.cs.ioc.ee/~james/Publications.html)  which I should really finish, well, today.

James

On Nov 4, 2011, at 1:29 PM, James Chapman wrote:

> Dear Alan + all,
>
> On Wed, Nov 2, 2011 at 6:26 PM, Alan Jeffrey <ajeffrey@...> wrote:
>> lambda-calculi. I've now worked through some of the details, and here is the
>> syntax of the simply-typed lambda-calculus.
>
> For contrast, here's renaming and substitution for well typed lambda
> terms. Renamings are just functions from variables to variables,
> substitutions are just functions form variables to terms. No clever
> representations here, no clever getting them both as a instance of a
> more general operation, I just wanted to use the interface to
> substitution suggested by the (relative) monadic nature of well-typed
> terms. The proof is a simplification of the paper proof in Altenkirch
> and Reus' paper "Monadic presentations of lambda terms using
> generalized inductive types" and follows the approximately the same
> structure. The development goes up to proving that the substitution
> operation commutes with composition of substitutions (just composition
> of functions) -- the third monad law. It's about 170 lines in all
> including the utilities prelude.
>
> module WellTypedTerms where
>
> -- Utilities
> data _≅_ {A : Set} : {A' : Set} → A → A' → Set where
>  refl : {a : A} → a ≅ a
>
> trans : ∀{A A' A''}{a : A}{a' : A'}{a'' : A''} → a ≅ a' → a' ≅ a'' → a ≅ a''
> trans refl p = p
>
> sym : ∀{A A'}{a : A}{a' : A'} → a ≅ a' → a' ≅ a
> sym refl = refl
>
> resp : ∀{A}{B : A → Set}(f : ∀ a → B a){a a' : A} → a ≅ a' → f a ≅ f a'
> resp f refl = refl
>
> resp2 : ∀{A}{B : A → Set}{C : (x : A) → B x → Set}(f : (x : A)(y : B
> x) → C x y){a a' : A} → a ≅ a' → {b : B a}{b' : B a'} → b ≅ b' → f a b
> ≅ f a' b'
> resp2 f refl refl = refl
>
> _•_ : {A : Set}{B : A → Set}{C : (a : A) → B a → Set} →
>      (∀{a} b → C a b) → (g : (∀ a → B a)) → ∀ a → C a (g a)
> f • g = λ a → f (g a)
>
> id : {A : Set} → A → A
> id a = a
>
> 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} { {a : A} → B' a} f g
>
> postulate ext : {A : Set}{B B' : A → Set}{f : ∀ a → B a}{g : ∀ a → B' a} →
>                (∀ a → f a ≅ g a) → f ≅ g
>
> --Well type lambda terms
>
> data Ty : Set where
>  ι   : Ty
>  _⇒_ : Ty → Ty → Ty
>
> data Con : Set where
>  ε   : Con
>  _<_ : Con → Ty → Con
>
> data Var : Con → Ty → Set where
>  vz : ∀{Γ σ} → Var (Γ < σ) σ
>  vs : ∀{Γ σ τ} → Var Γ σ → Var (Γ < τ) σ
>
> data Tm : Con → Ty → Set where
>  var : ∀{Γ σ} → Var Γ σ → Tm Γ σ
>  app : ∀{Γ σ τ} → Tm Γ (σ ⇒ τ) → Tm Γ σ → Tm Γ τ
>  lam : ∀{Γ σ τ} → Tm (Γ < σ) τ → Tm Γ (σ ⇒ τ)
>
> -- Renaming
>
> Ren : Con → Con → Set
> Ren Γ Δ = ∀ {σ} → Var Γ σ → Var Δ σ
>
> renId : ∀{Γ} → Ren Γ Γ
> renId = id
>
> renComp : ∀{B Γ Δ} → Ren Γ Δ → Ren B Γ → Ren B Δ
> renComp f g = f • g
>
> wk : ∀{Γ Δ σ} → Ren Γ Δ → Ren (Γ < σ) (Δ < σ)
> wk f vz     = vz
> wk f (vs i) = vs (f i)
>
> ren : ∀{Γ Δ} → Ren Γ Δ → ∀ {σ} → Tm Γ σ → Tm Δ σ
> ren f (var x)   = var (f x)
> ren f (app t u) = app (ren f t) (ren f u)
> ren f (lam t)   = lam (ren (wk f) t)
>
> wkid : ∀{Γ σ τ}(x : Var (Γ < τ) σ) → wk renId x ≅ renId x
> wkid vz     = refl
> wkid (vs x) = refl
>
> renid : ∀{Γ σ}(t : Tm Γ σ) → ren renId t ≅ id t
> renid (var x)   = refl
> renid (app t u) = resp2 app (renid t) (renid u)
> renid (lam t) = resp lam (trans (resp (λ (f : Ren _ _) → ren f t)
>                                      (iext (λ _ → ext wkid)))
>                                (renid t))
>
> wkcomp : ∀ {B Γ Δ}(f : Ren Γ Δ)(g : Ren B Γ){σ τ}(x : Var (B < σ) τ) →
>            wk (renComp f g) x ≅ renComp (wk f) (wk g) x
> wkcomp f g vz     = refl
> wkcomp f g (vs i) = refl
>
> rencomp : ∀ {B Γ Δ}(f : Ren Γ Δ)(g : Ren B Γ){σ}(t : Tm B σ) →
>            ren (renComp f g) t ≅ (ren f • ren g) t
> rencomp f g (var x)   = refl
> rencomp f g (app t u) = resp2 app (rencomp f g t) (rencomp f g u)
> rencomp f g (lam t)   = resp lam (trans (resp (λ (f : Ren _ _) → ren f t)
>                                              (iext λ _ → ext (wkcomp f g)))
>                                        (rencomp (wk f) (wk g) t))
>
> -- Substitutions
>
> Sub : Con → Con → Set
> Sub Γ Δ = ∀{σ} → Var Γ σ → Tm Δ σ
>
> lift : ∀{Γ Δ σ} → Sub Γ Δ → Sub (Γ < σ) (Δ < σ)
> lift f vz     = var vz
> lift f (vs x) = ren vs (f x)
>
> sub : ∀{Γ Δ} → Sub Γ Δ → ∀{σ} → Tm Γ σ → Tm Δ σ
> sub f (var x)   = f x
> sub f (app t u) = app (sub f t) (sub f u)
> sub f (lam t)   = lam (sub (lift f) t)
>
> subId : ∀{Γ} → Sub Γ Γ
> subId = var
>
> subComp : ∀{B Γ Δ} → Sub Γ Δ → Sub B Γ → Sub B Δ
> subComp f g = sub f • g
>
> liftid : ∀{Γ σ τ}(x : Var (Γ < σ) τ) → lift subId x ≅ subId x
> liftid vz     = refl
> liftid (vs x) = refl
>
> -- first monad law, the second holds definitionally
> subid : ∀{Γ σ}(t : Tm Γ σ) → sub subId t ≅ id t
> subid (var x)   = refl
> subid (app t u) = resp2 app (subid t) (subid u)
> subid (lam t)   = resp lam (trans (resp (λ (f : Sub _ _) → sub f t)
>                                        (iext λ _ → ext liftid))
>                                  (subid t))
>
> liftwk : ∀{B Γ Δ}(f : Sub Γ Δ)(g : Ren B Γ){σ τ}(x : Var (B < σ) τ) →
>            (lift f • wk g) x ≅ lift (f • g) x
> liftwk f g vz     = refl
> liftwk f g (vs x) = refl
>
> subren : ∀{B Γ Δ}(f : Sub Γ Δ)(g : Ren B Γ){σ}(t : Tm B σ) →
>         (sub f • ren g) t ≅ sub (f • g) t
> subren f g (var x)   = refl
> subren f g (app t u) = resp2 app (subren f g t) (subren f g u)
> subren f g (lam t)   = resp lam (trans (subren (lift f) (wk g) t)
>                                       (resp (λ (f : Sub _ _) → sub f t)
>                                             (iext λ _ → ext (liftwk f g))))
>
> renwklift : ∀{B Γ Δ}(f : Ren Γ Δ)(g : Sub B Γ){σ τ}(x : Var (B < σ) τ) →
>               (ren (wk f) • lift g) x ≅ lift (ren f • g) x
> renwklift f g vz     = refl
> renwklift f g (vs x) = trans (sym (rencomp (wk f) vs (g x)))
>                                (rencomp vs f (g x))
>
> rensub : ∀{B Γ Δ}(f : Ren Γ Δ)(g : Sub B Γ){σ}(t : Tm B σ) →
>         (ren f •  sub g) t ≅ sub (ren f • g) t
> rensub f g (var x)   = refl
> rensub f g (app t u) = resp2 app (rensub f g t) (rensub f g u)
> rensub f g (lam t)   = resp lam (trans (rensub (wk f) (lift g) t)
>                                       (resp (λ (f : Sub _ _) → sub f t)
>                                             (iext λ _ →
>                                               ext (renwklift f g))))
>
> liftcomp : ∀{B Γ Δ}(f : Sub Γ Δ)(g : Sub B Γ){σ τ}(x : Var (B < σ) τ) →
>           lift (subComp f g) x ≅ subComp (lift f) (lift g) x
> liftcomp f g vz     = refl
> liftcomp f g (vs x) = trans (rensub vs f (g x))
>                            (sym (subren (lift f) vs (g x)))
>
>
> subcomp : ∀{B Γ Δ}(f : Sub Γ Δ)(g : Sub B Γ){σ}(t : Tm B σ) →
>          sub (subComp f g) t ≅ (sub f • sub g) t
> subcomp f g (var x)   = refl
> subcomp f g (app t u) = resp2 app (subcomp f g t) (subcomp f g u)
> subcomp f g (lam t)   = resp lam (trans (resp (λ (f : Sub _ _) → sub f t)
>                                              (iext λ _ → ext (liftcomp f g)))
>                                        (subcomp (lift f) (lift g) t))
>
> Regards,
>
> James
```
4 Nov 2011 14:42

```On Fri, Nov 4, 2011 at 12:29 PM, James Chapman <james@...> wrote:
> [...] The development goes up to proving that the substitution
> operation commutes with composition of substitutions (just composition
> of functions) -- the third monad law. It's about 170 lines in all
> including the utilities prelude.

And yet, even without fancy representations, it can be trimmed down to
109 lines and many less intermediate constructions by working under a
context:

module WellTypedTerms where

-- Utilities
data _≅_ {A : Set} : {A' : Set} → A → A' → Set where
refl : {a : A} → a ≅ a

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

sym : ∀{A A'}{a : A}{a' : A'} → a ≅ a' → a' ≅ a
sym refl = refl

resp : ∀{A}{B : A → Set}(f : ∀ a → B a){a a' : A} → a ≅ a' → f a ≅ f a'
resp f refl = refl

resp2 : ∀{A}{B : A → Set}{C : (x : A) → B x → Set}(f : (x : A)(y : B x) → C x y)
{a a' : A} → a ≅ a' → {b : B a}{b' : B a'} → b ≅ b' → f a b ≅ f a' b'
resp2 f refl refl = refl

_•_ : {A : Set}{B : A → Set}{C : (a : A) → B a → Set} →
(∀ {a} b → C a b) → (g : (∀ (a : A) → B a)) → ∀ (a : A) → C a (g a)
f • g = λ a → f (g a)

id : {A : Set} → A → A
id a = a

--Well type lambda terms

data Ty : Set where
ι   : Ty
_⇒_ : Ty → Ty → Ty

data Con : Set where
ε   : Con
_<_ : Con → Ty → Con

_<<_ : Con -> Con -> Con
Γ << ε = Γ
Γ << (Δ < τ) = (Γ << Δ) < τ

data Var : Con → Ty → Set where
vz : ∀{Γ σ} → Var (Γ < σ) σ
vs : ∀{Γ σ τ} → Var Γ σ → Var (Γ < τ) σ

data Tm : Con → Ty → Set where
var : ∀{Γ σ} → Var Γ σ → Tm Γ σ
app : ∀{Γ σ τ} → Tm Γ (σ ⇒ τ) → Tm Γ σ → Tm Γ τ
lam : ∀{Γ σ τ} → Tm (Γ < σ) τ → Tm Γ (σ ⇒ τ)

-- Substitutions

Sub : Con → Con → Set
Sub Γ Δ = ∀ K {σ} → Var (Γ << K) σ → Tm (Δ << K) σ

sub : ∀{Γ Δ} → Sub Γ Δ → ∀ K {σ} → Tm (Γ << K) σ → Tm (Δ << K) σ
sub f K (var x)   = f K x
sub f K (app t u) = app (sub f K t) (sub f K u)
sub f K (lam t)   = lam (sub f (K < _) t)

subId : ∀{Γ} → Sub Γ Γ
subId = λ K x -> var x

subComp : ∀{B Γ Δ} → Sub Γ Δ → Sub B Γ → Sub B Δ
subComp f g K = sub f K • g K

-- first monad law, the second holds definitionally
subid : ∀{Γ}K{σ}(t : Tm (Γ << K) σ) → sub subId K t ≅ id t
subid K (var x)   = refl
subid K (app t u) = resp2 app (subid K t) (subid K u)
subid K (lam t)   = resp lam (subid (K < _) t)

-- Renaming

Ren : Con → Con → Set
Ren Γ Δ = ∀ K {σ} → Var (Γ << K) σ → Var (Δ << K) σ

renId : ∀{Γ} → Ren Γ Γ
renId = \ _ x -> x

renComp : ∀{B Γ Δ} → Ren Γ Δ → Ren B Γ → Ren B Δ
renComp f g = \ K -> f K • g K

ren : ∀{Γ Δ} → Ren Γ Δ → ∀ K {σ} → Tm (Γ << K) σ → Tm (Δ << K) σ
ren f K x = sub (λ K → subId K • f K) K x

renid : ∀{Γ} K {σ}(t : Tm (Γ << K) σ) → ren renId K t ≅ id t
renid = subid

rencomp : ∀ {B Γ Δ}(f : Ren Γ Δ)(g : Ren B Γ) K {σ}(t : Tm (B << K) σ) →
ren (renComp f g) K t ≅ (ren f K • ren g K) t
rencomp f g K (var x)   = refl
rencomp f g K (app t u) = resp2 app (rencomp f g K t) (rencomp f g K u)
rencomp {B}{Γ}{Δ} f g K (lam t) = resp lam (rencomp f g (K < _) t)

subcomp : ∀{B Γ Δ}(f : Sub Γ Δ)(g : Sub B Γ)K{σ}(t : Tm (B << K) σ) →
sub (subComp f g) K t ≅ (sub f K • sub g K) t
subcomp f g K (var x)   = refl
subcomp f g K (app t u) = resp2 app (subcomp f g K t) (subcomp f g K u)
subcomp f g K (lam t)   = resp lam (subcomp f g (K < _) t)

-- these are now corollaries
rensub : ∀{B Γ Δ}(f : Ren Γ Δ)(g : Sub B Γ)K{σ}(t : Tm (B << K) σ) →
(ren f K • sub g K) t ≅ sub (λ K -> ren f K • g K) K t
rensub f g K t = sym (subcomp (λ K → subId K • f K) g K t)

subren : ∀{B Γ Δ}(f : Sub Γ Δ)(g : Ren B Γ)K{σ}(t : Tm (B << K) σ) →
(sub f K • ren g K) t ≅ sub (λ K -> f K • g K) K t
subren f g K x = sym (subcomp f (λ K' → subId K' • g K') K x)
```
4 Nov 2011 15:18

```On Nov 4, 2011, at 3:42 PM, Andrea Vezzosi wrote:
> On Fri, Nov 4, 2011 at 12:29 PM, James Chapman <james@...> wrote:
> And yet, even without fancy representations, it can be trimmed down to
> 109 lines and many less intermediate constructions by working under a
> context:

Neat! Thanks, perhaps I should post my code to the agda list more often ;)

James
```
4 Nov 2011 18:55

```OK, that's pretty cool. The nasty case which hit me was proving
properties like "weakening of weakening is weakening":

weaken* A (weaken* B M) ≡ weaken* (A ++ B) M

which you can't even state without putting in some explicit associators.

This came up in the context of normalization by evaluation, which needs
a Kripke-like structure which extends the context on every function
application. Associators were really getting in the way, as I was
needing to prove a bunch of coherence properties. Have you tried getting
an NBE proof to go through in your setting?

A.

On 11/04/2011 06:29 AM, James Chapman wrote:
> Dear Alan + all,
>
> On Wed, Nov 2, 2011 at 6:26 PM, Alan Jeffrey<ajeffrey@...>  wrote:
>> lambda-calculi. I've now worked through some of the details, and here is the
>> syntax of the simply-typed lambda-calculus.
>
> For contrast, here's renaming and substitution for well typed lambda
> terms. Renamings are just functions from variables to variables,
> substitutions are just functions form variables to terms. No clever
> representations here, no clever getting them both as a instance of a
> more general operation, I just wanted to use the interface to
> substitution suggested by the (relative) monadic nature of well-typed
> terms. The proof is a simplification of the paper proof in Altenkirch
> and Reus' paper "Monadic presentations of lambda terms using
> generalized inductive types" and follows the approximately the same
> structure. The development goes up to proving that the substitution
> operation commutes with composition of substitutions (just composition
> of functions) -- the third monad law. It's about 170 lines in all
> including the utilities prelude.
>
> module WellTypedTerms where
>
> -- Utilities
> data _≅_ {A : Set} : {A' : Set} → A → A' → Set where
>    refl : {a : A} → a ≅ a
>
> trans : ∀{A A' A''}{a : A}{a' : A'}{a'' : A''} → a ≅ a' → a' ≅ a'' → a ≅ a''
> trans refl p = p
>
> sym : ∀{A A'}{a : A}{a' : A'} → a ≅ a' → a' ≅ a
> sym refl = refl
>
> resp : ∀{A}{B : A → Set}(f : ∀ a → B a){a a' : A} → a ≅ a' → f a ≅ f a'
> resp f refl = refl
>
> resp2 : ∀{A}{B : A → Set}{C : (x : A) → B x → Set}(f : (x : A)(y : B
> x) → C x y){a a' : A} → a ≅ a' → {b : B a}{b' : B a'} → b ≅ b' → f a b
> ≅ f a' b'
> resp2 f refl refl = refl
>
> _•_ : {A : Set}{B : A → Set}{C : (a : A) → B a → Set} →
>        (∀{a} b → C a b) → (g : (∀ a → B a)) → ∀ a → C a (g a)
> f • g = λ a → f (g a)
>
> id : {A : Set} → A → A
> id a = a
>
> 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} { {a : A} → B' a} f g
>
> postulate ext : {A : Set}{B B' : A → Set}{f : ∀ a → B a}{g : ∀ a → B' a} →
>                  (∀ a → f a ≅ g a) → f ≅ g
>
> --Well type lambda terms
>
> data Ty : Set where
>    ι   : Ty
>    _⇒_ : Ty → Ty → Ty
>
> data Con : Set where
>    ε   : Con
>    _<_ : Con → Ty → Con
>
> data Var : Con → Ty → Set where
>    vz : ∀{Γ σ} → Var (Γ<  σ) σ
>    vs : ∀{Γ σ τ} → Var Γ σ → Var (Γ<  τ) σ
>
> data Tm : Con → Ty → Set where
>    var : ∀{Γ σ} → Var Γ σ → Tm Γ σ
>    app : ∀{Γ σ τ} → Tm Γ (σ ⇒ τ) → Tm Γ σ → Tm Γ τ
>    lam : ∀{Γ σ τ} → Tm (Γ<  σ) τ → Tm Γ (σ ⇒ τ)
>
> -- Renaming
>
> Ren : Con → Con → Set
> Ren Γ Δ = ∀ {σ} → Var Γ σ → Var Δ σ
>
> renId : ∀{Γ} → Ren Γ Γ
> renId = id
>
> renComp : ∀{B Γ Δ} → Ren Γ Δ → Ren B Γ → Ren B Δ
> renComp f g = f • g
>
> wk : ∀{Γ Δ σ} → Ren Γ Δ → Ren (Γ<  σ) (Δ<  σ)
> wk f vz     = vz
> wk f (vs i) = vs (f i)
>
> ren : ∀{Γ Δ} → Ren Γ Δ → ∀ {σ} → Tm Γ σ → Tm Δ σ
> ren f (var x)   = var (f x)
> ren f (app t u) = app (ren f t) (ren f u)
> ren f (lam t)   = lam (ren (wk f) t)
>
> wkid : ∀{Γ σ τ}(x : Var (Γ<  τ) σ) → wk renId x ≅ renId x
> wkid vz     = refl
> wkid (vs x) = refl
>
> renid : ∀{Γ σ}(t : Tm Γ σ) → ren renId t ≅ id t
> renid (var x)   = refl
> renid (app t u) = resp2 app (renid t) (renid u)
> renid (lam t) = resp lam (trans (resp (λ (f : Ren _ _) → ren f t)
>                                        (iext (λ _ → ext wkid)))
>                                  (renid t))
>
> wkcomp : ∀ {B Γ Δ}(f : Ren Γ Δ)(g : Ren B Γ){σ τ}(x : Var (B<  σ) τ) →
>              wk (renComp f g) x ≅ renComp (wk f) (wk g) x
> wkcomp f g vz     = refl
> wkcomp f g (vs i) = refl
>
> rencomp : ∀ {B Γ Δ}(f : Ren Γ Δ)(g : Ren B Γ){σ}(t : Tm B σ) →
>              ren (renComp f g) t ≅ (ren f • ren g) t
> rencomp f g (var x)   = refl
> rencomp f g (app t u) = resp2 app (rencomp f g t) (rencomp f g u)
> rencomp f g (lam t)   = resp lam (trans (resp (λ (f : Ren _ _) → ren f t)
>                                                (iext λ _ → ext (wkcomp f g)))
>                                          (rencomp (wk f) (wk g) t))
>
> -- Substitutions
>
> Sub : Con → Con → Set
> Sub Γ Δ = ∀{σ} → Var Γ σ → Tm Δ σ
>
> lift : ∀{Γ Δ σ} → Sub Γ Δ → Sub (Γ<  σ) (Δ<  σ)
> lift f vz     = var vz
> lift f (vs x) = ren vs (f x)
>
> sub : ∀{Γ Δ} → Sub Γ Δ → ∀{σ} → Tm Γ σ → Tm Δ σ
> sub f (var x)   = f x
> sub f (app t u) = app (sub f t) (sub f u)
> sub f (lam t)   = lam (sub (lift f) t)
>
> subId : ∀{Γ} → Sub Γ Γ
> subId = var
>
> subComp : ∀{B Γ Δ} → Sub Γ Δ → Sub B Γ → Sub B Δ
> subComp f g = sub f • g
>
> liftid : ∀{Γ σ τ}(x : Var (Γ<  σ) τ) → lift subId x ≅ subId x
> liftid vz     = refl
> liftid (vs x) = refl
>
> -- first monad law, the second holds definitionally
> subid : ∀{Γ σ}(t : Tm Γ σ) → sub subId t ≅ id t
> subid (var x)   = refl
> subid (app t u) = resp2 app (subid t) (subid u)
> subid (lam t)   = resp lam (trans (resp (λ (f : Sub _ _) → sub f t)
>                                          (iext λ _ → ext liftid))
>                                    (subid t))
>
> liftwk : ∀{B Γ Δ}(f : Sub Γ Δ)(g : Ren B Γ){σ τ}(x : Var (B<  σ) τ) →
>              (lift f • wk g) x ≅ lift (f • g) x
> liftwk f g vz     = refl
> liftwk f g (vs x) = refl
>
> subren : ∀{B Γ Δ}(f : Sub Γ Δ)(g : Ren B Γ){σ}(t : Tm B σ) →
>           (sub f • ren g) t ≅ sub (f • g) t
> subren f g (var x)   = refl
> subren f g (app t u) = resp2 app (subren f g t) (subren f g u)
> subren f g (lam t)   = resp lam (trans (subren (lift f) (wk g) t)
>                                         (resp (λ (f : Sub _ _) → sub f t)
>                                               (iext λ _ → ext (liftwk f g))))
>
> renwklift : ∀{B Γ Δ}(f : Ren Γ Δ)(g : Sub B Γ){σ τ}(x : Var (B<  σ) τ) →
>                 (ren (wk f) • lift g) x ≅ lift (ren f • g) x
> renwklift f g vz     = refl
> renwklift f g (vs x) = trans (sym (rencomp (wk f) vs (g x)))
>                                  (rencomp vs f (g x))
>
> rensub : ∀{B Γ Δ}(f : Ren Γ Δ)(g : Sub B Γ){σ}(t : Tm B σ) →
>           (ren f •  sub g) t ≅ sub (ren f • g) t
> rensub f g (var x)   = refl
> rensub f g (app t u) = resp2 app (rensub f g t) (rensub f g u)
> rensub f g (lam t)   = resp lam (trans (rensub (wk f) (lift g) t)
>                                         (resp (λ (f : Sub _ _) → sub f t)
>                                               (iext λ _ →
>                                                 ext (renwklift f g))))
>
> liftcomp : ∀{B Γ Δ}(f : Sub Γ Δ)(g : Sub B Γ){σ τ}(x : Var (B<  σ) τ) →
>             lift (subComp f g) x ≅ subComp (lift f) (lift g) x
> liftcomp f g vz     = refl
> liftcomp f g (vs x) = trans (rensub vs f (g x))
>                              (sym (subren (lift f) vs (g x)))
>
>
> subcomp : ∀{B Γ Δ}(f : Sub Γ Δ)(g : Sub B Γ){σ}(t : Tm B σ) →
>            sub (subComp f g) t ≅ (sub f • sub g) t
> subcomp f g (var x)   = refl
> subcomp f g (app t u) = resp2 app (subcomp f g t) (subcomp f g u)
> subcomp f g (lam t)   = resp lam (trans (resp (λ (f : Sub _ _) → sub f t)
>                                                (iext λ _ → ext (liftcomp f g)))
>                                          (subcomp (lift f) (lift g) t))
>
> Regards,
>
> James
```
4 Nov 2011 19:15

```On 2011-11-04 18:55, Alan Jeffrey wrote:
> This came up in the context of normalization by evaluation, which needs
> a Kripke-like structure which extends the context on every function
> application. Associators were really getting in the way, as I was
> needing to prove a bunch of coherence properties. Have you tried getting
> an NBE proof to go through in your setting?

I don't know about James' setting, but I've implemented something close
to NBE [*] in a well-typed way for a dependently typed object language,
and didn't have any problems with associativity (once I found the right
definitions):

The key trick to avoid problems with associativity was to use cons-based
context extensions.

[*] I didn't prove uniqueness of normal forms, but rather its negation
(almost).

--

--
```
5 Nov 2011 02:58

```Yes, it may be that if I'd found the right collection of cons- vs-
snoc-lists I'd have been able to get NBE to go through without
associators. At this point, using difference lists around allows me to
be sloppy about associativity, and have it all magically go through.

So far the main annoyances with difference lists I've found are:

a) Huge normal forms for terms, which tend to bog Agda down, especially
in proofs with lots of holes.

b) A side-effect of (a) is that error messages or anything else which
prints a normal form aren't much use, which makes proving properties a
bit error-prone.

c) There are some unifications on difference lists that Agda fails to
make, the most annoying of which is unifying (a ∷ as) with (b ∷ bs)
doesn't unify a with b or as with bs, which is something weird to do
with unification happening under lambdas.

A.

On 11/04/2011 01:15 PM, Nils Anders Danielsson wrote:
> On 2011-11-04 18:55, Alan Jeffrey wrote:
>> This came up in the context of normalization by evaluation, which needs
>> a Kripke-like structure which extends the context on every function
>> application. Associators were really getting in the way, as I was
>> needing to prove a bunch of coherence properties. Have you tried getting
>> an NBE proof to go through in your setting?
>
> I don't know about James' setting, but I've implemented something close
> to NBE [*] in a well-typed way for a dependently typed object language,
> and didn't have any problems with associativity (once I found the right
> definitions):
>
>
> The key trick to avoid problems with associativity was to use cons-based
> context extensions.
>
> [*] I didn't prove uniqueness of normal forms, but rather its negation
> (almost).
>
```
5 Nov 2011 11:47

```I haven't tried an NBE proof with the version of renaming and
substitution I posted yesterday. I have done something similar during
my PhD. I used OPEs in the end (which I described early in this thread
and Randy pointed to copious prior art).

data OPE : Con -> Con -> Set where
done : OPE ε ε
keep : forall {Γ Δ} σ -> OPE Γ Δ -> OPE (Γ < σ) (Δ < σ)
skip : forall {Γ Δ} σ -> OPE Γ Δ -> OPE (Γ < σ) Δ

I had exactly this problem as you, for me it was with kripke logical
predicates. Instead of defining the kripke-like part as saying:

/a strongly computable function is one that given an strongly
computable  argument in an extended context, and after weakening the
function so that it is in the same context, will give a strongly
computable result./

I defined it using the kripke like bit of strong computability roughly
as follows:

SCV : forall {Γ σ} -> Val Γ σ -> Set
SCV {Γ} {σ ⇒ τ} v       = forall {B}(f : OPE B Γ)(a : Val B σ) -> SCV a ->
SCV  {B} {τ} (oapp f v \$\$ a)
SCV ...

i.e. /a strongly computable function is one that given a strongly
computable argument in an arbitrary context B, and a order preserving
embedding from the functions context Γ into B, and after applying the
embedding to the function, we get a strongly computable result./

The context B is arbitrary but OPE Γ B is only inhabited if B is
'larger'. applying oapp twice (composing them) doesn't lead to the
same problem as your weaken as the source and target contexts are just
variables, just like composing functions. OPEs are exactly the
renamings which don't shrink the context and hence useful here.

Regards,

James

On Fri, Nov 4, 2011 at 7:55 PM, Alan Jeffrey <ajeffrey <at> bell-labs.com> wrote:
> OK, that's pretty cool. The nasty case which hit me was proving properties
> like "weakening of weakening is weakening":
>
>  weaken* A (weaken* B M) ≡ weaken* (A ++ B) M
>
> which you can't even state without putting in some explicit associators.
>
> This came up in the context of normalization by evaluation, which needs a
> Kripke-like structure which extends the context on every function
> application. Associators were really getting in the way, as I was needing to
> prove a bunch of coherence properties. Have you tried getting an NBE proof
> to go through in your setting?
>
> A.
>
> On 11/04/2011 06:29 AM, James Chapman wrote:
>>
>> Dear Alan + all,
>>
>> On Wed, Nov 2, 2011 at 6:26 PM, Alan Jeffrey<ajeffrey <at> bell-labs.com>
>>  wrote:
>>>
>>> lambda-calculi. I've now worked through some of the details, and here is
>>> the
>>> syntax of the simply-typed lambda-calculus.
>>
>> For contrast, here's renaming and substitution for well typed lambda
>> terms. Renamings are just functions from variables to variables,
>> substitutions are just functions form variables to terms. No clever
>> representations here, no clever getting them both as a instance of a
>> more general operation, I just wanted to use the interface to
>> substitution suggested by the (relative) monadic nature of well-typed
>> terms. The proof is a simplification of the paper proof in Altenkirch
>> and Reus' paper "Monadic presentations of lambda terms using
>> generalized inductive types" and follows the approximately the same
>> structure. The development goes up to proving that the substitution
>> operation commutes with composition of substitutions (just composition
>> of functions) -- the third monad law. It's about 170 lines in all
>> including the utilities prelude.
>>
>> module WellTypedTerms where
>>
>> -- Utilities
>> data _≅_ {A : Set} : {A' : Set} → A → A' → Set where
>>   refl : {a : A} → a ≅ a
>>
>> trans : ∀{A A' A''}{a : A}{a' : A'}{a'' : A''} → a ≅ a' → a' ≅ a'' → a ≅
>> a''
>> trans refl p = p
>>
>> sym : ∀{A A'}{a : A}{a' : A'} → a ≅ a' → a' ≅ a
>> sym refl = refl
>>
>> resp : ∀{A}{B : A → Set}(f : ∀ a → B a){a a' : A} → a ≅ a' → f a ≅ f a'
>> resp f refl = refl
>>
>> resp2 : ∀{A}{B : A → Set}{C : (x : A) → B x → Set}(f : (x : A)(y : B
>> x) → C x y){a a' : A} → a ≅ a' → {b : B a}{b' : B a'} → b ≅ b' → f a b
>> ≅ f a' b'
>> resp2 f refl refl = refl
>>
>> _•_ : {A : Set}{B : A → Set}{C : (a : A) → B a → Set} →
>>       (∀{a} b → C a b) → (g : (∀ a → B a)) → ∀ a → C a (g a)
>> f • g = λ a → f (g a)
>>
>> id : {A : Set} → A → A
>> id a = a
>>
>> 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} { {a : A} → B' a} f g
>>
>> postulate ext : {A : Set}{B B' : A → Set}{f : ∀ a → B a}{g : ∀ a → B' a} →
>>                 (∀ a → f a ≅ g a) → f ≅ g
>>
>> --Well type lambda terms
>>
>> data Ty : Set where
>>   ι   : Ty
>>   _⇒_ : Ty → Ty → Ty
>>
>> data Con : Set where
>>   ε   : Con
>>   _<_ : Con → Ty → Con
>>
>> data Var : Con → Ty → Set where
>>   vz : ∀{Γ σ} → Var (Γ<  σ) σ
>>   vs : ∀{Γ σ τ} → Var Γ σ → Var (Γ<  τ) σ
>>
>> data Tm : Con → Ty → Set where
>>   var : ∀{Γ σ} → Var Γ σ → Tm Γ σ
>>   app : ∀{Γ σ τ} → Tm Γ (σ ⇒ τ) → Tm Γ σ → Tm Γ τ
>>   lam : ∀{Γ σ τ} → Tm (Γ<  σ) τ → Tm Γ (σ ⇒ τ)
>>
>> -- Renaming
>>
>> Ren : Con → Con → Set
>> Ren Γ Δ = ∀ {σ} → Var Γ σ → Var Δ σ
>>
>> renId : ∀{Γ} → Ren Γ Γ
>> renId = id
>>
>> renComp : ∀{B Γ Δ} → Ren Γ Δ → Ren B Γ → Ren B Δ
>> renComp f g = f • g
>>
>> wk : ∀{Γ Δ σ} → Ren Γ Δ → Ren (Γ<  σ) (Δ<  σ)
>> wk f vz     = vz
>> wk f (vs i) = vs (f i)
>>
>> ren : ∀{Γ Δ} → Ren Γ Δ → ∀ {σ} → Tm Γ σ → Tm Δ σ
>> ren f (var x)   = var (f x)
>> ren f (app t u) = app (ren f t) (ren f u)
>> ren f (lam t)   = lam (ren (wk f) t)
>>
>> wkid : ∀{Γ σ τ}(x : Var (Γ<  τ) σ) → wk renId x ≅ renId x
>> wkid vz     = refl
>> wkid (vs x) = refl
>>
>> renid : ∀{Γ σ}(t : Tm Γ σ) → ren renId t ≅ id t
>> renid (var x)   = refl
>> renid (app t u) = resp2 app (renid t) (renid u)
>> renid (lam t) = resp lam (trans (resp (λ (f : Ren _ _) → ren f t)
>>                                       (iext (λ _ → ext wkid)))
>>                                 (renid t))
>>
>> wkcomp : ∀ {B Γ Δ}(f : Ren Γ Δ)(g : Ren B Γ){σ τ}(x : Var (B<  σ) τ) →
>>             wk (renComp f g) x ≅ renComp (wk f) (wk g) x
>> wkcomp f g vz     = refl
>> wkcomp f g (vs i) = refl
>>
>> rencomp : ∀ {B Γ Δ}(f : Ren Γ Δ)(g : Ren B Γ){σ}(t : Tm B σ) →
>>             ren (renComp f g) t ≅ (ren f • ren g) t
>> rencomp f g (var x)   = refl
>> rencomp f g (app t u) = resp2 app (rencomp f g t) (rencomp f g u)
>> rencomp f g (lam t)   = resp lam (trans (resp (λ (f : Ren _ _) → ren f t)
>>                                               (iext λ _ → ext (wkcomp f
>> g)))
>>                                         (rencomp (wk f) (wk g) t))
>>
>> -- Substitutions
>>
>> Sub : Con → Con → Set
>> Sub Γ Δ = ∀{σ} → Var Γ σ → Tm Δ σ
>>
>> lift : ∀{Γ Δ σ} → Sub Γ Δ → Sub (Γ<  σ) (Δ<  σ)
>> lift f vz     = var vz
>> lift f (vs x) = ren vs (f x)
>>
>> sub : ∀{Γ Δ} → Sub Γ Δ → ∀{σ} → Tm Γ σ → Tm Δ σ
>> sub f (var x)   = f x
>> sub f (app t u) = app (sub f t) (sub f u)
>> sub f (lam t)   = lam (sub (lift f) t)
>>
>> subId : ∀{Γ} → Sub Γ Γ
>> subId = var
>>
>> subComp : ∀{B Γ Δ} → Sub Γ Δ → Sub B Γ → Sub B Δ
>> subComp f g = sub f • g
>>
>> liftid : ∀{Γ σ τ}(x : Var (Γ<  σ) τ) → lift subId x ≅ subId x
>> liftid vz     = refl
>> liftid (vs x) = refl
>>
>> -- first monad law, the second holds definitionally
>> subid : ∀{Γ σ}(t : Tm Γ σ) → sub subId t ≅ id t
>> subid (var x)   = refl
>> subid (app t u) = resp2 app (subid t) (subid u)
>> subid (lam t)   = resp lam (trans (resp (λ (f : Sub _ _) → sub f t)
>>                                         (iext λ _ → ext liftid))
>>                                   (subid t))
>>
>> liftwk : ∀{B Γ Δ}(f : Sub Γ Δ)(g : Ren B Γ){σ τ}(x : Var (B<  σ) τ) →
>>             (lift f • wk g) x ≅ lift (f • g) x
>> liftwk f g vz     = refl
>> liftwk f g (vs x) = refl
>>
>> subren : ∀{B Γ Δ}(f : Sub Γ Δ)(g : Ren B Γ){σ}(t : Tm B σ) →
>>          (sub f • ren g) t ≅ sub (f • g) t
>> subren f g (var x)   = refl
>> subren f g (app t u) = resp2 app (subren f g t) (subren f g u)
>> subren f g (lam t)   = resp lam (trans (subren (lift f) (wk g) t)
>>                                        (resp (λ (f : Sub _ _) → sub f t)
>>                                              (iext λ _ → ext (liftwk f
>> g))))
>>
>> renwklift : ∀{B Γ Δ}(f : Ren Γ Δ)(g : Sub B Γ){σ τ}(x : Var (B<  σ) τ) →
>>                (ren (wk f) • lift g) x ≅ lift (ren f • g) x
>> renwklift f g vz     = refl
>> renwklift f g (vs x) = trans (sym (rencomp (wk f) vs (g x)))
>>                                 (rencomp vs f (g x))
>>
>> rensub : ∀{B Γ Δ}(f : Ren Γ Δ)(g : Sub B Γ){σ}(t : Tm B σ) →
>>          (ren f •  sub g) t ≅ sub (ren f • g) t
>> rensub f g (var x)   = refl
>> rensub f g (app t u) = resp2 app (rensub f g t) (rensub f g u)
>> rensub f g (lam t)   = resp lam (trans (rensub (wk f) (lift g) t)
>>                                        (resp (λ (f : Sub _ _) → sub f t)
>>                                              (iext λ _ →
>>                                                ext (renwklift f g))))
>>
>> liftcomp : ∀{B Γ Δ}(f : Sub Γ Δ)(g : Sub B Γ){σ τ}(x : Var (B<  σ) τ) →
>>            lift (subComp f g) x ≅ subComp (lift f) (lift g) x
>> liftcomp f g vz     = refl
>> liftcomp f g (vs x) = trans (rensub vs f (g x))
>>                             (sym (subren (lift f) vs (g x)))
>>
>>
>> subcomp : ∀{B Γ Δ}(f : Sub Γ Δ)(g : Sub B Γ){σ}(t : Tm B σ) →
>>           sub (subComp f g) t ≅ (sub f • sub g) t
>> subcomp f g (var x)   = refl
>> subcomp f g (app t u) = resp2 app (subcomp f g t) (subcomp f g u)
>> subcomp f g (lam t)   = resp lam (trans (resp (λ (f : Sub _ _) → sub f t)
>>                                               (iext λ _ → ext (liftcomp f
>> g)))
>>                                         (subcomp (lift f) (lift g) t))
>>
>> Regards,
>>
>> James
>
```
```_______________________________________________
Agda mailing list
Agda@...
https://lists.chalmers.se/mailman/listinfo/agda
```
5 Nov 2011 20:14

```Fair enough, if you phrase the Kripke structure in terms of subcontext
inclusion rather than context extension, then I can see how it goes

A.

On 11/05/2011 05:47 AM, James Chapman wrote:
> I haven't tried an NBE proof with the version of renaming and
> substitution I posted yesterday. I have done something similar during
> my PhD. I used OPEs in the end (which I described early in this thread
> and Randy pointed to copious prior art).
>
> data OPE : Con ->  Con ->  Set where
>    done : OPE ε ε
>    keep : forall {Γ Δ} σ ->  OPE Γ Δ ->  OPE (Γ<  σ) (Δ<  σ)
>    skip : forall {Γ Δ} σ ->  OPE Γ Δ ->  OPE (Γ<  σ) Δ
>
> I had exactly this problem as you, for me it was with kripke logical
> predicates. Instead of defining the kripke-like part as saying:
>
> /a strongly computable function is one that given an strongly
> computable  argument in an extended context, and after weakening the
> function so that it is in the same context, will give a strongly
> computable result./
>
> I defined it using the kripke like bit of strong computability roughly
> as follows:
>
> SCV : forall {Γ σ} ->  Val Γ σ ->  Set
> SCV {Γ} {σ ⇒ τ} v       = forall {B}(f : OPE B Γ)(a : Val B σ) ->  SCV a ->
>    SCV  {B} {τ} (oapp f v \$\$ a)
> SCV ...
>
> i.e. /a strongly computable function is one that given a strongly
> computable argument in an arbitrary context B, and a order preserving
> embedding from the functions context Γ into B, and after applying the
> embedding to the function, we get a strongly computable result./
>
> The context B is arbitrary but OPE Γ B is only inhabited if B is
> 'larger'. applying oapp twice (composing them) doesn't lead to the
> same problem as your weaken as the source and target contexts are just
> variables, just like composing functions. OPEs are exactly the
> renamings which don't shrink the context and hence useful here.
>
> Regards,
>
> James
>
> On Fri, Nov 4, 2011 at 7:55 PM, Alan Jeffrey<ajeffrey@...>  wrote:
>> OK, that's pretty cool. The nasty case which hit me was proving properties
>> like "weakening of weakening is weakening":
>>
>>   weaken* A (weaken* B M) ≡ weaken* (A ++ B) M
>>
>> which you can't even state without putting in some explicit associators.
>>
>> This came up in the context of normalization by evaluation, which needs a
>> Kripke-like structure which extends the context on every function
>> application. Associators were really getting in the way, as I was needing to
>> prove a bunch of coherence properties. Have you tried getting an NBE proof
>> to go through in your setting?
>>
>> A.
>>
>> On 11/04/2011 06:29 AM, James Chapman wrote:
>>>
>>> Dear Alan + all,
>>>
>>> On Wed, Nov 2, 2011 at 6:26 PM, Alan Jeffrey<ajeffrey@...>
>>>   wrote:
>>>>
>>>> lambda-calculi. I've now worked through some of the details, and here is
>>>> the
>>>> syntax of the simply-typed lambda-calculus.
>>>
>>> For contrast, here's renaming and substitution for well typed lambda
>>> terms. Renamings are just functions from variables to variables,
>>> substitutions are just functions form variables to terms. No clever
>>> representations here, no clever getting them both as a instance of a
>>> more general operation, I just wanted to use the interface to
>>> substitution suggested by the (relative) monadic nature of well-typed
>>> terms. The proof is a simplification of the paper proof in Altenkirch
>>> and Reus' paper "Monadic presentations of lambda terms using
>>> generalized inductive types" and follows the approximately the same
>>> structure. The development goes up to proving that the substitution
>>> operation commutes with composition of substitutions (just composition
>>> of functions) -- the third monad law. It's about 170 lines in all
>>> including the utilities prelude.
>>>
>>> module WellTypedTerms where
>>>
>>> -- Utilities
>>> data _≅_ {A : Set} : {A' : Set} → A → A' → Set where
>>>    refl : {a : A} → a ≅ a
>>>
>>> trans : ∀{A A' A''}{a : A}{a' : A'}{a'' : A''} → a ≅ a' → a' ≅ a'' → a ≅
>>> a''
>>> trans refl p = p
>>>
>>> sym : ∀{A A'}{a : A}{a' : A'} → a ≅ a' → a' ≅ a
>>> sym refl = refl
>>>
>>> resp : ∀{A}{B : A → Set}(f : ∀ a → B a){a a' : A} → a ≅ a' → f a ≅ f a'
>>> resp f refl = refl
>>>
>>> resp2 : ∀{A}{B : A → Set}{C : (x : A) → B x → Set}(f : (x : A)(y : B
>>> x) → C x y){a a' : A} → a ≅ a' → {b : B a}{b' : B a'} → b ≅ b' → f a b
>>> ≅ f a' b'
>>> resp2 f refl refl = refl
>>>
>>> _•_ : {A : Set}{B : A → Set}{C : (a : A) → B a → Set} →
>>>        (∀{a} b → C a b) → (g : (∀ a → B a)) → ∀ a → C a (g a)
>>> f • g = λ a → f (g a)
>>>
>>> id : {A : Set} → A → A
>>> id a = a
>>>
>>> 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} { {a : A} → B' a} f g
>>>
>>> postulate ext : {A : Set}{B B' : A → Set}{f : ∀ a → B a}{g : ∀ a → B' a} →
>>>                  (∀ a → f a ≅ g a) → f ≅ g
>>>
>>> --Well type lambda terms
>>>
>>> data Ty : Set where
>>>    ι   : Ty
>>>    _⇒_ : Ty → Ty → Ty
>>>
>>> data Con : Set where
>>>    ε   : Con
>>>    _<_ : Con → Ty → Con
>>>
>>> data Var : Con → Ty → Set where
>>>    vz : ∀{Γ σ} → Var (Γ<    σ) σ
>>>    vs : ∀{Γ σ τ} → Var Γ σ → Var (Γ<    τ) σ
>>>
>>> data Tm : Con → Ty → Set where
>>>    var : ∀{Γ σ} → Var Γ σ → Tm Γ σ
>>>    app : ∀{Γ σ τ} → Tm Γ (σ ⇒ τ) → Tm Γ σ → Tm Γ τ
>>>    lam : ∀{Γ σ τ} → Tm (Γ<    σ) τ → Tm Γ (σ ⇒ τ)
>>>
>>> -- Renaming
>>>
>>> Ren : Con → Con → Set
>>> Ren Γ Δ = ∀ {σ} → Var Γ σ → Var Δ σ
>>>
>>> renId : ∀{Γ} → Ren Γ Γ
>>> renId = id
>>>
>>> renComp : ∀{B Γ Δ} → Ren Γ Δ → Ren B Γ → Ren B Δ
>>> renComp f g = f • g
>>>
>>> wk : ∀{Γ Δ σ} → Ren Γ Δ → Ren (Γ<    σ) (Δ<    σ)
>>> wk f vz     = vz
>>> wk f (vs i) = vs (f i)
>>>
>>> ren : ∀{Γ Δ} → Ren Γ Δ → ∀ {σ} → Tm Γ σ → Tm Δ σ
>>> ren f (var x)   = var (f x)
>>> ren f (app t u) = app (ren f t) (ren f u)
>>> ren f (lam t)   = lam (ren (wk f) t)
>>>
>>> wkid : ∀{Γ σ τ}(x : Var (Γ<    τ) σ) → wk renId x ≅ renId x
>>> wkid vz     = refl
>>> wkid (vs x) = refl
>>>
>>> renid : ∀{Γ σ}(t : Tm Γ σ) → ren renId t ≅ id t
>>> renid (var x)   = refl
>>> renid (app t u) = resp2 app (renid t) (renid u)
>>> renid (lam t) = resp lam (trans (resp (λ (f : Ren _ _) → ren f t)
>>>                                        (iext (λ _ → ext wkid)))
>>>                                  (renid t))
>>>
>>> wkcomp : ∀ {B Γ Δ}(f : Ren Γ Δ)(g : Ren B Γ){σ τ}(x : Var (B<    σ) τ) →
>>>              wk (renComp f g) x ≅ renComp (wk f) (wk g) x
>>> wkcomp f g vz     = refl
>>> wkcomp f g (vs i) = refl
>>>
>>> rencomp : ∀ {B Γ Δ}(f : Ren Γ Δ)(g : Ren B Γ){σ}(t : Tm B σ) →
>>>              ren (renComp f g) t ≅ (ren f • ren g) t
>>> rencomp f g (var x)   = refl
>>> rencomp f g (app t u) = resp2 app (rencomp f g t) (rencomp f g u)
>>> rencomp f g (lam t)   = resp lam (trans (resp (λ (f : Ren _ _) → ren f t)
>>>                                                (iext λ _ → ext (wkcomp f
>>> g)))
>>>                                          (rencomp (wk f) (wk g) t))
>>>
>>> -- Substitutions
>>>
>>> Sub : Con → Con → Set
>>> Sub Γ Δ = ∀{σ} → Var Γ σ → Tm Δ σ
>>>
>>> lift : ∀{Γ Δ σ} → Sub Γ Δ → Sub (Γ<    σ) (Δ<    σ)
>>> lift f vz     = var vz
>>> lift f (vs x) = ren vs (f x)
>>>
>>> sub : ∀{Γ Δ} → Sub Γ Δ → ∀{σ} → Tm Γ σ → Tm Δ σ
>>> sub f (var x)   = f x
>>> sub f (app t u) = app (sub f t) (sub f u)
>>> sub f (lam t)   = lam (sub (lift f) t)
>>>
>>> subId : ∀{Γ} → Sub Γ Γ
>>> subId = var
>>>
>>> subComp : ∀{B Γ Δ} → Sub Γ Δ → Sub B Γ → Sub B Δ
>>> subComp f g = sub f • g
>>>
>>> liftid : ∀{Γ σ τ}(x : Var (Γ<    σ) τ) → lift subId x ≅ subId x
>>> liftid vz     = refl
>>> liftid (vs x) = refl
>>>
>>> -- first monad law, the second holds definitionally
>>> subid : ∀{Γ σ}(t : Tm Γ σ) → sub subId t ≅ id t
>>> subid (var x)   = refl
>>> subid (app t u) = resp2 app (subid t) (subid u)
>>> subid (lam t)   = resp lam (trans (resp (λ (f : Sub _ _) → sub f t)
>>>                                          (iext λ _ → ext liftid))
>>>                                    (subid t))
>>>
>>> liftwk : ∀{B Γ Δ}(f : Sub Γ Δ)(g : Ren B Γ){σ τ}(x : Var (B<    σ) τ) →
>>>              (lift f • wk g) x ≅ lift (f • g) x
>>> liftwk f g vz     = refl
>>> liftwk f g (vs x) = refl
>>>
>>> subren : ∀{B Γ Δ}(f : Sub Γ Δ)(g : Ren B Γ){σ}(t : Tm B σ) →
>>>           (sub f • ren g) t ≅ sub (f • g) t
>>> subren f g (var x)   = refl
>>> subren f g (app t u) = resp2 app (subren f g t) (subren f g u)
>>> subren f g (lam t)   = resp lam (trans (subren (lift f) (wk g) t)
>>>                                         (resp (λ (f : Sub _ _) → sub f t)
>>>                                               (iext λ _ → ext (liftwk f
>>> g))))
>>>
>>> renwklift : ∀{B Γ Δ}(f : Ren Γ Δ)(g : Sub B Γ){σ τ}(x : Var (B<    σ) τ) →
>>>                 (ren (wk f) • lift g) x ≅ lift (ren f • g) x
>>> renwklift f g vz     = refl
>>> renwklift f g (vs x) = trans (sym (rencomp (wk f) vs (g x)))
>>>                                  (rencomp vs f (g x))
>>>
>>> rensub : ∀{B Γ Δ}(f : Ren Γ Δ)(g : Sub B Γ){σ}(t : Tm B σ) →
>>>           (ren f •  sub g) t ≅ sub (ren f • g) t
>>> rensub f g (var x)   = refl
>>> rensub f g (app t u) = resp2 app (rensub f g t) (rensub f g u)
>>> rensub f g (lam t)   = resp lam (trans (rensub (wk f) (lift g) t)
>>>                                         (resp (λ (f : Sub _ _) → sub f t)
>>>                                               (iext λ _ →
>>>                                                 ext (renwklift f g))))
>>>
>>> liftcomp : ∀{B Γ Δ}(f : Sub Γ Δ)(g : Sub B Γ){σ τ}(x : Var (B<    σ) τ) →
>>>             lift (subComp f g) x ≅ subComp (lift f) (lift g) x
>>> liftcomp f g vz     = refl
>>> liftcomp f g (vs x) = trans (rensub vs f (g x))
>>>                              (sym (subren (lift f) vs (g x)))
>>>
>>>
>>> subcomp : ∀{B Γ Δ}(f : Sub Γ Δ)(g : Sub B Γ){σ}(t : Tm B σ) →
>>>            sub (subComp f g) t ≅ (sub f • sub g) t
>>> subcomp f g (var x)   = refl
>>> subcomp f g (app t u) = resp2 app (subcomp f g t) (subcomp f g u)
>>> subcomp f g (lam t)   = resp lam (trans (resp (λ (f : Sub _ _) → sub f t)
>>>                                                (iext λ _ → ext (liftcomp f
>>> g)))
>>>                                          (subcomp (lift f) (lift g) t))
>>>
>>> Regards,
>>>
>>> James
>>
```
6 Nov 2011 20:14

```On Sat, Nov 5, 2011 at 8:14 PM, Alan Jeffrey <ajeffrey@...> wrote:
> Fair enough, if you phrase the Kripke structure in terms of subcontext
> inclusion rather than context extension, then I can see how it goes through

Exactly, and arbitrary renamings seem to do the work here (scroll to
the bottom):
```
21 Nov 2011 20:17

```I've now finished up the NBE algorithm for the simply-typed
lambda-calculus. It defines a reduction semantics, and uses NBE to show
that every term reduces to one in normal form.

At this point, I'm afraid I think of this as an interesting idea, but
one where some pragmatic nastiness gets in the way of it being useful.
The main problems are:

- Huge normal forms, which slow Agda down horribly.

- Incomprehensible normal forms, which make debugging remarkably difficult.

- Less unification -- from unifying (a :: as) with (b :: bs) Agda
doesn't unify a with b or as with bs.

The implementation is up at https://github.com/agda/agda-assoc-free

A.

On 11/02/2011 11:26 AM, Jeffrey, Alan S A (Alan) wrote:
> Hi everyone,
>
> lambda-calculi. I've now worked through some of the details, and here is
> the syntax of the simply-typed lambda-calculus:
>
>> https://github.com/agda/agda-frp-js/blob/master/src/agda/FRP/JS/Model/STLambdaC/Exp.agda
>
> The interesting thing is weakening, with type:
>
>     weaken+ : ∀ B Γ Δ {T} → Exp (B ++ Δ) T → Exp (B ++ Γ ++ Δ) T
>
> and (news just in!) weakening commutes with itself (up to propositional
> equality):
>
>     weaken+ Φ Ψ (B ++ Γ ++ Δ) (weaken+ (Φ ++ B) Γ Δ M)
>       ≡ weaken+ (Φ ++ Ψ ++ B) Γ Δ (weaken+ Φ Ψ (B ++ Δ) M)
>
> Note that you can't even state this property without associativity on
> the nose, since the lhs has type (Φ ++ Ψ ++ (B ++ Γ ++ Δ)) and the rhs
> has type ((Φ ++ Ψ ++ B) ++ Γ ++ Δ).
>
> The proof makes use of a list-membership type, defined in:
>
>> https://github.com/agda/agda-frp-js/blob/master/src/agda/FRP/JS/DList.agda
>
> It satisfies weakening on the left and right:
>
>     _≪_ : ∀ {A a as} → (a ∈ as) → ∀ bs → (a ∈ (as ++ bs))
>     _≫_ : ∀ {A a bs} → ∀ as → (a ∈ bs) → (a ∈ (as ++ bs))
>
> and moreover has left and right units and associativity properties, all
> up to beta-equivalence (that is, all these properties have proof refl):
>
>     (a∈as ≪ []) ≡ a∈as
>     ([] ≫ a∈as) ≡ a∈as
>     (a∈as ≪ bs ≪ cs) ≡ (a∈as ≪ bs ++ cs)
>     ((as ≫ a∈bs) ≪ cs) ≡ (as ≫ (a∈bs ≪ cs))
>     (as ≫ bs ≫ a∈cs) ≡ (as ≫ bs ≫ a∈cs)
>
> Under the hood, this is implemented in terms of difference naturals
> (that is an implementation of ℕ where + and ♯0 form a monoid up to
> beta-equivalence), and an implementation of difference lists such that
> the length function is a monoid homomorphism up to beta-equivalence:
>
>     (len (as ++ bs) ≡ (len as + len bs))
>     (len [] ≡ ♯0)
>
> With all that in place, the proof of weakening is pretty
> straightforward. The only case which requires any work is variables, and
> a typical case is:
>
>     begin
>       xweaken+ Φ Ψ (B ++ Γ ++ Δ) (case Φ (B ++ Γ ++ Δ) (Φ ≫ x ≪ Γ ≪ Δ))
>     ≡⟨ cong (xweaken+ Φ Ψ (B ++ Γ ++ Δ)) (case-≫ Φ (x ≪ Γ ≪ Δ)) ⟩
>       (Φ ≫ Ψ ≫ x ≪ Γ ≪ Δ)
>     ≡⟨ cong (xweaken+ (Φ ++ Ψ ++ B) Γ Δ) (sym (case-≪ (Φ ≫ Ψ ≫ x) Δ)) ⟩
>       xweaken+ (Φ ++ Ψ ++ B) Γ Δ (case (Φ ++ Ψ ++ B) Δ (Φ ≫ Ψ ≫ x ≪ Δ))
>     ∎
>
> I don't really want to think about what this proof would look like with
> all the associativity wiring made explicit.
>
> There is still a bit of annoying associativity left, because I can't see
> how to get coproducts to associate on the nose, so there's lots of gore
> needed to define a case function:
>
>     data Case {A} a (as bs : List A) : Set where
>       inj₁ : (a∈as : a ∈ as) → Case a as bs
>       inj₂ : (a∈bs : a ∈ bs) → Case a as bs
>
>     case : ∀ {A a} as bs → (a ∈ (as ++ bs)) → Case {A} a as bs
>
> and then prove that it satisfies associativity (up to propositional
> equality, not beta-equivalence).
>
> A.
>
> On 10/26/2011 09:48 AM, Jeffrey, Alan S A (Alan) wrote:
>> Hi everyone,
>>
>> A quick note about a trick for representing lists (or any other monoid)
>> up to associativity. Am I reinventing a wheel here?
>>
>> I've been doing some mucking around recently with proofs about
>> lambda-calculi and was hitting annoying problems with associativity
>> on lists. A prototypical example is:
>>
>>      weakening : ∀ {A a} (as bs cs : List A) →
>>       (a ∈ (as ++ cs)) → (a ∈ (as ++ bs ++ cs))
>>
>> It's easy to prove that ++ is associative, but making use of that fact
>> is rather painful, as there's lots of manual wiring with subst and cong,
>> for example:
>>
>>      weaken2 : ∀ {A a} (as bs cs ds : List A) →
>>        (a ∈ (as ++ bs ++ ds)) → (a ∈ (as ++ bs ++ cs ++ ds))
>>      weaken2 {A} {a} as bs cs ds a∈es =
>>        subst (λ X → (a ∈ X)) (++-assoc as bs (cs ++ ds))
>>          (weakening (as ++ bs) cs ds
>>            (subst (λ X → (a ∈ X)) (sym (++-assoc as bs ds)) a∈es))
>>
>> This gets tiresome pretty rapidly. Oh if only there were a data
>> structure which represented lists, but for which ++ was associative up
>> to beta reduction... Oh look there already is one, it's called
>> difference lists. Quoting the standard library:
>>
>>      DiffList : Set → Set
>>      DiffList a = List a → List a
>>
>>      _++_ : ∀ {a} → DiffList a → DiffList a → DiffList a
>>      xs ++ ys = λ k → xs (ys k)
>>
>> Unfortunately, difference lists are not isomorphic to lists: there's a
>> lot more functions on lists than just concatenation functions. This
>> causes headaches (e.g. writing inductive functions on difference lists).
>>
>> A first shot at fixing this is to write a data structure for those
>> difference lists which are concatenations:
>>
>>      record Seq (A : Set) : Set where
>>        constructor seq
>>        field
>>          list : List A
>>          fun : List A → List A
>>          ok : fun ≡ _++_ list  -- Broken
>>
>> It's pretty straightforward to define the monoidal structure for Seq:
>>
>>      ε : ∀ {A} → Seq A
>>      ε = seq [] id refl
>>
>>       _+_ : ∀ {A} → Seq A → Seq A → Seq A
>>      (seq as f f✓) + (seq bs g g✓) = seq (f bs) (f ∘ g) (...easy lemma...)
>>
>> Unfortunately, we're back to square one again, because + is only
>> associative up to propositional equality, not beta reduction. This time,
>> it's the ok field that gets in the way. So we can fix that, and just
>> make the ok field irrelevant, that is:
>>
>>      record Seq (A : Set) : Set where
>>        constructor seq
>>        field
>>          list : List A
>>          fun : List A → List A
>>          .ok : fun ≡ _++_ list  -- Fixed
>>
>>      open Seq public renaming (list to [_])
>>
>> Hooray, + is now associative up to beta reduction:
>>
>>      +-assoc : ∀ {A} (as bs cs : Seq A) →
>>        ((as + bs) + cs) ≡ (as + (bs + cs))
>>      +-assoc as bs cs = refl
>>
>>
>>      ≡-relevant : ∀ {A : Set} {a b : A} → .(a ≡ b) → (a ≡ b)
>>
>> we can define:
>>
>>      data Case {A : Set} : Seq A → Set where
>>        [] : Case ε
>>        _∷_ : ∀ a as → Case (a ◁ as)
>>
>>      case : ∀ {A} (as : Seq A) → Case as
>>
>> and this gives us recursive functions over Seq (which somewhat to my
>> surprise actually get past the termination checker), for example:
>>
>>      ids : ∀ {A} → Seq A → Seq A
>>      ids as        with case as
>>      ids .(a ◁ as) | a ∷ as = a ◁ ids as
>>      ids .ε        | []     = ε
>>
>> For example, we can now define weakening:
>>
>>      weakening : ∀ {A a} (as bs cs : Seq A) →
>>        (a ∈ [ as + cs ]) → (a ∈ [ as + bs + cs ])
>>
>> and use it up to associativity without worrying hand-coded wiring:
>>
>>      weaken2 : ∀ {A a} (as bs cs ds : Seq A) →
>>        (a ∈ [ as + bs + ds ]) → (a ∈ [ as + bs + cs + ds ])
>>      weaken2 as bs = weakening (as + bs)
>>
>> Hooray, cake! Eating it!
>>
>> I suspect this trick works for most any monoid, so you can do
>> associativity on naturals, vectors, partial orders with join, etc. etc.
>>
>> The idea of using difference lists to represent lists is standard, but
>> as far as I know, this use of irrelevant equalities to get structural
>> recursion is new. Anyone know of any prior art?
>>
>> A.
```
22 Mar 2012 15:40

```Hi Alan,

I remembered your idea when working with Frederic Kettelhoit on an
implementation of Fingertrees which are parametrized by a monoid.

free.  Is there a way to also get the right-unit for free?

Cheers,
Andreas

On 11/21/11 8:17 PM, Alan Jeffrey wrote:
> I've now finished up the NBE algorithm for the simply-typed
> lambda-calculus. It defines a reduction semantics, and uses NBE to show
> that every term reduces to one in normal form.
>
> At this point, I'm afraid I think of this as an interesting idea, but
> one where some pragmatic nastiness gets in the way of it being useful.
> The main problems are:
>
> - Huge normal forms, which slow Agda down horribly.
>
> - Incomprehensible normal forms, which make debugging remarkably difficult.
>
> - Less unification -- from unifying (a :: as) with (b :: bs) Agda
> doesn't unify a with b or as with bs.
>
> The implementation is up at https://github.com/agda/agda-assoc-free
>
> A.
>
> On 11/02/2011 11:26 AM, Jeffrey, Alan S A (Alan) wrote:
>> Hi everyone,
>>
>> lambda-calculi. I've now worked through some of the details, and here is
>> the syntax of the simply-typed lambda-calculus:
>>
>>> https://github.com/agda/agda-frp-js/blob/master/src/agda/FRP/JS/Model/STLambdaC/Exp.agda
>>>
>>
>> The interesting thing is weakening, with type:
>>
>> weaken+ : ∀ B Γ Δ {T} → Exp (B ++ Δ) T → Exp (B ++ Γ ++ Δ) T
>>
>> and (news just in!) weakening commutes with itself (up to propositional
>> equality):
>>
>> weaken+ Φ Ψ (B ++ Γ ++ Δ) (weaken+ (Φ ++ B) Γ Δ M)
>> ≡ weaken+ (Φ ++ Ψ ++ B) Γ Δ (weaken+ Φ Ψ (B ++ Δ) M)
>>
>> Note that you can't even state this property without associativity on
>> the nose, since the lhs has type (Φ ++ Ψ ++ (B ++ Γ ++ Δ)) and the rhs
>> has type ((Φ ++ Ψ ++ B) ++ Γ ++ Δ).
>>
>> The proof makes use of a list-membership type, defined in:
>>
>>> https://github.com/agda/agda-frp-js/blob/master/src/agda/FRP/JS/DList.agda
>>>
>>
>> It satisfies weakening on the left and right:
>>
>> _≪_ : ∀ {A a as} → (a ∈ as) → ∀ bs → (a ∈ (as ++ bs))
>> _≫_ : ∀ {A a bs} → ∀ as → (a ∈ bs) → (a ∈ (as ++ bs))
>>
>> and moreover has left and right units and associativity properties, all
>> up to beta-equivalence (that is, all these properties have proof refl):
>>
>> (a∈as ≪ []) ≡ a∈as
>> ([] ≫ a∈as) ≡ a∈as
>> (a∈as ≪ bs ≪ cs) ≡ (a∈as ≪ bs ++ cs)
>> ((as ≫ a∈bs) ≪ cs) ≡ (as ≫ (a∈bs ≪ cs))
>> (as ≫ bs ≫ a∈cs) ≡ (as ≫ bs ≫ a∈cs)
>>
>> Under the hood, this is implemented in terms of difference naturals
>> (that is an implementation of ℕ where + and ♯0 form a monoid up to
>> beta-equivalence), and an implementation of difference lists such that
>> the length function is a monoid homomorphism up to beta-equivalence:
>>
>> (len (as ++ bs) ≡ (len as + len bs))
>> (len [] ≡ ♯0)
>>
>> With all that in place, the proof of weakening is pretty
>> straightforward. The only case which requires any work is variables, and
>> a typical case is:
>>
>> begin
>> xweaken+ Φ Ψ (B ++ Γ ++ Δ) (case Φ (B ++ Γ ++ Δ) (Φ ≫ x ≪ Γ ≪ Δ))
>> ≡⟨ cong (xweaken+ Φ Ψ (B ++ Γ ++ Δ)) (case-≫ Φ (x ≪ Γ ≪ Δ)) ⟩
>> (Φ ≫ Ψ ≫ x ≪ Γ ≪ Δ)
>> ≡⟨ cong (xweaken+ (Φ ++ Ψ ++ B) Γ Δ) (sym (case-≪ (Φ ≫ Ψ ≫ x) Δ)) ⟩
>> xweaken+ (Φ ++ Ψ ++ B) Γ Δ (case (Φ ++ Ψ ++ B) Δ (Φ ≫ Ψ ≫ x ≪ Δ))
>> ∎
>>
>> I don't really want to think about what this proof would look like with
>> all the associativity wiring made explicit.
>>
>> There is still a bit of annoying associativity left, because I can't see
>> how to get coproducts to associate on the nose, so there's lots of gore
>> needed to define a case function:
>>
>> data Case {A} a (as bs : List A) : Set where
>> inj₁ : (a∈as : a ∈ as) → Case a as bs
>> inj₂ : (a∈bs : a ∈ bs) → Case a as bs
>>
>> case : ∀ {A a} as bs → (a ∈ (as ++ bs)) → Case {A} a as bs
>>
>> and then prove that it satisfies associativity (up to propositional
>> equality, not beta-equivalence).
>>
>> A.
>>
>> On 10/26/2011 09:48 AM, Jeffrey, Alan S A (Alan) wrote:
>>> Hi everyone,
>>>
>>> A quick note about a trick for representing lists (or any other monoid)
>>> up to associativity. Am I reinventing a wheel here?
>>>
>>> I've been doing some mucking around recently with proofs about
>>> lambda-calculi and was hitting annoying problems with associativity
>>> on lists. A prototypical example is:
>>>
>>> weakening : ∀ {A a} (as bs cs : List A) →
>>> (a ∈ (as ++ cs)) → (a ∈ (as ++ bs ++ cs))
>>>
>>> It's easy to prove that ++ is associative, but making use of that fact
>>> is rather painful, as there's lots of manual wiring with subst and cong,
>>> for example:
>>>
>>> weaken2 : ∀ {A a} (as bs cs ds : List A) →
>>> (a ∈ (as ++ bs ++ ds)) → (a ∈ (as ++ bs ++ cs ++ ds))
>>> weaken2 {A} {a} as bs cs ds a∈es =
>>> subst (λ X → (a ∈ X)) (++-assoc as bs (cs ++ ds))
>>> (weakening (as ++ bs) cs ds
>>> (subst (λ X → (a ∈ X)) (sym (++-assoc as bs ds)) a∈es))
>>>
>>> This gets tiresome pretty rapidly. Oh if only there were a data
>>> structure which represented lists, but for which ++ was associative up
>>> to beta reduction... Oh look there already is one, it's called
>>> difference lists. Quoting the standard library:
>>>
>>> DiffList : Set → Set
>>> DiffList a = List a → List a
>>>
>>> _++_ : ∀ {a} → DiffList a → DiffList a → DiffList a
>>> xs ++ ys = λ k → xs (ys k)
>>>
>>> Unfortunately, difference lists are not isomorphic to lists: there's a
>>> lot more functions on lists than just concatenation functions. This
>>> causes headaches (e.g. writing inductive functions on difference lists).
>>>
>>> A first shot at fixing this is to write a data structure for those
>>> difference lists which are concatenations:
>>>
>>> record Seq (A : Set) : Set where
>>> constructor seq
>>> field
>>> list : List A
>>> fun : List A → List A
>>> ok : fun ≡ _++_ list -- Broken
>>>
>>> It's pretty straightforward to define the monoidal structure for Seq:
>>>
>>> ε : ∀ {A} → Seq A
>>> ε = seq [] id refl
>>>
>>> _+_ : ∀ {A} → Seq A → Seq A → Seq A
>>> (seq as f f✓) + (seq bs g g✓) = seq (f bs) (f ∘ g) (...easy lemma...)
>>>
>>> Unfortunately, we're back to square one again, because + is only
>>> associative up to propositional equality, not beta reduction. This time,
>>> it's the ok field that gets in the way. So we can fix that, and just
>>> make the ok field irrelevant, that is:
>>>
>>> record Seq (A : Set) : Set where
>>> constructor seq
>>> field
>>> list : List A
>>> fun : List A → List A
>>> .ok : fun ≡ _++_ list -- Fixed
>>>
>>> open Seq public renaming (list to [_])
>>>
>>> Hooray, + is now associative up to beta reduction:
>>>
>>> +-assoc : ∀ {A} (as bs cs : Seq A) →
>>> ((as + bs) + cs) ≡ (as + (bs + cs))
>>> +-assoc as bs cs = refl
>>>
>>>
>>> ≡-relevant : ∀ {A : Set} {a b : A} → .(a ≡ b) → (a ≡ b)
>>>
>>> we can define:
>>>
>>> data Case {A : Set} : Seq A → Set where
>>> [] : Case ε
>>> _∷_ : ∀ a as → Case (a ◁ as)
>>>
>>> case : ∀ {A} (as : Seq A) → Case as
>>>
>>> and this gives us recursive functions over Seq (which somewhat to my
>>> surprise actually get past the termination checker), for example:
>>>
>>> ids : ∀ {A} → Seq A → Seq A
>>> ids as with case as
>>> ids .(a ◁ as) | a ∷ as = a ◁ ids as
>>> ids .ε | [] = ε
>>>
>>> For example, we can now define weakening:
>>>
>>> weakening : ∀ {A a} (as bs cs : Seq A) →
>>> (a ∈ [ as + cs ]) → (a ∈ [ as + bs + cs ])
>>>
>>> and use it up to associativity without worrying hand-coded wiring:
>>>
>>> weaken2 : ∀ {A a} (as bs cs ds : Seq A) →
>>> (a ∈ [ as + bs + ds ]) → (a ∈ [ as + bs + cs + ds ])
>>> weaken2 as bs = weakening (as + bs)
>>>
>>> Hooray, cake! Eating it!
>>>
>>> I suspect this trick works for most any monoid, so you can do
>>> associativity on naturals, vectors, partial orders with join, etc. etc.
>>>
>>> The idea of using difference lists to represent lists is standard, but
>>> as far as I know, this use of irrelevant equalities to get structural
>>> recursion is new. Anyone know of any prior art?
>>>
>>> A.
> _______________________________________________
> Agda mailing list
> Agda@...
> https://lists.chalmers.se/mailman/listinfo/agda
>

--

--
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel@...
http://www2.tcs.ifi.lmu.de/~abel/
```
22 Mar 2012 15:47

```The version that's up on github does both left- and right-units as well
as associativity. The canonical example is difference naturals:

https://github.com/agda/agda-assoc-free/blob/master/src/AssocFree/DNat.agda

which includes:

-- Addition forms a monoid on the nose

+-assoc : ∀ l m n → (((l + m) + n) ≡ (l + (m + n)))
+-assoc l m n = refl

+-unit₁ : ∀ n → ((♯0 + n) ≡ n)
+-unit₁ n = refl

+-unit₂ : ∀ n → ((n + ♯0) ≡ n)
+-unit₂ n = refl

Don't forget what I said about incomprehensible and huge normal forms
getting in the way of debugging!

A.

On 03/22/2012 09:40 AM, Andreas Abel wrote:
> Hi Alan,
>
> I remembered your idea when working with Frederic Kettelhoit on an
> implementation of Fingertrees which are parametrized by a monoid.
>
> free.  Is there a way to also get the right-unit for free?
>
> Cheers,
> Andreas
>
> On 11/21/11 8:17 PM, Alan Jeffrey wrote:
>> I've now finished up the NBE algorithm for the simply-typed
>> lambda-calculus. It defines a reduction semantics, and uses NBE to show
>> that every term reduces to one in normal form.
>>
>> At this point, I'm afraid I think of this as an interesting idea, but
>> one where some pragmatic nastiness gets in the way of it being useful.
>> The main problems are:
>>
>> - Huge normal forms, which slow Agda down horribly.
>>
>> - Incomprehensible normal forms, which make debugging remarkably difficult.
>>
>> - Less unification -- from unifying (a :: as) with (b :: bs) Agda
>> doesn't unify a with b or as with bs.
>>
>> The implementation is up at https://github.com/agda/agda-assoc-free
>>
>> A.
>>
>> On 11/02/2011 11:26 AM, Jeffrey, Alan S A (Alan) wrote:
>>> Hi everyone,
>>>
>>> lambda-calculi. I've now worked through some of the details, and here is
>>> the syntax of the simply-typed lambda-calculus:
>>>
>>>> https://github.com/agda/agda-frp-js/blob/master/src/agda/FRP/JS/Model/STLambdaC/Exp.agda
>>>>
>>>
>>> The interesting thing is weakening, with type:
>>>
>>> weaken+ : ∀ B Γ Δ {T} → Exp (B ++ Δ) T → Exp (B ++ Γ ++ Δ) T
>>>
>>> and (news just in!) weakening commutes with itself (up to propositional
>>> equality):
>>>
>>> weaken+ Φ Ψ (B ++ Γ ++ Δ) (weaken+ (Φ ++ B) Γ Δ M)
>>> ≡ weaken+ (Φ ++ Ψ ++ B) Γ Δ (weaken+ Φ Ψ (B ++ Δ) M)
>>>
>>> Note that you can't even state this property without associativity on
>>> the nose, since the lhs has type (Φ ++ Ψ ++ (B ++ Γ ++ Δ)) and the rhs
>>> has type ((Φ ++ Ψ ++ B) ++ Γ ++ Δ).
>>>
>>> The proof makes use of a list-membership type, defined in:
>>>
>>>> https://github.com/agda/agda-frp-js/blob/master/src/agda/FRP/JS/DList.agda
>>>>
>>>
>>> It satisfies weakening on the left and right:
>>>
>>> _≪_ : ∀ {A a as} → (a ∈ as) → ∀ bs → (a ∈ (as ++ bs))
>>> _≫_ : ∀ {A a bs} → ∀ as → (a ∈ bs) → (a ∈ (as ++ bs))
>>>
>>> and moreover has left and right units and associativity properties, all
>>> up to beta-equivalence (that is, all these properties have proof refl):
>>>
>>> (a∈as ≪ []) ≡ a∈as
>>> ([] ≫ a∈as) ≡ a∈as
>>> (a∈as ≪ bs ≪ cs) ≡ (a∈as ≪ bs ++ cs)
>>> ((as ≫ a∈bs) ≪ cs) ≡ (as ≫ (a∈bs ≪ cs))
>>> (as ≫ bs ≫ a∈cs) ≡ (as ≫ bs ≫ a∈cs)
>>>
>>> Under the hood, this is implemented in terms of difference naturals
>>> (that is an implementation of ℕ where + and ♯0 form a monoid up to
>>> beta-equivalence), and an implementation of difference lists such that
>>> the length function is a monoid homomorphism up to beta-equivalence:
>>>
>>> (len (as ++ bs) ≡ (len as + len bs))
>>> (len [] ≡ ♯0)
>>>
>>> With all that in place, the proof of weakening is pretty
>>> straightforward. The only case which requires any work is variables, and
>>> a typical case is:
>>>
>>> begin
>>> xweaken+ Φ Ψ (B ++ Γ ++ Δ) (case Φ (B ++ Γ ++ Δ) (Φ ≫ x ≪ Γ ≪ Δ))
>>> ≡⟨ cong (xweaken+ Φ Ψ (B ++ Γ ++ Δ)) (case-≫ Φ (x ≪ Γ ≪ Δ)) ⟩
>>> (Φ ≫ Ψ ≫ x ≪ Γ ≪ Δ)
>>> ≡⟨ cong (xweaken+ (Φ ++ Ψ ++ B) Γ Δ) (sym (case-≪ (Φ ≫ Ψ ≫ x) Δ)) ⟩
>>> xweaken+ (Φ ++ Ψ ++ B) Γ Δ (case (Φ ++ Ψ ++ B) Δ (Φ ≫ Ψ ≫ x ≪ Δ))
>>> ∎
>>>
>>> I don't really want to think about what this proof would look like with
>>> all the associativity wiring made explicit.
>>>
>>> There is still a bit of annoying associativity left, because I can't see
>>> how to get coproducts to associate on the nose, so there's lots of gore
>>> needed to define a case function:
>>>
>>> data Case {A} a (as bs : List A) : Set where
>>> inj₁ : (a∈as : a ∈ as) → Case a as bs
>>> inj₂ : (a∈bs : a ∈ bs) → Case a as bs
>>>
>>> case : ∀ {A a} as bs → (a ∈ (as ++ bs)) → Case {A} a as bs
>>>
>>> and then prove that it satisfies associativity (up to propositional
>>> equality, not beta-equivalence).
>>>
>>> A.
>>>
>>> On 10/26/2011 09:48 AM, Jeffrey, Alan S A (Alan) wrote:
>>>> Hi everyone,
>>>>
>>>> A quick note about a trick for representing lists (or any other monoid)
>>>> up to associativity. Am I reinventing a wheel here?
>>>>
>>>> I've been doing some mucking around recently with proofs about
>>>> lambda-calculi and was hitting annoying problems with associativity
>>>> on lists. A prototypical example is:
>>>>
>>>> weakening : ∀ {A a} (as bs cs : List A) →
>>>> (a ∈ (as ++ cs)) → (a ∈ (as ++ bs ++ cs))
>>>>
>>>> It's easy to prove that ++ is associative, but making use of that fact
>>>> is rather painful, as there's lots of manual wiring with subst and cong,
>>>> for example:
>>>>
>>>> weaken2 : ∀ {A a} (as bs cs ds : List A) →
>>>> (a ∈ (as ++ bs ++ ds)) → (a ∈ (as ++ bs ++ cs ++ ds))
>>>> weaken2 {A} {a} as bs cs ds a∈es =
>>>> subst (λ X → (a ∈ X)) (++-assoc as bs (cs ++ ds))
>>>> (weakening (as ++ bs) cs ds
>>>> (subst (λ X → (a ∈ X)) (sym (++-assoc as bs ds)) a∈es))
>>>>
>>>> This gets tiresome pretty rapidly. Oh if only there were a data
>>>> structure which represented lists, but for which ++ was associative up
>>>> to beta reduction... Oh look there already is one, it's called
>>>> difference lists. Quoting the standard library:
>>>>
>>>> DiffList : Set → Set
>>>> DiffList a = List a → List a
>>>>
>>>> _++_ : ∀ {a} → DiffList a → DiffList a → DiffList a
>>>> xs ++ ys = λ k → xs (ys k)
>>>>
>>>> Unfortunately, difference lists are not isomorphic to lists: there's a
>>>> lot more functions on lists than just concatenation functions. This
>>>> causes headaches (e.g. writing inductive functions on difference lists).
>>>>
>>>> A first shot at fixing this is to write a data structure for those
>>>> difference lists which are concatenations:
>>>>
>>>> record Seq (A : Set) : Set where
>>>> constructor seq
>>>> field
>>>> list : List A
>>>> fun : List A → List A
>>>> ok : fun ≡ _++_ list -- Broken
>>>>
>>>> It's pretty straightforward to define the monoidal structure for Seq:
>>>>
>>>> ε : ∀ {A} → Seq A
>>>> ε = seq [] id refl
>>>>
>>>> _+_ : ∀ {A} → Seq A → Seq A → Seq A
>>>> (seq as f f✓) + (seq bs g g✓) = seq (f bs) (f ∘ g) (...easy lemma...)
>>>>
>>>> Unfortunately, we're back to square one again, because + is only
>>>> associative up to propositional equality, not beta reduction. This time,
>>>> it's the ok field that gets in the way. So we can fix that, and just
>>>> make the ok field irrelevant, that is:
>>>>
>>>> record Seq (A : Set) : Set where
>>>> constructor seq
>>>> field
>>>> list : List A
>>>> fun : List A → List A
>>>> .ok : fun ≡ _++_ list -- Fixed
>>>>
>>>> open Seq public renaming (list to [_])
>>>>
>>>> Hooray, + is now associative up to beta reduction:
>>>>
>>>> +-assoc : ∀ {A} (as bs cs : Seq A) →
>>>> ((as + bs) + cs) ≡ (as + (bs + cs))
>>>> +-assoc as bs cs = refl
>>>>
>>>>
>>>> ≡-relevant : ∀ {A : Set} {a b : A} → .(a ≡ b) → (a ≡ b)
>>>>
>>>> we can define:
>>>>
>>>> data Case {A : Set} : Seq A → Set where
>>>> [] : Case ε
>>>> _∷_ : ∀ a as → Case (a ◁ as)
>>>>
>>>> case : ∀ {A} (as : Seq A) → Case as
>>>>
>>>> and this gives us recursive functions over Seq (which somewhat to my
>>>> surprise actually get past the termination checker), for example:
>>>>
>>>> ids : ∀ {A} → Seq A → Seq A
>>>> ids as with case as
>>>> ids .(a ◁ as) | a ∷ as = a ◁ ids as
>>>> ids .ε | [] = ε
>>>>
>>>> For example, we can now define weakening:
>>>>
>>>> weakening : ∀ {A a} (as bs cs : Seq A) →
>>>> (a ∈ [ as + cs ]) → (a ∈ [ as + bs + cs ])
>>>>
>>>> and use it up to associativity without worrying hand-coded wiring:
>>>>
>>>> weaken2 : ∀ {A a} (as bs cs ds : Seq A) →
>>>> (a ∈ [ as + bs + ds ]) → (a ∈ [ as + bs + cs + ds ])
>>>> weaken2 as bs = weakening (as + bs)
>>>>
>>>> Hooray, cake! Eating it!
>>>>
>>>> I suspect this trick works for most any monoid, so you can do
>>>> associativity on naturals, vectors, partial orders with join, etc. etc.
>>>>
>>>> The idea of using difference lists to represent lists is standard, but
>>>> as far as I know, this use of irrelevant equalities to get structural
>>>> recursion is new. Anyone know of any prior art?
>>>>
>>>> A.
>> _______________________________________________
>> Agda mailing list
>> Agda@...
>> https://lists.chalmers.se/mailman/listinfo/agda
>>
>
```
22 Mar 2012 17:22

```Thanks!

That extra comes with your revised definition of difference lists.
Sounds good!

Is it that the irrelevant proofs show up in the error messages always?
Maybe it would be helpful to be able to switch of printing of irrelevant
terms?

Cheers,
Andreas

On 3/22/12 3:47 PM, Alan Jeffrey wrote:
> The version that's up on github does both left- and right-units as well
> as associativity. The canonical example is difference naturals:
>
>
> https://github.com/agda/agda-assoc-free/blob/master/src/AssocFree/DNat.agda
>
> which includes:
>
> -- Addition forms a monoid on the nose
>
> +-assoc : ∀ l m n → (((l + m) + n) ≡ (l + (m + n)))
> +-assoc l m n = refl
>
> +-unit₁ : ∀ n → ((♯0 + n) ≡ n)
> +-unit₁ n = refl
>
> +-unit₂ : ∀ n → ((n + ♯0) ≡ n)
> +-unit₂ n = refl
>
> Don't forget what I said about incomprehensible and huge normal forms
> getting in the way of debugging!
>
> A.
>
> On 03/22/2012 09:40 AM, Andreas Abel wrote:
>> Hi Alan,
>>
>> I remembered your idea when working with Frederic Kettelhoit on an
>> implementation of Fingertrees which are parametrized by a monoid.
>>
>> free. Is there a way to also get the right-unit for free?
>>
>> Cheers,
>> Andreas
>>
>> On 11/21/11 8:17 PM, Alan Jeffrey wrote:
>>> I've now finished up the NBE algorithm for the simply-typed
>>> lambda-calculus. It defines a reduction semantics, and uses NBE to show
>>> that every term reduces to one in normal form.
>>>
>>> At this point, I'm afraid I think of this as an interesting idea, but
>>> one where some pragmatic nastiness gets in the way of it being useful.
>>> The main problems are:
>>>
>>> - Huge normal forms, which slow Agda down horribly.
>>>
>>> - Incomprehensible normal forms, which make debugging remarkably
>>> difficult.
>>>
>>> - Less unification -- from unifying (a :: as) with (b :: bs) Agda
>>> doesn't unify a with b or as with bs.
>>>
>>> The implementation is up at https://github.com/agda/agda-assoc-free
>>>
>>> A.
>>>
>>> On 11/02/2011 11:26 AM, Jeffrey, Alan S A (Alan) wrote:
>>>> Hi everyone,
>>>>
>>>> lambda-calculi. I've now worked through some of the details, and
>>>> here is
>>>> the syntax of the simply-typed lambda-calculus:
>>>>
>>>>> https://github.com/agda/agda-frp-js/blob/master/src/agda/FRP/JS/Model/STLambdaC/Exp.agda
>>>>>
>>>>>
>>>>
>>>> The interesting thing is weakening, with type:
>>>>
>>>> weaken+ : ∀ B Γ Δ {T} → Exp (B ++ Δ) T → Exp (B ++ Γ ++ Δ) T
>>>>
>>>> and (news just in!) weakening commutes with itself (up to propositional
>>>> equality):
>>>>
>>>> weaken+ Φ Ψ (B ++ Γ ++ Δ) (weaken+ (Φ ++ B) Γ Δ M)
>>>> ≡ weaken+ (Φ ++ Ψ ++ B) Γ Δ (weaken+ Φ Ψ (B ++ Δ) M)
>>>>
>>>> Note that you can't even state this property without associativity on
>>>> the nose, since the lhs has type (Φ ++ Ψ ++ (B ++ Γ ++ Δ)) and the rhs
>>>> has type ((Φ ++ Ψ ++ B) ++ Γ ++ Δ).
>>>>
>>>> The proof makes use of a list-membership type, defined in:
>>>>
>>>>> https://github.com/agda/agda-frp-js/blob/master/src/agda/FRP/JS/DList.agda
>>>>>
>>>>>
>>>>
>>>> It satisfies weakening on the left and right:
>>>>
>>>> _≪_ : ∀ {A a as} → (a ∈ as) → ∀ bs → (a ∈ (as ++ bs))
>>>> _≫_ : ∀ {A a bs} → ∀ as → (a ∈ bs) → (a ∈ (as ++ bs))
>>>>
>>>> and moreover has left and right units and associativity properties, all
>>>> up to beta-equivalence (that is, all these properties have proof refl):
>>>>
>>>> (a∈as ≪ []) ≡ a∈as
>>>> ([] ≫ a∈as) ≡ a∈as
>>>> (a∈as ≪ bs ≪ cs) ≡ (a∈as ≪ bs ++ cs)
>>>> ((as ≫ a∈bs) ≪ cs) ≡ (as ≫ (a∈bs ≪ cs))
>>>> (as ≫ bs ≫ a∈cs) ≡ (as ≫ bs ≫ a∈cs)
>>>>
>>>> Under the hood, this is implemented in terms of difference naturals
>>>> (that is an implementation of ℕ where + and ♯0 form a monoid up to
>>>> beta-equivalence), and an implementation of difference lists such that
>>>> the length function is a monoid homomorphism up to beta-equivalence:
>>>>
>>>> (len (as ++ bs) ≡ (len as + len bs))
>>>> (len [] ≡ ♯0)
>>>>
>>>> With all that in place, the proof of weakening is pretty
>>>> straightforward. The only case which requires any work is variables,
>>>> and
>>>> a typical case is:
>>>>
>>>> begin
>>>> xweaken+ Φ Ψ (B ++ Γ ++ Δ) (case Φ (B ++ Γ ++ Δ) (Φ ≫ x ≪ Γ ≪ Δ))
>>>> ≡⟨ cong (xweaken+ Φ Ψ (B ++ Γ ++ Δ)) (case-≫ Φ (x ≪ Γ ≪ Δ)) ⟩
>>>> (Φ ≫ Ψ ≫ x ≪ Γ ≪ Δ)
>>>> ≡⟨ cong (xweaken+ (Φ ++ Ψ ++ B) Γ Δ) (sym (case-≪ (Φ ≫ Ψ ≫ x) Δ)) ⟩
>>>> xweaken+ (Φ ++ Ψ ++ B) Γ Δ (case (Φ ++ Ψ ++ B) Δ (Φ ≫ Ψ ≫ x ≪ Δ))
>>>> ∎
>>>>
>>>> I don't really want to think about what this proof would look like with
>>>> all the associativity wiring made explicit.
>>>>
>>>> There is still a bit of annoying associativity left, because I can't
>>>> see
>>>> how to get coproducts to associate on the nose, so there's lots of gore
>>>> needed to define a case function:
>>>>
>>>> data Case {A} a (as bs : List A) : Set where
>>>> inj₁ : (a∈as : a ∈ as) → Case a as bs
>>>> inj₂ : (a∈bs : a ∈ bs) → Case a as bs
>>>>
>>>> case : ∀ {A a} as bs → (a ∈ (as ++ bs)) → Case {A} a as bs
>>>>
>>>> and then prove that it satisfies associativity (up to propositional
>>>> equality, not beta-equivalence).
>>>>
>>>> A.
>>>>
>>>> On 10/26/2011 09:48 AM, Jeffrey, Alan S A (Alan) wrote:
>>>>> Hi everyone,
>>>>>
>>>>> A quick note about a trick for representing lists (or any other
>>>>> monoid)
>>>>> up to associativity. Am I reinventing a wheel here?
>>>>>
>>>>> I've been doing some mucking around recently with proofs about
>>>>> lambda-calculi and was hitting annoying problems with associativity
>>>>> on lists. A prototypical example is:
>>>>>
>>>>> weakening : ∀ {A a} (as bs cs : List A) →
>>>>> (a ∈ (as ++ cs)) → (a ∈ (as ++ bs ++ cs))
>>>>>
>>>>> It's easy to prove that ++ is associative, but making use of that fact
>>>>> is rather painful, as there's lots of manual wiring with subst and
>>>>> cong,
>>>>> for example:
>>>>>
>>>>> weaken2 : ∀ {A a} (as bs cs ds : List A) →
>>>>> (a ∈ (as ++ bs ++ ds)) → (a ∈ (as ++ bs ++ cs ++ ds))
>>>>> weaken2 {A} {a} as bs cs ds a∈es =
>>>>> subst (λ X → (a ∈ X)) (++-assoc as bs (cs ++ ds))
>>>>> (weakening (as ++ bs) cs ds
>>>>> (subst (λ X → (a ∈ X)) (sym (++-assoc as bs ds)) a∈es))
>>>>>
>>>>> This gets tiresome pretty rapidly. Oh if only there were a data
>>>>> structure which represented lists, but for which ++ was associative up
>>>>> to beta reduction... Oh look there already is one, it's called
>>>>> difference lists. Quoting the standard library:
>>>>>
>>>>> DiffList : Set → Set
>>>>> DiffList a = List a → List a
>>>>>
>>>>> _++_ : ∀ {a} → DiffList a → DiffList a → DiffList a
>>>>> xs ++ ys = λ k → xs (ys k)
>>>>>
>>>>> Unfortunately, difference lists are not isomorphic to lists: there's a
>>>>> lot more functions on lists than just concatenation functions. This
>>>>> causes headaches (e.g. writing inductive functions on difference
>>>>> lists).
>>>>>
>>>>> A first shot at fixing this is to write a data structure for those
>>>>> difference lists which are concatenations:
>>>>>
>>>>> record Seq (A : Set) : Set where
>>>>> constructor seq
>>>>> field
>>>>> list : List A
>>>>> fun : List A → List A
>>>>> ok : fun ≡ _++_ list -- Broken
>>>>>
>>>>> It's pretty straightforward to define the monoidal structure for Seq:
>>>>>
>>>>> ε : ∀ {A} → Seq A
>>>>> ε = seq [] id refl
>>>>>
>>>>> _+_ : ∀ {A} → Seq A → Seq A → Seq A
>>>>> (seq as f f✓) + (seq bs g g✓) = seq (f bs) (f ∘ g) (...easy lemma...)
>>>>>
>>>>> Unfortunately, we're back to square one again, because + is only
>>>>> associative up to propositional equality, not beta reduction. This
>>>>> time,
>>>>> it's the ok field that gets in the way. So we can fix that, and just
>>>>> make the ok field irrelevant, that is:
>>>>>
>>>>> record Seq (A : Set) : Set where
>>>>> constructor seq
>>>>> field
>>>>> list : List A
>>>>> fun : List A → List A
>>>>> .ok : fun ≡ _++_ list -- Fixed
>>>>>
>>>>> open Seq public renaming (list to [_])
>>>>>
>>>>> Hooray, + is now associative up to beta reduction:
>>>>>
>>>>> +-assoc : ∀ {A} (as bs cs : Seq A) →
>>>>> ((as + bs) + cs) ≡ (as + (bs + cs))
>>>>> +-assoc as bs cs = refl
>>>>>
>>>>>
>>>>> ≡-relevant : ∀ {A : Set} {a b : A} → .(a ≡ b) → (a ≡ b)
>>>>>
>>>>> we can define:
>>>>>
>>>>> data Case {A : Set} : Seq A → Set where
>>>>> [] : Case ε
>>>>> _∷_ : ∀ a as → Case (a ◁ as)
>>>>>
>>>>> case : ∀ {A} (as : Seq A) → Case as
>>>>>
>>>>> and this gives us recursive functions over Seq (which somewhat to my
>>>>> surprise actually get past the termination checker), for example:
>>>>>
>>>>> ids : ∀ {A} → Seq A → Seq A
>>>>> ids as with case as
>>>>> ids .(a ◁ as) | a ∷ as = a ◁ ids as
>>>>> ids .ε | [] = ε
>>>>>
>>>>> For example, we can now define weakening:
>>>>>
>>>>> weakening : ∀ {A a} (as bs cs : Seq A) →
>>>>> (a ∈ [ as + cs ]) → (a ∈ [ as + bs + cs ])
>>>>>
>>>>> and use it up to associativity without worrying hand-coded wiring:
>>>>>
>>>>> weaken2 : ∀ {A a} (as bs cs ds : Seq A) →
>>>>> (a ∈ [ as + bs + ds ]) → (a ∈ [ as + bs + cs + ds ])
>>>>> weaken2 as bs = weakening (as + bs)
>>>>>
>>>>> Hooray, cake! Eating it!
>>>>>
>>>>> I suspect this trick works for most any monoid, so you can do
>>>>> associativity on naturals, vectors, partial orders with join, etc.
>>>>> etc.
>>>>>
>>>>> The idea of using difference lists to represent lists is standard, but
>>>>> as far as I know, this use of irrelevant equalities to get structural
>>>>> recursion is new. Anyone know of any prior art?
>>>>>
>>>>> A.
>>> _______________________________________________
>>> Agda mailing list
>>> Agda@...
>>> https://lists.chalmers.se/mailman/listinfo/agda
>>>
>>
>

--

--
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel@...
http://www2.tcs.ifi.lmu.de/~abel/
```
22 Mar 2012 17:30

```Switching off printing irrelevant arguments would certainly help with
debugging. The terms will still be huge, so Agda may be sloooowwww.

A.

On 03/22/2012 11:22 AM, Andreas Abel wrote:
> Thanks!
>
> That extra comes with your revised definition of difference lists.
> Sounds good!
>
> Is it that the irrelevant proofs show up in the error messages always?
> Maybe it would be helpful to be able to switch of printing of irrelevant
> terms?
>
> Cheers,
> Andreas
>
> On 3/22/12 3:47 PM, Alan Jeffrey wrote:
>> The version that's up on github does both left- and right-units as well
>> as associativity. The canonical example is difference naturals:
>>
>>
>> https://github.com/agda/agda-assoc-free/blob/master/src/AssocFree/DNat.agda
>>
>> which includes:
>>
>> -- Addition forms a monoid on the nose
>>
>> +-assoc : ∀ l m n → (((l + m) + n) ≡ (l + (m + n)))
>> +-assoc l m n = refl
>>
>> +-unit₁ : ∀ n → ((♯0 + n) ≡ n)
>> +-unit₁ n = refl
>>
>> +-unit₂ : ∀ n → ((n + ♯0) ≡ n)
>> +-unit₂ n = refl
>>
>> Don't forget what I said about incomprehensible and huge normal forms
>> getting in the way of debugging!
>>
>> A.
>>
>> On 03/22/2012 09:40 AM, Andreas Abel wrote:
>>> Hi Alan,
>>>
>>> I remembered your idea when working with Frederic Kettelhoit on an
>>> implementation of Fingertrees which are parametrized by a monoid.
>>>
>>> free. Is there a way to also get the right-unit for free?
>>>
>>> Cheers,
>>> Andreas
>>>
>>> On 11/21/11 8:17 PM, Alan Jeffrey wrote:
>>>> I've now finished up the NBE algorithm for the simply-typed
>>>> lambda-calculus. It defines a reduction semantics, and uses NBE to show
>>>> that every term reduces to one in normal form.
>>>>
>>>> At this point, I'm afraid I think of this as an interesting idea, but
>>>> one where some pragmatic nastiness gets in the way of it being useful.
>>>> The main problems are:
>>>>
>>>> - Huge normal forms, which slow Agda down horribly.
>>>>
>>>> - Incomprehensible normal forms, which make debugging remarkably
>>>> difficult.
>>>>
>>>> - Less unification -- from unifying (a :: as) with (b :: bs) Agda
>>>> doesn't unify a with b or as with bs.
>>>>
>>>> The implementation is up at https://github.com/agda/agda-assoc-free
>>>>
>>>> A.
>>>>
>>>> On 11/02/2011 11:26 AM, Jeffrey, Alan S A (Alan) wrote:
>>>>> Hi everyone,
>>>>>
>>>>> lambda-calculi. I've now worked through some of the details, and
>>>>> here is
>>>>> the syntax of the simply-typed lambda-calculus:
>>>>>
>>>>>> https://github.com/agda/agda-frp-js/blob/master/src/agda/FRP/JS/Model/STLambdaC/Exp.agda
>>>>>>
>>>>>>
>>>>>
>>>>> The interesting thing is weakening, with type:
>>>>>
>>>>> weaken+ : ∀ B Γ Δ {T} → Exp (B ++ Δ) T → Exp (B ++ Γ ++ Δ) T
>>>>>
>>>>> and (news just in!) weakening commutes with itself (up to propositional
>>>>> equality):
>>>>>
>>>>> weaken+ Φ Ψ (B ++ Γ ++ Δ) (weaken+ (Φ ++ B) Γ Δ M)
>>>>> ≡ weaken+ (Φ ++ Ψ ++ B) Γ Δ (weaken+ Φ Ψ (B ++ Δ) M)
>>>>>
>>>>> Note that you can't even state this property without associativity on
>>>>> the nose, since the lhs has type (Φ ++ Ψ ++ (B ++ Γ ++ Δ)) and the rhs
>>>>> has type ((Φ ++ Ψ ++ B) ++ Γ ++ Δ).
>>>>>
>>>>> The proof makes use of a list-membership type, defined in:
>>>>>
>>>>>> https://github.com/agda/agda-frp-js/blob/master/src/agda/FRP/JS/DList.agda
>>>>>>
>>>>>>
>>>>>
>>>>> It satisfies weakening on the left and right:
>>>>>
>>>>> _≪_ : ∀ {A a as} → (a ∈ as) → ∀ bs → (a ∈ (as ++ bs))
>>>>> _≫_ : ∀ {A a bs} → ∀ as → (a ∈ bs) → (a ∈ (as ++ bs))
>>>>>
>>>>> and moreover has left and right units and associativity properties, all
>>>>> up to beta-equivalence (that is, all these properties have proof refl):
>>>>>
>>>>> (a∈as ≪ []) ≡ a∈as
>>>>> ([] ≫ a∈as) ≡ a∈as
>>>>> (a∈as ≪ bs ≪ cs) ≡ (a∈as ≪ bs ++ cs)
>>>>> ((as ≫ a∈bs) ≪ cs) ≡ (as ≫ (a∈bs ≪ cs))
>>>>> (as ≫ bs ≫ a∈cs) ≡ (as ≫ bs ≫ a∈cs)
>>>>>
>>>>> Under the hood, this is implemented in terms of difference naturals
>>>>> (that is an implementation of ℕ where + and ♯0 form a monoid up to
>>>>> beta-equivalence), and an implementation of difference lists such that
>>>>> the length function is a monoid homomorphism up to beta-equivalence:
>>>>>
>>>>> (len (as ++ bs) ≡ (len as + len bs))
>>>>> (len [] ≡ ♯0)
>>>>>
>>>>> With all that in place, the proof of weakening is pretty
>>>>> straightforward. The only case which requires any work is variables,
>>>>> and
>>>>> a typical case is:
>>>>>
>>>>> begin
>>>>> xweaken+ Φ Ψ (B ++ Γ ++ Δ) (case Φ (B ++ Γ ++ Δ) (Φ ≫ x ≪ Γ ≪ Δ))
>>>>> ≡⟨ cong (xweaken+ Φ Ψ (B ++ Γ ++ Δ)) (case-≫ Φ (x ≪ Γ ≪ Δ)) ⟩
>>>>> (Φ ≫ Ψ ≫ x ≪ Γ ≪ Δ)
>>>>> ≡⟨ cong (xweaken+ (Φ ++ Ψ ++ B) Γ Δ) (sym (case-≪ (Φ ≫ Ψ ≫ x) Δ)) ⟩
>>>>> xweaken+ (Φ ++ Ψ ++ B) Γ Δ (case (Φ ++ Ψ ++ B) Δ (Φ ≫ Ψ ≫ x ≪ Δ))
>>>>> ∎
>>>>>
>>>>> I don't really want to think about what this proof would look like with
>>>>> all the associativity wiring made explicit.
>>>>>
>>>>> There is still a bit of annoying associativity left, because I can't
>>>>> see
>>>>> how to get coproducts to associate on the nose, so there's lots of gore
>>>>> needed to define a case function:
>>>>>
>>>>> data Case {A} a (as bs : List A) : Set where
>>>>> inj₁ : (a∈as : a ∈ as) → Case a as bs
>>>>> inj₂ : (a∈bs : a ∈ bs) → Case a as bs
>>>>>
>>>>> case : ∀ {A a} as bs → (a ∈ (as ++ bs)) → Case {A} a as bs
>>>>>
>>>>> and then prove that it satisfies associativity (up to propositional
>>>>> equality, not beta-equivalence).
>>>>>
>>>>> A.
>>>>>
>>>>> On 10/26/2011 09:48 AM, Jeffrey, Alan S A (Alan) wrote:
>>>>>> Hi everyone,
>>>>>>
>>>>>> A quick note about a trick for representing lists (or any other
>>>>>> monoid)
>>>>>> up to associativity. Am I reinventing a wheel here?
>>>>>>
>>>>>> I've been doing some mucking around recently with proofs about
>>>>>> lambda-calculi and was hitting annoying problems with associativity
>>>>>> on lists. A prototypical example is:
>>>>>>
>>>>>> weakening : ∀ {A a} (as bs cs : List A) →
>>>>>> (a ∈ (as ++ cs)) → (a ∈ (as ++ bs ++ cs))
>>>>>>
>>>>>> It's easy to prove that ++ is associative, but making use of that fact
>>>>>> is rather painful, as there's lots of manual wiring with subst and
>>>>>> cong,
>>>>>> for example:
>>>>>>
>>>>>> weaken2 : ∀ {A a} (as bs cs ds : List A) →
>>>>>> (a ∈ (as ++ bs ++ ds)) → (a ∈ (as ++ bs ++ cs ++ ds))
>>>>>> weaken2 {A} {a} as bs cs ds a∈es =
>>>>>> subst (λ X → (a ∈ X)) (++-assoc as bs (cs ++ ds))
>>>>>> (weakening (as ++ bs) cs ds
>>>>>> (subst (λ X → (a ∈ X)) (sym (++-assoc as bs ds)) a∈es))
>>>>>>
>>>>>> This gets tiresome pretty rapidly. Oh if only there were a data
>>>>>> structure which represented lists, but for which ++ was associative up
>>>>>> to beta reduction... Oh look there already is one, it's called
>>>>>> difference lists. Quoting the standard library:
>>>>>>
>>>>>> DiffList : Set → Set
>>>>>> DiffList a = List a → List a
>>>>>>
>>>>>> _++_ : ∀ {a} → DiffList a → DiffList a → DiffList a
>>>>>> xs ++ ys = λ k → xs (ys k)
>>>>>>
>>>>>> Unfortunately, difference lists are not isomorphic to lists: there's a
>>>>>> lot more functions on lists than just concatenation functions. This
>>>>>> causes headaches (e.g. writing inductive functions on difference
>>>>>> lists).
>>>>>>
>>>>>> A first shot at fixing this is to write a data structure for those
>>>>>> difference lists which are concatenations:
>>>>>>
>>>>>> record Seq (A : Set) : Set where
>>>>>> constructor seq
>>>>>> field
>>>>>> list : List A
>>>>>> fun : List A → List A
>>>>>> ok : fun ≡ _++_ list -- Broken
>>>>>>
>>>>>> It's pretty straightforward to define the monoidal structure for Seq:
>>>>>>
>>>>>> ε : ∀ {A} → Seq A
>>>>>> ε = seq [] id refl
>>>>>>
>>>>>> _+_ : ∀ {A} → Seq A → Seq A → Seq A
>>>>>> (seq as f f✓) + (seq bs g g✓) = seq (f bs) (f ∘ g) (...easy lemma...)
>>>>>>
>>>>>> Unfortunately, we're back to square one again, because + is only
>>>>>> associative up to propositional equality, not beta reduction. This
>>>>>> time,
>>>>>> it's the ok field that gets in the way. So we can fix that, and just
>>>>>> make the ok field irrelevant, that is:
>>>>>>
>>>>>> record Seq (A : Set) : Set where
>>>>>> constructor seq
>>>>>> field
>>>>>> list : List A
>>>>>> fun : List A → List A
>>>>>> .ok : fun ≡ _++_ list -- Fixed
>>>>>>
>>>>>> open Seq public renaming (list to [_])
>>>>>>
>>>>>> Hooray, + is now associative up to beta reduction:
>>>>>>
>>>>>> +-assoc : ∀ {A} (as bs cs : Seq A) →
>>>>>> ((as + bs) + cs) ≡ (as + (bs + cs))
>>>>>> +-assoc as bs cs = refl
>>>>>>
>>>>>>
>>>>>> ≡-relevant : ∀ {A : Set} {a b : A} → .(a ≡ b) → (a ≡ b)
>>>>>>
>>>>>> we can define:
>>>>>>
>>>>>> data Case {A : Set} : Seq A → Set where
>>>>>> [] : Case ε
>>>>>> _∷_ : ∀ a as → Case (a ◁ as)
>>>>>>
>>>>>> case : ∀ {A} (as : Seq A) → Case as
>>>>>>
>>>>>> and this gives us recursive functions over Seq (which somewhat to my
>>>>>> surprise actually get past the termination checker), for example:
>>>>>>
>>>>>> ids : ∀ {A} → Seq A → Seq A
>>>>>> ids as with case as
>>>>>> ids .(a ◁ as) | a ∷ as = a ◁ ids as
>>>>>> ids .ε | [] = ε
>>>>>>
>>>>>> For example, we can now define weakening:
>>>>>>
>>>>>> weakening : ∀ {A a} (as bs cs : Seq A) →
>>>>>> (a ∈ [ as + cs ]) → (a ∈ [ as + bs + cs ])
>>>>>>
>>>>>> and use it up to associativity without worrying hand-coded wiring:
>>>>>>
>>>>>> weaken2 : ∀ {A a} (as bs cs ds : Seq A) →
>>>>>> (a ∈ [ as + bs + ds ]) → (a ∈ [ as + bs + cs + ds ])
>>>>>> weaken2 as bs = weakening (as + bs)
>>>>>>
>>>>>> Hooray, cake! Eating it!
>>>>>>
>>>>>> I suspect this trick works for most any monoid, so you can do
>>>>>> associativity on naturals, vectors, partial orders with join, etc.
>>>>>> etc.
>>>>>>
>>>>>> The idea of using difference lists to represent lists is standard, but
>>>>>> as far as I know, this use of irrelevant equalities to get structural
>>>>>> recursion is new. Anyone know of any prior art?
>>>>>>
>>>>>> A.
>>>> _______________________________________________
>>>> Agda mailing list
>>>> Agda@...
>>>> https://lists.chalmers.se/mailman/listinfo/agda
>>>>
>>>
>>
>
```
4 Nov 2011 11:48

```On 2011-10-26 16:48, Alan Jeffrey wrote:
> The idea of using difference lists to represent lists is standard, but
> as far as I know, this use of irrelevant equalities to get structural
> recursion is new. Anyone know of any prior art?

I've used the two tricks independently, but I haven't seen them used
together.

One of the tricks (old code, hence Set1, forall and -> rather than Set₁,
∀ and →):

-- I am using difference lists to get associativity "for free". This
-- makes it possible to state the right-assoc lemma below without
-- using any casts.

record TypeList : Set1 where
infixr 5 _⟶_
field
_⟶_    : Set -> Set
map    : forall {a b} -> (a -> b) -> _⟶_ a -> _⟶_ b
map-id : forall a -> map (id {A = a}) ≡ id
map-∘  : forall {a b c} (f : b -> c) (g : a -> b) ->
map (f ∘ g) ≡ map f ∘ map g

The other:

-- Families of functions which, on the semantic side, correspond to
-- the application of a given context morphism

record [_⟶_] {t₁ t₂} (T₁ : Term-like t₁) (T₂ : Term-like t₂)
{Γ Δ : Ctxt} (ρ̂ : Γ ⇨̂ Δ) : Set (i ⊔ u ⊔ e ⊔ t₁ ⊔ t₂) where
constructor _,_

open Term-like T₁ renaming (_⊢_ to _⊢₁_; ⟦_⟧ to ⟦_⟧₁)
open Term-like T₂ renaming (_⊢_ to _⊢₂_; ⟦_⟧ to ⟦_⟧₂)

field
function     : ∀ σ → Γ ⊢₁ σ → Δ ⊢₂ σ /̂ ρ̂
.corresponds :
∀ σ (t : Γ ⊢₁ σ) → ⟦ t ⟧₁ /̂Val ρ̂ ≅-Value ⟦ function σ t ⟧₂

In this case the identity and associativity laws hold by definition
(because they hold automatically for function composition/identity).
However, in the end I decided not to use this approach, because I didn't
want to rely on yet another not-universally-accepted feature of Agda.

--

--
```
4 Nov 2011 19:01

```On 11/04/2011 05:48 AM, Nils Anders Danielsson wrote:
> On 2011-10-26 16:48, Alan Jeffrey wrote:
>> The idea of using difference lists to represent lists is standard, but
>> as far as I know, this use of irrelevant equalities to get structural
>> recursion is new. Anyone know of any prior art?
>
> I've used the two tricks independently, but I haven't seen them used
> together.

This is my feeling, that the two tricks have been kicking around for a
while, and this is just the requisite bit of glue to stick them together.

> However, in the end I decided not to use this approach, because I didn't
> want to rely on yet another not-universally-accepted feature of Agda.

Indeed. I'm on thin ice here, as the postulate for relevance of
propositional equality is a bit dodgy. I'm not entirely sure how it
would be formalized in homotopy types (it implies that there is a
canonical path between any two connected points, but who knows what that
does to the theory).

A.
```

Gmane