{- 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 -> tt } fununit (A: U) (f g: A -> unit) (p: (x: A) -> Path unit (f x) (g x)) : Path (A -> unit) f g = \(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 (P (p@i)) b0 b1 = pP (p@i) (comp (P (p@i/\j)) b0 [(i=0) -> <_>b0]) (comp (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 = (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 = \ (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) -> \(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' -> 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' -> 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) -> sA (propNeg (neg A) (dneg A x) (dneg A y) @ i)) ---------------------- isContrProp (A : U) (h : isContr A) : isProp A = \(a b : A) -> 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) -> 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 ( 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) -> \(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 (B (p@i)) t.2 u.2) = substInv U isProp T0 T1 rem rem1 where P : Path U (B t.1) (B u.1) = 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