more on setquot. on the way to define an equality test for hz

diff --git a/examples/equiv.ctt b/examples/equiv.ctt
index 6105336a0cdd015cf9dcb3f1f8272986a30a36b2..4b24fa7891bfaa97d74a6518d48bbdd35e1f9b99 100644 (file)
--- a/examples/equiv.ctt
+++ b/examples/equiv.ctt
@@ -12,7 +12,8 @@ isEquiv (A B : U) (f : A -> B) : U = (y : B) -> isContr (fiber A B f y)
 equiv (A B : U) : U = (f : A -> B) * isEquiv A B f
 
 propIsEquiv (A B : U) (f : A -> B)
-  : prop (isEquiv A B f) = \ (u0 u1:isEquiv A B f) -> <i> \ (y:B) -> propIsContr (fiber A B f y) (u0 y) (u1 y) @ i
+  : prop (isEquiv A B f) = 
+  \ (u0 u1:isEquiv A B f) -> <i> \ (y:B) -> propIsContr (fiber A B f y) (u0 y) (u1 y) @ i
 
 equivLemma (A B : U)
   : (v w : equiv A B) -> Id (A -> B) v.1 w.1 -> Id (equiv A B) v w

diff --git a/examples/hz.ctt b/examples/hz.ctt
index 28052040446eb5dfea01358f1296cf8ca97d9678..dfb847dbc32ce84f923f0dbd6bbd054af08dfb3f 100644 (file)
--- a/examples/hz.ctt
+++ b/examples/hz.ctt
@@ -8,16 +8,18 @@ nat2 : U = and nat nat
 
 rel : eqrel nat2 = (r,rem)
   where
-  r : hrel nat2) = \(x y : nat2) -> 
+  r : hrel nat2 = \(x y : nat2) -> 
     (Id nat (add x.1 y.2) (add x.2 y.1),natSet (add x.1 y.2) (add x.2 y.1))
     
-  rem : iseqrel nat2 r = ((rem1,refl nat2),rem2)
-   where
-   rem1 : istrans nat2 r = undefined
-   rem2 : issymm nat2 r = undefined
+  rem : iseqrel nat2 r = undefined -- ((rem1,refl nat2),rem2)
+   -- where
+   -- rem1 : istrans nat2 r = undefined
+   -- rem2 : issymm nat2 r = undefined
 
-hz : U = setquot nat2 rel
+hz : U = setquot nat2 rel.1
 zeroz : hz = setquotpr nat2 rel (zero,zero)
 onez : hz = setquotpr nat2 rel (one,zero)
 
-test : neg (Id hz zeroz onez) = undefined
\ No newline at end of file
+discretehz : discrete hz = undefined
+
+test01 : bool = discretetobool hz discretehz zeroz onez
\ No newline at end of file

diff --git a/examples/prelude.ctt b/examples/prelude.ctt
index 6c7f348c7e82d0554b6c394bf466ff9d0b2f2684..d9b2163020262dc3f31dadd569f8548a0fbc5df5 100644 (file)
--- a/examples/prelude.ctt
+++ b/examples/prelude.ctt
@@ -143,8 +143,13 @@ propSet (A : U) (h : prop A) (a b : A) (p q : Id A a b) : Id (Id A a b) p q =
                 , (j=0) -> h a (p @ i)
                 , (j=1) -> h a (q @ i)]
 
-propIsProp (A : U) (f g : prop A) : Id (prop A) f g =
- <i> \(a b :A) -> (propSet A f a b (f a b) (g a b)) @ i
+
+propIsProp (A : U) : prop (prop A) =
+  \(f g : prop A) ->
+    <i> \(a b : A) -> (propSet A f a b (f a b) (g a b)) @ i
+
+-- propIsProp (A : U) (f g : prop A) : Id (prop A) f g =
+--  <i> \(a b :A) -> (propSet A f a b (f a b) (g a b)) @ i
 
 setIsProp (A : U) (f g : set A) : Id (set A) f g =
  <i> \(a b :A) -> (propIsProp (Id A a b) (f a b) (g a b)) @ i
@@ -221,13 +226,14 @@ setUnit : set Unit = propSet Unit propUnit
 data or (A B : U) = inl (a : A)
                   | inr (b : B)
 
+propOr (A B : U) (hA : prop A) (hB : prop B) (h : A -> neg B) : prop (or A B) = undefined
+
 stable (A:U) : U = neg (neg A) -> A
 
 const (A : U) (f : A -> A) : U = (x y : A) -> Id A (f x) (f y)
 
 exConst (A : U) : U = (f:A -> A) * const A f
 
-
 propN0 : prop N0 = \ (x y:N0) -> efq (Id N0 x y) x
 
 propNeg (A:U) : prop (neg A) = \ (f g:neg A) -> <i>\(x:A) -> (propN0 (f x) (g x))@i
@@ -236,6 +242,9 @@ dNeg (A:U) (a:A) : neg (neg A) = \ (h : neg A) -> h a
 
 dec (A : U) : U = or A (neg A)
 
+propDec (A : U) (h : prop A) : prop (dec A) =
+  propOr A (neg A) h (propNeg A) (\(x : A) (h : neg A) -> h x)
+
 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))

diff --git a/examples/setquot.ctt b/examples/setquot.ctt
index 1d92302a6a1737c9fe2de5aa61907e43564dae3c..09fdb3875164b67038b6be5c73141cda23f44900 100644 (file)
--- a/examples/setquot.ctt
+++ b/examples/setquot.ctt
@@ -38,24 +38,23 @@ 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 that logical equivalence is equiv for props
--- equivhProp (P P' : hProp) (f : P.1 -> P'.1) (g : P'.1 -> P.1) : equiv P.1 P'.1 = undefined
--- (f,isEquivf)
---   where
---   isEquivf : isEquiv P.1 P'.1 f = (s,t)
---     where
---     s (y : P'.1) : fiber P.1 P'.1 f y = (g y,P'.2 (f (g y)) y)
---     t (y : P'.1) (w : fiber P.1 P'.1 f y) : Id ((x :  P.1) * Id P'.1 (f x) y) (s y) w =
---       subtypeEquality P.1 (\(x :  P.1) -> Id P'.1 (f x) y) pb (s y) w r1
---       where
---       pb (x : P.1) : (a b : Id P'.1 (f x) y) -> Id (Id P'.1 (f x) y) a b = propSet P'.1 P'.2 (f x) y
---       r1 : Id P.1 (s y).1 w.1 = P.2 (s y).1 w.1
+equivhProp (P P' : hProp) (f : P.1 -> P'.1) (g : P'.1 -> P.1) : equiv P.1 P'.1 =
+  (f,isEquivf)
+   where
+   isEquivf (y : P'.1) : isContr (fiber P.1 P'.1 f y) = (s,t)
+    where
+    s : fiber P.1 P'.1 f y = (g y,P'.2 y (f (g y)))
+    t (w : fiber P.1 P'.1 f y) : Id ((x :  P.1) * Id P'.1 y (f x)) s w =
+      subtypeEquality P.1 (\(x :  P.1) -> Id P'.1 y (f x)) pb s w r1
+       where
+       pb (x : P.1) : (a b : Id P'.1 y (f x)) -> Id (Id P'.1 y (f x)) a b = propSet P'.1 P'.2 y (f x)
+       r1 : Id P.1 s.1 w.1 = P.2 s.1 w.1
 
 -- Proof of uahp using full univalence
--- uahp' (P P' : hProp) (f : P.1 -> P'.1) (g : P'.1 -> P.1) : Id hProp P P' = undefined
-  -- subtypeEquality U prop propIsProp P P' rem
-  -- where
-  -- rem : Id U P.1 P'.1 =
-  --   invEq (Id U P.1 P'.1) (equiv P.1 P'.1) (univalence P.1 P'.1) (equivhProp P P' f g)
+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 = transport (<i> corrUniv P.1 P'.1 @ -i) (equivhProp P P' f g)
 
 -- Direct proof of uahp
 uahp (P P' : hProp) (f : P.1 -> P'.1) (g : P'.1 -> P.1) : Id hProp P P' =
@@ -176,6 +175,59 @@ setquotunivprop (X : U) (R : eqrel X) (P : setquot X R.1 -> hProp)
      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
 
+setquotuniv2prop (X : U) (R : eqrel X) (P : setquot X R.1 -> setquot X R.1 -> hProp)
+  (ps : (x x' : X) -> (P (setquotpr X R x) (setquotpr X R x')).1) (c c' : setquot X R.1) : (P c c').1 =
+    setquotunivprop X R (\ (c0' : setquot X R.1) -> P c c0')
+      (\ (x : X) -> setquotunivprop X R (\ (c0 : setquot X R.1) -> P c0 (setquotpr X R x))
+                      (\ (x0 : X) -> ps x0 x) c) c'
+
+isincl (X Y : U) (f : X -> Y) : U = (y : Y) -> prop (fiber X Y f y)
+
+iscompsetquotpr (X : U) (R : eqrel X) (x x' : X) (a : (R.1 x x').1) :
+  Id (setquot X R.1) (setquotpr X R x) (setquotpr X R x') = undefined
+
+weqpathsinsetquot (X : U) (R : eqrel X) (x x' : X) : 
+  equiv (R.1 x x').1 (Id (setquot X R.1) (setquotpr X R x) (setquotpr X R x')) = undefined
+
+isdecprop (X : U) : U = and (prop X) (dec X)
+
+propisdecprop (X : U): prop (isdecprop X) = 
+  propSig (prop X) (\ (_ : prop X) -> dec X) rem1 rem2
+  where
+  rem1 : prop (prop X) = propIsProp X
+  rem2 : prop X -> prop (dec X) = propDec X
+
+isdeceqif (X : U) (h : (x x' : X) -> isdecprop (Id X x x')) : discrete X = 
+  \(x x' : X) -> (h x x').2
+
+propEquiv (X Y : U) (w : equiv X Y) : prop X -> prop Y = subst U prop X Y rem
+  where
+  rem : Id U X Y = transport (<i> corrUniv X Y @ -i) w
+
+isdecpropweqf (X Y : U) (w : equiv X Y) (hX : isdecprop X) : isdecprop Y = (rem1,rem2 hX.2)
+  where
+  rem1 : prop Y = propEquiv X Y w hX.1
+  rem2 : dec X -> dec Y = split
+    inl x -> inl (w.1 x)
+    inr nx -> inr (\(y : Y) -> nx (invEq X Y w y))
+
+isdiscretesetquot (X : U) (R : eqrel X) (is : (x x' : X) -> isdecprop (R.1 x x').1) :
+  discrete (setquot X R.1) = isdeceqif (setquot X R.1) rem
+  where
+  rem : (x x' : setquot X R.1) -> isdecprop (Id (setquot X R.1) x x') =
+    setquotuniv2prop X R 
+      (\(x0 x0' : setquot X R.1) -> (isdecprop (Id (setquot X R.1) x0 x0'),
+                                     propisdecprop (Id (setquot X R.1) x0 x0'))) rem'
+    where
+    rem' (x0 x0' : X) : isdecprop (Id (setquot X R.1) (setquotpr X R x0) (setquotpr X R x0')) =
+      isdecpropweqf (R.1 x0 x0').1 (Id (setquot X R.1) (setquotpr X R x0) (setquotpr X R x0')) 
+                    (weqpathsinsetquot X R x0 x0') (is x0 x0')
+
+discretetobool (X : U) (h : discrete X) (x y : X) : bool = rem (h x y)
+  where
+  rem : dec (Id X x y) -> bool = split
+    inl _ -> true
+    inr _ -> false
 
 -- The bool exercise: