From: Anders Mörtberg Date: Thu, 14 Jan 2016 21:56:45 +0000 (-0500) Subject: more on setquot. on the way to define an equality test for hz X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=886503e98e415388ef788974d528c7a47d757847;p=cubicaltt.git more on setquot. on the way to define an equality test for hz --- diff --git a/examples/equiv.ctt b/examples/equiv.ctt index 6105336..4b24fa7 100644 --- 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) -> \ (y:B) -> propIsContr (fiber A B f y) (u0 y) (u1 y) @ i + : prop (isEquiv A B f) = + \ (u0 u1:isEquiv A B f) -> \ (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 2805204..dfb847d 100644 --- 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 6c7f348..d9b2163 100644 --- 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 = - \(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) -> + \(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 = +-- \(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 = \(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) -> \(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 1d92302..09fdb38 100644 --- 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 ( 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 ( 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: