From: Anders Mörtberg <andersmortberg@gmail.com>
Date: Fri, 15 Jan 2016 03:55:34 +0000 (-0500)
Subject: setquot is a set
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=138fd1cceecd62fd7cd03bb2979eb142c9aec658;p=cubicaltt.git

setquot is a set
---

diff --git a/examples/setquot.ctt b/examples/setquot.ctt
index ec2db10..0efaa96 100644
--- a/examples/setquot.ctt
+++ b/examples/setquot.ctt
@@ -183,17 +183,14 @@ setquotuniv2prop (X : U) (R : eqrel X) (P : setquot X R.1 -> setquot X R.1 -> hP
       (\ (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)
-
-
--- Theorem isasetsetquot {X : UU} (R : hrel X) : isaset (setquot R).
--- Proof.
--- apply (isasetsubset (@pr1 _ _) (isasethsubtypes X)).
--- apply isinclpr1; intro x.
--- apply isapropiseqclass.
--- Defined.
+setsetquot (X : U) (R : hrel X) : set (setquot X R) =
+  setSig (hsubtypes X) (\(A : hsubtypes X) -> iseqclass X R A)
+    sA sB
+    where
+    sA : set (hsubtypes X) = sethsubtypes X
+    sB (x : hsubtypes X) : set (iseqclass X R x) = propSet (iseqclass X R x) (propiseqclass X R x)
 
-setsetquot (X : U) (R : hrel X) : set (setquot X R) = undefined
+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