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 z = fiber z.1 A z.2

sub21 : (A:U) -> subset2 A -> subset1 A
sub21 A P = (Sigma A P,\ x -> x.1)

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 (\x -> x.1)) P (lem1Sub A P)

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

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

lem2SecSub : (A X:U) (f:X -> A) -> 
               isEquiv X (Sigma A (fiber X A f)) (\ x -> (f x,(x,refl A (f x))))
lem2SecSub A X f =  gradLemma X Y g h rgh sgh
 where
    F : A -> U
    F = fiber X A f 

    Y : U
    Y = Sigma A F

    h : Y -> A
    h y = y.1

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

    h : Y -> X
    h y = y.2.1

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

    sw1 : Y -> Z
    sw1 y = (y.2.1,(y.1,y.2.2))

    sw2 : Z -> Y
    sw2 z = (z.2.1,(z.1,z.2.2))

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

    rgh : (y:Y) -> Id Y (g (h y)) y
    rgh y = lem y.2
              where 
               lem : (xp : Sigma X (\ x -> Id A (f x) y.1)) -> Id Y (g (h (y.1,xp))) (y.1,xp)
               lem xp = lem1
                            where
                              x:X
                              x = xp.1

                              p : Id A (f x) y.1
                              p = xp.2

                              C : (v u:A) -> Id A v u -> U
                              C v u q =  Id (Sigma A (Id A v)) (v,refl A v) (u,q)

                              lem5 : (v:A) -> C v v (refl A v)
                              lem5 v = refl (Sigma A (Id A v)) (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 (Id A (f x))) (f x,refl A (f x)) (y.1,p)
                              lem3 = lem4 (f x) y.1 xp.2 

                              lem2 : Id Z (x,(f x,refl A (f x))) (x,(y.1,xp.2))
                              lem2 = mapOnPath (Sigma A (Id A (f x)))
                                          (Sigma X (\ x -> Sigma A (Id A (f x))))
                                          (\ z -> (x,z)) 
                                          (f x,refl A (f x)) (y.1,xp.2) lem3

                              lem1 : Id Y (f x,(x,refl A (f x))) (y.1,xp)
                              lem1 = mapOnPath Z Y sw2 (x,(f x,refl A (f x))) (x,(y.1,p)) lem2

secsub : (A:U) -> (z : subset1 A) -> Id (subset1 A) (sub21 A (sub12 A z)) z
secsub A z = lemSecSub A z.1 Y g (lem2SecSub A z.1 z.2) h
   where
    X : U
    X = z.1

    F : A -> U
    F = fiber X A z.2

    Y : U
    Y = Sigma A F
  
    f : X -> A
    f = z.2

    h : Y -> A
    h y = y.1

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

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)