From 0cdd084498c3f5de53a26ae756e4a9f33625fa1f Mon Sep 17 00:00:00 2001
From: =?utf8?q?Anders=20M=C3=B6rtberg?= <andersmortberg@gmail.com>
Date: Mon, 30 Oct 2017 16:07:40 -0400
Subject: [PATCH] direct proofs that things are sets

---
 examples/nat.ctt     | 30 ++++++++++++++++++++++++++++++
 examples/prelude.ctt | 36 ++++++++++++++++++++++++++++++++++++
 2 files changed, 66 insertions(+)

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 (<i> 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 (<i> suc (pred (p @ i))) (<_> suc n)
+                 (pinv (suc n) (suc n) p)
+                 (<i j> suc (lem n (<k> 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' -> <i> 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 (<i> 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 (<i> 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 (<i> inl (qa.1 @ i)) (<_> inl a) qa.2
+                (<i j> 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 (<i> inr (qb.1 @ i)) (<_> inr b) qb.2
+                (<i j> 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)
-- 
2.34.1