From: Anders Mörtberg Date: Mon, 30 Oct 2017 20:07:40 +0000 (-0400) Subject: direct proofs that things are sets X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=0cdd084498c3f5de53a26ae756e4a9f33625fa1f;p=cubicaltt.git direct proofs that things are sets --- diff --git a/examples/nat.ctt b/examples/nat.ctt index 47eee38..25f9a80 100644 --- a/examples/nat.ctt +++ b/examples/nat.ctt @@ -117,3 +117,33 @@ equalNat : nat -> nat -> bool = split suc m -> split@(nat -> bool) with zero -> false suc n -> equalNat m n + +-- Direct proof that nat is a set: +invP : (n m : nat) (p : Path nat n m) -> U = split + zero -> split@((m : nat) (p : Path nat zero m) -> U) with + zero -> \(p : Path nat zero zero) -> + Path (Path nat zero zero) p (<_> zero) + suc m -> \(p : Path nat zero (suc m)) -> N0 + suc n -> split@((m : nat) (p : Path nat (suc n) m) -> U) with + zero -> \(p : Path nat (suc n) zero) -> N0 + suc m -> \(p : Path nat (suc n) (suc m)) -> + Path (Path nat (suc n) (suc m)) p ( suc (pred (p @ i))) + +-- using J for now +pinv : (n m : nat) (p : Path nat n m) -> invP n m p = split + zero -> J nat zero (invP zero) (<_ _> zero) + suc n -> J nat (suc n) (invP (suc n)) (<_ _> suc n) + +lem : (n : nat) (p : Path nat n n) -> Path (Path nat n n) p (<_> n) = split + zero -> pinv zero zero + suc n -> \(p : Path nat (suc n) (suc n)) -> + compPath (Path nat (suc n) (suc n)) p ( suc (pred (p @ i))) (<_> suc n) + (pinv (suc n) (suc n) p) + ( suc (lem n ( pred (p @ k)) @ i @ j)) + +natset' (n : nat) : (m : nat) (p q : Path nat n m) -> Path (Path nat n m) q p = + J nat n (\(m : nat)(p : Path nat n m) -> + (q : Path nat n m) -> Path (Path nat n m) q p) + (lem n) + +setnat (n m : nat) (p q : Path nat n m) : Path (Path nat n m) p q = natset' n m q p diff --git a/examples/prelude.ctt b/examples/prelude.ctt index 4c3a480..6465191 100644 --- a/examples/prelude.ctt +++ b/examples/prelude.ctt @@ -268,6 +268,42 @@ propOr (A B : U) (hA : prop A) (hB : prop B) (h : A -> neg B) : prop (or A B) = inl b' -> efq (Path (or A B) (inr a') (inl b')) (h b' a') inr b' -> inr (hB a' b' @ i) +-- Direct proof that or A B is a set if A and B are: +invOr (A B : U) : (u v : or A B) (p : Path (or A B) u v) -> U = split + inl a -> split@((v : or A B) -> (p : Path (or A B) (inl a) v) -> U) with + inl a' -> \(p : Path (or A B) (inl a) (inl a')) -> + (q : Path A a a') * (Path (Path (or A B) (inl a) (inl a')) p ( inl (q @ i))) + inr b' -> \(p : Path (or A B) (inl a) (inr b')) -> N0 + inr b -> split@((v : or A B) -> (p : Path (or A B) (inr b) v) -> U) with + inl a' -> \(p : Path (or A B) (inr b) (inl a')) -> N0 + inr b' -> \(p : Path (or A B) (inr b) (inr b')) -> + (q : Path B b b') * (Path (Path (or A B) (inr b) (inr b')) p ( inr (q @ i))) + +pinvOr (A B : U) : (u v : or A B) (p : Path (or A B) u v) -> invOr A B u v p = split + inl a -> J (or A B) (inl a) (invOr A B (inl a)) (<_> a,<_ _> inl a) + inr b -> J (or A B) (inr b) (invOr A B (inr b)) (<_> b,<_ _> inr b) + +lemOr (A B : U) (setA : set A) (setB : set B) : + (u : or A B) (p : Path (or A B) u u) -> Path (Path (or A B) u u) p (<_> u) = split + inl a -> \(p : Path (or A B) (inl a) (inl a)) -> + let qa : invOr A B (inl a) (inl a) p = pinvOr A B (inl a) (inl a) p + in compPath (Path (or A B) (inl a) (inl a)) p ( inl (qa.1 @ i)) (<_> inl a) qa.2 + ( inl (setA a a qa.1 (<_> a) @ i @ j)) + inr b -> \(p : Path (or A B) (inr b) (inr b)) -> + let qb : invOr A B (inr b) (inr b) p = pinvOr A B (inr b) (inr b) p + in compPath (Path (or A B) (inr b) (inr b)) p ( inr (qb.1 @ i)) (<_> inr b) qb.2 + ( inr (setB b b qb.1 (<_> b) @ i @ j)) + +orset' (A B : U) (setA : set A) (setB : set B) (u : or A B) : + (v : or A B) (p q : Path (or A B) u v) -> Path (Path (or A B) u v) q p = + J (or A B) u (\(v : or A B) (p : Path (or A B) u v) -> + (q : Path (or A B) u v) -> Path (Path (or A B) u v) q p) + (lemOr A B setA setB u) + +orset (A B : U) (setA : set A) (setB : set B) (u v : or A B) (p q : Path (or A B) u v) : + Path (Path (or A B) u v) p q = orset' A B setA setB u v q p + + stable (A:U) : U = neg (neg A) -> A const (A : U) (f : A -> A) : U = (x y : A) -> Path A (f x) (f y)