From: Anders Mörtberg Date: Fri, 11 Dec 2015 21:14:57 +0000 (-0500) Subject: Clean setquot X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=5c24e27b82934042ca92aafdeff70819c2c9e038;p=cubicaltt.git Clean setquot --- diff --git a/examples/prelude.ctt b/examples/prelude.ctt index f4825b1..20d5b43 100644 --- a/examples/prelude.ctt +++ b/examples/prelude.ctt @@ -241,6 +241,8 @@ injective (A B : U) (f : A -> B) : U = and (A B : U) : U = (_ : A) * B +propAnd (A B : U) (pA : prop A) (pB : prop B) : prop (and A B) = + propSig A (\(_ : A) -> B) pA (\(_ : A) -> pB) isoId (A B : U) (f : A -> B) (g : B -> A) (s : (y : B) -> Id B (f (g y)) y) diff --git a/examples/setquot.ctt b/examples/setquot.ctt index 030ad41..c4b4974 100644 --- a/examples/setquot.ctt +++ b/examples/setquot.ctt @@ -5,8 +5,6 @@ import sigma import pi import univalence --- First prove and rename things to be closer to UniMath: - 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 @@ -14,64 +12,33 @@ subtypeEquality (A : U) (B : A -> U) (pB : (x : A) -> prop (B x)) rem : Id U (Id A s.1 t.1) (Id (sig A B) s t) = lemSigProp A B pB s t @ -i -isaprop : U -> U = prop -isaset : U -> U = set - -weq : U -> U -> U = equiv -invweq (A B : U) : weq A B -> B -> A = invEq A B - -dirprod : U -> U -> U = and - -isapropDirprod (A B : U) (pA : isaprop A) (pB : isaprop B) : isaprop (dirprod A B) = - propSig A (\(_ : A) -> B) pA (\(_ : A) -> pB) - - - - -- (* Propositions *) --- Definition hProp := total2 (fun X : UU => isaprop X). -hProp : U = (X : U) * isaprop X +hProp : U = (X : U) * prop X --- Definition ishinh_UU (X : UU) := ∀ P : hProp, ((X -> pr1 P) -> pr1 P). ishinh_UU (X : U) : U = (P : hProp) -> ((X -> P.1) -> P.1) --- Lemma isapropishinh (X : UU) : isaprop (ishinh_UU X). --- Proof. --- apply impred; intro P. --- apply impred; intro f. --- apply (pr2 P). --- Defined. -isapropishinh (X : U) : isaprop (ishinh_UU X) = +propishinh (X : U) : prop (ishinh_UU X) = propPi hProp (\(P : hProp) -> ((X -> P.1) -> P.1)) rem1 where - rem1 (P : hProp) : isaprop ((X -> P.1) -> P.1) = + rem1 (P : hProp) : prop ((X -> P.1) -> P.1) = propPi (X -> P.1) (\(_ : X -> P.1) -> P.1) (\(f : X -> P.1) -> P.2) --- Definition ishinh (X : UU) : hProp := hProppair (ishinh_UU X) (isapropishinh X). -ishinh (X : U) : hProp = (ishinh_UU X,isapropishinh X) +ishinh (X : U) : hProp = (ishinh_UU X,propishinh X) --- Definition hinhpr {X : UU} : X -> pr1 (ishinh X) := --- fun (x : X) (P : hProp) (f : X -> pr1 P) => f x. hinhpr (X : U) : X -> (ishinh X).1 = \(x : X) (P : hProp) (f : X -> P.1) -> f x - --- Definition hinhuniv {X : UU} {P : hProp} (f : X -> pr1 P) --- (inhX : pr1 (ishinh X)) : pr1 P := inhX P f. hinhuniv (X : U) (P : hProp) (f : X -> P.1) (inhX : (ishinh X).1) : P.1 = inhX P f --- Definition hdisj (P Q : UU) : hProp := ishinh (coprod P Q). hdisj (P Q : U) : hProp = ishinh (or P Q) --- Definition hdisj_in1 {P Q : UU} : P -> pr1 (hdisj P Q) := fun X => hinhpr (ii1 X). --- Definition hdisj_in2 {P Q : UU} : Q -> pr1 (hdisj P Q) := fun X => hinhpr (ii2 X). 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 weq for props -weqhProp (P P' : hProp) (f : P.1 -> P'.1) (g : P'.1 -> P.1) : weq P.1 P'.1 = (f,isEquivf) +-- 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 = (f,isEquivf) where isEquivf : isEquiv P.1 P'.1 f = (s,t) where @@ -83,140 +50,52 @@ weqhProp (P P' : hProp) (f : P.1 -> P'.1) (g : P'.1 -> P.1) : weq P.1 P'.1 = (f, r1 : Id P.1 (s y).1 w.1 = P.2 (s y).1 w.1 -- Proof of uahp using full univalence --- Axiom uahp : ∀ P P' : hProp, (pr1 P -> pr1 P') -> (pr1 P' -> pr1 P) -> P = P'. uahp' (P P' : hProp) (f : P.1 -> P'.1) (g : P'.1 -> P.1) : Id hProp P P' = - subtypeEquality U isaprop propIsProp P P' rem + subtypeEquality U prop propIsProp P P' rem where rem : Id U P.1 P'.1 = - invweq (Id U P.1 P'.1) (weq P.1 P'.1) (univalence P.1 P'.1) (weqhProp P P' f g) + invEq (Id U P.1 P'.1) (equiv P.1 P'.1) (univalence P.1 P'.1) (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' = - subtypeEquality U isaprop propIsProp P P' rem + subtypeEquality U prop propIsProp P P' rem where rem : Id U P.1 P'.1 = isoId P.1 P'.1 f g s t where s (y : P'.1) : Id P'.1 (f (g y)) y = P'.2 (f (g y)) y t (x : P.1) : Id P.1 (g (f x)) x = P.2 (g (f x)) x - - --- Definition weqtopathshProp {P P' : hProp} (w : weq (pr1 P) (pr1 P')) : P = P' := --- uahp P P' w (invweq w). --- weqtopathshProp (P P' : hProp) (w : weq P.1 P'.1) : Id hProp P P' = --- uahp P P' w.1 (invweq P.1 P'.1 w) - --- The Coq proof that hProp is a set: - --- Definition eqweqmaphProp {P P' : hProp} (e: @paths hProp P P') : weq (pr1 P) (pr1 P'). --- Proof. --- destruct e. --- apply idweq. --- Defined. - --- Definition weqpathsweqhProp {P P' : hProp} (w : weq (pr1 P) (pr1 P')) : --- eqweqmaphProp (weqtopathshProp w) = w. --- Proof. --- apply proofirrelevance. --- apply (isapropweqtoprop (pr1 P) (pr1 P') (pr2 P')). --- Defined. - --- Theorem univfromtwoaxiomshProp (P P' : hProp) : isweq (@eqweqmaphProp P P'). --- Proof. --- set (P1 := fun XY : hProp × hProp => pr1 XY = pr2 XY). --- set (P2 := fun XY : hProp × hProp => weq (pr1 (pr1 XY)) (pr1 (pr2 XY))). --- set (Z1 := total2 P1). --- set (Z2 := total2 P2). --- set (f := totalfun _ _ (fun XY : hProp × hProp => --- @eqweqmaphProp (pr1 XY) (pr2 XY)) : Z1 -> Z2). --- set (g := totalfun _ _ (fun XY : hProp × hProp => --- @weqtopathshProp (pr1 XY) (pr2 XY)) : Z2 -> Z1). --- assert (efg : ∀ z2 : Z2, f (g z2) = z2). --- intros. induction z2 as [ XY w] . --- exact (maponpaths (fun w : weq (pr1 (pr1 XY)) (pr1 (pr2 XY)) => tpair P2 XY w) --- (@weqpathsweqhProp (pr1 XY) (pr2 XY) w)). - --- set (h := fun a1 : Z1 => (pr1 (pr1 a1))). --- assert (egf0 : ∀ a1 : Z1, pr1 (g (f a1)) = pr1 a1). --- intro; apply idpath. --- assert (egf1 : ∀ a1 a1' : Z1, pr1 a1' = pr1 a1 -> a1' = a1). --- intros ? ? X . --- set (X' := maponpaths (@pr1 _ _ ) X). --- assert (is : isweq h). --- apply (isweqpr1pr1 hProp). --- apply (invmaponpathsweq (weqpair h is) _ _ X'). --- set (egf := fun a1 => (egf1 _ _ (egf0 a1))). --- set (is2 := gradth _ _ egf efg). --- apply (isweqtotaltofib P1 P2 (fun XY : hProp × hProp => --- @eqweqmaphProp (pr1 XY) (pr2 XY)) is2 (dirprodpair P P')). --- Defined. - --- Definition weqeqweqhProp (P P' : hProp) := weqpair _ (univfromtwoaxiomshProp P P') . - --- Lemma isasethProp : isaset hProp. --- Proof. --- unfold isaset. --- intros x x'. --- apply (isofhlevelweqb (S O) (weqeqweqhProp x x') --- (isapropweqtoprop (pr1 x) (pr1 x') (pr2 x'))). --- Defined. - - - -- A short proof that hProp form a set using univalence: (this is not needed!) -isapropweq (X Y : U) (H : isaprop Y) (f g : weq X Y) : Id (weq X Y) f g = +propequiv (X Y : U) (H : prop Y) (f g : equiv X Y) : Id (equiv X Y) f g = equivLemma X Y f g ( \(x : X) -> H (f.1 x) (g.1 x) @ i) -isapropidU (X Y : U) : Id U X Y -> isaprop Y -> isaprop X = substInv U isaprop X Y +propidU (X Y : U) : Id U X Y -> prop Y -> prop X = substInv U prop X Y -isasethProp (P P' : hProp) : isaprop (Id hProp P P') = - isapropidU (Id hProp P P') (weq P.1 P'.1) rem (isapropweq P.1 P'.1 P'.2) +sethProp (P P' : hProp) : prop (Id hProp P P') = + propidU (Id hProp P P') (equiv P.1 P'.1) rem (propequiv P.1 P'.1 P'.2) where - rem1 : Id U (Id hProp P P') (Id U P.1 P'.1) = lemSigProp U isaprop propIsProp P P' - rem2 : Id U (Id U P.1 P'.1) (weq P.1 P'.1) = univalence1 P.1 P'.1 - rem : Id U (Id hProp P P') (weq P.1 P'.1) = - compId U (Id hProp P P') (Id U P.1 P'.1) (weq P.1 P'.1) rem1 rem2 - - - + rem1 : Id U (Id hProp P P') (Id U P.1 P'.1) = lemSigProp U prop propIsProp P P' + rem2 : Id U (Id U P.1 P'.1) (equiv P.1 P'.1) = univalence1 P.1 P'.1 + rem : Id U (Id hProp P P') (equiv P.1 P'.1) = + compId U (Id hProp P P') (Id U P.1 P'.1) (equiv P.1 P'.1) rem1 rem2 -- (* Sets *) --- Definition hsubtypes (X : UU) := X -> hProp . hsubtypes (X : U) : U = X -> hProp --- Definition carrier {X : UU} (A : hsubtypes X) : UU := @total2 X (fun x : X => pr1 (A x)). carrier (X : U) (A : hsubtypes X) : U = sig X (\(x : X) -> (A x).1) --- Lemma isasethsubtypes (X : UU) : isaset (hsubtypes X). --- Proof. --- change (isofhlevel 2 (hsubtypes X)). --- apply impred; intro. --- apply isasethProp. --- Defined. --- isasethsubtypes (X : U) : isaset (hsubtypes X) = --- setPi X (\(_ : X) -> hProp) (\(_ : X) -> isasethProp) +sethsubtypes (X : U) : set (hsubtypes X) = + setPi X (\(_ : X) -> hProp) (\(_ : X) -> sethProp) -- Definition hrel (X : UU) := X -> X -> hProp. hrel (X : U) : U = X -> X -> hProp --- Definition iseqclass {X : UU} (R : hrel X) (A : hsubtypes X) := --- pr1 (ishinh (carrier A)) --- × (∀ x1 x2 : X, pr1 (R x1 x2) -> pr1 (A x1) -> pr1 (A x2)) --- × (∀ x1 x2 : X, pr1 (A x1) -> pr1 (A x2) -> pr1 (R x1 x2)). iseqclass (X : U) (R : hrel X) (A : hsubtypes X) : U = - dirprod (dirprod (ishinh (carrier X A)).1 + 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) --- Definition eqax0 {X : UU} {R : hrel X} {A : hsubtypes X} : --- iseqclass R A -> pr1 (ishinh (carrier A)) := fun S => pr1 S. --- Definition eqax1 {X : UU} {R : hrel X} {A : hsubtypes X} : --- iseqclass R A -> ∀ x1 x2 : X, pr1 (R x1 x2) -> pr1 (A x1) -> pr1 (A x2) := --- fun S => pr1 (pr2 S). --- Definition eqax2 {X : UU} {R : hrel X} {A : hsubtypes X} : --- iseqclass R A -> ∀ x1 x2 : X, pr1 (A x1) -> pr1 (A x2) -> pr1 (R x1 x2) := --- fun S => pr2 (pr2 S). 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) : @@ -224,26 +103,15 @@ eqax1 (X : U) (R : hrel X) (A : hsubtypes X) (eqc : iseqclass X R A) : 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 --- Lemma isapropiseqclass {X : UU} (R : hrel X) (A : hsubtypes X) : --- isaprop (iseqclass R A) . --- Proof. --- apply isofhleveldirprod. --- - apply (isapropishinh (carrier A)). --- - apply isofhleveldirprod. --- + repeat (apply impred; intro). --- apply (pr2 (A t0)). --- + repeat (apply impred; intro). --- apply (pr2 (R t t0)). --- Defined. -isapropiseqclass (X : U) (R : hrel X) (A : hsubtypes X) : isaprop (iseqclass X R A) = - isapropDirprod (dirprod (ishinh (carrier X A)).1 +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) - (isapropDirprod (ishinh (carrier X A)).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 : isaprop (ishinh (carrier X A)).1 = isapropishinh (carrier X A) + p1 : prop (ishinh (carrier X A)).1 = propishinh (carrier X A) -- This proof is quite cool, but it looks ugly... p2 (f g : (x1 x2 : X) -> (R x1 x2).1 -> (A x1).1 -> (A x2).1) : @@ -256,90 +124,28 @@ isapropiseqclass (X : U) (R : hrel X) (A : hsubtypes X) : isaprop (iseqclass X R \(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 --- Definition hSet:= total2 (fun X : UU => isaset X) . -hSet : U = (X : U) * isaset X +hSet : U = (X : U) * set X --- Definition isrefl {X : UU} (R : hrel X) := ∀ x : X, pr1 (R x x). --- Definition issymm {X : UU} (R : hrel X) := ∀ (x1 x2 : X), pr1 (R x1 x2) -> pr1 (R x2 x1). --- Definition istrans {X : UU} (R : hrel X) := --- ∀ (x1 x2 x3 : X), pr1 (R x1 x2) -> pr1 (R x2 x3) -> pr1 (R x1 x3). 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 --- Definition ispreorder {X : UU} (R : hrel X) := istrans R × isrefl R . -ispreorder (X : U) (R : hrel X) : U = dirprod (istrans X R) (isrefl X R) +ispreorder (X : U) (R : hrel X) : U = and (istrans X R) (isrefl X R) --- Definition iseqrel {X : UU} (R : hrel X) := ispreorder R × issymm R. -iseqrel (X : U) (R : hrel X) : U = dirprod (ispreorder X R) (issymm X R) +iseqrel (X : U) (R : hrel X) : U = and (ispreorder X R) (issymm X R) --- Definition eqrel (X : UU) := total2 (fun R : hrel X => iseqrel R). eqrel (X : U) : U = (R : hrel X) * (iseqrel X R) --- Definition eqrelrefl {X : UU} (R : eqrel X) : isrefl (pr1 R) := --- pr2 (pr1 (pr2 R)). --- Definition eqrelsymm {X : UU} (R : eqrel X) : issymm (pr1 R) := pr2 (pr2 R). --- Definition eqreltrans {X : UU} (R : eqrel X) : istrans (pr1 R) := --- pr1 (pr1 (pr2 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 --- Definition hSetpair X i := tpair isaset X i : hSet. --- hSetpair (X : U) (iss : isaset X) : hSet = (X,iss) - --- Definition boolset : hSet := hSetpair bool isasetbool. -isasetbool : isaset bool = setbool -boolset : hSet = (bool,isasetbool) +boolset : hSet = (bool,setbool) --- Definition setquot {X : UU} (R : hrel X) := total2 (fun A => iseqclass R A). --- Definition pr1setquot {X : UU} (R : hrel X) : setquot R -> (hsubtypes X) := --- @pr1 _ (fun A => iseqclass R A). 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 --- Lemma isinclpr1setquot {X : UU} (R : hrel X) : isincl (pr1setquot R). --- Proof . --- apply isinclpr1; intro x0. --- apply isapropiseqclass. --- Defined. - --- Definition setquottouu0 {X : UU} (R : hrel X) (a : setquot R) := --- carrier (pr1 a). --- setquottouu0 (X : U) (R : hrel X) (a : setquot X R) : U = --- carrier X a.1 - --- Theorem isasetsetquot {X : UU} (R : hrel X) : isaset (setquot R). --- Proof. --- apply (isasetsubset (@pr1 _ _) (isasethsubtypes X)). --- apply isinclpr1; intro x. --- apply isapropiseqclass. --- Defined. --- isasetsetquot (X : U) (R : hrel X) : isaset (setquot X R) = undefined - --- Definition setquotinset {X : UU} (R : hrel X) : hSet := --- hSetpair _ (isasetsetquot R). --- setquotinset (X : U) (R : hrel X) : hSet = --- hSetpair (setquot X R) (isasetsetquot X R) - --- Theorem setquotpr {X : UU} (R : eqrel X) : X -> setquot (pr1 R). --- Proof. --- intros X0. --- set (rax := eqrelrefl R). --- set (sax := eqrelsymm R). --- set (tax := eqreltrans R). --- split with (fun x : X => (pr1 R) X0 x). --- split. --- exact (hinhpr (tpair _ X0 (rax X0))). --- assert (a1 : ∀ x1 x2 : X, pr1 (pr1 R x1 x2) -> pr1 (pr1 R X0 x1) -> pr1 (pr1 R X0 x2)). --- intros x1 x2 X1 X2. --- now apply (tax X0 x1 x2 X2 X1). --- split. --- assumption. --- intros x1 x2 X1 X2. --- now apply (tax x1 X0 x2 (sax X0 x1 X1) X2). --- Defined. 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 @@ -350,27 +156,10 @@ setquotpr (X : U) (R : eqrel X) (X0 : X) : setquot X R.1 = (A,((p1,p2),p3)) 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 - --- Lemma setquotl0 {X : UU} (R : eqrel X) (c : setquot (pr1 R)) --- (x : setquottouu0 _ c) : setquotpr R (pr1 x) = c. --- Proof. --- apply subtypeEquality. --- intro a. --- apply isapropiseqclass. --- apply funextsec; intro x0. --- destruct c as [A iseq]. --- destruct x as [x is]. --- simpl in *. --- apply uahp. --- - intro r. --- exact (eqax1 iseq _ _ r is). --- - intro a. --- exact (eqax2 iseq _ _ is a). --- Defined. 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) : isaprop (iseqclass X R.1 A) = isapropiseqclass X R.1 A + 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 @@ -378,17 +167,6 @@ setquotl0 (X : U) (R : eqrel X) (c : setquot X R.1) (x : carrier X c.1) : 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 --- Theorem setquotunivprop {X : UU} (R : eqrel X) (P : setquot (pr1 R) -> hProp) --- (ps : ∀ x : X, pr1 (P (setquotpr R x))) : ∀ c : setquot (pr1 R), pr1 (P c). --- Proof. --- intro c. --- apply (@hinhuniv (carrier (pr1 c)) (P c)). --- - intro x. --- set (e := setquotl0 R c x). --- apply (eqweqmaphProp (maponpaths P e)). --- exact (ps (pr1 x)). --- - apply (eqax0 (pr2 c)). --- Defined. 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 @@ -398,144 +176,106 @@ setquotunivprop (X : U) (R : eqrel X) (P : setquot X R.1 -> hProp) rem : (ishinh (carrier X c.1)).1 = eqax0 X R.1 c.1 c.2 - - -- Finally the exercise: --- Definition R : eqrel bool. --- Proof. --- refine (_,,_). --- { intros x y. exists (x=y). apply isasetbool. } --- split. --- - split. --- + intros x y z. apply pathscomp0. --- + intros x. reflexivity. --- - intros x y. apply pathsinv0. --- Defined. R : eqrel bool = (r1,r2) where - r1 : hrel bool = \(x y : bool) -> (Id bool x y,isasetbool x y) + r1 : hrel bool = \(x y : bool) -> (Id bool x y,setbool x y) r2 : iseqrel bool r1 = ((compId bool,refl bool),inv bool) --- Definition T : hSet := setquotinset (pr1 R). --- T : hSet = setquotinset bool R.1 - --- Definition true' : setquot (pr1 R) := setquotpr R true. --- Definition false' : setquot (pr1 R) := setquotpr R false. -true' : setquot bool R.1 = setquotpr bool R true -false' : setquot bool R.1 = setquotpr bool R false +bool' : U = setquot bool R.1 +true' : bool' = setquotpr bool R true +false' : bool' = setquotpr bool R false --- (* Version of predicate based on hdisj (ie truncated sum) *) +P' (t : bool') : hProp = + hdisj (Id bool' t true') (Id bool' t false') --- Definition P' (t : pr1 T) : hProp := hdisj (t = true') (t = false'). -P' (t : setquot bool R.1) : hProp = - hdisj (Id (setquot bool R.1) t true') (Id (setquot bool R.1) t false') - --- Lemma K' (t : pr1 T) : pr1 (P' t). --- Proof. --- apply setquotunivprop. intros x. unfold P'. --- induction x as [x|x]. --- - apply hdisj_in1. reflexivity. --- - apply hdisj_in2. reflexivity. --- Defined. -K' (t : setquot bool R.1) : (P' t).1 = setquotunivprop bool R P' ps t +K' (t : bool') : (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') - --- 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 + false -> hdisj_in2 (Id bool' false' true') + (Id bool' false' false') (<_> false') + true -> hdisj_in1 (Id bool' true' true') + (Id bool' true' false') (<_> true') --- Print Assumptions K'. +test : (P' true').1 = hdisj_in1 (Id bool' true' true') + (Id bool' true' false') (<_> true') +test' : (P' true').1 = K' true' -test : (P' true').1 = hdisj_in1 (Id (setquot bool R.1) true' true') - (Id (setquot bool R.1) true' false') (<_> true') +test'' : Id (P' true').1 test test' = (P' true').2 test test' --- Goal K' true' = hdisj_in1 (idpath true'). --- try reflexivity. (* Error: Unable to unify "L'" with "K' true'". *) --- Abort. +-- These two terms are not convertible: -- test' : Id (P' true').1 (K' true') -- (hdisj_in1 (Id (setquot bool R.1) true' true') (Id (setquot bool R.1) true' false') (<_> true')) = -- <_> K' true' --- This takes too long: --- > :n K' true' - - +-- Another test: +true'neqfalse' (H : Id bool' true' false') : N0 = falseNeqTrue rem1 + where + rem : Id U (Id bool true true) (Id bool false true) = ((H @ i).1 true).1 + rem1 : Id bool false true = comp rem (<_> true) [] +test1 (x : bool') (H1 : Id bool' x true') (H2 : Id bool' x false') : N0 = true'neqfalse' rem + where + rem : Id bool' true' false' = comp (<_> bool') x [(i = 0) -> H1, (i = 1) -> H2] +test2 (x : bool') (p1 : (ishinh (Id bool' x true')).1) + (p2 : (ishinh (Id bool' x false')).1) : N0 = + hinhuniv (Id bool' x true') (N0,propN0) rem p1 + where + rem (H1 : Id bool' x true') : N0 = + hinhuniv (Id bool' x false') (N0,propN0) + (\(H2 : Id bool' x false') -> test1 x H1 H2) p2 +-- shorthand for this big type +T (x : bool') : U = or (ishinh (Id bool' x true')).1 (ishinh (Id bool' x false')).1 +-- test3 (x : bool') : prop (T x) +test3 (x : bool') : (a b : T x) -> Id (T x) a b = split + inl a' -> rem + where + rem : (b : T x) -> Id (T x) (inl a') b = split + inl b' -> inl (propishinh (Id bool' x true') a' b' @ i) + inr b' -> efq (Id (T x) (inl a') (inr b')) (test2 x a' b') + inr a' -> rem + where + rem : (b : T x) -> Id (T x) (inr a') b = split + inl b' -> efq (Id (T x) (inr a') (inl b')) (test2 x b' a') + inr b' -> inr (propishinh (Id bool' x false') a' b' @ i) +f (x : bool') : or (ishinh (Id bool' x true')).1 (ishinh (Id bool' x false')).1 -> bool = split + inl _ -> true + inr _ -> false +bar (x : bool') : or (Id bool' x true') (Id bool' x false') -> + or (ishinh (Id bool' x true')).1 (ishinh (Id bool' x false')).1 = split + inl p -> inl (hinhpr (Id bool' x true') p) + inr p -> inr (hinhpr (Id bool' x false') p) --- Not translated yet: +-- finally the map: +foo (x : bool') (x' : (P' x).1) : bool = f x rem + where + rem : or (ishinh (Id bool' x true')).1 (ishinh (Id bool' x false')).1 = + hinhuniv (or (Id bool' x true') (Id bool' x false')) + (or (ishinh (Id bool' x true')).1 (ishinh (Id bool' x false')).1,test3 x) + (bar x) x' +-- > :n testfoo +-- NORMEVAL: true +-- Time: 0m0.490s +testfoo : bool = foo true' (K' true') --- (* Version of predicate based on sum *) +testfoo' : Id bool (foo true' (K' true')) true = foo true' (K' true') --- (* preliminary results *) --- Lemma iscompsetquotpr {X : UU} (R : eqrel X) (x x' : X) (a : pr1 (pr1 R x x')) : --- setquotpr R x = setquotpr R x'. --- Proof. --- apply (invmaponpathsincl _ (isinclpr1setquot (pr1 R))); simpl. --- apply funextsec; intro x0. --- apply uahp. --- - intro r0. --- exact (eqreltrans R _ _ _ (eqrelsymm R _ _ a) r0). --- - intro x0'. --- exact (eqreltrans R _ _ _ a x0'). --- Defined. --- Theorem weqpathsinsetquot {X : UU} (R : eqrel X) (x x' : X) : --- weq (pr1 (pr1 R x x')) (setquotpr R x = setquotpr R x'). --- Proof. --- split with (iscompsetquotpr R x x'). --- apply isweqimplimpl. --- - intro e. --- set (e' := maponpaths (pr1setquot (pr1 R)) e). --- set (e'' := maponpaths (fun f => f x') e'). --- exact (eqweqmaphProp (pathsinv0 e'') (eqrelrefl R x')). --- - exact (pr2 (pr1 R x x')). --- - exact (isasetsetquot (pr1 R) (setquotpr R x) (setquotpr R x')). --- Defined. --- Lemma C P Q : isaprop P -> isaprop Q -> (P -> ¬Q) -> isaprop (sum P Q). --- Proof. --- intros i j n. apply invproofirrelevance. intros a b. --- induction a as [a|a]. --- - induction b as [b|b]. --- + apply maponpaths, i. --- + induction (n a b). --- - induction b as [b|b]. --- + induction (n b a). --- + apply maponpaths, j. --- Defined. +-- Tests of checking normal forms: --- Definition P : pr1 T -> hProp. --- Proof. --- intros t. exists (sum (t = true') (t = false')). apply C. --- - apply (pr2 T). --- - apply (pr2 T). --- - intros p q. --- exact (nopathstruetofalse (invmap (weqpathsinsetquot R true false) (!p @ q))). --- Defined. +ntrue' : bool' = (\(x : bool) -> (IdP ( bool) true x,lem8 x),((\(P : sig U (\(X : U) -> (a b : X) -> IdP ( X) a b)) -> \(f : (sig bool (\(x : bool) -> IdP ( bool) true x)) -> P.1) -> f ((true, true)),\(x1 x2 : bool) -> \(X1 : IdP ( bool) x1 x2) -> \(X2 : IdP ( bool) true x1) -> comp ( bool) (X2 @ i0) [ (i0 = 0) -> true, (i0 = 1) -> X1 @ i1 ]),\(x1 x2 : bool) -> \(X1 : IdP ( bool) true x1) -> \(X2 : IdP ( bool) true x2) -> comp ( bool) (X1 @ -i0) [ (i0 = 0) -> x1, (i0 = 1) -> X2 @ i1 ])) --- Lemma K t : pr1 (P t). --- Proof. --- apply setquotunivprop. intros x. unfold P; simpl. --- induction x as [x|x]. --- - apply ii1. reflexivity. --- - apply ii2. reflexivity. --- Defined. +-- Why is this not working? Bug in pretty printer? +-- ntest : (P' true').1 = \(P : sig U (\(X : U) -> (a b : X) -> IdP ( X) a b)) -> \(f : or (IdP ( sig (bool -> (sig U (\(X : U) -> (a b : X) -> IdP ( X) a b))) (\(A : bool -> (sig U (\(X : U) -> (a b : X) -> IdP ( X) a b))) -> sig (sig ((P0 : sig U (\(X : U) -> (a b : X) -> IdP ( X) a b)) -> ((sig bool (\(x : bool) -> (A x).1)) -> P0.1) -> P0.1) (\(_ : (P0 : sig U (\(X : U) -> (a b : X) -> IdP ( X) a b)) -> ((sig bool (\(x : bool) -> (A x).1)) -> P0.1) -> P0.1) -> (x1 x2 : bool) -> (IdP ( bool) x1 x2) -> ((A x1).1 -> (A x2).1))) (\(_ : sig ((P0 : sig U (\(X : U) -> (a b : X) -> IdP ( X) a b)) -> ((sig bool (\(x : bool) -> (A x).1)) -> P0.1) -> P0.1) (\(_ : (P0 : sig U (\(X : U) -> (a b : X) -> IdP ( X) a b)) -> ((sig bool (\(x : bool) -> (A x).1)) -> P0.1) -> P0.1) -> (x1 x2 : bool) -> (IdP ( bool) x1 x2) -> ((A x1).1 -> (A x2).1))) -> (x1 x2 : bool) -> (A x1).1 -> ((A x2).1 -> (IdP ( bool) x1 x2))))) ((\(x : bool) -> (IdP ( bool) true x,lem8 x),((\(P0 : sig U (\(X : U) -> (a b : X) -> IdP ( X) a b)) -> \(f : (sig bool (\(x : bool) -> IdP ( bool) true x)) -> P0.1) -> f ((true, true)),\(x1 x2 : bool) -> \(X1 : IdP ( bool) x1 x2) -> \(X2 : IdP ( bool) true x1) -> comp ( bool) (X2 @ i0) [ (i0 = 0) -> true, (i0 = 1) -> X1 @ i1 ]),\(x1 x2 : bool) -> \(X1 : IdP ( bool) true x1) -> \(X2 : IdP ( bool) true x2) -> comp ( bool) (X1 @ -i0) [ (i0 = 0) -> x1, (i0 = 1) -> X2 @ i1 ]))) ((\(x : bool) -> (IdP ( bool) true x,lem8 x),((\(P0 : sig U (\(X : U) -> (a b : X) -> IdP ( X) a b)) -> \(f : (sig bool (\(x : bool) -> IdP ( bool) true x)) -> P0.1) -> f ((true, true)),\(x1 x2 : bool) -> \(X1 : IdP ( bool) x1 x2) -> \(X2 : IdP ( bool) true x1) -> comp ( bool) (X2 @ i0) [ (i0 = 0) -> true, (i0 = 1) -> X1 @ i1 ]),\(x1 x2 : bool) -> \(X1 : IdP ( bool) true x1) -> \(X2 : IdP ( bool) true x2) -> comp ( bool) (X1 @ -i0) [ (i0 = 0) -> x1, (i0 = 1) -> X2 @ i1 ]))), IdP ( sig (bool -> (sig U (\(X : U) -> (a b : X) -> IdP ( X) a b))) (\(A : bool -> (sig U (\(X : U) -> (a b : X) -> IdP ( X) a b))) -> sig (sig ((P0 : sig U (\(X : U) -> (a b : X) -> IdP ( X) a b)) -> ((sig bool (\(x : bool) -> (A x).1)) -> P0.1) -> P0.1) (\(_ : (P0 : sig U (\(X : U) -> (a b : X) -> IdP ( X) a b)) -> ((sig bool (\(x : bool) -> (A x).1)) -> P0.1) -> P0.1) -> (x1 x2 : bool) -> (IdP ( bool) x1 x2) -> ((A x1).1 -> (A x2).1))) (\(_ : sig ((P0 : sig U (\(X : U) -> (a b : X) -> IdP ( X) a b)) -> ((sig bool (\(x : bool) -> (A x).1)) -> P0.1) -> P0.1) (\(_ : (P0 : sig U (\(X : U) -> (a b : X) -> IdP ( X) a b)) -> ((sig bool (\(x : bool) -> (A x).1)) -> P0.1) -> P0.1) -> (x1 x2 : bool) -> (IdP ( bool) x1 x2) -> ((A x1).1 -> (A x2).1))) -> (x1 x2 : bool) -> (A x1).1 -> ((A x2).1 -> (IdP ( bool) x1 x2))))) ((\(x : bool) -> (IdP ( bool) true x,lem8 x),((\(P0 : sig U (\(X : U) -> (a b : X) -> IdP ( X) a b)) -> \(f : (sig bool (\(x : bool) -> IdP ( bool) true x)) -> P0.1) -> f ((true, true)),\(x1 x2 : bool) -> \(X1 : IdP ( bool) x1 x2) -> \(X2 : IdP ( bool) true x1) -> comp ( bool) (X2 @ i0) [ (i0 = 0) -> true, (i0 = 1) -> X1 @ i1 ]),\(x1 x2 : bool) -> \(X1 : IdP ( bool) true x1) -> \(X2 : IdP ( bool) true x2) -> comp ( bool) (X1 @ -i0) [ (i0 = 0) -> x1, (i0 = 1) -> X2 @ i1 ]))) ((\(x : bool) -> (IdP ( bool) false x,lem7 x),((\(P0 : sig U (\(X : U) -> (a b : X) -> IdP ( X) a b)) -> \(f : (sig bool (\(x : bool) -> IdP ( bool) false x)) -> P0.1) -> f ((false, false)),\(x1 x2 : bool) -> \(X1 : IdP ( bool) x1 x2) -> \(X2 : IdP ( bool) false x1) -> comp ( bool) (X2 @ i0) [ (i0 = 0) -> false, (i0 = 1) -> X1 @ i1 ]),\(x1 x2 : bool) -> \(X1 : IdP ( bool) false x1) -> \(X2 : IdP ( bool) false x2) -> comp ( bool) (X1 @ -i0) [ (i0 = 0) -> x1, (i0 = 1) -> X2 @ i1 ])))) -> P.1) -> f (inl ( (\(x : bool) -> (IdP ( bool) true x,lem8 x),((\(P0 : sig U (\(X : U) -> (a b : X) -> IdP ( X) a b)) -> \(f0 : (sig bool (\(x : bool) -> IdP ( bool) true x)) -> P0.1) -> f0 ((true, true)),\(x1 x2 : bool) -> \(X1 : IdP ( bool) x1 x2) -> \(X2 : IdP ( bool) true x1) -> comp ( bool) (X2 @ i0) [ (i0 = 0) -> true, (i0 = 1) -> X1 @ i1 ]),\(x1 x2 : bool) -> \(X1 : IdP ( bool) true x1) -> \(X2 : IdP ( bool) true x2) -> comp ( bool) (X1 @ -i0) [ (i0 = 0) -> x1, (i0 = 1) -> X2 @ i1 ])))) --- Print Assumptions K. --- Goal K true' = ii1 (idpath true'). --- try reflexivity. (* Error: Unable to unify "L" with "K true'". *) --- Abort. diff --git a/examples/shortsetquot.ctt b/examples/shortsetquot.ctt deleted file mode 100644 index e52bb55..0000000 --- a/examples/shortsetquot.ctt +++ /dev/null @@ -1,264 +0,0 @@ -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) - -bool' : U = setquot bool R.1 -true' : bool' = setquotpr bool R true -false' : bool' = setquotpr bool R false - -P' (t : bool') : hProp = - hdisj (Id bool' t true') (Id bool' t false') - -K' (t : bool') : (P' t).1 = setquotunivprop bool R P' ps t - where - ps : (x : bool) -> (P' (setquotpr bool R x)).1 = split - false -> hdisj_in2 (Id bool' false' true') - (Id bool' false' false') (<_> false') - true -> hdisj_in1 (Id bool' true' true') - (Id bool' true' false') (<_> true') - -test : (P' true').1 = hdisj_in1 (Id bool' true' true') - (Id bool' true' false') (<_> true') - -test' : (P' true').1 = K' true' - -test'' : Id (P' true').1 test test' = (P' true').2 test test' - --- These two terms are not convertible: --- test' : Id (P' true').1 (K' true') --- (hdisj_in1 (Id (setquot bool R.1) true' true') (Id (setquot bool R.1) true' false') (<_> true')) = --- <_> K' true' - - - --- Another test: - -true'neqfalse' (H : Id bool' true' false') : N0 = falseNeqTrue rem1 - where - rem : Id U (Id bool true true) (Id bool false true) = ((H @ i).1 true).1 - rem1 : Id bool false true = comp rem (<_> true) [] - -test1 (x : bool') (H1 : Id bool' x true') (H2 : Id bool' x false') : N0 = true'neqfalse' rem - where - rem : Id bool' true' false' = comp (<_> bool') x [(i = 0) -> H1, (i = 1) -> H2] - -test2 (x : bool') (p1 : (ishinh (Id bool' x true')).1) - (p2 : (ishinh (Id bool' x false')).1) : N0 = - hinhuniv (Id bool' x true') (N0,propN0) rem p1 - where - rem (H1 : Id bool' x true') : N0 = - hinhuniv (Id bool' x false') (N0,propN0) - (\(H2 : Id bool' x false') -> test1 x H1 H2) p2 - --- shorthand for this big type -T (x : bool') : U = or (ishinh (Id bool' x true')).1 (ishinh (Id bool' x false')).1 - --- test3 (x : bool') : prop (T x) -test3 (x : bool') : (a b : T x) -> Id (T x) a b = split - inl a' -> rem - where - rem : (b : T x) -> Id (T x) (inl a') b = split - inl b' -> inl (propishinh (Id bool' x true') a' b' @ i) - inr b' -> efq (Id (T x) (inl a') (inr b')) (test2 x a' b') - inr a' -> rem - where - rem : (b : T x) -> Id (T x) (inr a') b = split - inl b' -> efq (Id (T x) (inr a') (inl b')) (test2 x b' a') - inr b' -> inr (propishinh (Id bool' x false') a' b' @ i) - -f (x : bool') : or (ishinh (Id bool' x true')).1 (ishinh (Id bool' x false')).1 -> bool = split - inl _ -> true - inr _ -> false - -bar (x : bool') : or (Id bool' x true') (Id bool' x false') -> - or (ishinh (Id bool' x true')).1 (ishinh (Id bool' x false')).1 = split - inl p -> inl (hinhpr (Id bool' x true') p) - inr p -> inr (hinhpr (Id bool' x false') p) - --- finally the map: -foo (x : bool') (x' : (P' x).1) : bool = f x rem - where - rem : or (ishinh (Id bool' x true')).1 (ishinh (Id bool' x false')).1 = - hinhuniv (or (Id bool' x true') (Id bool' x false')) - (or (ishinh (Id bool' x true')).1 (ishinh (Id bool' x false')).1,test3 x) - (bar x) x' - --- > :n testfoo --- NORMEVAL: true --- Time: 0m0.490s -testfoo : bool = foo true' (K' true') - -testfoo' : Id bool (foo true' (K' true')) true = foo true' (K' true') - - - - --- Tests of checking normal forms: - -ntrue' : bool' = (\(x : bool) -> (IdP ( bool) true x,lem8 x),((\(P : sig U (\(X : U) -> (a b : X) -> IdP ( X) a b)) -> \(f : (sig bool (\(x : bool) -> IdP ( bool) true x)) -> P.1) -> f ((true, true)),\(x1 x2 : bool) -> \(X1 : IdP ( bool) x1 x2) -> \(X2 : IdP ( bool) true x1) -> comp ( bool) (X2 @ i0) [ (i0 = 0) -> true, (i0 = 1) -> X1 @ i1 ]),\(x1 x2 : bool) -> \(X1 : IdP ( bool) true x1) -> \(X2 : IdP ( bool) true x2) -> comp ( bool) (X1 @ -i0) [ (i0 = 0) -> x1, (i0 = 1) -> X2 @ i1 ])) - --- Why is this not working? Bug in pretty printer? --- ntest : (P' true').1 = \(P : sig U (\(X : U) -> (a b : X) -> IdP ( X) a b)) -> \(f : or (IdP ( sig (bool -> (sig U (\(X : U) -> (a b : X) -> IdP ( X) a b))) (\(A : bool -> (sig U (\(X : U) -> (a b : X) -> IdP ( X) a b))) -> sig (sig ((P0 : sig U (\(X : U) -> (a b : X) -> IdP ( X) a b)) -> ((sig bool (\(x : bool) -> (A x).1)) -> P0.1) -> P0.1) (\(_ : (P0 : sig U (\(X : U) -> (a b : X) -> IdP ( X) a b)) -> ((sig bool (\(x : bool) -> (A x).1)) -> P0.1) -> P0.1) -> (x1 x2 : bool) -> (IdP ( bool) x1 x2) -> ((A x1).1 -> (A x2).1))) (\(_ : sig ((P0 : sig U (\(X : U) -> (a b : X) -> IdP ( X) a b)) -> ((sig bool (\(x : bool) -> (A x).1)) -> P0.1) -> P0.1) (\(_ : (P0 : sig U (\(X : U) -> (a b : X) -> IdP ( X) a b)) -> ((sig bool (\(x : bool) -> (A x).1)) -> P0.1) -> P0.1) -> (x1 x2 : bool) -> (IdP ( bool) x1 x2) -> ((A x1).1 -> (A x2).1))) -> (x1 x2 : bool) -> (A x1).1 -> ((A x2).1 -> (IdP ( bool) x1 x2))))) ((\(x : bool) -> (IdP ( bool) true x,lem8 x),((\(P0 : sig U (\(X : U) -> (a b : X) -> IdP ( X) a b)) -> \(f : (sig bool (\(x : bool) -> IdP ( bool) true x)) -> P0.1) -> f ((true, true)),\(x1 x2 : bool) -> \(X1 : IdP ( bool) x1 x2) -> \(X2 : IdP ( bool) true x1) -> comp ( bool) (X2 @ i0) [ (i0 = 0) -> true, (i0 = 1) -> X1 @ i1 ]),\(x1 x2 : bool) -> \(X1 : IdP ( bool) true x1) -> \(X2 : IdP ( bool) true x2) -> comp ( bool) (X1 @ -i0) [ (i0 = 0) -> x1, (i0 = 1) -> X2 @ i1 ]))) ((\(x : bool) -> (IdP ( bool) true x,lem8 x),((\(P0 : sig U (\(X : U) -> (a b : X) -> IdP ( X) a b)) -> \(f : (sig bool (\(x : bool) -> IdP ( bool) true x)) -> P0.1) -> f ((true, true)),\(x1 x2 : bool) -> \(X1 : IdP ( bool) x1 x2) -> \(X2 : IdP ( bool) true x1) -> comp ( bool) (X2 @ i0) [ (i0 = 0) -> true, (i0 = 1) -> X1 @ i1 ]),\(x1 x2 : bool) -> \(X1 : IdP ( bool) true x1) -> \(X2 : IdP ( bool) true x2) -> comp ( bool) (X1 @ -i0) [ (i0 = 0) -> x1, (i0 = 1) -> X2 @ i1 ]))), IdP ( sig (bool -> (sig U (\(X : U) -> (a b : X) -> IdP ( X) a b))) (\(A : bool -> (sig U (\(X : U) -> (a b : X) -> IdP ( X) a b))) -> sig (sig ((P0 : sig U (\(X : U) -> (a b : X) -> IdP ( X) a b)) -> ((sig bool (\(x : bool) -> (A x).1)) -> P0.1) -> P0.1) (\(_ : (P0 : sig U (\(X : U) -> (a b : X) -> IdP ( X) a b)) -> ((sig bool (\(x : bool) -> (A x).1)) -> P0.1) -> P0.1) -> (x1 x2 : bool) -> (IdP ( bool) x1 x2) -> ((A x1).1 -> (A x2).1))) (\(_ : sig ((P0 : sig U (\(X : U) -> (a b : X) -> IdP ( X) a b)) -> ((sig bool (\(x : bool) -> (A x).1)) -> P0.1) -> P0.1) (\(_ : (P0 : sig U (\(X : U) -> (a b : X) -> IdP ( X) a b)) -> ((sig bool (\(x : bool) -> (A x).1)) -> P0.1) -> P0.1) -> (x1 x2 : bool) -> (IdP ( bool) x1 x2) -> ((A x1).1 -> (A x2).1))) -> (x1 x2 : bool) -> (A x1).1 -> ((A x2).1 -> (IdP ( bool) x1 x2))))) ((\(x : bool) -> (IdP ( bool) true x,lem8 x),((\(P0 : sig U (\(X : U) -> (a b : X) -> IdP ( X) a b)) -> \(f : (sig bool (\(x : bool) -> IdP ( bool) true x)) -> P0.1) -> f ((true, true)),\(x1 x2 : bool) -> \(X1 : IdP ( bool) x1 x2) -> \(X2 : IdP ( bool) true x1) -> comp ( bool) (X2 @ i0) [ (i0 = 0) -> true, (i0 = 1) -> X1 @ i1 ]),\(x1 x2 : bool) -> \(X1 : IdP ( bool) true x1) -> \(X2 : IdP ( bool) true x2) -> comp ( bool) (X1 @ -i0) [ (i0 = 0) -> x1, (i0 = 1) -> X2 @ i1 ]))) ((\(x : bool) -> (IdP ( bool) false x,lem7 x),((\(P0 : sig U (\(X : U) -> (a b : X) -> IdP ( X) a b)) -> \(f : (sig bool (\(x : bool) -> IdP ( bool) false x)) -> P0.1) -> f ((false, false)),\(x1 x2 : bool) -> \(X1 : IdP ( bool) x1 x2) -> \(X2 : IdP ( bool) false x1) -> comp ( bool) (X2 @ i0) [ (i0 = 0) -> false, (i0 = 1) -> X1 @ i1 ]),\(x1 x2 : bool) -> \(X1 : IdP ( bool) false x1) -> \(X2 : IdP ( bool) false x2) -> comp ( bool) (X1 @ -i0) [ (i0 = 0) -> x1, (i0 = 1) -> X2 @ i1 ])))) -> P.1) -> f (inl ( (\(x : bool) -> (IdP ( bool) true x,lem8 x),((\(P0 : sig U (\(X : U) -> (a b : X) -> IdP ( X) a b)) -> \(f0 : (sig bool (\(x : bool) -> IdP ( bool) true x)) -> P0.1) -> f0 ((true, true)),\(x1 x2 : bool) -> \(X1 : IdP ( bool) x1 x2) -> \(X2 : IdP ( bool) true x1) -> comp ( bool) (X2 @ i0) [ (i0 = 0) -> true, (i0 = 1) -> X1 @ i1 ]),\(x1 x2 : bool) -> \(X1 : IdP ( bool) true x1) -> \(X2 : IdP ( bool) true x2) -> comp ( bool) (X1 @ -i0) [ (i0 = 0) -> x1, (i0 = 1) -> X2 @ i1 ])))) - -