From: Anders Mörtberg Date: Thu, 3 Dec 2015 14:30:41 +0000 (-0500) Subject: add a short version of setquot X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=5821973481883bb3b538af0ab77baeb6129f7297;p=cubicaltt.git add a short version of setquot --- diff --git a/examples/bool.ctt b/examples/bool.ctt index a10709c..c542ce4 100644 --- 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 ( 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) -> 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) -> lem2 (p@i) (q@i) (p@i/\k) (q@i/\k) @ j + +lem4 : (y:bool) (p:Id bool false y) -> Id bool false y = split + false -> \ (p : Id bool false false) -> 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) -> lem5 (p@i) (q@i) (p@i/\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 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) = + 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 = + 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 = + \(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 = + \(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 = + \(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'