Comments on: Coinduction, observationally

By: Conor

Conor — Sun, 18 Apr 2010 10:51:24 +0000

Hi divip. I’m sorry I took my eye off the blog. You seem to have found your way in the end. => and & are, as you found, just a notational convenience for nondependent special cases of Pi and Sg.

By: divip

divip — Sun, 04 Apr 2010 22:01:08 +0000

Oh. I found the sources in the Agda mailing list archives:
https://lists.chalmers.se/pipermail/agda/2010/001696.html
I apologize for the disturbance.

By: divip

divip — Sun, 04 Apr 2010 10:13:12 +0000

Now I have

_=>_ : Ty PROP -> Ty PROP -> Ty PROP
a => b = `Pi’ (`Prf’ a) \ _ -> b

_&_ : {k : Sort} -> Ty k -> Ty k -> Ty k
a & b = `Sg’ a \ n2 -> b

Still I am not sure that it is right.
I realised I need a deeper insight…

By: divip

divip — Fri, 02 Apr 2010 23:57:12 +0000

OK, Maybe I have got it:

_=>_ : Ty PROP -> Ty PROP -> Ty PROP
`0′ => b = `1′ — is this useful?
`1′ => b = b — is this useful?
a => b = `Pi’ (`Prf’ a) \ _ -> b

_&_ : {k : Sort} -> Ty k -> Ty k -> Ty k
`0′ & _ = `0′ — is this useful?
`1′ & x = x — is this useful?
a & b = `Pi’ `2′ (pp a b)

pp : {X : Set} -> X -> X -> Two -> X
pp a b tt = a
pp a b ff = b

By: divip

divip — Fri, 02 Apr 2010 19:14:55 +0000

What does
`Sg’ Sl (`INu’ Sl Cl Rl nl) & `Sg’ Sr (`INu’ Sr Cr Rr nr)
mean?
I can not define _=>_ and _&_.
For _=>_ I got to

_=>_ : Ty PROP -> Ty PROP -> Ty PROP
`0′ => b = `1′
`1′ => b = b
`Pi’ S T => b = {!!}
`Sg’ S T => b = {!!}
`INu’ S C R n s => b = {!!}