{- Prop Module:
   - Prop Theorems;
   Copyright (c) Groupoid Infinity, 2014-2018.

   HoTT 3.3 Mere propositions. -}

module prop where
import proto
import path
import sigma

-- datatype properties: decideability, discretness, stability
efq        (A: U): empty -> A = emptyRec A
neg        (A: U): U = A -> empty
dneg  (A:U) (a:A): neg (neg A) = \(h: neg A) -> h a
neg        (A: U): U = A -> empty
dec        (A: U): U = either A (neg A)
stable     (A: U): U = neg (neg A) -> A
discrete   (A: U): U = (a b: A) -> dec (Path A a b)

-- see HoTT 3.4 Classical vs. intuitionistic logic

propUnit : isProp unit = split tt -> split@((x:unit) -> Path unit tt x) with { tt -> <i> tt }

fununit (A: U) (f g: A -> unit)
     (p: (x: A) -> Path unit (f x) (g x))
     : Path (A -> unit) f g
     = <i> \(a: A) -> p a @ i

-- Exists(A,B) = ||Sigma(A,B)||

lemPropF (A : U) (P : A -> U) (pP : (x : A) -> isProp (P x)) (a0 a1 :A)
         (p : Path A a0 a1) (b0 : P a0) (b1 : P a1)
       : PathP (<i>P (p@i)) b0 b1
       = <i> pP (p@i) (comp (<j>P (p@i/\j)) b0 [(i=0) -> <_>b0])
                      (comp (<j>P (p@i\/-j)) b1 [(i=1) -> <_>b1]) @ i

lemSig (A : U) (B : A -> U) (pB : (x : A) -> isProp (B x))
       (u v : (x:A) * B x) (p : Path A u.1 v.1)
     : Path ((x:A) * B x) u v
     = <i> (p@i,(lemPropF A B pB u.1 v.1 p u.2 v.2)@i)

propSig (A : U) (B : A -> U) (pA : isProp A)
        (pB : (x : A) -> isProp (B x)) (t u : (x:A) * B x)
      : Path ((x:A) * B x) t u
      = lemSig A B pB t u (pA t.1 u.1)

-- Forall(A,B) = ||Pi(A,B)||

propPi (A : U) (B: A -> U) (h: (x : A) -> isProp (B x)) (f0 f1: (x: A) -> B x) : Path ((x: A) -> B x) f0 f1
  = <i> \ (x:A) -> (h x (f0 x) (f1 x)) @ i

propPi2 (A: U) (B: A -> A -> U) (h: (x y: A) -> isProp (B x y)): isProp ((x y: A) -> B x y)
  = let p (a: A): isProp ((b: A) -> B a b) = propPi A (B a) (h a)
        B1 (a: A): U = (b: A) -> B a b
     in propPi A B1 p

propPi3 (A: U) (B: A -> A -> A -> U) (h: (x y z: A) -> isProp (B x y z)): isProp ((x y z: A) -> B x y z)
  = let p (a b: A): isProp ((c : A) -> B a b c) = propPi A (B a b) (h a b)
        B1 (a b: A): U = (c: A) -> B a b c
     in propPi2 A B1 p

---------

propN0 : isProp empty = \ (x y: empty) -> efq (Path empty x y) x

propNeg (A:U) : isProp (neg A) = \ (f g:neg A) -> <i>\(x:A) -> (propN0 (f x) (g x))@i

propOr (A B : U) (hA : isProp A) (hB : isProp B) (h : A -> neg B) : isProp (either A B) = split
    inl a' -> split@((b : either A B) -> Path (either A B) (inl a') b) with
        inl b' -> <i> inl (hA a' b' @ i)
        inr b' -> efq (Path (either A B) (inl a') (inr b')) (h a' b')
    inr a' -> split@((b : either A B) -> Path (either A B) (inr a') b) with
        inl b' -> efq (Path (either A B) (inr a') (inl b')) (h b' a')
        inr b' -> <i> inr (hB a' b' @ i)

propDec (A : U) (h : isProp A) : isProp (dec A) =
  propOr A (neg A) h (propNeg A) (\(x : A) (h : neg A) -> h x)

propAnd (A B : U) (pA : isProp A) (pB : isProp B) : isProp (prod A B) =
  propSig A (\(_ : A) -> B) pA (\(_ : A) -> pB)

---------

decEqCong (A B : U) (f : A -> B) (g : B -> A) : dec A -> dec B = split
  inl a -> inl (f a)
  inr h -> inr (\ (b:B) -> h (g b))

decStable (A:U) : dec A -> stable A = split
 inl a -> \ (h :neg (neg A)) -> a
 inr b -> \ (h :neg (neg A)) -> efq A (h b)

decConst (A : U) : dec A -> exConst A = split
  inl a -> (\ (x:A)  -> a, \ (x y:A) -> refl A a)
  inr h -> (\ (x:A) -> x, \ (x y:A) -> efq (Path A x y) (h x))

stableConst (A : U) (sA: stable A) : exConst A =
 (\ (x:A) -> sA (dneg A x),\ (x y:A) -> <i>sA (propNeg (neg A) (dneg A x) (dneg A y) @ i))

----------------------
isContrProp (A : U) (h : isContr A) : isProp A =
  \(a b : A) -> <i> comp (<_> A) h.1 [ (i = 0) -> h.2 a, (i = 1) -> h.2 b ]

isPropContr (A : U) (h : isProp A) : isContr A = undefined

lemProp (A : U) (h : A -> isProp A) : isProp A = \(a : A) -> h a a

propSet (A : U) (h : isProp A) : isSet A =
 \(a b : A) (p q : Path A a b) ->
   <j i> comp (<_> A) a [ (i=0) -> h a a
                        , (i=1) -> h a b
                        , (j=0) -> h a (p @ i)
                        , (j=1) -> h a (q @ i)]

propIsContr (A : U) : isProp (isContr A) = lemProp (isContr A) rem where
  rem (t : isContr A) : isProp (isContr A) = propSig A T pA pB where
  T (x : A) : U = (y : A) -> Path A x y
  pA (x y : A) : Path A x y = composition A x t.1 y (<i> t.2 x @ -i) (t.2 y)
  pB (x : A) : isProp (T x) = propPi A (\ (y : A) -> Path A x y) (propSet A pA x)

propIsProp (A : U) : isProp (isProp A) =
  \(f g : isProp A) -> <i> \(a b : A) ->
    propSet A f a b (f a b) (g a b) @ i

corSigProp (A:U) (B:A-> U) (pB : (x:A) -> isProp (B x)) (t u : Sigma A B) (p:Path A t.1 u.1) :
  isProp (PathP (<i>B (p@i)) t.2 u.2) = substInv U isProp T0 T1 rem rem1
 where P : Path U (B t.1) (B u.1) = <i>B (p@i)
       T0 : U = PathP P t.2 u.2
       T1 : U = Path (B u.1) (transport P t.2) u.2
       rem : Path U T0 T1 = pathSig0 A B t u p
       v2 : B u.1 = transport P t.2
       rem1 : isProp T1 = propSet (B u.1) (pB u.1) v2 u.2