module heterogeneous where

import primitives
import prelude
import gradLemma

eqFst : (A : U) (B : A -> U) (u v : Sigma A B) ->
        Id (Sigma A B) u v -> Id A u.1 v.1
eqFst A B = mapOnPath (Sigma A B) A (\x -> x.1)

eqSnd : (A : U) (B : A -> U) (u v : Sigma A B) (p : Id (Sigma A B) u v) ->
        IdS A B u.1 v.1 (eqFst A B u v p) u.2 v.2
eqSnd A B = mapOnPathD (Sigma A B) (\x -> B x.1) (\x -> x.2)

eqPair1 : (A : U) (B : A -> U) (a0 a1 : A) (b0 : B a0) (b1 : B a1) ->
        Id (Sigma A B) (a0,b0) (a1,b1) -> Id A a0 a1
eqPair1 A B a0 a1 b0 b1 = eqFst A B (a0,b0) (a1,b1)

-- eqPair2 : (A : U) (B : A -> U) (a0 a1 : A) (b0 : B a0) (b1 : B a1)
--        (p : Id (Sigma A B) (pair a0 b0) (pair a1 b1)) ->
--        IdS A B a0 a1 (eqPair1 A B a0 a1 b0 b1 p) b0 b1
-- eqPair2 A B a0 a1 b0 b1 = eqSnd A B (pair a0 b0) (pair a1 b1)

-- conversion test:
reflIdIdP : (A:U) (a b : A) -> Id U (Id A a b) (IdP A A (refl U A) a b)
reflIdIdP A a b = refl U (Id A a b)

-- conversion test:
reflS : (A:U) (F:A -> U) (a:A) (b : F a) -> IdS A F a a (refl A a) b b
reflS A F a b = refl (F a) b

-- conversion test:
composeMapOnPath : (A : U) (B : A -> U) (u v : Sigma A B) ->
                   (p : Id (Sigma A B) u v) ->
  Id (Id U (B u.1) (B v.1))
    (mapOnPath (Sigma A B) U (\x -> B x.1) u v p)
    (mapOnPath A U B u.1 v.1 (mapOnPath (Sigma A B) A (\x -> x.1) u v p))
composeMapOnPath A B u v p = refl (Id U (B u.1) (B v.1))
          (mapOnPath (Sigma A B) U (\x -> B x.1) u v p)

eqFstSnd : (A : U) (B : A -> U) (a0 a1 : A) (b0 : B a0) (b1 : B a1) ->
           Id U
             (Id (Sigma A B) (a0, b0) (a1, b1))
	     (Sigma (Id A a0 a1) (\p -> IdS A B a0 a1 p b0 b1))
eqFstSnd A B a0 a1 b0 b1 = isEquivEq IdSig SigId f
                           (gradLemma IdSig SigId f g (refl SigId) (refl IdSig))
  where IdSig : U
        IdSig = Id (Sigma A B) (a0, b0) (a1, b1)

        SigId : U
        SigId = Sigma (Id A a0 a1) (\p -> IdS A B a0 a1 p b0 b1)

        f : IdSig -> SigId
        f p = (eqFst A B (a0,b0) (a1,b1) p, eqSnd  A B (a0,b0) (a1,b1) p)


        g : SigId -> IdSig
        g z =  mapOnPathS A B (Sigma A B) (\a b -> (a, b)) a0 a1 z.1 b0 b1 z.2


eqSubstSig : (A : U) (B : A -> U) (a0 a1 : A) (p:Id A a0 a1) (b0 : B a0) (b1 : B a1) ->
           Id U (IdS A B a0 a1 p b0 b1) (Id (B a1) (subst A B a0 a1 p b0) b1)
eqSubstSig A B a0 =
 J A a0 (\ a1 p -> (b0 : B a0) (b1 : B a1) ->
                    Id U (IdS A B a0 a1 p b0 b1) (Id (B a1) (subst A B a0 a1 p b0) b1))
        rem
  where rem :(b0 b1 :B a0) -> Id U (Id (B a0) b0 b1) (Id (B a0) (subst A B a0 a0 (refl A a0) b0) b1)
        rem b0 b1 = mapOnPath (B a0) U (\ b -> Id (B a0) b b1)
                     b0 (subst A B a0 a0 (refl A a0) b0) (substeq A B a0 b0)

pairEq : (A B:U) (a0 a1:A) (b0 b1:B) -> Id A a0 a1 -> Id B b0 b1 ->
         Id (and A B) (a0, b0) (a1, b1)
pairEq A B a0 a1 b0 b1 p q =
 appOnPath B (and A B) f0 f1 b0 b1 rem q
  where f0 : B -> and A B
        f0 y = (a0, y)
        f1 : B -> and A B
        f1 y = (a1, y)
        rem : Id (B -> and A B) f0 f1
        rem = mapOnPath A (B -> and A B) (\ x y -> (x, y)) a0 a1 p

test : (A B:U) (a0 a1:A) (b0 b1:B) (p:Id A a0 a1) (q:Id B b0 b1) ->
         Id (Id A a0 a1)
            p
            (mapOnPath (and A B) A (\x -> x.1) (a0, b0) (a1, b1)
                       (pairEq A B a0 a1 b0 b1 p q))
test A B a0 a1 b0 b1 p q = refl (Id A a0 a1) p