module cong where

import set
import function

-- All of these lemmas on mapOnPath will be trivial with definitional equalities

congRefl : (A B : U) (f : A -> B) (a : A) -> 
           Id (Id B (f a) (f a)) (refl B (f a)) (mapOnPath A B f a a (refl A a))
congRefl A B f a = refl (Id B (f a) (f a)) (refl B (f a))

congId : (A : U) (a0 a1 : A) -> 
         Id (Id A a0 a1 -> Id A a0 a1) (id (Id A a0 a1)) (mapOnPath A A (id A) a0 a1)
congId A a0 a1 = funExt (Id A a0 a1) (\_ -> Id A a0 a1) (id (Id A a0 a1)) 
                        (mapOnPath A A (id A) a0 a1) (rem a0 a1)
  where
  rem1 : (u : A) -> Id (Id A u u) (refl A u) (mapOnPath A A (id A) u u (refl A u))
  rem1 = congRefl A A (id A)

  rem : (u0 u1 : A) -> (p : Id A u0 u1) -> Id (Id A u0 u1) p (mapOnPath A A (id A) u0 u1 p) 
  rem u0 = J A u0 (\u1 p -> Id (Id A u0 u1) p (mapOnPath A A (id A) u0 u1 p)) (rem1 u0)

congComp : (A B C : U) (f : A -> B) (g : B -> C) (a0 a1 : A) -> 
           Id (Id A a0 a1 -> Id C (g (f a0)) (g (f a1))) 
              (mapOnPath A C (\x -> g (f x)) a0 a1)
              (\p -> mapOnPath B C g (f a0) (f a1) (mapOnPath A B f a0 a1 p))
congComp A B C f g a0 a1 = funExt (Id A a0 a1) (\_ -> Tgf a0 a1)
                                  (conggf a0 a1) (\p -> congg a0 a1 (congf a0 a1 p)) (rem a0 a1)
  where
  Tgf : (a0 a1 : A) -> U 
  Tgf a0 a1 = Id C (g (f a0)) (g (f a1))

  congf : (a0 a1 : A) -> Id A a0 a1 -> Id B (f a0) (f a1)
  congf = mapOnPath A B f
  
  congg : (a0 a1 : A) -> Id B (f a0) (f a1) -> Tgf a0 a1
  congg a0 a1 = mapOnPath B C g (f a0) (f a1)

  conggf : (a0 a1 : A) -> Id A a0 a1 -> Tgf a0 a1
  conggf = mapOnPath A C (\x -> g (f x))

  rem : (a0 a1 : A) (p : Id A a0 a1) -> 
        Id (Tgf a0 a1) (conggf a0 a1 p) (congg a0 a1 (congf a0 a1 p))
  rem a = J A a (\a1 p -> Id (Tgf a a1) (conggf a a1 p) (congg a a1 (congf a a1 p)))
             rem1
    where
    rem2 : Id (Tgf a a) (refl C (g (f a))) (conggf a a (refl A a))
    rem2 = congRefl A C (\x -> g (f x)) a

    rem4 : Id (Id B (f a) (f a)) (refl B (f a)) (congf a a (refl A a))
    rem4 = congRefl A B f a

    rem3 : Id (Tgf a a) (congg a a (refl B (f a))) (congg a a (congf a a (refl A a)))
    rem3 = mapOnPath (Id B (f a) (f a)) (Tgf a a) (congg a a) (refl B (f a)) 
                (congf a a (refl A a)) rem4

    rem5 : Id (Tgf a a) (refl C (g (f a))) (congg a a (refl B (f a)))
    rem5 = congRefl B C g (f a)

    rem1 : Id (Tgf a a) (conggf a a (refl A a)) (congg a a (congf a a (refl A a)))
    rem1 = compUp (Tgf a a) (refl C (g (f a))) (conggf a a (refl A a))
                              (congg a a (refl B (f a))) (congg a a (congf a a (refl A a)))
                    rem2 rem3 rem5