module gradLemma where

import equivProp
import BoolEqBool

corrstId : (A : U) (a : A) -> prop (fiber A A (id A) a)
corrstId A a v0 v1 = compInv (pathTo A a) (sId A a) v0 v1 (tId A a v0) (tId A a v1)

corr2stId : (A : U) (h : A -> A) (ph : (x : A) -> Id A (h x) x) (a : A) ->
            prop (fiber A A h a)
corr2stId A h ph a = substInv (A -> A) (\h -> prop (fiber A A h a)) h (id A) rem (corrstId A a)
  where
  rem : Id (A -> A) h (id A)
  rem = funExt A (\_ -> A) h (id A) ph


gradLemma : (A B : U) (f : A -> B) (g : B -> A) -> section A B f g -> retract A B f g ->
            isEquiv A B f
gradLemma A B f g sfg rfg = isEquivSection A B f g sfg rem
  where
  injf : injective A B f
  injf = retractInj A B f g rfg

  rem : (b : B) -> prop (Sigma A (\a -> Id B (f a) b))
  rem b z0 z1 = rem5
   where
    E : A -> U
    E a = Id B (f a) b
    F : A -> U
    F a = Id A (g (f a)) (g b)
    G : A -> U
    G a = Id B (f (g (f a))) (f (g b))

    cg : (a:A) -> E a -> F a
    cg a = mapOnPath B A g (f a) b

    cf : (a:A) -> F a -> G a
    cf a = mapOnPath A B f (g (f a)) (g b)

    cfg : (a:A) -> E a -> G a
    cfg a = mapOnPath B B (\ x -> f (g x)) (f a) b

    pcf : Sigma A F -> Sigma A G
    pcf z = (z.1, cf z.1 z.2)

    pcg : Sigma A E -> Sigma A F
    pcg z = (z.1, cg z.1 z.2)

    fg : B -> B
    fg y = f (g y)

    pc : (u:B -> B) -> Sigma A E -> Sigma A (\ a -> Id B (u (f a)) (u b))
    pc u z = (z.1, mapOnPath B B u (f z.1) b z.2)

    rem1 : prop (Sigma A F)
    rem1 = corr2stId A (\ x -> g (f x)) rfg (g b)

    rem2 : Id (Sigma A F) (pcg z0) (pcg z1)
    rem2 = rem1 (pcg z0) (pcg z1)

    rem3 : Id (Sigma A G) (pcf (pcg z0)) (pcf (pcg z1))
    rem3 = mapOnPath (Sigma A F) (Sigma A G) pcf (pcg z0) (pcg z1) rem2

    rem4 : Id (B -> B) fg (id B)
    rem4 = funExt B (\ _ -> B)  fg (id B) sfg

    rem5 : Id (Sigma A E) (pc (id B) z0) (pc (id B) z1)
    rem5 = subst (B->B)
             (\ u -> Id (Sigma A (\ x -> Id B (u (f x)) (u b))) (pc u z0) (pc u z1)) fg (id B) rem4 rem3

-- isomorphic types are equal

isoId : (A B:U) ->  (f : A -> B) (g : B -> A) -> section A B f g -> retract A B f g ->
            Id U A B
isoId A B f g sfg rfg = isEquivEq A B f (gradLemma A B f g sfg rfg)

-- some applications of the gradlemma

propId : (A B:U) ->  prop A -> prop B ->  (f : A -> B) (g : B -> A) ->
            Id U A B
propId A B pA pB f g = isEquivEq A B f (gradLemma A B f g sfg rfg)
 where
  sfg : (b:B) -> Id B (f (g b)) b
  sfg b = pB (f (g b)) b

  rfg : (a:A) -> Id A (g (f a)) a
  rfg a = pA (g (f a)) a