https://lists.chalmers.se/pipermail/agda/2010/001696.html

I apologize for the disturbance. ]]>

_=>_ : 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…

_=>_ : 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

`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 = {!!}