From: Anders Mörtberg Date: Fri, 15 Jan 2016 19:08:23 +0000 (-0500) Subject: Finish the last undefined in setquot X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=3a1f9a1271cb9e8f6c03caa3cde804313099e89b;p=cubicaltt.git Finish the last undefined in setquot --- diff --git a/examples/setquot.ctt b/examples/setquot.ctt index 0efaa96..ce7b072 100644 --- a/examples/setquot.ctt +++ b/examples/setquot.ctt @@ -190,12 +190,22 @@ setsetquot (X : U) (R : hrel X) : set (setquot X R) = sA : set (hsubtypes X) = sethsubtypes X sB (x : hsubtypes X) : set (iseqclass X R x) = propSet (iseqclass X R x) (propiseqclass X R x) -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) : + Id (setquot X R.1) (setquotpr X R x) (setquotpr X R x') = + subtypeEquality (hsubtypes X) (iseqclass X R.1) rem1 (setquotpr X R x) (setquotpr X R x') rem2 + where + rem1 (x : hsubtypes X) : prop (iseqclass X R.1 x) = propiseqclass X R.1 x + rem2 : Id (hsubtypes X) (setquotpr X R x).1 (setquotpr X R x').1 = + \(x0 : X) -> rem x0 @ i + where + rem (x0 : X) : Id hProp (R.1 x x0) (R.1 x' x0) = uahp (R.1 x x0) (R.1 x' x0) f g + where + f (r0 : (R.1 x x0).1) : (R.1 x' x0).1 = + eqreltrans X R x' x x0 (eqrelsymm X R x x' a) r0 + g (r0 : (R.1 x' x0).1) : (R.1 x x0).1 = + eqreltrans X R x x' x0 a r0 + +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')) = (iscompsetquotpr X R x x',rem) where @@ -213,17 +223,18 @@ weqpathsinsetquot (X : U) (R : eqrel X) (x x' : X) : rem2 : Id hProp (R.1 x x') (R.1 x' x') = (e @ i).1 x' rem1 : Id hProp (R.1 x' x') (R.1 x x') = rem2 @ -i pA : prop (R.1 x x').1 = (R.1 x x').2 - pB : prop (Id (setquot X R.1) (setquotpr X R x) (setquotpr X R x')) = setsetquot X R.1 (setquotpr X R x) (setquotpr X R x') + pB : prop (Id (setquot X R.1) (setquotpr X R x) (setquotpr X R x')) = + setsetquot X R.1 (setquotpr X R x) (setquotpr X R x') isdecprop (X : U) : U = and (prop X) (dec X) -propisdecprop (X : U): prop (isdecprop 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 = +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 @@ -241,12 +252,12 @@ isdiscretesetquot (X : U) (R : eqrel X) (is : (x x' : X) -> isdecprop (R.1 x x') 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 + 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')) + 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)