module omega where

import univalence

Omega : U
Omega = Sigma U prop

-- Omega is the -set- of truth values
-- not trivial and needs the following Lemmas

-- if B is a family of proposition over A then Sigma A B -> A is injective

lemPInj1 :  (A : U) (B : A -> U) -> ((x:A) -> prop (B x)) -> (a0 a1:A) -> (p:Id A a0 a1) ->
            (b0:B a0) -> (b1:B a1) -> Id (Sigma A B) (pair a0 b0) (pair a1 b1)
lemPInj1 A B pB a0 =  J A a0 C rem
 where
  C : (a1:A) -> Id A a0 a1 -> U
  C a1 p = (b0:B a0) -> (b1:B a1) -> Id (Sigma A B) (pair a0 b0) (pair a1 b1)

  rem : C a0 (refl A a0)
  rem b0 b1 = cong (B a0) (Sigma A B) (\ b -> pair a0 b) b0 b1 (pB a0 b0 b1)

lemPropInj : (A : U) (B : A -> U) -> ((x:A) -> prop (B x)) -> injective (Sigma A B) A (fst A B)
lemPropInj A B pB =
 split 
  pair a0 b0 -> split
                 pair a1 b1 -> \ p -> lemPInj1 A B pB a0 a1 p b0 b1

lemPInj2 :  (A : U) (B : A -> U) -> (pB: (x:A) -> prop (B x)) -> (z:Sigma A B) ->
            Id (Id (Sigma A B) z z) (refl (Sigma A B) z) (lemPropInj A B pB z z (refl A (fst A B z)))
lemPInj2 A B pB = 
 split 
  pair a b -> rem
   where
    T : U
    T = Sigma A B 

    L : U
    L = Id T (pair a b) (pair a b)

    C : (a1:A) -> Id A a a1 -> U
    C a1 p = (b0 : B a) ->  (b1:B a1) -> Id T (pair a b0) (pair a1 b1)

    rem2 : C a (refl A a)
    rem2 b0 b1 = cong (B a) T (\ b -> pair a b) b0 b1 (pB a b0 b1)

    rem1 : Id (C a (refl A a)) rem2 (lemPInj1 A B pB a a (refl A a))
    rem1 = Jeq A a C rem2
             
    Lb : U
    Lb = Id (B a) b b

    rem4 : Id Lb  (refl (B a) b) (pB a b b)
    rem4 = propUIP (B a) (pB a) b b (refl (B a) b) (pB a b b)

    rem3 : Id L (cong (B a) T (\ b -> pair a b) b b (refl (B a) b)) (rem2 b b)
    rem3 = cong Lb L (cong (B a) T (\ b -> pair a b) b b) (refl (B a) b) (pB a b b) rem4
        
    rem5 : Id ((b1 : B a) -> Id T (pair a b) (pair a b1)) (rem2 b) (lemPInj1 A B pB a a (refl A a) b)
    rem5 = appEq (B a) (\ b0 -> (b1 : B a) -> Id T (pair a b0) (pair a b1)) b rem2 (lemPInj1 A B pB a a (refl A a)) rem1
     
    rem6 : Id L (rem2 b b) (lemPInj1 A B pB a a (refl A a) b b)
    rem6 = appEq (B a) (\ b1 -> Id T (pair a b) (pair a b1)) b (rem2 b) (lemPInj1 A B pB a a (refl A a) b) rem5

    rem7 : Id L (refl T (pair a b)) (cong (B a) T (\ b -> pair a b) b b (refl (B a) b))
    rem7 = congRefl (B a) T (\ b -> pair a b) b

    rem8 : Id L (refl T (pair a b)) (rem2 b b)
    rem8 = comp L (refl T (pair a b)) (cong (B a) T (\ b -> pair a b) b b (refl (B a) b)) (rem2 b b) rem7 rem3

    rem : Id L (refl T (pair a b)) (lemPInj1 A B pB a a (refl A a) b b)
    rem = comp L (refl T (pair a b)) (rem2 b b) (lemPInj1 A B pB a a (refl A a) b b) rem8 rem6

-- we should be able to deduce from all this that Omega is a set

isTrue : Omega -> U
isTrue = fst U prop

lemIsTrue : (x y : Omega) -> (isTrue x -> isTrue y) -> (isTrue y -> isTrue x) -> Id Omega x y
lemIsTrue x y f g = injf x y rem
 where 
   G : (x:Omega) -> prop (isTrue x)
   G = snd U prop

   injf : injective Omega U isTrue
   injf = lemPropInj U prop propIsProp

   rem : Id U (isTrue x) (isTrue y)
   rem = propId (isTrue x) (isTrue y) (G x) (G y) f g 


omegaIsSet : set Omega
omegaIsSet = rem4
 where
   rem : (A:U) -> prop (prop A)
   rem = propIsProp

   g : (x:Omega) -> prop (isTrue x)
   g = snd U prop

   injf : injective Omega U isTrue
   injf = lemPropInj U prop rem 

   rem1 : (z:Omega) -> Id (Id Omega z z) (refl Omega z) (injf z z (refl U (isTrue z)))
   rem1 = lemPInj2 U prop rem
   
   rem2 : (x y : Omega) -> (p : Id Omega x y) -> Id (Id Omega x y) p (injf x y (cong Omega U isTrue x y p))
   rem2 = lemInj Omega U isTrue injf rem1

   rem3 : (x y : Omega) -> prop (Id U (isTrue x) (isTrue y))
   rem3 x y = idPropIsProp (isTrue x) (isTrue y) (g x) (g y)

   rem4 : (x y : Omega) -> (p q : Id Omega x y) -> Id (Id Omega x y) p q
   rem4 x y p q = compDown (Id Omega x y) p (injf x y (h p)) q (injf x y (h q)) rem6 rem7 rem8
     where
        h : Id Omega x y -> Id U (isTrue x) (isTrue y)
        h = cong Omega U isTrue x y

        rem5 : Id (Id U (isTrue x) (isTrue y)) (h p) (h q)
        rem5 = rem3 x y (h p) (h q)

        rem6 : Id (Id Omega x y) p (injf x y (h p))
        rem6 = rem2 x y p

        rem7 : Id (Id Omega x y) q (injf x y (h q))
        rem7 = rem2 x y q

        rem8 : Id (Id Omega x y) (injf x y (h p)) (injf x y (h q))
        rem8 = cong (Id U (isTrue x) (isTrue y)) (Id Omega x y) (injf x y) (h p) (h q) rem5