module lemId where

import prelude

-- general lemmas about Identity type

comp : (A : U) -> (a b c : A) -> Id A a b -> Id A b c -> Id A a c
comp A a b c p q = subst A (Id A a) b c q p

compInvIdr : (A : U) -> (a b : A) -> (p : Id A a b) -> Id (Id A a b) p (comp A a b b p (refl A b))
compInvIdr A a b p = substeq A (\x -> Id A a x) b p

inv : (A : U) -> (a b :A) -> Id A a b -> Id A b a
inv A a b p = subst A (\ x -> Id A x a) a b p (refl A a)

invRefl : (A:U) -> (a:A) -> Id (Id A a a) (refl A a) (inv A a a (refl A a))
invRefl A a = substeq A  (\ x -> Id A x a) a (refl A a)

compIdr : (A : U) -> (a b : A) -> (p : Id A a b) -> Id (Id A a b) (comp A a b b p (refl A b)) p
compIdr A a b p = inv (Id A a b) p (comp A a b b p (refl A b)) (compInvIdr A a b p)

compInvIdl : (A : U) -> (b c : A) -> (q : Id A b c) ->
          Id (Id A b c) q (comp A b b c (refl A b) q)
compInvIdl A b c q = J A b (\c q -> Id (Id A b c) q (comp A b b c (refl A b) q)) rem c q
  where
    rem : Id (Id A b b) (refl A b) (comp A b b b (refl A b) (refl A b))
    rem = compInvIdr A b b (refl A b)

compIdl : (A : U) -> (b c : A) -> (q : Id A b c) ->
             Id (Id A b c) (comp A b b c (refl A b) q) q
compIdl A b c q = inv (Id A b c) q (comp A b b c (refl A b) q) (compInvIdl A b c q)

compInv : (A : U) -> (a b c : A) -> Id A a b -> Id A a c -> Id A b c
compInv A a b c p r = subst A (\ x -> Id A x c) a b p r

compInvIdl' : (A : U) (a b : A) (p : Id A a b) ->
               Id (Id A a b) p (compInv A a a b (refl A a) p)
compInvIdl' A a b p = substeq A (\x -> Id A x b) a p

idEuclid : (A : U) -> euclidean A (Id A)
idEuclid A a b c p r = comp A a c b p (inv A b c r)

compUp : (A:U) -> (a a' b b':A) -> Id A a a' -> Id A b b' -> Id A a b -> Id A a' b'
compUp A a a' b b' p q r =
 subst A (\ x -> Id A x b') a a' p rem
 where
  rem : Id A a b'
  rem = comp A a b b' r q

compDown : (A:U) -> (a a' b b':A) -> Id A a a' -> Id A b b' -> Id A a' b' -> Id A a b
compDown A a a' b b' p q r =
 subst A (\ x -> Id A a x) b' b (inv A b b' q) rem
 where
  rem : Id A a b'
  rem = comp A a a' b' p r

lemInv : (A:U) -> (a b c : A) -> (p : Id A a b) -> (q : Id A b c) ->
         Id (Id A b c) q (compInv A a b c p (comp A a b c p q))
lemInv A a b c p q =
 J A a (\ b p -> (c : A) (q : Id A b c) ->
        Id (Id A b c) q (compInv A a b c p (comp A a b c p q))) rem b p c q
 where
  rem1 : (c : A) (q : Id A a c) ->
          Id (Id A a c) (comp A a a c (refl A a) q)
                        (compInv A a a c (refl A a) (comp A a a c (refl A a) q))
  rem1 c q = compInvIdl' A a c (comp A a a c (refl A a) q)

  rem2 : (c : A) (q : Id A a c) -> Id (Id A a c) q (comp A a a c (refl A a) q)
  rem2 c q = compInvIdl A a c q

  rem : (c : A) (q : Id A a c) ->
          Id (Id A a c) q (compInv A a a c (refl A a) (comp A a a c (refl A a) q))
  rem c q = comp (Id A a c) q
                        (comp A a a c (refl A a) q)
                        (compInv A a a c (refl A a) (comp A a a c (refl A a) q))
                        (rem2 c q)
                        (rem1 c q)

lemSimpl : (A:U) -> (a b c : A) -> (p : Id A a b) -> (q q' : Id A b c) ->
   Id (Id A a c) (comp A a b c p q) (comp A a b c p q') -> Id (Id A b c) q q'
lemSimpl A a b c p q q' h =
 compDown (Id A b c)
           q (compInv A a b c p (comp A a b c p q)) q' (compInv A a b c p (comp A a b c p q'))
           rem rem1 rem2
 where
   rem : Id (Id A b c) q (compInv A a b c p (comp A a b c p q))
   rem = lemInv A a b c p q

   rem1 : Id (Id A b c) q' (compInv A a b c p (comp A a b c p q'))
   rem1 = lemInv A a b c p q'

   rem2 : Id (Id A b c) (compInv A a b c p (comp A a b c p q))
                        (compInv A a b c p (comp A a b c p q'))
   rem2 = cong (Id A a c) (Id A b c) (compInv A a b c p)
               (comp A a b c p q) (comp A a b c p q') h

eqSigma : (A : U) (B : A -> U) (a b : A) (p : Id A a b)
          (u : B a) (v : B b) (q : Id (B b) (subst A B a b p u) v) ->
          Id (Sigma A B) (pair a u) (pair b v)
eqSigma A B a =
  J A a (\b p -> (u : B a) (v : B b) (q : Id (B b) (subst A B a b p u) v) ->
         Id (Sigma A B) (pair a u) (pair b v)) rem2
  where
    rem1 : (u v : B a) -> Id (B a) u v ->
           Id (Sigma A B) (pair a u) (pair a v)
    rem1 = cong (B a) (Sigma A B) (\x -> pair a x)

    rem2 : (u v : B a) -> Id (B a) (subst A B a a (refl A a) u) v ->
           Id (Sigma A B) (pair a u) (pair a v)
    rem2 u v q = rem1 u v q'
      where q' : Id (B a) u v
            q' = comp (B a) u (subst A B a a (refl A a) u) v (substeq A B a u) q

eqPropFam : (A : U) (B : A -> U) (h : propFam A B) (au bv : Sigma A B) ->
            Id A (fst A B au) (fst A B bv) -> Id (Sigma A B) au bv
eqPropFam A B h = split
  pair a u -> split
    pair b v -> \p -> eqSigma A B a b p u v (h b (subst A B a b p u) v)