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) (a0,b0) (a1,b1)
lemPInj1 A B pB a0 a1 p = subst A C a0 a1 p rem
 where
  C : A -> U                                      -- (a1:A) -> Id A a0 a1 -> U
  C a1 = (b0:B a0) -> (b1:B a1) -> Id (Sigma A B) (a0,b0) (a1,b1)

  rem : C a0
  rem b0 b1 = mapOnPath (B a0) (Sigma A B) (\ b -> (a0,b)) b0 b1 (pB a0 b0 b1)

lemPropInj : (A : U) (B : A -> U) -> ((x:A) -> prop (B x)) -> injective (Sigma A B) A (\ z -> z.1)
lemPropInj A B pB z0 z1 p = lemPInj1 A B pB z0.1 z1.1 p z0.2 z1.2


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 z.1))
lemPInj2 A B pB z = rem
   where
    T : U
    T = Sigma A B

    a:A
    a = z.1

    b : B a
    b = z.2

    L : U
    L = Id T z z

    C : A -> U
    C a1 = (b0 : B a) ->  (b1:B a1) -> Id T (z.1,b0) (a1,b1)

    rem2 : C a
    rem2 b0 b1 = mapOnPath (B a) T (\ b -> (z.1,b)) b0 b1 (pB a b0 b1)

    rem1 : Id (C a) rem2 (lemPInj1 A B pB a a (refl A a))
    rem1 = substeq A C a 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 (mapOnPath (B a) T (\ b -> (a,b)) b b (refl (B a) b)) (rem2 b b)
    rem3 = mapOnPath Lb L (mapOnPath (B a) T (\ b -> (a,b)) b b) (refl (B a) b) (pB a b b) rem4

    rem5 : Id ((b1 : B a) -> Id T (a,b) (a,b1)) (rem2 b) (lemPInj1 A B pB a a (refl A a) b)
    rem5 = appEq (B a) (\ b0 -> (b1 : B a) -> Id T (a,b0) (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 (a,b) (a,b1)) b
                (rem2 b) (lemPInj1 A B pB a a (refl A a) b) rem5

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

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

isTrue : Omega -> U
isTrue z = z.1

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
   injf : injective Omega U isTrue
   injf = lemPropInj U prop propIsProp

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

lemInj : (A B : U) (f : A -> B) -> (injf : injective A B f)
              -> ((x:A) -> Id (Id A x x) (refl A x) (injf x x (refl B (f x))))
              -> (x y : A) -> (p:Id A x y) -> Id (Id A x y) p (injf x y (mapOnPath A B f x y p))
lemInj A B f injf h x =
 J A x (\ y p -> Id (Id A x y) p (injf x y (mapOnPath A B f x y p))) (h x)

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

   g : (x:Omega) -> prop (isTrue x)
   g x = x.2

   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 (mapOnPath 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))
                       (rem2 x y p) (rem2 x y q) rem8
     where
        h : Id Omega x y -> Id U (isTrue x) (isTrue y)
        h = mapOnPath 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)

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