add a short version of setquot

diff --git a/examples/bool.ctt b/examples/bool.ctt
index a10709c4a1053472ba8dbade1bb9df7703a65888..c542ce4711f297569307e715396eed5d33366284 100644 (file)
--- a/examples/bool.ctt
+++ b/examples/bool.ctt
@@ -4,6 +4,10 @@ import hedberg
 
 data bool = false | true
 
+
+-- Proof that bool is a set using hedberg:
+
+
 caseBool (A : U) (f t : A) : bool -> A = split
  false -> f
  true  -> t
@@ -26,7 +30,44 @@ boolDec : (b1 b2 : bool) -> dec (Id bool b1 b2) = split
    false -> inr trueNeqFalse
    true -> inl (<i> true)
 
-setbool : set bool = hedberg bool boolDec
+setbool' : set bool = hedberg bool boolDec
+
+
+-- Direct proof that bool is a set:
+
+lem1 : (y:bool) (p:Id bool true y) -> Id bool true y = split
+ false -> \ (p : Id bool true false) -> p
+ true -> \ (p : Id bool true true) -> <i>true
+
+lem2 : (x y :bool)  (p:Id bool true x) (q:Id bool true y) -> Id bool x y = split
+ false -> \ (y:bool) (p:Id bool true false) (q:Id bool true y) -> efq (Id bool false y) (trueNeqFalse p)
+ true -> \ (y:bool) (p:Id bool true true) (q:Id bool true y) -> lem1 y q
+
+lem3 : prop (Id bool true true) =
+ \ (p q:Id bool true true) -> <j i>lem2 (p@i) (q@i) (<k>p@i/\k) (<k>q@i/\k) @ j
+
+lem4 : (y:bool) (p:Id bool false y) -> Id bool false y = split
+ false -> \ (p : Id bool false false) -> <i>false
+ true -> \ (p : Id bool false true) -> p 
+
+lem5 : (x y :bool)  (p:Id bool false x) (q:Id bool false y) -> Id bool x y = split
+ false -> \ (y:bool) (p:Id bool false false) (q:Id bool false y) -> lem4 y q
+ true -> \ (y:bool) (p:Id bool false true) (q:Id bool false y) -> efq (Id bool true y) (falseNeqTrue p)
+
+lem6 : prop (Id bool false false) =
+ \ (p q:Id bool false false) -> <j i>lem5 (p@i) (q@i) (<k>p@i/\k) (<k>q@i/\k) @ j
+
+lem7 : (y:bool) (p:Id bool false y) (q:Id bool false y) -> Id (Id bool false y) p q = split
+ false -> lem6
+ true -> \ (p:Id bool false true) (q:Id bool false true) -> efq (Id (Id bool false true) p q) (falseNeqTrue p)
+
+lem8 : (y:bool) (p:Id bool true y) (q:Id bool true y) -> Id (Id bool true y) p q = split
+ false -> \ (p:Id bool true false) (q:Id bool true false) -> efq (Id (Id bool true false) p q) (trueNeqFalse p)
+ true -> lem3
+
+setbool : set bool = split
+ false -> lem7
+ true -> lem8
 
 
       ---------------------------------------------------------

diff --git a/examples/shortsetquot.ctt b/examples/shortsetquot.ctt
new file mode 100644 (file)
index 0000000..2be6de5
--- /dev/null
+++ b/examples/shortsetquot.ctt
@@ -0,0 +1,185 @@
+module shortsetquot where
+
+import bool
+import sigma
+
+subtypeEquality (A : U) (B : A -> U) (pB : (x : A) -> prop (B x))
+                (s t : (x : A) * B x) : Id A s.1 t.1 -> Id (sig A B) s t =
+  trans (Id A s.1 t.1) (Id (sig A B) s t) rem
+    where
+    rem : Id U (Id A s.1 t.1) (Id (sig A B) s t) =
+      <i> lemSigProp A B pB s t @ -i
+
+propAnd (A B : U) (pA : prop A) (pB : prop B) :
+  prop (and A B) = propSig A (\(_ : A) -> B) pA (\(_ : A) -> pB)
+
+
+
+
+-- (* Propositions *)
+
+hProp : U = (X : U) * prop X
+
+-- Impredicative encoding of propositional truncation
+ishinh_UU (X : U) : U = (P : hProp) -> ((X -> P.1) -> P.1)
+
+propishinh (X : U) : prop (ishinh_UU X) =
+  propPi hProp (\(P : hProp) -> ((X -> P.1) -> P.1)) rem1
+  where
+   rem1 (P : hProp) : prop ((X -> P.1) -> P.1) =
+     propPi (X -> P.1) (\(_ : X -> P.1) -> P.1) (\(f : X -> P.1) -> P.2)
+
+ishinh (X : U) : hProp = (ishinh_UU X,propishinh X)
+
+hinhpr (X : U) : X -> (ishinh X).1 =
+  \(x : X) (P : hProp) (f : X -> P.1) -> f x
+
+hinhuniv (X : U) (P : hProp) (f : X -> P.1) (inhX : (ishinh X).1) : P.1 =
+  inhX P f
+
+-- Truncated sum
+hdisj (P Q : U) : hProp = ishinh (or P Q)
+
+hdisj_in1 (P Q : U) (X : P) : (hdisj P Q).1 = hinhpr (or P Q) (inl X)
+hdisj_in2 (P Q : U) (X : Q) : (hdisj P Q).1 = hinhpr (or P Q) (inr X)
+
+-- Direct proof of uahp
+uahp (P P' : hProp) (f : P.1 -> P'.1) (g : P'.1 -> P.1) : Id hProp P P' =
+  subtypeEquality U prop propIsProp P P' rem
+  where
+  rem : Id U P.1 P'.1 =
+    <i> glue B [ (i = 0) -> (A,f,g,s,t)
+               , (i = 1) -> (B,idfun B,idfun B,refl B,refl B) ]
+    where A : U = P.1
+          B : U = P'.1
+          s (y : B) : Id B (f (g y)) y = P'.2 (f (g y)) y
+          t (x : A) : Id A (g (f x)) x = P.2 (g (f x)) x
+
+
+-- (* Sets *)
+
+hSet : U = (X : U) * set X
+
+hsubtypes (X : U) : U = X -> hProp
+
+carrier (X : U) (A : hsubtypes X) : U = sig X (\(x : X) -> (A x).1)
+
+hrel (X : U) : U = X -> X -> hProp
+
+iseqclass (X : U) (R : hrel X) (A : hsubtypes X) : U =
+  and (and (ishinh (carrier X A)).1
+           ((x1 x2 : X) -> (R x1 x2).1 -> (A x1).1 -> (A x2).1))
+           ((x1 x2 : X) -> (A x1).1 -> (A x2).1 -> (R x1 x2).1)
+
+eqax0 (X : U) (R : hrel X) (A : hsubtypes X) (eqc : iseqclass X R A) :
+  (ishinh (carrier X A)).1 = eqc.1.1
+eqax1 (X : U) (R : hrel X) (A : hsubtypes X) (eqc : iseqclass X R A) :
+  (x1 x2 : X) -> (R x1 x2).1 -> (A x1).1 -> (A x2).1 = eqc.1.2
+eqax2 (X : U) (R : hrel X) (A : hsubtypes X) (eqc : iseqclass X R A) :
+  (x1 x2 : X) -> (A x1).1 -> (A x2).1 -> (R x1 x2).1 = eqc.2
+
+propiseqclass (X : U) (R : hrel X) (A : hsubtypes X) : prop (iseqclass X R A) =
+  propAnd (and (ishinh (carrier X A)).1
+               ((x1 x2 : X) -> (R x1 x2).1 -> (A x1).1 -> (A x2).1))
+                 ((x1 x2 : X) -> (A x1).1 -> (A x2).1 -> (R x1 x2).1)
+                 (propAnd (ishinh (carrier X A)).1
+                                 ((x1 x2 : X) -> (R x1 x2).1 -> (A x1).1 -> (A x2).1) p1 p2)
+                 p3
+  where
+  p1 : prop (ishinh (carrier X A)).1 = propishinh (carrier X A)
+
+  p2 (f g : (x1 x2 : X) -> (R x1 x2).1 -> (A x1).1 -> (A x2).1) :
+   Id ((x1 x2 : X) -> (R x1 x2).1 -> (A x1).1 -> (A x2).1) f g =
+    <i> \(x1 x2 : X) (h1 : (R x1 x2).1) (h2 : (A x1).1) ->
+         (A x2).2 (f x1 x2 h1 h2) (g x1 x2 h1 h2) @ i
+
+  p3 (f g : (x1 x2 : X) -> (A x1).1 -> (A x2).1 -> (R x1 x2).1) :
+    Id ((x1 x2 : X) -> (A x1).1 -> (A x2).1 -> (R x1 x2).1) f g =
+   <i> \(x1 x2 : X) (h1 : (A x1).1) (h2 : (A x2).1) ->
+        (R x1 x2).2 (f x1 x2 h1 h2) (g x1 x2 h1 h2) @ i
+
+
+isrefl (X : U) (R : hrel X) : U = (x : X) -> (R x x).1
+issymm (X : U) (R : hrel X) : U = (x1 x2 : X) -> (R x1 x2).1 -> (R x2 x1).1
+istrans (X : U) (R : hrel X) : U =
+  (x1 x2 x3 : X) -> (R x1 x2).1 -> (R x2 x3).1 -> (R x1 x3).1
+
+ispreorder (X : U) (R : hrel X) : U = and (istrans X R) (isrefl X R)
+
+iseqrel (X : U) (R : hrel X) : U = and (ispreorder X R) (issymm X R)
+
+eqrel (X : U) : U = (R : hrel X) * (iseqrel X R)
+
+eqrelrefl (X : U) (R : eqrel X) : isrefl X R.1 = R.2.1.2
+eqrelsymm (X : U) (R : eqrel X) : issymm X R.1 = R.2.2
+eqreltrans (X : U) (R : eqrel X) : istrans X R.1 = R.2.1.1
+
+setquot (X : U) (R : hrel X) : U = (A : hsubtypes X) * (iseqclass X R A)
+pr1setquot (X : U) (R : hrel X) (Q : setquot X R) : hsubtypes X = Q.1
+
+-- Canonical surjection to the quotient
+setquotpr (X : U) (R : eqrel X) (X0 : X) : setquot X R.1 = (A,((p1,p2),p3))
+   where
+   rax : isrefl X R.1 = eqrelrefl X R
+   sax : issymm X R.1 = eqrelsymm X R
+   tax : istrans X R.1 = eqreltrans X R
+   A : hsubtypes X = \(x : X) -> R.1 X0 x
+   p1 : (ishinh (carrier X A)).1 = hinhpr (carrier X A) (X0,rax X0)
+   p2 (x1 x2 : X) (X1 : (R.1 x1 x2).1) (X2 : (A x1).1) : (A x2).1 =
+     tax X0 x1 x2 X2 X1
+   p3 (x1 x2 : X) (X1 : (A x1).1) (X2 : (A x2).1) : (R.1 x1 x2).1 =
+     tax x1 X0 x2 (sax X0 x1 X1) X2
+
+setquotl0 (X : U) (R : eqrel X) (c : setquot X R.1) (x : carrier X c.1) :
+  Id (setquot X R.1) (setquotpr X R x.1) c =
+    subtypeEquality (hsubtypes X) (iseqclass X R.1) p (setquotpr X R x.1) c rem
+  where
+  p (A : hsubtypes X) : prop (iseqclass X R.1 A) = propiseqclass X R.1 A
+  rem : Id (hsubtypes X) (setquotpr X R x.1).1 c.1 =
+    <i> \(x : X) -> (rem' x) @ i -- inlined use of funext
+     where rem' (a : X) : Id hProp ((setquotpr X R x.1).1 a) (c.1 a) =
+            uahp ((setquotpr X R x.1).1 a) (c.1 a) l2r r2l   -- This is where uahp appears
+              where
+              l2r (r : ((setquotpr X R x.1).1 a).1) : (c.1 a).1 =
+                eqax1 X R.1 c.1 c.2 x.1 a r x.2
+              r2l : (c.1 a).1 -> ((setquotpr X R x.1).1 a).1 =
+                eqax2 X R.1 c.1 c.2 x.1 a x.2
+
+setquotunivprop (X : U) (R : eqrel X) (P : setquot X R.1 -> hProp)
+  (ps : (x : X) -> (P (setquotpr X R x)).1) (c : setquot X R.1) : (P c).1 =
+    hinhuniv (carrier X c.1) (P c) f rem
+   where
+   f (x : carrier X c.1) : (P c).1 =
+     let e : Id (setquot X R.1) (setquotpr X R x.1) c = setquotl0 X R c x
+     in subst (setquot X R.1) (\(w : setquot X R.1) -> (P w).1) (setquotpr X R x.1) c e (ps x.1)
+   rem : (ishinh (carrier X c.1)).1 = eqax0 X R.1 c.1 c.2
+
+
+
+-- Finally the exercise:
+
+R : eqrel bool = (r1,r2)
+  where
+  r1 : hrel bool = \(x y : bool) -> (Id bool x y,setbool x y)
+  r2 : iseqrel bool r1 = ((compId bool,refl bool),inv bool)
+
+true' : setquot bool R.1 = setquotpr bool R true
+false' : setquot bool R.1 = setquotpr bool R false
+
+P' (t : setquot bool R.1) : hProp =
+  hdisj (Id (setquot bool R.1) t true') (Id (setquot bool R.1) t false')
+
+K' (t : setquot bool R.1) : (P' t).1 = setquotunivprop bool R P' ps t
+  where
+  ps : (x : bool) -> (P' (setquotpr bool R x)).1 = split
+    false -> hdisj_in2 (Id (setquot bool R.1) false' true')
+                       (Id (setquot bool R.1) false' false') (<_> false')
+    true  -> hdisj_in1 (Id (setquot bool R.1) true' true')
+                       (Id (setquot bool R.1) true' false') (<_> true')
+
+test : (P' true').1 = hdisj_in1 (Id (setquot bool R.1) true' true')
+                                (Id (setquot bool R.1) true' false') (<_> true')
+
+
+-- This takes too long:
+-- > :n K' true'