module subset where

import univalence
import equivTotal
import elimEquiv

-- a non trivial equivalence: two different ways to represent subsets
-- this is not finished
-- it should provide a non trivial equivalence

subset1 : U -> U
subset1 A = Sigma U (\ X -> X -> A)

subset2 : U -> U
subset2 A = A -> U

-- map in both directions

sub12 : (A:U) -> subset1 A -> subset2 A
sub12 A = split
           pair X f -> fiber X A f

sub21 : (A:U) -> subset2 A -> subset1 A
sub21 A P = pair (Sigma A P) (fst A P)

retsub : (A:U) -> (P : subset2 A) -> Id (subset2 A) (sub12 A (sub21 A P)) P
retsub A P = funExt A (\ _ -> U) (fiber (Sigma A P) A (fst A P)) P (lem1Sub A P)


-- in the other direction we use a corollary of equivalence

eqSigmaEquiv : (A B :U) (f:A -> B) -> isEquiv A B f -> (Q:B -> U) -> Id U (Sigma A (\ x -> Q (f x))) (Sigma B Q)
eqSigmaEquiv A = elimIsEquiv A C rem
 where
  C : (B:U) -> (A->B) -> U
  C B f = (Q:B->U) -> Id U (Sigma A (\ y -> Q (f y))) (Sigma B Q)

  rem : (Q:A->U) -> Id U (Sigma A (\ y -> Q y)) (Sigma A Q)
  rem Q =  cong (A -> U) U (Sigma A) (\ y -> Q y) Q (funExt A (\ _ -> U) (\ y -> Q y) Q(\ y -> refl U (Q y)))

-- but actually this is not this consequence that we need

lemSecSub : (A X Y:U)(g:X->Y) -> isEquiv X Y g -> (f:Y -> A) ->
    Id (subset1 A) (pair Y f) (pair X (\ y -> f (g y))) 
lemSecSub A X = elimIsEquiv X P rem
 where
  P : (Y:U) -> (X->Y) -> U
  P Y g = (f:Y -> A) -> Id (subset1 A) (pair Y f) (pair X (\ y -> f (g y))) 

  rem : (f:X -> A) -> Id (subset1 A) (pair X f) (pair X (\ y -> f y)) 
  rem f = cong (X->A) (subset1 A) (\ h -> pair X h) f (\ y -> f y) 
                 (funExt X (\ _ -> A) f (\ y -> f y) (\ y -> refl A (f y)))

lem2SecSub : (A X:U) (f:X -> A) -> isEquiv X (Sigma A (fiber X A f)) (\ x -> pair (f x) (pair x (refl A (f x))))
lem2SecSub A X f = rem2
 where
    F : A -> U
    F = fiber X A f 

    Y : U
    Y = Sigma A F

    h : Y -> A
    h = fst A F

    g : X -> Y
    g x = pair (f x) (pair x (refl A (f x)))

    h : Y -> X
    h = split
         pair a xp -> fst X (\ x -> Id A (f x) a) xp

    Z : U
    Z = Sigma X (\ x -> Sigma A (\ a -> Id A (f x) a))

    sw1 : Y -> Z
    sw1 = split
           pair a xp -> asw1 xp
              where asw1 : Sigma X (\ x -> Id A (f x) a) -> Z
                    asw1 = split 
                             pair x p -> pair x (pair a p)

    sw2 : Z -> Y
    sw2 = split
           pair x ap -> asw2 ap
              where asw2 : Sigma A (\ a -> Id A (f x) a) -> Y
                    asw2 = split 
                             pair a p -> pair a (pair x p)

    lemsw : (y:Y) -> Id Y (sw2 (sw1 y)) y
    lemsw = split
             pair a xp -> lemsw1 xp
               where lemsw1 : (xp : Sigma X (\ x -> Id A (f x) a)) -> Id Y (sw2 (sw1 (pair a xp))) (pair a xp)
                     lemsw1 = split
                               pair x p -> refl Y (pair a (pair x p))               

    sgh : (x:X) -> Id X (h (g x)) x
    sgh x = refl X x

    rgh : (y:Y) -> Id Y (g (h y)) y
    rgh = split
           pair a xp -> lem xp
             where 
               lem : (xp : Sigma X (\ x -> Id A (f x) a)) -> Id Y (g (h (pair a xp))) (pair a xp)
               lem = split
                       pair x p -> lem1
                            where
                              C : (v u:A) -> Id A v u -> U
                              C v u q =  Id (Sigma A (\ w -> Id A v w)) (pair v (refl A v)) (pair u q)

                              lem5 : (v:A) -> C v v (refl A v)
                              lem5 v = refl (Sigma A (\ w -> Id A v w)) (pair v (refl A v))

                              lem4 : (v u:A) (q: Id A v u) -> C v u q
                              lem4 v =  J A v (C v) (lem5 v)

                              lem3 : Id (Sigma A (\ u -> Id A (f x) u)) (pair (f x) (refl A (f x))) (pair a p)
                              lem3 = lem4 (f x) a p 

                              lem2 : Id Z (pair x (pair (f x) (refl A (f x)))) (pair x (pair a p))
                              lem2 = cong (Sigma A (\ a -> Id A (f x) a))
                                          (Sigma X (\ x -> Sigma A (\ a -> Id A (f x) a)))
                                          (\ z -> pair x z) 
                                          (pair (f x) (refl A (f x))) (pair a p) lem3

                              lem1 : Id Y (pair (f x) (pair x (refl A (f x)))) (pair a (pair x p))
                              lem1 = cong Z Y sw2 (pair x (pair (f x) (refl A (f x)))) (pair x (pair a p)) lem2

    rem2 : isEquiv X Y g
    rem2 = gradLemma X Y g h rgh sgh


secsub : (A:U) -> (z : subset1 A) -> Id (subset1 A) (sub21 A (sub12 A z)) z
secsub A = 
 split
  pair X f -> rem
   where
    F : A -> U
    F = fiber X A f 

    Y : U
    Y = Sigma A F

    h : Y -> A
    h = fst A F

    g : X -> Y
    g x = pair (f x) (pair x (refl A (f x)))

    rem2 : isEquiv X Y (\ x -> g x)
    rem2 = lem2SecSub A X f 

    rem1 : Id (subset1 A) (pair Y h) (pair X (\ x -> f x))
    rem1 = lemSecSub A X Y g rem2 h

    rem3 : Id (subset1 A) (pair X (\ x -> f x)) (pair X f)
    rem3 = cong (X->A) (subset1 A) (\ h -> pair X h) 
                (\ x -> f x) f (funExt X (\ _ -> A) (\ x-> f x) f (\x -> refl A (f x)))

    rem : Id (subset1 A) (pair Y h) (pair X f)
    rem = comp (subset1 A) (pair Y h) (pair X (\ x -> f x)) (pair X f) rem1 rem3

thmSubset : (A:U) -> Id U (subset1 A) (subset2 A)
thmSubset A = isEquivEq (subset1 A) (subset2 A) (sub12 A) rem
 where rem : isEquiv (subset1 A) (subset2 A) (sub12 A)
       rem = gradLemma (subset1 A) (subset2 A) (sub12 A) (sub21 A) (retsub A) (secsub A)