module axChoice where

import contr

-- an interesting isomorphism/equality

idTelProp : (A:U) (B:A -> U) (C:(x:A) -> B x -> U) -> 
              Id U ((x:A) -> Sigma (B x) (C x)) (Sigma ((x:A) -> B x) (\ f -> (x:A) -> C x (f x)))
idTelProp A B C = isoId T0 T1 f g sfg rfg 
 where
  T0 : U 
  T0 = (x:A) -> Sigma (B x) (C x) 

  T1 : U 
  T1 = Sigma ((x:A) -> B x) (\ f -> (x:A) -> C x (f x))

  f : T0 -> T1
  f = \ s -> pair (\ x -> fst (B x) (C x) (s x)) (\ x -> snd (B x) (C x) (s x))

  g : T1 -> T0
  g = split
       pair u v -> \ x -> pair (u x) (v x)

  sfg : (y:T1) -> Id T1 (f (g y)) y
  sfg = split
         pair u v -> rem u v 
           where
             rem2 : (u:Pi A B) (v:(x:A) -> C x (u x)) -> Id T1 (pair (\ x -> u x) (\ x -> v x)) (pair (\ x -> u x) (\ x -> v x))
             rem2 u v = refl T1 (pair (\ x -> u x) (\ x -> v x))

             rem1 : (u:Pi A B) (v:(x:A) -> C x (u x)) -> Id T1 (pair (\ x -> u x) (\ x -> v x)) (pair (\ x -> u x) v)
             rem1 u = funSplit A (\ x -> C x (u x)) (\ v -> Id T1 (pair (\ x -> u x) (\ x -> v x)) (pair (\ x -> u x) v)) (rem2 u)

             rem : (u:Pi A B) (v:(x:A) -> C x (u x)) -> Id T1 (pair (\ x -> u x) (\ x -> v x)) (pair u v)
             rem = funSplit A B (\ u -> (v:(x:A) -> C x (u x)) -> Id T1 (pair (\ x -> u x) (\ x -> v x)) (pair u v)) rem1

  rfg : (s:T0) -> Id T0 (g (f s)) s
  rfg s = funExt A (\ x ->  Sigma (B x) (C x)) (g (f s)) s rem
    where
      rem : (x:A) -> Id (Sigma (B x) (C x)) (pair (fst (B x) (C x) (s x)) (snd (B x) (C x) (s x))) (s x)
      rem x = surjPair (B x) (C x) (s x)

-- we deduce from this equality that isEquiv f is a proposition

propIsEquiv : (A B : U) -> (f : A -> B) -> prop (isEquiv A B f)
propIsEquiv A B f = subst U prop ((y:B) -> contr' (fiber A B f y)) (isEquiv A B f) rem rem1
 where 
   rem : Id U ((y:B) -> contr' (fiber A B f y)) (isEquiv A B f) 
   rem = idTelProp B (fiber A B f) (\ y -> \ s -> (v :fiber A B f y) -> Id (fiber A B f y) s v)

   rem1 : prop ((y:B) -> contr' (fiber A B f y))
   rem1 = isPropProd B (\ y -> contr' (fiber A B f y)) (\ y -> contr'IsProp (fiber A B f y))