[Agda] John Major equality

[Marcin Benke]

I have merged the "Equality" branch into HEAD. This means that Agda now 
has John Major equality.

Here's (hopefully explanatory) example:

-- Certain British politician now lives in the Prelude...
--JMeq(A::Set)(a::A)::(B::Set) -> (b::B) -> Set
--  = idata same::_ A a

-- ...and he's a reflexive guy:
reflJM(A::Set)(a::A)::JMeq A a A a
 = same at _

-- ... as well as substitutive
substJM(A::Set)(P::A->Set)(a,b::A)(e::JMeq A a A b)(pa::P a)::P b
 = case e of
   (same)->
     pa

-- ... function application respects equality
resp (A::Set)(B::A->Set)
     (f1,f2::(x::A)->B x)
     (qf :: JMeq ((x::A)-> B x) f1 ((x::A)-> B x) f2)
     (a1,a2::A)
     (qa :: JMeq A a1 A a2)
     :: JMeq (B a1) (f1 a1)(B a2)(f2 a2)
 =            substJM A (\a2->JMeq (B a1) (f1 a1)(B a2)(f2 a2)) a1 a2 qa
                ((substJM (((x::A)-> B x))
                    (\(x::(y::A)->B y)->JMeq (B a1) (f1 a1) (B a1) (x a1))
                    f1 f2 qf same at _))


-- we can now easily define equality on dependent pairs (which was 
cumbersome before)
Sum (X::Set)(Y::X -> Set) :: Set
    = sig{fst :: X;
          snd :: Y fst;}

dep_pair (|X::Set)(|Y::X -> Set)(x::X)(y::Y x) :: Sum X Y
    = struct {
        fst = x;
        snd = y;}


eqSum(X::Set)(x1,x2::X)(qx::JMeq X x1 X x2)
     (Y::X->Set)(y1::Y x1)(y2::Y x2)(qy::JMeq (Y x1) y1 (Y x2) y2)
   ::JMeq (Sum X Y)(dep_pair x1 y1) (Sum X Y) (dep_pair x2 y2)
 = case qx of
   (same)->
     case qy of
     (same)->
       same at _ 


-- Marcin

P.S. Kudos to Conor McBride, Makoto Takeyama and Ulf Norell, who 
coimplemented JMEq.